mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

remove proviso for single index arrays

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-19 00:02:38 -08:00
parent 3e5abef145
commit 075773e519
1 changed files with 2 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -67,15 +67,11 @@ struct mbp_array_tg::impl {
}
bool is_wr_on_rhs(expr *lhs, expr *rhs) {
return (is_arr_write(rhs) && !is_arr_write(lhs));
return is_arr_write(rhs) && !is_arr_write(lhs);
}
bool is_arr_write(expr *t) {
return m_array_util.is_store1(t) && has_var(to_app(t));
}
bool is_arr_write(expr *t, expr*& a, expr*& i, expr*& v) {
return m_array_util.is_store1(t, a, i, v) && has_var(to_app(t));
return m_array_util.is_store(t) && has_var(to_app(t));
}
// Returns true if e has a subterm store(v) where v is a variable to be