From d450fd4227122bb5fae139f4c15ea1c4c8403db4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 May 2021 10:03:49 -0700
Subject: [PATCH] #5215

---
 src/qe/mbp/mbp_arith.cpp | 2 ++
 src/sat/smt/q_ematch.cpp | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 04385b392c9..eb394c59fd1 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 58ceab66213..74856ccbe5a 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);