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