From e2c5e2e39cb1118b7d452e56e0f149ffa43ae767 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 31 May 2021 12:32:33 -0700
Subject: [PATCH] na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/smt/array_axioms.cpp | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 26cfc08fe..5259f3168 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -197,12 +197,19 @@ namespace array {
expr_ref sel2(a.mk_select(sel2_args), m);
expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m);
+ bool new_prop = false;
+ if (!ctx.get_egraph().find(sel1))
+ new_prop = true;
+ if (!ctx.get_egraph().find(sel2))
+ new_prop = true;
+
euf::enode* s1 = e_internalize(sel1);
euf::enode* s2 = e_internalize(sel2);
TRACE("array",
tout << "select-store " << ctx.bpp(s1) << " " << ctx.bpp(s1->get_root()) << "\n";
tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";);
+
if (s1->get_root() == s2->get_root())
return new_prop;