From 79ababb00ad97f1b5d52d051045be8dc30c16834 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Mar 2021 11:38:33 -0800 Subject: [PATCH] force push --- src/sat/tactic/goal2sat.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d774e30a1..0a1e11b2b 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -280,7 +280,7 @@ struct goal2sat::imp : public sat::sat_internalizer { void cache(app* t, sat::literal l) override { - SASSERT(m_num_scopes == 0); + force_push(); SASSERT(!m_app2lit.contains(t)); SASSERT(!m_lit2app.contains(l.index())); m_app2lit.insert(t, l); @@ -817,6 +817,7 @@ struct goal2sat::imp : public sat::sat_internalizer { sat::literal result = m_result_stack.back(); m_result_stack.pop_back(); if (!result.sign() && m_map.to_bool_var(n) == sat::null_bool_var) { + force_push(); m_map.insert(n, result.var()); m_solver.set_external(result.var()); }