mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fix #1736

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-06 21:44:16 -07:00
parent ecb5c45d6f
commit dc932a93e2
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -7241,11 +7241,13 @@ class Optimize(Z3PPObject):
def assert_exprs(self, *args): def assert_exprs(self, *args):
"""Assert constraints as background axioms for the optimize solver.""" """Assert constraints as background axioms for the optimize solver."""
args = _get_args(args) args = _get_args(args)
s = BoolSort(self.ctx)
for arg in args: for arg in args:
if isinstance(arg, Goal) or isinstance(arg, AstVector): if isinstance(arg, Goal) or isinstance(arg, AstVector):
for f in arg: for f in arg:
Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast()) Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
else: else:
arg = s.cast(arg)
Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast()) Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
def add(self, *args): def add(self, *args):