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

#5646

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-11-03 08:52:48 -07:00
parent dd1e0fc561
commit af2cc460a9
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_recfun.cpp
View file

@ -254,14 +254,16 @@ namespace smt {
ctx.internalize_assertions(); ctx.internalize_assertions();
lit = mk_literal(fn); lit = mk_literal(fn);
} }
else if (m.is_true(r) || m.is_false(r)) else {
std::swap(l, r); if (m.is_true(r) || m.is_false(r))
else if (m.is_true(l)) std::swap(l, r);
lit = mk_literal(r); if (m.is_true(l))
else if (m.is_false(l)) lit = mk_literal(r);
lit = ~mk_literal(r); else if (m.is_false(l))
else lit = ~mk_literal(r);
lit = mk_eq(l, r, false); else
lit = mk_eq(l, r, false);
}
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);
return lit; return lit;
} }