mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

handle return status

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-04 20:19:15 +02:00
parent 4f6811a6a2
commit 053cb72cc2
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
examples/python/efsmt.py
View file

@ -16,20 +16,21 @@ def efsmt(ys, phi, maxloops = None):
while maxloops is None or loops <= maxloops: while maxloops is None or loops <= maxloops:
loops += 1 loops += 1
eres = E.check() eres = E.check()
if eres == unsat: if eres == sat:
return unsat
else:
emodel = E.model() emodel = E.model()
sub_phi = substitute(phi, [(x, emodel.eval(x, True)) for x in xs]) sub_phi = substitute(phi, [(x, emodel.eval(x, True)) for x in xs])
F.push() F.push()
F.add(Not(sub_phi)) F.add(Not(sub_phi))
if F.check() == sat: fres = F.check()
if fres == sat:
fmodel = F.model() fmodel = F.model()
sub_phi = substitute(phi, [(y, fmodel.eval(y, True)) for y in ys]) sub_phi = substitute(phi, [(y, fmodel.eval(y, True)) for y in ys])
E.add(sub_phi) E.add(sub_phi)
else: else:
return sat, [(x, emodel.eval(x, True)) for x in xs] return fres, [(x, emodel.eval(x, True)) for x in xs]
F.pop() F.pop()
else:
return eres
return unknown return unknown
x, y, z = Reals("x y z") x, y, z = Reals("x y z")