From 9cb1a0f09483babff5bce783629104d3d82c8e33 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 14:24:53 -0700 Subject: [PATCH] fix #2253 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 3 ++- src/tactic/arith/lia2card_tactic.cpp | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 7ca2c774b..25d3640ac 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -361,7 +361,8 @@ namespace opt { void context::fix_model(model_ref& mdl) { if (mdl && !m_model_fixed.contains(mdl.get())) { - TRACE("opt", tout << "fix-model\n";); + TRACE("opt", m_fm->display(tout << "fix-model\n"); + m_model_converter->display(tout);); (*m_fm)(mdl); apply(m_model_converter, mdl); m_model_fixed.push_back(mdl.get()); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 027b6d91c..c2c90284c 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -143,7 +143,9 @@ public: expr_ref last_v(m); if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card"); if (hi == 0) { - return expr_ref(a.mk_int(0), m); + expr* r = a.mk_int(0); + m_mc->add(x->get_decl(), r); + return expr_ref(r, m); } if (lo > 0) { xs.push_back(a.mk_int(lo));