mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

remove Z3_bool_opt #5757

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-07 11:52:10 -08:00
parent 7baa4f88b0
commit 199daead50
7 changed files with 37 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/bool_rewriter.cpp
View file

@ -722,12 +722,12 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return BR_DONE;
}
if (m().is_not(rhs))
if (m().is_not(rhs))
std::swap(lhs, rhs);
if (m().is_not(lhs, lhs)) {
result = m().mk_not(m().mk_eq(lhs, rhs));
return BR_REWRITE2;
if (m().is_not(lhs, lhs)) {
result = m().mk_not(m().mk_eq(lhs, rhs));
return BR_REWRITE2;
}
if (unfolded) {