diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 83e83cfe7..1acbb592b 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1261,8 +1261,7 @@ namespace opt {
             m_var2value[x] = eval(result);
             TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
         }
-        else 
-            retire_row(row_id1);
+        retire_row(row_id1);
         return result;
     }
     
diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index a2101e2d1..8b855a758 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -319,6 +319,14 @@ namespace mbp {
                     tids.insert(v, mbo.add_var(r, a.is_int(v)));
                 }
             }
+
+            // bail on variables in non-linear sub-terms
+            for (auto& kv : tids) {
+                expr* e = kv.m_key;
+                if (is_arith(e) && !var_mark.is_marked(e)) 
+                    mark_rec(fmls_mark, e);                
+            }
+
             if (m_check_purified) {
                 for (expr* fml : fmls) 
                     mark_rec(fmls_mark, fml);                
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 9c652ac10..739cbf9b7 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -288,8 +288,7 @@ namespace euf {
         expr* e = m_bool_var2expr.get(l.var(), nullptr);
         TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
         if (!e) 
-            return;        
-        
+            return;                
         euf::enode* n = m_egraph.find(e);
         if (!n)
             return;
@@ -303,21 +302,28 @@ namespace euf {
         SASSERT(l == get_literal(c));
 	    if (n->value_conflict()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
+            euf::enode* r = n->get_root();
+            euf::enode* rb = sign ? mk_true() : mk_false();
+            sat::literal rl(r->bool_var(), r->value() == l_false);
             m_egraph.merge(n, nb, c);
+            m_egraph.merge(r, rb, to_ptr(rl));
+            SASSERT(m_egraph.inconsistent());
             return;
 	    }
         if (n->merge_tf()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }
-        if (!sign && n->is_equality()) {
-            SASSERT(!m.is_iff(e));
-            euf::enode* na = n->get_arg(0);
-            euf::enode* nb = n->get_arg(1);
-            m_egraph.merge(na, nb, c);
-        }
-        else if (sign && n->is_equality())
-            m_egraph.new_diseq(n);      
+        if (n->is_equality()) {
+            if (sign)
+                m_egraph.new_diseq(n);
+            else {
+                SASSERT(!m.is_iff(e));
+                euf::enode* na = n->get_arg(0);
+                euf::enode* nb = n->get_arg(1);
+                m_egraph.merge(na, nb, c);
+            }
+        }    
     }