diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 60a9bd734..7711ec4cd 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7241,11 +7241,13 @@ class Optimize(Z3PPObject): def assert_exprs(self, *args): """Assert constraints as background axioms for the optimize solver.""" args = _get_args(args) + s = BoolSort(self.ctx) for arg in args: if isinstance(arg, Goal) or isinstance(arg, AstVector): for f in arg: Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast()) else: + arg = s.cast(arg) Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast()) def add(self, *args):