From 7d976e4f4dfee996575a93f7d4fa1ef0eb43ac15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Mar 2020 06:49:38 +0100 Subject: [PATCH] fix #3120 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 6 +++--- src/sat/tactic/goal2sat.h | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5acf273fe..215fc0d91 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -879,11 +879,11 @@ private: } TRACE("sat", m_solver.display_model(tout);); sat::model ll_m = m_solver.get_model(); + mdl = alloc(model, m); if (m_sat_mc) { (*m_sat_mc)(ll_m); - } - mdl = alloc(model, m); - for (sat::bool_var v = 0; v < ll_m.size(); ++v) { + } + for (sat::bool_var v = 0; m_sat_mc && v < m_sat_mc->num_vars(); ++v) { expr* n = m_sat_mc->var2expr(v); if (!n || !is_app(n) || to_app(n)->get_num_args() > 0) { continue; diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 31e94bd74..7ccba173e 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -96,6 +96,7 @@ public: void set_env(ast_pp_util* visitor) override; void display(std::ostream& out) override; void get_units(obj_map& units) override; + unsigned num_vars() const { return m_var2expr.size(); } app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } expr_ref lit2expr(sat::literal l); void insert(sat::bool_var v, app * atom, bool aux);