From 74d327467f2fc93a2a6a416cc2d95b7d493cb77f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Feb 2022 19:26:27 -0600 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 7 +++++++ test/regress/regress0/arrays/issue4240.smt2 | 6 ++++++ test/regress/regress0/arrays/issue4414-2.smt2 | 10 ++++++++++ test/regress/regress0/arrays/issue4414.smt2 | 9 +++++++++ test/regress/regress0/arrays/issue4546-2.smt2 | 14 ++++++++++++++ test/regress/regress0/arrays/issue4546.smt2 | 6 ++++++ test/regress/regress0/arrays/issue4780-3.smt2 | 6 ++++++ test/regress/regress0/arrays/issue4780.smt2 | 18 ++++++++++++++++++ 8 files changed, 76 insertions(+) create mode 100644 test/regress/regress0/arrays/issue4240.smt2 create mode 100644 test/regress/regress0/arrays/issue4414-2.smt2 create mode 100644 test/regress/regress0/arrays/issue4414.smt2 create mode 100644 test/regress/regress0/arrays/issue4546-2.smt2 create mode 100644 test/regress/regress0/arrays/issue4546.smt2 create mode 100644 test/regress/regress0/arrays/issue4780-3.smt2 create mode 100644 test/regress/regress0/arrays/issue4780.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2843e6fd2..6a0ec1f73 100644 --- 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 index 000000000..008c0ed34 --- /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 index 000000000..8afdea802 --- /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 index 000000000..d84041fc9 --- /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 index 000000000..24d075be4 --- /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 index 000000000..d3b6f66c5 --- /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 index 000000000..51f3c98a7 --- /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 index 000000000..80cc1bc3d --- /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) -- 2.30.2