From b1724b2f629e71e7bdf8b104dd052bfc95b140f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Dec 2017 14:39:16 -0800 Subject: [PATCH] fix update to variables Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 257cf3b53..6d78bc331 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -926,7 +926,7 @@ model_converter* sat2goal::mc::translate(ast_translation& translator) { void sat2goal::mc::collect(ast_pp_util& visitor) { flush_gmc(); - collect(visitor); + if (m_gmc) m_gmc->collect(visitor); } void sat2goal::mc::display(std::ostream& out) { @@ -995,6 +995,10 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { } expr_ref sat2goal::mc::lit2expr(sat::literal l) { + if (!m_var2expr.get(l.var())) { + app* aux = m.mk_fresh_const(0, m.mk_bool_sort()); + m_var2expr.set(l.var(), aux); + } VERIFY(m_var2expr.get(l.var())); expr_ref result(m_var2expr.get(l.var()), m); if (l.sign()) {