diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/seq/seq-2var.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex1.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex2.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex3.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex4.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex5-dd.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex5.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-nemp.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-rewrites.smt2 | 44 |
9 files changed, 120 insertions, 0 deletions
diff --git a/test/regress/regress0/seq/seq-2var.smt2 b/test/regress/regress0/seq/seq-2var.smt2 new file mode 100644 index 000000000..3a0d8934f --- /dev/null +++ b/test/regress/regress0/seq/seq-2var.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) + +(assert (not (= x y))) + +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex1.smt2 b/test/regress/regress0/seq/seq-ex1.smt2 new file mode 100644 index 000000000..817ee5f8e --- /dev/null +++ b/test/regress/regress0/seq/seq-ex1.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_UFSLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun f ((Seq Int)) (Seq Bool)) + +(assert (not (= x y))) +(assert (not (= (f x) (f y)))) + +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex2.smt2 b/test/regress/regress0/seq/seq-ex2.smt2 new file mode 100644 index 000000000..89b9d3100 --- /dev/null +++ b/test/regress/regress0/seq/seq-ex2.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun z () Int) +(assert (> z 10)) +(assert (= (seq.len x) (seq.len y))) +(assert (= (seq.++ x (seq.unit z)) (seq.++ y (seq.unit 5)))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex3.smt2 b/test/regress/regress0/seq/seq-ex3.smt2 new file mode 100644 index 000000000..abafdeddf --- /dev/null +++ b/test/regress/regress0/seq/seq-ex3.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () (Seq (Seq Int))) +(declare-fun xp () (Seq (Seq Int))) +(declare-fun y () (Seq (Seq Int))) +(declare-fun yp () (Seq (Seq Int))) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun i () Int) +(declare-fun j () Int) +(declare-fun n () Int) +(assert (> i j)) +(assert (= (seq.extract z n 1) (seq.unit i))) +(assert (= (seq.extract w n 1) (seq.unit j))) +(assert (= x (seq.++ (seq.unit z) xp))) +(assert (= y (seq.++ (seq.unit w) yp))) +(assert (= x y)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex4.smt2 b/test/regress/regress0/seq/seq-ex4.smt2 new file mode 100644 index 000000000..93fed72c7 --- /dev/null +++ b/test/regress/regress0/seq/seq-ex4.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun z () (Seq Int)) +(declare-fun i () Int) +(declare-fun n () Int) +(assert (= (seq.extract z n 1) (seq.unit i))) +(assert (< (seq.len z) n)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex5-dd.smt2 b/test/regress/regress0/seq/seq-ex5-dd.smt2 new file mode 100644 index 000000000..d9ef5c8ba --- /dev/null +++ b/test/regress/regress0/seq/seq-ex5-dd.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun z () (Seq Int)) +(declare-fun i () Int) +(declare-fun n () Int) +(assert (> i 777)) +(assert (= (seq.extract z n 1) (seq.unit i))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex5.smt2 b/test/regress/regress0/seq/seq-ex5.smt2 new file mode 100644 index 000000000..9fa72bc6b --- /dev/null +++ b/test/regress/regress0/seq/seq-ex5.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun i () Int) +(assert (> i 777)) +(assert (not (= (seq.replace z (seq.unit i) w) z))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-nemp.smt2 b/test/regress/regress0/seq/seq-nemp.smt2 new file mode 100644 index 000000000..4eaee062f --- /dev/null +++ b/test/regress/regress0/seq/seq-nemp.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(assert (not (= x (as seq.empty (Seq Int))))) +(assert (= (seq.len x) 16)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-rewrites.smt2 b/test/regress/regress0/seq/seq-rewrites.smt2 new file mode 100644 index 000000000..a8bd7c1f2 --- /dev/null +++ b/test/regress/regress0/seq/seq-rewrites.smt2 @@ -0,0 +1,44 @@ +(set-logic QF_UFSLIA) +(set-info :status unsat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun z () Int) + +(assert +(or + +(not (= +(seq.replace (seq.++ (seq.unit 0) x) (seq.unit 1) (seq.unit 2)) +(seq.++ (seq.unit 0) (seq.replace x (seq.unit 1) (seq.unit 2))) +)) + +(not (= +(seq.at (seq.++ x (seq.unit 14)) (seq.len x)) +(seq.unit 14) +)) + +(not (= +(seq.at x z) +(seq.extract x z 1) +)) + +(not (= +(seq.contains (seq.++ x y) y) +true +)) + +(not (= +(seq.prefixof (seq.unit z) (seq.unit 4)) +(seq.suffixof (seq.unit z) (seq.unit 4)) +)) + +(not (= +(seq.rev (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +(seq.++ (seq.unit 3) (seq.unit 2) (seq.unit 1)) +)) + +)) + + + +(check-sat) |