Add regression for fixed issue 6700 (#8265)

Fixes #6700.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6e8f5a774c7dab33d4ddf2e4cb27686ac8de115f..474f446409fdf6c99cf4a4498e0efda40aa2f7fe 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -125,6 +125,7 @@ set(regress_0_tests
   regress0/arrays/issue5836.smt2
   regress0/arrays/issue6276-2.smt2
   regress0/arrays/issue6276.smt2
+  regress0/arrays/issue6700-inc-check-model.smt2
   regress0/arrays/issue6807-idem-rew.smt2
   regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/issue8103-1-weak-equiv-models.smt2

diff --git a/test/regress/regress0/arrays/issue6700-inc-check-model.smt2 b/test/regress/regress0/arrays/issue6700-inc-check-model.smt2
new file mode 100644 (file)
index 0000000..96494f5
--- /dev/null
+++ b/test/regress/regress0/arrays/issue6700-inc-check-model.smt2
@@ -0,0 +1,17 @@
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic QF_ALIA)
+(set-option :incremental true)
+(declare-fun v4 () Bool)
+(declare-fun v6 () Bool)
+(declare-fun v9 () Bool)
+(declare-fun i () Int)
+(declare-fun a () (Array Int Bool))
+(declare-fun v () Bool)
+(declare-fun v2 () Bool)
+(assert (xor v9 v9 v6 v2 v4 v (select (store a i false) 1) (select a 1)))
+(push)
+(assert (= i 0))
+(check-sat)
+(assert (not (xor v6 v2 v4 v (select a 1) (select a 1))))
+(check-sat)