From d9452279040ab25bcd2e594a281a99e68393fc06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Mar 2020 15:08:19 -0700 Subject: [PATCH] fix ? #3423 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 2 +- src/smt/dyn_ack.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6441f1462..787b7a8a2 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1691,7 +1691,7 @@ void cmd_context::display_model(model_ref& mdl) { add_declared_functions(*mdl); if (p.v1() || p.v2()) { std::ostringstream buffer; - model_v2_pp(buffer, *mdl, p.partial()); + model_v2_pp(buffer, *mdl, false); regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl; } else { regular_stream() << "(model " << std::endl; diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index eea3aef5c..aa4ec4ac2 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -360,6 +360,7 @@ namespace smt { if (m_clause2app_pair.find(cls, p)) { SASSERT(p.first && p.second); m_instantiated.erase(p); + m_clause2app_pair.erase(cls); SASSERT(!m_app_pair2num_occs.contains(p.first, p.second)); return; } @@ -367,6 +368,7 @@ namespace smt { if (m_triple.m_clause2apps.find(cls, tr)) { SASSERT(tr.first && tr.second && tr.third); m_triple.m_instantiated.erase(tr); + m_triple.m_clause2apps.erase(cls); SASSERT(!m_triple.m_app2num_occs.contains(tr.first, tr.second, tr.third)); return; }