mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #3044

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-18 23:08:59 -08:00
parent 4bad2dd92c
commit 953ea7c880
2 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_array.cpp
View file

@ -334,14 +334,17 @@ namespace smt {
enode * arg = ctx.get_enode(n->get_arg(0)); enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v_arg = arg->get_th_var(get_id()); theory_var v_arg = arg->get_th_var(get_id());
SASSERT(v_arg != null_theory_var); SASSERT(v_arg != null_theory_var);
if (!ctx.e_internalized(n)) ctx.internalize(n, false);
enode* e = ctx.get_enode(n);
if (is_select(n)) { if (is_select(n)) {
add_parent_select(v_arg, ctx.get_enode(n)); add_parent_select(v_arg, e);
} }
else { else {
SASSERT(is_store(n)); SASSERT(is_store(n));
if (m_params.m_array_laziness > 1) if (m_params.m_array_laziness > 1)
instantiate_axiom1(ctx.get_enode(n)); instantiate_axiom1(e);
add_parent_store(v_arg, ctx.get_enode(n)); add_parent_store(v_arg, e);
} }
} }

4
src/smt/theory_array_base.cpp
View file

@ -342,8 +342,8 @@ namespace smt {
args1.push_back(k); args1.push_back(k);
args2.push_back(k); args2.push_back(k);
} }
expr * sel1 = mk_select(args1.size(), args1.c_ptr()); expr_ref sel1(mk_select(args1.size(), args1.c_ptr()), m);
expr * sel2 = mk_select(args2.size(), args2.c_ptr()); expr_ref sel2(mk_select(args2.size(), args2.c_ptr()), m);
TRACE("ext", tout << mk_bounded_pp(sel1, m) << "\n" << mk_bounded_pp(sel2, m) << "\n";); TRACE("ext", tout << mk_bounded_pp(sel1, m) << "\n" << mk_bounded_pp(sel2, m) << "\n";);
literal n1_eq_n2 = mk_eq(e1, e2, true); literal n1_eq_n2 = mk_eq(e1, e2, true);
literal sel1_eq_sel2 = mk_eq(sel1, sel2, true); literal sel1_eq_sel2 = mk_eq(sel1, sel2, true);