#5223

Z3Prover · May 31, 2021 · 8d1dfb9 · 8d1dfb9
1 parent fe0727d
commit 8d1dfb9
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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;