From bc8681a0ea5441a7741b29380b118e59ad656d28 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Nov 2017 22:14:59 -0800 Subject: [PATCH] reset backtrack level after first backtrack Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 6 +++--- src/sat/sat_lookahead.cpp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 45fedc674..2ae7e6ced 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -5988,6 +5988,7 @@ class Solver(Z3PPObject): def __init__(self, solver=None, ctx=None): assert solver is None or ctx is not None self.ctx = _get_ctx(ctx) + self.backtrack_level = 4000000000 self.solver = None if solver is None: self.solver = Z3_mk_solver(self.ctx.ref()) @@ -6283,11 +6284,10 @@ class Solver(Z3PPObject): consequences = [ consequences[i] for i in range(sz) ] return CheckSatResult(r), consequences - def cube(self, level_ref): + def cube(self): """Get set of cubes""" while True: - backtrack_level = level_ref.backtrack_level - r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, backtrack_level), self.ctx) + r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, self.backtrack_level), self.ctx) if (is_false(r)): return if (is_true(r)): diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index e4878df42..27d174653 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2012,8 +2012,8 @@ namespace sat { set_conflict(); backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); } - backtrack_level = UINT_MAX; } + backtrack_level = UINT_MAX; depth = m_cube_state.m_cube.size(); if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {