From 3d5a95c11e92fd970aa0ba40cf748e44eb977dd9 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon, 28 Mar 2022 23:50:55 -0700
Subject: [PATCH] Fix for issue 5925: constant arrays should be nonlinear.
 (#8430)

Fixes #5925. The "nonlinear" optimization did not take constant arrays into account.
---
 src/theory/arrays/theory_arrays.cpp               |  1 +
 test/regress/cli/CMakeLists.txt                   |  2 ++
 test/regress/cli/regress0/arrays/issue5925-2.smt2 |  7 +++++++
 test/regress/cli/regress0/arrays/issue5925.smt2   | 12 ++++++++++++
 4 files changed, 22 insertions(+)
 create mode 100644 test/regress/cli/regress0/arrays/issue5925-2.smt2
 create mode 100644 test/regress/cli/regress0/arrays/issue5925.smt2

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b64f1d1da..72b05ec2d 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -795,6 +795,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     d_infoMap.setConstArr(node, node);
     Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
     d_defValues[node] = defaultValue;
+    setNonLinear(node);
     break;
   }
   default:
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index f7a26e535..8db3689eb 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -123,6 +123,8 @@ set(regress_0_tests
   regress0/arrays/issue5720.smt2
   regress0/arrays/issue5836-2.smt2
   regress0/arrays/issue5836.smt2
+  regress0/arrays/issue5925.smt2
+  regress0/arrays/issue5925-2.smt2
   regress0/arrays/issue6276-2.smt2
   regress0/arrays/issue6276.smt2
   regress0/arrays/issue6700-inc-check-model.smt2
diff --git a/test/regress/cli/regress0/arrays/issue5925-2.smt2 b/test/regress/cli/regress0/arrays/issue5925-2.smt2
new file mode 100644
index 000000000..0eba3619b
--- /dev/null
+++ b/test/regress/cli/regress0/arrays/issue5925-2.smt2
@@ -0,0 +1,7 @@
+; DISABLE-TESTER: proof
+(set-logic QF_A)
+(set-info :status unsat)
+(declare-const a (Array Bool Bool))
+(assert (= (store a true false) (store (store ((as const (Array Bool Bool)) true) true false) false false)))
+(assert (select a false))
+(check-sat)
diff --git a/test/regress/cli/regress0/arrays/issue5925.smt2 b/test/regress/cli/regress0/arrays/issue5925.smt2
new file mode 100644
index 000000000..40c0cb0a2
--- /dev/null
+++ b/test/regress/cli/regress0/arrays/issue5925.smt2
@@ -0,0 +1,12 @@
+; DISABLE-TESTER: proof
+(set-logic QF_ABV)
+(set-info :status unsat)
+(declare-const a (Array Bool Bool))
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const d Bool)
+(assert (= (store (store ((as const (Array Bool Bool)) true) true false) false false) (store a b c)))
+(assert b)
+(assert (= d (select a c)))
+(assert d)
+(check-sat)
-- 
2.30.2