mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix #2253

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-27 14:24:53 -07:00
parent 9f1b8db870
commit 9cb1a0f094
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_context.cpp
View file

@ -361,7 +361,8 @@ namespace opt {
void context::fix_model(model_ref& mdl) { void context::fix_model(model_ref& mdl) {
if (mdl && !m_model_fixed.contains(mdl.get())) { 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); (*m_fm)(mdl);
apply(m_model_converter, mdl); apply(m_model_converter, mdl);
m_model_fixed.push_back(mdl.get()); m_model_fixed.push_back(mdl.get());

4
src/tactic/arith/lia2card_tactic.cpp
View file

@ -143,7 +143,9 @@ public:
expr_ref last_v(m); expr_ref last_v(m);
if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card"); if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card");
if (hi == 0) { 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) { if (lo > 0) {
xs.push_back(a.mk_int(lo)); xs.push_back(a.mk_int(lo));