diff options
Diffstat (limited to 'test/regress/regress0')
44 files changed, 124 insertions, 39 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6608ae22d..43c77973f 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -86,7 +86,9 @@ TESTS = \ z3.620661-no-fv-trigger.smt2 \ bug_743.smt2 \ quaternion_ds1_symm_0428.fof.smt2 \ - bug749-rounding.smt2 + bug749-rounding.smt2 \ + RNDPRE_4_1-dd-nqe.smt2 \ + mix-complete-strat.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 new file mode 100644 index 000000000..6379d6cec --- /dev/null +++ b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --cbqi-nested-qe +; EXPECT: unsat +(set-logic LRA) + +(declare-fun c () Real) + +(assert +(forall ((?x2 Real)) +(exists ((?x3 Real)) +(and +(forall ((?x4 Real)) (or +(not (>= ?x4 4)) +(and (> c (+ ?x2 ?x3)) (> (+ c ?x3 ?x4) 0))) ) +(not (> (+ c ?x2 ?x3) 0)) ) +)) ) + +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 new file mode 100644 index 000000000..c2209f697 --- /dev/null +++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) + +(declare-sort U 0) +(declare-fun P (U) Bool) + +(assert (forall ((x U)) (P x))) + +(declare-fun u () U) +(assert (P u)) + +(declare-const a Int) +(declare-const b Int) +(assert (forall ((x Int)) (or (> x a) (< x b)))) + +(check-sat) diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 6078bfa19..b43a9a570 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -56,7 +56,9 @@ TESTS = \ fmf-nemp-2.smt2 \ trees-1.smt2 \ wand-false.smt2 \ - dup-nemp.smt2 + dup-nemp.smt2 \ + emp2-quant-unsat.smt2 \ + dispose-1.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 index d3245e33f..ebe52fa46 100644 --- a/test/regress/regress0/sep/chain-int.smt2 +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 index a0fc5a187..f68434f33 100755 --- a/test/regress/regress0/sep/crash1220.smt2 +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 new file mode 100644 index 000000000..3c0e7df32 --- /dev/null +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -0,0 +1,17 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const w Int) +(declare-const w1 Int) +(declare-const w2 Int) + +;------- f ------- +(assert (= w1 (as sep.nil Int))) +(assert (= w2 (as sep.nil Int))) +;----------------- + +(assert (pto w (as sep.nil Int))) +(assert (not (and (sep (and (emp 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) + +(check-sat) +;(get-model) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 index 766354cd9..b3e2088b1 100644 --- a/test/regress/regress0/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-sort Loc 0) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 009561128..98348f617 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 new file mode 100644 index 000000000..52d99d8c0 --- /dev/null +++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --quant-epr +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun u () U) + +(assert (sep (not (emp u)) (not (emp u)))) + +(assert (forall ((x U) (y U)) (= x y))) + +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 index 2981606d8..b857aec2a 100644 --- a/test/regress/regress0/sep/loop-1220.smt2 +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index e1e21dd10..a0766a7e0 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (not (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 index 0c93719c9..c807757d1 100755 --- a/test/regress/regress0/sep/nspatial-simp.smt2 +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 index b0dece248..28ed5c47b 100644 --- a/test/regress/regress0/sep/pto-01.smt2 +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 index f0b6d2dee..ab1cea0c8 100644 --- a/test/regress/regress0/sep/pto-02.smt2 +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 index 1734c93bb..9b0afda7a 100644 --- a/test/regress/regress0/sep/pto-04.smt2 +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 index c3330f036..a93fc4db8 100644 --- a/test/regress/regress0/sep/sep-01.smt2 +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 index 403bcf077..6f190d964 100644 --- a/test/regress/regress0/sep/sep-02.smt2 +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 index 427c44b50..8dce5acc7 100644 --- a/test/regress/regress0/sep/sep-03.smt2 +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 index 26a27eb22..356f866c1 100644 --- a/test/regress/regress0/sep/sep-find2.smt2 +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 index 8ddbdd05f..ab12c6461 100644 --- a/test/regress/regress0/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 index 1a69336a8..425e5ce3c 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 index e71e6a51a..7ada6ff06 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 index 191e7527f..7b6fc69e9 100644 --- a/test/regress/regress0/sep/sep-neg-simple.smt2 +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 index f89a9c0ac..53f890b0d 100644 --- a/test/regress/regress0/sep/sep-neg-swap.smt2 +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 index 9b4afe36a..3e595b5e9 100644 --- a/test/regress/regress0/sep/sep-nterm-again.smt2 +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 index 0178134cb..d4fb0fd52 100644 --- a/test/regress/regress0/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 index 772acd981..9522e2420 100644 --- a/test/regress/regress0/sep/sep-plus1.smt2 +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 index 6cdf51294..cedbb53eb 100755 --- a/test/regress/regress0/sep/sep-simp-unc.smt2 +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-sort U 0) (declare-fun x () U) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index fb58b9d10..9239fb770 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 index 0c0b6a9a3..70927ad82 100644 --- a/test/regress/regress0/sep/simple-neg-sat.smt2 +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 index ed3187a96..10e509e05 100644 --- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 index 1731174fa..1a9e76a8a 100644 --- a/test/regress/regress0/sep/split-find-unsat.smt2 +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 index 88e875f70..8a46d9fdd 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort Loc 0) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 index 0c0ee72ad..fa0aab591 100644 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (declare-fun y () Int) (declare-fun u () Int) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 9b4871323..1d799c8c9 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (wand (emp 0) (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2 index 642c0a8aa..65500f775 100644 --- a/test/regress/regress0/sep/wand-false.smt2 +++ b/test/regress/regress0/sep/wand-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x x) false)) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 index e8ee4252c..0db7330d1 100644 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (emp x) (pto x 3))) (check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2 index c317e8736..cce0f79e3 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (emp x))) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 index df4bfa6d8..120683f74 100755 --- a/test/regress/regress0/sep/wand-simp-sat.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 1))) (check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2 index 059e91317..c684d16ad 100755 --- a/test/regress/regress0/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 index 95bc85537..c9851661a 100755 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) (assert (emp x)) diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 4e1806aba..abb6c02b2 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -64,7 +64,8 @@ TESTS = \ union-1b.smt2 \ union-2.smt2 \ dt-simp-mem.smt2 \ - card3-ground.smt2 + card3-ground.smt2 \ + card-vc6-minimized.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/card-vc6-minimized.smt2 b/test/regress/regress0/sets/card-vc6-minimized.smt2 new file mode 100644 index 000000000..d7f4bdf1e --- /dev/null +++ b/test/regress/regress0/sets/card-vc6-minimized.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic QF_UFLIAFS) +(declare-fun x () Int) +(declare-fun c () (Set Int)) +(declare-fun alloc0 () (Set Int)) +(declare-fun alloc1 () (Set Int)) +(declare-fun alloc2 () (Set Int)) +(assert +(and (member x c) + (<= (card (setminus alloc1 alloc0)) 1) + (<= (card (setminus alloc2 alloc1)) + (card (setminus c (singleton x)))) + (> (card (setminus alloc2 alloc0)) (card c)) +)) +(check-sat) |