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 b64f1d1da5ed86e0f59adffe87c396728553b5ae..72b05ec2d3e2d6bae49d596872b764d8673ebdf3 100644 (file)
--- 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 f7a26e535a66f1c1833c5c00467a44abb7a4f373..8db3689eb61e86b5af671bdea0d8fd902301a3ce 100644 (file)
--- 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 (file)
index 0000000..0eba361
--- /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 (file)
index 0000000..40c0cb0
--- /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)