From 953ea7c88069d2221547035a3dd21166703c822d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Feb 2020 23:08:59 -0800
Subject: [PATCH] fix #3044
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_array.cpp | 9 ++++++---
src/smt/theory_array_base.cpp | 4 ++--
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index d80660727..65095e5b3 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -334,14 +334,17 @@ namespace smt {
enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v_arg = arg->get_th_var(get_id());
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)) {
- add_parent_select(v_arg, ctx.get_enode(n));
+ add_parent_select(v_arg, e);
}
else {
SASSERT(is_store(n));
if (m_params.m_array_laziness > 1)
- instantiate_axiom1(ctx.get_enode(n));
- add_parent_store(v_arg, ctx.get_enode(n));
+ instantiate_axiom1(e);
+ add_parent_store(v_arg, e);
}
}
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 8e681c7ab..e63474479 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -342,8 +342,8 @@ namespace smt {
args1.push_back(k);
args2.push_back(k);
}
- expr * sel1 = mk_select(args1.size(), args1.c_ptr());
- expr * sel2 = mk_select(args2.size(), args2.c_ptr());
+ expr_ref sel1(mk_select(args1.size(), args1.c_ptr()), m);
+ 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";);
literal n1_eq_n2 = mk_eq(e1, e2, true);
literal sel1_eq_sel2 = mk_eq(sel1, sel2, true);