search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
114 stars 43 forks source link

Fix issue with GMP backed pysmt #321

Closed cdonovick closed 1 year ago

cdonovick commented 1 year ago

I bug was reported to me by @cterrill26 when pySMT uses GMP to for integer constants that the converter fails (see https://github.com/pysmt/pysmt/blob/master/pysmt/constants.py).

This bug results from (repr(formula.constant_value()) returning "mpz(value)" (with value being an integer constant) where we want "value". Using str instead of repr resolves this problem.

I submit no tests of this change as doing so would require building with GMP present and without.