mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix unsound rewrite

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-20 18:55:40 +01:00
parent f075dc2882
commit 53ca65a62e
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -5954,6 +5954,7 @@ bool seq_rewriter::reduce_non_overlap(expr_ref_vector& ls, expr_ref_vector& rs,
*/ */
bool seq_rewriter::reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) { bool seq_rewriter::reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) {
ptr_buffer<expr> es; ptr_buffer<expr> es;
if (ls.empty() || rs.empty()) if (ls.empty() || rs.empty())
return true; return true;
es.append(ls.size(), ls.data()); es.append(ls.size(), ls.data());
@ -5976,7 +5977,12 @@ bool seq_rewriter::reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs,
if (!is_unit_value(r)) if (!is_unit_value(r))
return true; return true;
} }
return any_of(es, [&](expr* e) { return is_unit_value(e); }); if (es.empty())
return true;
for (expr* e : es)
if (!is_unit_value(e))
return true;
return false;
} }
bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) { bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) {