From fe0727d8891856f34881320190d3ad957c94ab6d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 31 May 2021 12:29:31 -0700
Subject: [PATCH] #5223

---
 src/sat/smt/array_axioms.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 0954ef096..6ab6df192 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -177,15 +177,16 @@ namespace array {
 
         if (expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root())
             return false;
-
-        sel1_args.push_back(store);
-        sel2_args.push_back(store->get_arg(0));
-        
         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));
+        
         
         for (unsigned i = 1; i < num_args; i++) {
             sel1_args.push_back(select->get_arg(i));
@@ -204,6 +205,7 @@ namespace array {
 
         if (s1->get_root() == s2->get_root())
             return false;
+            return new_prop;
 
         sat::literal sel_eq = sat::null_literal;
         auto init_sel_eq = [&]() {
@@ -213,7 +215,6 @@ namespace array {
             return s().value(sel_eq) != l_true;
         };
 
-        bool new_prop = false;
         for (unsigned i = 1; i < num_args; i++) {
             expr* idx1 = store->get_arg(i);
             expr* idx2 = select->get_arg(i);