mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
b49ffb8a87
commit
616fc2cbd5
|
@ -732,7 +732,7 @@ void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, exp
|
|||
auto check_reduce = [&](expr* a, expr* b) {
|
||||
if (bv.is_extract(a, lo, hi, x) && lo > 0 && hi + 1 == bv.get_bv_size(x) && bv.is_numeral(b, r) && r == 0) {
|
||||
// insert x -> x[0,lo-1] ++ n into sub
|
||||
new_term = bv.mk_concat(bv.mk_extract(lo - 1, 0, x), b);
|
||||
new_term = bv.mk_concat(b, bv.mk_extract(lo - 1, 0, x));
|
||||
m_sub.insert(x, new_term);
|
||||
n = j.get_fml();
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue