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));