mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5215

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-19 10:03:49 -07:00
parent 7b3a587505
commit d450fd4227
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/qe/mbp/mbp_arith.cpp
View file

@ -374,6 +374,8 @@ namespace mbp {
ts.push_back(var2expr(index2expr, v)); ts.push_back(var2expr(index2expr, v));
if (!d.m_coeff.is_zero()) if (!d.m_coeff.is_zero())
ts.push_back(a.mk_numeral(d.m_coeff, is_int)); 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); t = mk_add(ts);
if (!d.m_div.is_one() && is_int) if (!d.m_div.is_one() && is_int)
t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int)); t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));

2
src/sat/smt/q_ematch.cpp
View file

@ -166,9 +166,9 @@ namespace q {
todo.push_back(e); todo.push_back(e);
while (!todo.empty()) { while (!todo.empty()) {
expr* t = todo.back(); expr* t = todo.back();
todo.pop_back();
if (m_mark.is_marked(t)) if (m_mark.is_marked(t))
continue; continue;
todo.pop_back();
m_mark.mark(t); m_mark.mark(t);
if (is_ground(t)) { if (is_ground(t)) {
add_watch(ctx.get_egraph().find(t), clause_idx); add_watch(ctx.get_egraph().find(t), clause_idx);