mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

build fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-11-17 10:15:01 -08:00
parent b9455c3692
commit a9f9d3ddf4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -109,7 +109,7 @@ struct mbp_array_tg::impl {
bool is_rd_wr(expr *t) { bool is_rd_wr(expr *t) {
expr* a, *idx; expr* a, *idx;
return m_array_util.is_select1(t, a, idx) && return m_array_util.is_select1(t, a, idx) &&
m_array_util.is_store(a) & m_array_util.is_store(a) &&
has_stores(a); has_stores(a);
} }
@ -208,7 +208,7 @@ struct mbp_array_tg::impl {
if (in) { if (in) {
SASSERT(m_mdl.are_equal(j, eq_index)); SASSERT(m_mdl.are_equal(j, eq_index));
peq p_new = peq p_new =
mk_wr_peq(to_app(a, p.rhs(), indices); mk_wr_peq(a, p.rhs(), indices);
m_tg.add_eq(j, eq_index); m_tg.add_eq(j, eq_index);
expr_ref p_new_expr(m); expr_ref p_new_expr(m);
p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq(); p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq();