mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix #3954

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-14 08:17:57 -07:00
parent b8c069c6b7
commit 2a0537af69
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_array_full.cpp
View file

@ -89,7 +89,8 @@ namespace smt {
d_full->m_parent_maps.push_back(s); d_full->m_parent_maps.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps)); m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps));
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode * n : d->m_parent_selects) { for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
enode * n = d->m_parent_selects[i];
if (!m_params.m_array_cg || n->is_cgr()) { if (!m_params.m_array_cg || n->is_cgr()) {
instantiate_select_map_axiom(n, s); instantiate_select_map_axiom(n, s);
} }
@ -172,7 +173,8 @@ namespace smt {
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(consts)); m_trail_stack.push(push_back_trail<theory_array, enode *, false>(consts));
consts.push_back(cnst); consts.push_back(cnst);
instantiate_default_const_axiom(cnst); instantiate_default_const_axiom(cnst);
for (enode * n : d->m_parent_selects) { for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
enode * n = d->m_parent_selects[i];
SASSERT(is_select(n)); SASSERT(is_select(n));
instantiate_select_const_axiom(n, cnst); instantiate_select_const_axiom(n, cnst);
} }