search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

`Z3_solver_reset` may not properly reset parser context #7260

Closed pclayton closed 2 weeks ago

pclayton commented 2 weeks ago

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:

>>> s.reset()
>>> s.from_string("(declare-const r1 Bool)")

This may be related to https://github.com/Z3Prover/z3/commit/815518d introduced in 4.9.0 but I haven't checked. Or have I misunderstood how Z3_solver_reset interacts with parser contexts?