diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 | 24 |
1 files changed, 12 insertions, 12 deletions
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)) |