From cb7e53aae4f32ff9090b87eb148f6477cf137195 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Nov 2017 10:04:32 -0800 Subject: [PATCH] reset backtrack level at each cube Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Solver.cs | 6 +++--- src/api/python/z3/z3.py | 4 +++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 4a779e91b..24a0bbc61 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -364,9 +364,10 @@ namespace Microsoft.Z3 /// public IEnumerable Cube() { - int rounds = 0; while (true) { - BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, BacktrackLevel)); + var lvl = BacktrackLevel; + BacktrackLevel = uint.MaxValue; + BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl)); if (r.IsFalse) { break; } @@ -374,7 +375,6 @@ namespace Microsoft.Z3 yield return r; break; } - ++rounds; yield return r; } } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 2ae7e6ced..1402d1ce7 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6287,7 +6287,9 @@ class Solver(Z3PPObject): def cube(self): """Get set of cubes""" while True: - r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, self.backtrack_level), self.ctx) + lvl = self.backtrack_level + self.backtrack_level = 4000000000 + r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx) if (is_false(r)): return if (is_true(r)):