mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix #3599

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 13:53:32 -07:00
parent e2a247a64a
commit ea6f9eb9b6
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_array_full.cpp
View file

@ -187,8 +187,9 @@ namespace smt {
ptr_vector<enode> & as_arrays = m_var_data_full[v]->m_as_arrays;
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(as_arrays));
as_arrays.push_back(arr);
instantiate_default_as_array_axiom(arr);
for (enode * n : d->m_parent_selects) {
instantiate_default_as_array_axiom(arr);
for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
enode* n = d->m_parent_selects[i];
SASSERT(is_select(n));
instantiate_select_as_array_axiom(n, arr);
}