You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When switching from Z3 4.8.12 to 4.13.0, I have found that Z3_solver_from_string produces an error where it did not previously. With 4.13.0, there is no error the first time a solver s is used. However, after s has been reset using Z3_solver_reset, Z3_solver_from_string produces an error if the string argument declares a const that was previously declared before s was reset. This can be seen in the following Python transcript:
$ python -i
Python 3.11.4 (tags/v3.11.4:d2340ef, Jun 7 2023, 05:45:37) [MSC v.1934 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> s = Solver()
>>> s.from_string("(declare-const r1 Bool)")
>>> s.reset()
>>> s.from_string("(declare-const r1 Bool)")
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "C:\msys64\usr\share\python\Lib\site-packages\z3\z3.py", line 7274, in from_string
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
File "C:\msys64\usr\share\python\Lib\site-packages\z3\z3core.py", line 4138, in Z3_solver_from_string
_elems.Check(a0)
File "C:\msys64\usr\share\python\Lib\site-packages\z3\z3core.py", line 1554, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 23: invalid declaration, constant \'r1\' (with the given signature) already declared")\n'
Strangely, after this error, resetting s again does appear to clear the parser context because no error is produced when the declaration is repeated:
When switching from Z3 4.8.12 to 4.13.0, I have found that
Z3_solver_from_string
produces an error where it did not previously. With 4.13.0, there is no error the first time a solvers
is used. However, afters
has been reset usingZ3_solver_reset
,Z3_solver_from_string
produces an error if the string argument declares a const that was previously declared befores
was reset. This can be seen in the following Python transcript:Strangely, after this error, resetting
s
again does appear to clear the parser context because no error is produced when the declaration is repeated:This may be related to 815518d introduced in 4.9.0 but I haven't checked. Or have I misunderstood how
Z3_solver_reset
interacts with parser contexts?The text was updated successfully, but these errors were encountered: