#5454

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 16, 2021 · 3d13c03 · 3d13c03
1 parent 6a3ba64
commit 3d13c03
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 10 deletions.
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
@@ -175,18 +175,14 @@ namespace array {
         ptr_buffer<expr> sel1_args, sel2_args;
         unsigned num_args = select->get_num_args();
 
-        if (select->get_arg(0) != store && expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root()) 
-            return false;
         bool has_diff = false;
         for (unsigned i = 1; i < num_args; i++) 
             has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
         if (!has_diff)
             return false;
 
-
         sel1_args.push_back(store);
-        sel2_args.push_back(store->get_arg(0));
-
+        sel2_args.push_back(store->get_arg(0));        
 
         for (unsigned i = 1; i < num_args; i++) {
             sel1_args.push_back(select->get_arg(i));

diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
@@ -228,11 +228,8 @@ namespace array {
 
         auto& d = get_var_data(v);
 
-        for (euf::enode* lambda : d.m_lambdas) {
-            expr* e = lambda->get_expr();
-            if (a.is_const(e) || a.is_map(e)) 
-                propagate_select_axioms(d, lambda);
-        }
+        for (euf::enode* lambda : d.m_lambdas) 
+            propagate_select_axioms(d, lambda);        
 
         for (euf::enode* lambda : d.m_parent_lambdas)
             propagate_select_axioms(d, lambda);