From: Clark Barrett <barrett@cs.stanford.edu>
Date: Tue, 29 Mar 2022 06:50:55 +0000 (-0700)
Subject: Fix for issue 5925: constant arrays should be nonlinear. (#8430)
X-Git-Tag: cvc5-1.0.0~144
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d5a95c11e92fd970aa0ba40cf748e44eb977dd9;p=cvc5.git

Fix for issue 5925: constant arrays should be nonlinear. (#8430)

Fixes #5925. The "nonlinear" optimization did not take constant arrays into account.
---

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)