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

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-11 21:08:53 +02:00
parent cab1076514
commit a4f4975092
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -401,7 +401,12 @@ namespace q {
for (expr* arg : ors) { for (expr* arg : ors) {
bool sign = m.is_not(arg, arg); bool sign = m.is_not(arg, arg);
expr* l, *r; expr* l, *r;
if (!m.is_eq(arg, l, r) || is_ground(arg)) { if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
l = to_app(arg)->get_arg(0);
r = to_app(arg)->get_arg(1);
sign = !sign;
}
else if (!m.is_eq(arg, l, r) || is_ground(arg)) {
l = arg; l = arg;
r = sign ? m.mk_false() : m.mk_true(); r = sign ? m.mk_false() : m.mk_true();
sign = false; sign = false;