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

---
 src/sat/smt/array_axioms.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 6ab6df192..26cfc08fe 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -204,7 +204,6 @@ namespace array {
               tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";);
 
         if (s1->get_root() == s2->get_root())
-            return false;
             return new_prop;
 
         sat::literal sel_eq = sat::null_literal;