mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-09-01 04:58:41 -07:00
commit 74a2bf1588
11 changed files with 332 additions and 193 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -127,13 +127,13 @@ namespace euf {
SASSERT(n);
SASSERT(m_egraph.is_equality(n));
SASSERT(!l.sign());
m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1));
break;
case constraint::kind_t::lit:
n = m_var2node[l.var()];
SASSERT(n);
SASSERT(m.is_bool(n->get_owner()));
m_egraph.explain_eq<unsigned>(m_explain, n, (l.sign() ? mk_false() : mk_true()), false);
m_egraph.explain_eq<unsigned>(m_explain, n, (l.sign() ? mk_false() : mk_true()));
break;
default:
IF_VERBOSE(0, verbose_stream() << (unsigned)j.kind() << "\n");