diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 04385b392..eb394c59f 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -374,6 +374,8 @@ namespace mbp {
                     ts.push_back(var2expr(index2expr, v));                
                 if (!d.m_coeff.is_zero())
                     ts.push_back(a.mk_numeral(d.m_coeff, is_int));
+                if (ts.empty())
+                    ts.push_back(a.mk_numeral(rational(0), is_int));
                 t = mk_add(ts);
                 if (!d.m_div.is_one() && is_int) 
                     t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));                
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 58ceab662..74856ccbe 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -166,9 +166,9 @@ namespace q {
         todo.push_back(e);
         while (!todo.empty()) {
             expr* t = todo.back();
+            todo.pop_back();
             if (m_mark.is_marked(t))
                 continue;
-            todo.pop_back();
             m_mark.mark(t);
             if (is_ground(t)) {
                 add_watch(ctx.get_egraph().find(t), clause_idx);