diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/burns4.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 | 24 | ||||
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/regexp003.smt2 | 13 |
4 files changed, 28 insertions, 12 deletions
diff --git a/test/regress/regress0/quantifiers/burns4.smt2 b/test/regress/regress0/quantifiers/burns4.smt2 index 886d6f5c8..72023fd4f 100644 --- a/test/regress/regress0/quantifiers/burns4.smt2 +++ b/test/regress/regress0/quantifiers/burns4.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 index 5f20cb3b5..615d43fe8 100644 --- a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -112,18 +112,18 @@ (assert (! (= (smap$f id$e) id$b) :named a12)) (assert (! (= (smap$a id$) id$e) :named a13)) (assert (! (= (smap$b id$a) id$d) :named a14)) -(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern (fun_app$j id$b ?v0))) :named a15)) -(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern (fun_app$i id$c ?v0))) :named a16)) -(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern (fun_app$e id$d ?v0))) :named a17)) -(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern (fun_app$c id$e ?v0))) :named a18)) -(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern (fun_app$d id$ ?v0))) :named a19)) -(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern (fun_app$f id$a ?v0))) :named a20)) -(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern (fun_app$j id$b ?v0))) :named a21)) -(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern (fun_app$i id$c ?v0))) :named a22)) -(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern (fun_app$e id$d ?v0))) :named a23)) -(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern (fun_app$c id$e ?v0))) :named a24)) -(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern (fun_app$d id$ ?v0))) :named a25)) -(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern (fun_app$f id$a ?v0))) :named a26)) +(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a15)) +(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a16)) +(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a17)) +(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a18)) +(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a19)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a20)) +(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a21)) +(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a22)) +(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a23)) +(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a24)) +(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a25)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a26)) (assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$ (smap$g ?v0 ?v1) ?v2) (fun_app$ ?v0 (snth$a ?v1 ?v2)))) :named a27)) (assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$b (smap$h ?v0 ?v1) ?v2) (fun_app$k ?v0 (snth$a ?v1 ?v2)))) :named a28)) (assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$ (smap$i ?v0 ?v1) ?v2) (fun_app$l ?v0 (snth$c ?v1 ?v2)))) :named a29)) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index c15e93cd8..865d05cd2 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -37,6 +37,7 @@ TESTS = \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ + regexp003.smt2 \ leadingzero001.smt2 \ loop001.smt2 \ loop002.smt2 \ diff --git a/test/regress/regress0/strings/regexp003.smt2 b/test/regress/regress0/strings/regexp003.smt2 new file mode 100644 index 000000000..601689958 --- /dev/null +++ b/test/regress/regress0/strings/regexp003.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-const s String)
+
+(assert (str.in.re s (re.inter
+ (re.++ (str.to.re "a") (re.* (str.to.re "b"))
+ (re.inter (str.to.re "c") (re.* (str.to.re "c"))))
+ (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))
+ )))
+
+(check-sat)
|