Add regression for some fixed array issues (#8145)

Found while checking whether the latest fix solves array issues, these were already resolved.
Fixes #4414.
Fixes #4546.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2843e6fd28972794ca55e8415279cda484b5d2a0..6a0ec1f73b490d245fc82672566b26184b49ed6e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -111,6 +111,13 @@ set(regress_0_tests
   regress0/arrays/incorrect9.smtv1.smt2
   regress0/arrays/issue3813-massign-assert.smt2
   regress0/arrays/issue3814.smt2
+  regress0/arrays/issue4240.smt2
+  regress0/arrays/issue4414-2.smt2
+  regress0/arrays/issue4414.smt2
+  regress0/arrays/issue4546-2.smt2
+  regress0/arrays/issue4546.smt2
+  regress0/arrays/issue4780-3.smt2
+  regress0/arrays/issue4780.smt2
   regress0/arrays/issue4927-unsat-cores.smt2
   regress0/arrays/issue6807-idem-rew.smt2
   regress0/arrays/issue7596-define-array-uminus.smt2

diff --git a/test/regress/regress0/arrays/issue4240.smt2 b/test/regress/regress0/arrays/issue4240.smt2
new file mode 100644 (file)
index 0000000..008c0ed
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4240.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_AUFBV)
+(set-info :status sat)
+(declare-const arr-414726656414253458_-8019474897564551692-0 (Array (_ BitVec 8) Bool))
+(declare-const bv_8-1 (_ BitVec 8))
+(assert (= (store arr-414726656414253458_-8019474897564551692-0 (bvadd bv_8-1 bv_8-1) true) arr-414726656414253458_-8019474897564551692-0))
+(check-sat)

diff --git a/test/regress/regress0/arrays/issue4414-2.smt2 b/test/regress/regress0/arrays/issue4414-2.smt2
new file mode 100644 (file)
index 0000000..8afdea8
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4414-2.smt2
@@ -0,0 +1,10 @@
+(set-option :check-models true)
+(set-option :check-unsat-cores true)
+(set-logic QF_ALIA)
+(set-info :status sat)
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c (Array Int Int))
+(assert (= c ((as const (Array Int Int)) 0)))
+(assert (= a (select c b)))
+(check-sat)

diff --git a/test/regress/regress0/arrays/issue4414.smt2 b/test/regress/regress0/arrays/issue4414.smt2
new file mode 100644 (file)
index 0000000..d84041f
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4414.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --check-models --check-unsat-cores
+; EXPECT: sat
+(set-logic QF_AUFLIA)
+(declare-const a (Array Int Int))
+(declare-const b (Array Int Int))
+(assert (= a ((as const (Array Int Int)) 0)))
+(assert (distinct b ((as const (Array Int Int)) 1)))
+(assert (= (store a 2 3) (store b 2 3)))
+(check-sat)

diff --git a/test/regress/regress0/arrays/issue4546-2.smt2 b/test/regress/regress0/arrays/issue4546-2.smt2
new file mode 100644 (file)
index 0000000..24d075b
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4546-2.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic QF_AUFBV)
+(declare-const bv_58-0 (_ BitVec 4))
+(check-sat)
+(declare-const arr1 (Array (_ BitVec 4) Bool))
+(check-sat)
+(assert (xor false true false true true true true true true (select arr1 bv_58-0)))
+(check-sat)
+(assert (select arr1 (bvxor bv_58-0 bv_58-0 bv_58-0 (bvlshr bv_58-0 bv_58-0))))
+(check-sat)

diff --git a/test/regress/regress0/arrays/issue4546.smt2 b/test/regress/regress0/arrays/issue4546.smt2
new file mode 100644 (file)
index 0000000..d3b6f66
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4546.smt2
@@ -0,0 +1,6 @@
+(set-logic AUFBV)
+(set-info :status sat)
+(declare-const bv_9-0 (_ BitVec 9))
+(declare-const arr-7002743857821263698_366759559579120535-0 (Array (_ BitVec 9) Bool))
+(assert (select arr-7002743857821263698_366759559579120535-0 (bvshl bv_9-0 bv_9-0)))
+(check-sat)

diff --git a/test/regress/regress0/arrays/issue4780-3.smt2 b/test/regress/regress0/arrays/issue4780-3.smt2
new file mode 100644 (file)
index 0000000..51f3c98
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4780-3.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_ABV)
+(set-info :status sat)
+(declare-const bv_25-0 (_ BitVec 25))
+(declare-const arr0 (Array (_ BitVec 25) Bool))
+(assert (select arr0 (bvnot bv_25-0)))
+(check-sat)

diff --git a/test/regress/regress0/arrays/issue4780.smt2 b/test/regress/regress0/arrays/issue4780.smt2
new file mode 100644 (file)
index 0000000..80cc1bc
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4780.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun c () (_ BitVec 32))
+(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun e () (_ BitVec 32))
+(declare-fun ep () (_ BitVec 32))
+(declare-fun eq () (_ BitVec 32))
+(assert (= (_ bv1 1) (bvand (bvashr (bvsdiv (_ bv1 1) (ite (= (_ bv1
+1) (ite (= b (_ bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))
+(ite (= (_ bv0 1) (ite (= eq (bvadd c a)) (_ bv1 1) (_ bv0 1))) (_ bv1
+1) (_ bv0 1))) (ite (= (ite (= ep (bvadd eq (_ bv4 32))) (_ bv1 1) (_
+bv0 1)) (ite (= e (bvshl (concat (_ bv0 24) (select d (bvadd ep (_ bv3
+32)))) (_ bv24 32))) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv1 1) (ite (= (_
+bv1 32) (bvlshr e (_ bv31 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+1))) (_ bv1 1) (_ bv0 1)))))
+(check-sat)