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

fix #6061

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-31 19:09:10 -07:00
parent e9cff33feb
commit a9d70fca1a
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/arith_solver.cpp
View file

@ -321,7 +321,7 @@ namespace arith {
reset_evidence();
for (auto ev : e)
set_evidence(ev.ci());
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2);
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2); // TODO add equality explanation
ctx.propagate(n1, n2, jst->to_index());
return true;
}
@ -756,7 +756,7 @@ namespace arith {
set_evidence(ci4);
enode* x = var2enode(v1);
enode* y = var2enode(v2);
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y);
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y); // TODO add equality explanation
ctx.propagate(x, y, jst->to_index());
}

2
src/smt/mam.cpp
View file

@ -1952,7 +1952,7 @@ namespace {
m_args[i] = m_registers[pc->m_iregs[i]]->get_root();
SASSERT(n != 0);
do {
if (n->get_decl() == f) {
if (n->get_decl() == f && n->get_num_args() == num_args) {
unsigned i = 0;
for (; i < num_args; i++) {
if (n->get_arg(i)->get_root() != m_args[i])