pysmt/pysmt

Issues

• Create node does not raise TypeError

  #784 opened a month ago by annabeks
  0

• Any plans for Floating point support?

  #783 opened 3 months ago by bavalpey
  1

• Add type-hints to pysmt code

  #780 opened 4 months ago by enmag
  2

• floating points are not printed as floating points

  #778 opened 4 months ago by MikolasJanota
  1

• CVC4 has been superseded by CVC5 - please update the project

  #744 opened 4 months ago by yurivict
  2

• Add labels to the constraints to mimic `assert_and_track` from Z3 in pySMT

  #752 opened 2 years ago by pkalita595
  1

• Unable to use UFNRA

  #777 opened 4 months ago by MikolasJanota
  0

• pyximport has no attribute 'build_module'

  #776 opened 5 months ago by ntinouldinho
  0

• Substitution with term containing bound variables

  #774 opened 5 months ago by maul-esel
  1

• The imp module is removed in Python 3.12

  #769 opened 9 months ago by dvzrv
  4

• Substituting Function Symbols without providing Interpretations

  #767 opened a year ago by cvick32
  3

• Can't install the MathSAT solver on Mac OS Ventura + Apple silicon (M2)

  #762 opened a year ago by paolomorettin
  2

• distutils is removed from Python 3.12 standard library

  #764 opened a year ago by hauff
  1

• Z3 works while Yices fails simple example

  #753 opened a year ago by matteocarde
  9

• Support for continuous subtraction

  #763 opened a year ago by fuqi-jia
  2

• Support Cython 3.0.0

  #759 opened a year ago by kesslermaximilian
  1

• SMTLIB Parser cant parse MOD operation

  #760 opened a year ago by PinkFrojdSenjak
  0

• Fastest way to create a (big) model

  #758 opened a year ago by MarcoMochi
  3

• Using solvers that are obtained by other means (such as homebrew)

  #757 opened a year ago by algebravic
  1

• Cannot install msat solver on MacOs with M1

  #709 opened 3 years ago by chiara-camilla-rambaldi-migliore
  11

• Failing to install solvers on Apple M1 chip

  #751 opened 2 years ago by ninell-oldenburg
  4

• Your thought about Integration to IDE.

  #749 opened 2 years ago by PorcoRosso85
  2

• The "bvxnor" operator seems to be misdefined

  #747 opened 2 years ago by YikeZhou
  1

• Substitution issue for ForAll using MGSubstituter

  #746 opened 2 years ago by SSharath-Kumar
  3

• Mathsat support for NRA and NTA

  #729 opened 2 years ago by masinag
  10

• Converting PySMT formulas to Z3Py ones

  #742 opened 2 years ago by panda2134
  4

• CNF conversion improvement

  #743 opened 2 years ago by masinag
  0

• Question about evaluate-command in pysmt/smtlib/script.py

  #716 opened 3 years ago by alxxalx
  6

• Division by constant

  #741 opened 2 years ago by TuomLarsen
  0

• ImportError: No module named shortcuts

  #737 opened 2 years ago by ashfaq92
  5

• SmtLibScript generates invalid SMT declare-const instrutions when writing on file

  #736 opened 2 years ago by gabriele-costa
  0

• Unexpected solution to an ILP instance encoded as a logical formula

  #735 opened 2 years ago by akumm2k
  1

• test_ackermannization_for_examples failure

  #731 opened 2 years ago by marcogario
  1

• TypeError: '<=' not supported between instances of 'str' and 'Logic' (PySMT==0.9.1.dev139)

  #708 opened 2 years ago by danyalette
  2

• Reading SMT-LIB causes Errors

  #692 opened 2 years ago by lycurgus8
  4

• Make FormulaContextualizer singleton in env

  #696 opened 2 years ago by enmag
  2

• Find all solutions

  #725 opened 2 years ago by fortierq
  2

• pysmt-install: Installed yices binary is broken on older platforms

  #690 opened 2 years ago by csH7KmCC9
  7

• Error installing CVC4 on Ubuntu 20.04 (Python 3.8.10)

  #707 opened 2 years ago by danyalette
  4

• Spring Cleaning 2022 :broom:

  #717 opened 3 years ago by marcogario
  2

• Tag the source

  #693 opened 2 years ago by fabaff
  1

• Solver timeout

  #689 opened 3 years ago by csH7KmCC9
  3

• Is Linear Integer Arithmetic (LIA) supported?

  #715 opened 3 years ago by jparsert
  2

• No Solver is available

  #704 opened 3 years ago by UnReAlKiNg
  1

• Question about the efsmt example

  #702 opened 3 years ago by rainoftime
  2

• Parser problem on `<->`

  #701 opened 3 years ago by aehyvari
  0

• msat named unsatcore might ignore non-boolean assumption

  #694 opened 3 years ago by enmag
  0

• Improve the CLI of `pysmt-install`

  #687 opened 4 years ago by mikand
  0

• Error installing pysmt

  #686 opened 4 years ago by HeyItsBethany3
  6

• BDD-based solver gives segfault with swig4

  #682 opened 4 years ago by mikand
  2