diff options
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/decision/issue5454-2.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress1/decision/issue5454-3.smt2 | 14 | ||||
| -rw-r--r-- | test/regress/regress1/decision/issue5454.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress1/decision/issue5785.smt2 | 15 | ||||
| -rw-r--r-- | test/regress/regress1/decision/jh-test1.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/decision/wishue114.smt2 | 33 | ||||
| -rw-r--r-- | test/regress/regress1/decision/wishue115.smt2 | 30 | ||||
| -rw-r--r-- | test/regress/regress1/decision/wishue116.smt2 | 23 | ||||
| -rw-r--r-- | test/regress/regress1/decision/wishue149-2.smt2 | 9 | ||||
| -rw-r--r-- | test/regress/regress1/decision/wishue149-3.smt2 | 9 | ||||
| -rw-r--r-- | test/regress/regress1/decision/wishue160.smt2 | 9 | ||||
| -rw-r--r-- | test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 | 1 |
13 files changed, 170 insertions, 1 deletions
diff --git a/test/regress/regress1/decision/issue5454-2.smt2 b/test/regress/regress1/decision/issue5454-2.smt2 new file mode 100644 index 000000000..d943a0020 --- /dev/null +++ b/test/regress/regress1/decision/issue5454-2.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ANIA) +(declare-fun i () Int) +(declare-fun a () (Array Int Bool)) +(declare-fun b () (Array Bool (Array Int Bool))) +(assert (= (store b (>= i 0) a) (store b false (store (store a 0 true) i true)))) +(check-sat) diff --git a/test/regress/regress1/decision/issue5454-3.smt2 b/test/regress/regress1/decision/issue5454-3.smt2 new file mode 100644 index 000000000..5c8c826f2 --- /dev/null +++ b/test/regress/regress1/decision/issue5454-3.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLIA) +(declare-fun v () Bool) +(declare-fun i () Int) +(declare-fun i8 () Int) +(declare-fun u (Int Int Int Int Int Int) Bool) +(declare-fun ar () (Array Bool Bool)) +(declare-fun a () (Array Int Int)) +(declare-fun arr-- () (Array Bool Int)) +(declare-fun arr () (Array Bool (Array Int Bool))) +(declare-fun arr- () (Array Bool (Array Bool (Array Int Bool)))) +(assert (= arr- (store (store arr- false arr) (or (u (- 1) (select a i8) i (- 1) (select arr-- (select ar (= ar (store ar v true)))) 0) (not (u (- 1) (select a i8) i (- 1) (select arr-- (select ar (= ar (store ar v true)))) 0))) arr))) +(check-sat) diff --git a/test/regress/regress1/decision/issue5454.smt2 b/test/regress/regress1/decision/issue5454.smt2 new file mode 100644 index 000000000..0eadf3412 --- /dev/null +++ b/test/regress/regress1/decision/issue5454.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFNIA) +(declare-fun _substvar_298_ () (Array Int Bool)) +(declare-fun _substvar_379_ () (Array Bool (Array Int Bool))) +(declare-fun _substvar_400_ () (Array Bool (Array Int Bool))) +(declare-fun i0 () Int) +(declare-fun arr--325748303185799905_1467848600759014513-0 () (Array Int Bool)) +(declare-fun arr-1467848600759014513_3143370635870088364-0 () (Array Bool (Array Int Bool))) +(assert (= _substvar_400_ (store arr-1467848600759014513_3143370635870088364-0 false (store (store arr--325748303185799905_1467848600759014513-0 776 true) i0 true)) (store arr-1467848600759014513_3143370635870088364-0 (>= i0 776) _substvar_298_) _substvar_379_)) +(check-sat) diff --git a/test/regress/regress1/decision/issue5785.smt2 b/test/regress/regress1/decision/issue5785.smt2 new file mode 100644 index 000000000..1bf48a1b2 --- /dev/null +++ b/test/regress/regress1/decision/issue5785.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fmf-fun -i --decision=justification +; EXPECT: sat +(set-logic ALRA) +(set-option :fmf-fun true) +(declare-fun v2 () Bool) +(declare-sort S0 0) +(declare-fun arr--1494941102250395870_2811598136228140380-0 () (Array Bool S0)) +(declare-fun arr-2811598136228140380_-1494941102250395870-0 () (Array S0 Bool)) +(push) +(assert (select arr-2811598136228140380_-1494941102250395870-0 (select arr--1494941102250395870_2811598136228140380-0 false))) +(push) +(pop) +(pop) +(assert (select arr-2811598136228140380_-1494941102250395870-0 (select (store arr--1494941102250395870_2811598136228140380-0 v2 (select arr--1494941102250395870_2811598136228140380-0 true)) true))) +(check-sat) diff --git a/test/regress/regress1/decision/jh-test1.smt2 b/test/regress/regress1/decision/jh-test1.smt2 new file mode 100644 index 000000000..31b72e787 --- /dev/null +++ b/test/regress/regress1/decision/jh-test1.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ALL) +(declare-const size4 String) +(declare-const p2_size Int) +(assert (= 1 (+ 1 (ite (= 1 p2_size) (str.to_code size4) 0)))) +(check-sat) diff --git a/test/regress/regress1/decision/wishue114.smt2 b/test/regress/regress1/decision/wishue114.smt2 new file mode 100644 index 000000000..9bdcf562d --- /dev/null +++ b/test/regress/regress1/decision/wishue114.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(check-sat) +(assert (and (and v1 v2) (and (or true (and (or false v1) v1)) (or (and false v1) v3)))) +(assert true) +(assert (or (and (or (and (or v4 v4) false) v2) (and true (or (and v5 true) (and v6 v5)))) v2)) +(assert v3) +(check-sat) +(assert false) +(assert true) +(assert (and (or (and v7 (and (and v2 v6) (and false v8))) (and (or (and v8 false) true) (and v6 true))) (and true v3))) +(push) +(assert v7) +(check-sat) +(assert true) +(pop) +(push) +(check-sat) +(check-sat) diff --git a/test/regress/regress1/decision/wishue115.smt2 b/test/regress/regress1/decision/wishue115.smt2 new file mode 100644 index 000000000..d8335654a --- /dev/null +++ b/test/regress/regress1/decision/wishue115.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(check-sat) +(assert (or (not (and (or v1 (and v1 true)) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (and v1 false)))) false)) +(assert (or (or (not true) (and (and (not v1) (or v1 v1)) v1)) (or (and (not (not v2)) (forall ((q0_1 Bool) (q0_2 Bool)) (and q0_2 q0_2))) (and (not (and true v3)) (or (not v1) v2))))) +(check-sat) +(check-sat) +(assert (not (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (and (not (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool) (q1_4 Bool)) false)) (not (forall ((q1_1 Bool)) q0_2)))))) +(assert (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool) (q0_5 Bool)) (not v1))) +(push) +(check-sat) +(assert (and (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool) (q1_4 Bool)) (not (forall ((q2_1 Bool)) true)))) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (not (or q0_3 (forall ((q1_1 Bool)) v4)))))) +(assert (or (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool)) (not q1_1))) v1)) +(assert v5) +(check-sat) +(assert (not (forall ((q0_1 Bool)) (and (or (or true q0_1) (and false q0_1)) (not true))))) +(pop) diff --git a/test/regress/regress1/decision/wishue116.smt2 b/test/regress/regress1/decision/wishue116.smt2 new file mode 100644 index 000000000..3cfb1540b --- /dev/null +++ b/test/regress/regress1/decision/wishue116.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(assert (and (or (or (and (or false v1) v2) (not (not v3))) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (forall ((q1_1 Bool)) q1_1))) true)) +(check-sat) +(assert (or (not v2) (or (and (or (and v4 true) v2) (forall ((q0_1 Bool)) (not true))) (not (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (forall ((q1_1 Bool) (q1_2 Bool)) v1)))))) +(push) +(assert (not v5)) +(assert (not true)) +(pop) +(push) +(check-sat) +(pop) +(assert true) diff --git a/test/regress/regress1/decision/wishue149-2.smt2 b/test/regress/regress1/decision/wishue149-2.smt2 new file mode 100644 index 000000000..6095a4940 --- /dev/null +++ b/test/regress/regress1/decision/wishue149-2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLIA) +(declare-const v4 Bool) +(declare-const v6 Bool) +(declare-const arr0 (Array Bool Int)) +(declare-const arr1 (Array Bool (Array Bool Int))) +(assert (= (store arr1 v6 (store arr0 true 0)) (store arr1 true (store (store (store arr0 true 0) v4 0) true 96)) arr1 arr1)) +(check-sat) diff --git a/test/regress/regress1/decision/wishue149-3.smt2 b/test/regress/regress1/decision/wishue149-3.smt2 new file mode 100644 index 000000000..fbd200f66 --- /dev/null +++ b/test/regress/regress1/decision/wishue149-3.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLRA) +(declare-fun _substvar_323_ () Bool) +(declare-sort S0 0) +(declare-const arr-8825057447867329665_7821057345541224443-0 (Array Bool S0)) +(declare-const arr--3985848114402943554_-2673408464765268945-0 (Array Real (Array Bool S0))) +(assert (not (= (select arr--3985848114402943554_-2673408464765268945-0 0.0) (store (store arr-8825057447867329665_7821057345541224443-0 _substvar_323_ (select arr-8825057447867329665_7821057345541224443-0 true)) false (select arr-8825057447867329665_7821057345541224443-0 false)) arr-8825057447867329665_7821057345541224443-0 arr-8825057447867329665_7821057345541224443-0))) +(check-sat) diff --git a/test/regress/regress1/decision/wishue160.smt2 b/test/regress/regress1/decision/wishue160.smt2 new file mode 100644 index 000000000..8497a66fc --- /dev/null +++ b/test/regress/regress1/decision/wishue160.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ALIA) +(set-option :repeat-simp true) +(set-option :sygus-rr-synth-check true) +(declare-fun v6 () Bool) +(declare-const arr-7579056739068271278_-8074447279386590332-0 (Array Bool Int)) +(assert (= false false false (= arr-7579056739068271278_-8074447279386590332-0 (store arr-7579056739068271278_-8074447279386590332-0 v6 746)) false false false)) +(check-sat) diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 61f0f207b..21405dfdb 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ho --finite-model-find -q +; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 index 45727743f..796d7e753 100644 --- a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 +++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-jh-rlv-order ; REQUIRES: symfpu ; EXPECT: unsat (set-logic AUFBVFPDTNIRA) |