mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #6457

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-24 14:41:50 +07:00
parent 4ac5e51e3a
commit eceeb295fc
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2388,7 +2388,9 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
expr* a = nullptr, *b = nullptr, *c = nullptr;
if (m().is_ite(lhs, a, b, c)) {
bool_rewriter rw(m());
result = rw.mk_ite(a, rw.mk_eq(b, rhs), rw.mk_eq(c, rhs));
expr_ref e1(rw.mk_eq(b, rhs), m());
expr_ref e2(rw.mk_eq(c, rhs), m());
result = rw.mk_ite(a, e1, e2);
return BR_REWRITE2;
}