From 35eb21bc35a996b0fef387062f29673b78a7b189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Jan 2019 09:06:41 -0800 Subject: [PATCH] fix extraction of trail Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 04d7456b8..43b361b5f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6731,7 +6731,7 @@ class Solver(Z3PPObject): """Return trail and decision levels of the solver state after a check() call. """ trail = self.trail() - levels = (ctypes.c_uint * len(trail)) + levels = (ctypes.c_uint * len(trail))() Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels) return trail, levels diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index fd795dbc7..f0712da38 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -324,7 +324,7 @@ public: depth.resize(sz); for (unsigned i = 0; i < sz; ++i) { auto bv = m_map.to_bool_var(vars[i]); - depth = bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); + depth[i] = bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); } }