The crash you observed has been fixed, and the fix will be available in the next release. If you try the "unstable" (work-in-progress) branch, you should get the expected behavior. You can retrieve the unstable branch using
git clone https://git01.codeplex.com/z3 -b unstable
The API parse_smt2_string
provides only basic support for parsing formulas in SMT 2.0 format. It does not keep the annotations :named
. We will address this and other limitations in future versions. In the meantime, we should use "answer literals" such as p1
and assertions of the form:
solver.add(z3.Implies(p1, z3.Not(0 == 0)))
In the "unstable" branch, we also support the following new API. It "simulates" the :named
assertions used in the SMT 2.0 standard.
def assert_and_track(self, a, p):
"""Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
If `p` is a string, it will be automatically converted into a Boolean constant.
>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Solver()
>>> s.set(unsat_core=True)
>>> s.assert_and_track(x > 0, 'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0, p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True
"""
...