From 34fc0276e9130b522a9322917d73897d7b9f7bf5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Aug 2021 17:52:31 -0700
Subject: [PATCH] Update array_axioms.cpp
---
src/sat/smt/array_axioms.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 99c7ebd18..fda2d67aa 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -176,7 +176,7 @@ namespace array {
unsigned num_args = select->get_num_args();
expr* arg = select->get_arg(0);
- if (arg != store && !can_beta_reduce(arg) && expr2enode(arg)->get_root() == expr2enode(store)->get_root())
+ if (false && arg != store && !can_beta_reduce(arg) && expr2enode(arg)->get_root() == expr2enode(store)->get_root())
return false;
bool has_diff = false;
for (unsigned i = 1; i < num_args; i++)