Compute model basis only for fmf. Add another co-datatype regression.

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5dc8bb3847ded0b07a21b8e3c1f1ea62a35cfb64..a95de086a7bda2a0e2b7e86c76e098ee58e2b79f 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -398,9 +398,11 @@ void TermDb::reset( Theory::Effort effort ){
     if( !it->second.empty() ){
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node n = it->second[i];
-        computeModelBasisArgAttribute( n );
         if( hasTermCurrent( n ) ){
           if( !n.getAttribute(NoMatchAttribute()) ){
+            if( options::finiteModelFind() ){
+              computeModelBasisArgAttribute( n );
+            }
             computeArgReps( n );
             if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
               NoMatchAttribute nma;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c109924358ec7ab200ba446ddf14eeeb62d69485..899d035ea21ba8e3b7b656030f90cf3ec686cb02 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -295,13 +295,15 @@ void QuantifiersEngine::check( Theory::Effort e ){
       return;
     }
 
+    Trace("quant-engine-debug2") << "Reset term db..." << std::endl;
     d_term_db->reset( e );
     d_eq_query->reset();
     if( d_rel_dom ){
       d_rel_dom->reset();
     }
     d_model->reset_round();
-    for( int i=0; i<(int)d_modules.size(); i++ ){
+    for( unsigned i=0; i<d_modules.size(); i++ ){
+      Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
       d_modules[i]->reset_round( e );
     }
     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
@@ -333,7 +335,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       if( success ){
         //check each module
-        for( int i=0; i<(int)qm.size(); i++ ){
+        for( unsigned i=0; i<qm.size(); i++ ){
           Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
           qm[i]->check( e, quant_e );
         }

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 41f66f92fc7e38bc3075741c8782fc753ec052c6..f8cc9ea35c5b046815167f9ecf30146d503d9cfd 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -44,7 +44,8 @@ TESTS =       \
        ARI176e1.smt2 \
         bi-artm-s.smt2 \
        simp-typ-test.smt2 \
-       macros-int-real.smt2
+       macros-int-real.smt2 \
+       stream-x2014-09-18-unsat.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2

diff --git a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2
new file mode 100644 (file)
index 0000000..5f20cb3
--- /dev/null
+++ b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2
@@ -0,0 +1,183 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort A$ 0)
+(declare-sort B$ 0)
+(declare-sort A_set$ 0)
+(declare-sort B_set$ 0)
+(declare-sort A_a_fun$ 0)
+(declare-sort A_b_fun$ 0)
+(declare-sort B_a_fun$ 0)
+(declare-sort B_b_fun$ 0)
+(declare-sort A_stream_set$ 0)
+(declare-sort B_stream_set$ 0)
+(declare-sort A_a_stream_fun$ 0)
+(declare-sort A_b_stream_fun$ 0)
+(declare-sort A_stream_a_fun$ 0)
+(declare-sort A_stream_b_fun$ 0)
+(declare-sort B_a_stream_fun$ 0)
+(declare-sort B_b_stream_fun$ 0)
+(declare-sort B_stream_a_fun$ 0)
+(declare-sort B_stream_b_fun$ 0)
+(declare-sort A_stream_stream_set$ 0)
+(declare-sort B_stream_stream_set$ 0)
+(declare-sort A_stream_a_stream_fun$ 0)
+(declare-sort B_stream_b_stream_fun$ 0)
+(declare-sort A_stream_stream_a_stream_stream_fun$ 0)
+(declare-sort B_stream_stream_b_stream_stream_fun$ 0)
+(declare-sort A_stream_stream_stream_a_stream_stream_stream_fun$ 0)
+(declare-sort B_stream_stream_stream_b_stream_stream_stream_fun$ 0)
+(declare-datatypes () ((Nat$ (zero$) (suc$ (pred$ Nat$)))))
+(declare-codatatypes () ((A_stream$ (sCons$ (shd$ A$) (stl$ A_stream$)))
+  (B_stream$ (sCons$a (shd$a B$) (stl$a B_stream$)))
+  (B_stream_stream$ (sCons$b (shd$b B_stream$) (stl$b B_stream_stream$)))
+  (B_stream_stream_stream$ (sCons$c (shd$c B_stream_stream$) (stl$c B_stream_stream_stream$)))
+  (A_stream_stream$ (sCons$d (shd$d A_stream$) (stl$d A_stream_stream$)))
+  (A_stream_stream_stream$ (sCons$e (shd$e A_stream_stream$) (stl$e A_stream_stream_stream$)))))
+(declare-fun f$ () B_a_fun$)
+(declare-fun x$ () B$)
+(declare-fun id$ () B_b_fun$)
+(declare-fun id$a () A_a_fun$)
+(declare-fun id$b () B_stream_stream_b_stream_stream_fun$)
+(declare-fun id$c () A_stream_stream_a_stream_stream_fun$)
+(declare-fun id$d () A_stream_a_stream_fun$)
+(declare-fun id$e () B_stream_b_stream_fun$)
+(declare-fun id$f () B_stream_stream_stream_b_stream_stream_stream_fun$)
+(declare-fun id$g () A_stream_stream_stream_a_stream_stream_stream_fun$)
+(declare-fun smap$ (B_a_fun$ B_stream$) A_stream$)
+(declare-fun snth$ (B_stream_stream$ Nat$) B_stream$)
+(declare-fun sdrop$ (Nat$ B_stream_stream$) B_stream_stream$)
+(declare-fun smap$a (B_b_fun$) B_stream_b_stream_fun$)
+(declare-fun smap$b (A_a_fun$) A_stream_a_stream_fun$)
+(declare-fun smap$c (B_stream_stream_b_stream_stream_fun$) B_stream_stream_stream_b_stream_stream_stream_fun$)
+(declare-fun smap$d (A_stream_stream_a_stream_stream_fun$) A_stream_stream_stream_a_stream_stream_stream_fun$)
+(declare-fun smap$e (A_stream_a_stream_fun$) A_stream_stream_a_stream_stream_fun$)
+(declare-fun smap$f (B_stream_b_stream_fun$) B_stream_stream_b_stream_stream_fun$)
+(declare-fun smap$g (B_b_stream_fun$ B_stream$) B_stream_stream$)
+(declare-fun smap$h (B_a_stream_fun$ B_stream$) A_stream_stream$)
+(declare-fun smap$i (A_b_stream_fun$ A_stream$) B_stream_stream$)
+(declare-fun smap$j (A_a_stream_fun$ A_stream$) A_stream_stream$)
+(declare-fun smap$k (A_b_fun$ A_stream$) B_stream$)
+(declare-fun smap$l (B_stream_b_fun$ B_stream_stream$) B_stream$)
+(declare-fun smap$m (A_stream_b_fun$ A_stream_stream$) B_stream$)
+(declare-fun smap$n (B_stream_a_fun$ B_stream_stream$) A_stream$)
+(declare-fun smap$o (A_stream_a_fun$ A_stream_stream$) A_stream$)
+(declare-fun snth$a (B_stream$ Nat$) B$)
+(declare-fun snth$b (A_stream_stream$ Nat$) A_stream$)
+(declare-fun snth$c (A_stream$ Nat$) A$)
+(declare-fun member$ (B_stream$ B_stream_set$) Bool)
+(declare-fun sdrop$a (Nat$ B_stream$) B_stream$)
+(declare-fun sdrop$b (Nat$ A_stream_stream$) A_stream_stream$)
+(declare-fun sdrop$c (Nat$ A_stream$) A_stream$)
+(declare-fun fun_app$ (B_b_stream_fun$ B$) B_stream$)
+(declare-fun member$a (B$ B_set$) Bool)
+(declare-fun member$b (A$ A_set$) Bool)
+(declare-fun member$c (A_stream$ A_stream_set$) Bool)
+(declare-fun member$d (B_stream_stream$ B_stream_stream_set$) Bool)
+(declare-fun member$e (A_stream_stream$ A_stream_stream_set$) Bool)
+(declare-fun streams$ (B_set$) B_stream_set$)
+(declare-fun fun_app$a (A_a_stream_fun$ A$) A_stream$)
+(declare-fun fun_app$b (B_a_fun$ B$) A$)
+(declare-fun fun_app$c (B_stream_b_stream_fun$ B_stream$) B_stream$)
+(declare-fun fun_app$d (B_b_fun$ B$) B$)
+(declare-fun fun_app$e (A_stream_a_stream_fun$ A_stream$) A_stream$)
+(declare-fun fun_app$f (A_a_fun$ A$) A$)
+(declare-fun fun_app$g (B_stream_stream_stream_b_stream_stream_stream_fun$ B_stream_stream_stream$) B_stream_stream_stream$)
+(declare-fun fun_app$h (A_stream_stream_stream_a_stream_stream_stream_fun$ A_stream_stream_stream$) A_stream_stream_stream$)
+(declare-fun fun_app$i (A_stream_stream_a_stream_stream_fun$ A_stream_stream$) A_stream_stream$)
+(declare-fun fun_app$j (B_stream_stream_b_stream_stream_fun$ B_stream_stream$) B_stream_stream$)
+(declare-fun fun_app$k (B_a_stream_fun$ B$) A_stream$)
+(declare-fun fun_app$l (A_b_stream_fun$ A$) B_stream$)
+(declare-fun fun_app$m (A_b_fun$ A$) B$)
+(declare-fun fun_app$n (B_stream_b_fun$ B_stream$) B$)
+(declare-fun fun_app$o (A_stream_b_fun$ A_stream$) B$)
+(declare-fun fun_app$p (B_stream_a_fun$ B_stream$) A$)
+(declare-fun fun_app$q (A_stream_a_fun$ A_stream$) A$)
+(declare-fun siterate$ (B_b_fun$) B_b_stream_fun$)
+(declare-fun streams$a (A_set$) A_stream_set$)
+(declare-fun streams$b (B_stream_set$) B_stream_stream_set$)
+(declare-fun streams$c (A_stream_set$) A_stream_stream_set$)
+(declare-fun siterate$a (A_a_fun$) A_a_stream_fun$)
+(assert (! (not (= (smap$ f$ (fun_app$ (siterate$ id$) x$)) (fun_app$a (siterate$a id$a) (fun_app$b f$ x$)))) :named a0))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (fun_app$c (smap$a ?v0) (fun_app$ (siterate$ ?v0) ?v1)) (fun_app$ (siterate$ ?v0) (fun_app$d ?v0 ?v1)))) :named a1))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (fun_app$e (smap$b ?v0) (fun_app$a (siterate$a ?v0) ?v1)) (fun_app$a (siterate$a ?v0) (fun_app$f ?v0 ?v1)))) :named a2))
+(assert (! (forall ((?v0 B_stream_stream_stream$)) (= (fun_app$g (smap$c id$b) ?v0) ?v0)) :named a3))
+(assert (! (forall ((?v0 A_stream_stream_stream$)) (= (fun_app$h (smap$d id$c) ?v0) ?v0)) :named a4))
+(assert (! (forall ((?v0 A_stream_stream$)) (= (fun_app$i (smap$e id$d) ?v0) ?v0)) :named a5))
+(assert (! (forall ((?v0 B_stream_stream$)) (= (fun_app$j (smap$f id$e) ?v0) ?v0)) :named a6))
+(assert (! (forall ((?v0 B_stream$)) (= (fun_app$c (smap$a id$) ?v0) ?v0)) :named a7))
+(assert (! (forall ((?v0 A_stream$)) (= (fun_app$e (smap$b id$a) ?v0) ?v0)) :named a8))
+(assert (! (= (smap$c id$b) id$f) :named a9))
+(assert (! (= (smap$d id$c) id$g) :named a10))
+(assert (! (= (smap$e id$d) id$c) :named a11))
+(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_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))
+(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$b (smap$j ?v0 ?v1) ?v2) (fun_app$a ?v0 (snth$c ?v1 ?v2)))) :named a30))
+(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$a (smap$k ?v0 ?v1) ?v2) (fun_app$m ?v0 (snth$c ?v1 ?v2)))) :named a31))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$c (fun_app$e (smap$b ?v0) ?v1) ?v2) (fun_app$f ?v0 (snth$c ?v1 ?v2)))) :named a32))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$a (fun_app$c (smap$a ?v0) ?v1) ?v2) (fun_app$d ?v0 (snth$a ?v1 ?v2)))) :named a33))
+(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$c (smap$ ?v0 ?v1) ?v2) (fun_app$b ?v0 (snth$a ?v1 ?v2)))) :named a34))
+(assert (! (forall ((?v0 Nat$) (?v1 B_b_stream_fun$) (?v2 B_stream$)) (= (sdrop$ ?v0 (smap$g ?v1 ?v2)) (smap$g ?v1 (sdrop$a ?v0 ?v2)))) :named a35))
+(assert (! (forall ((?v0 Nat$) (?v1 B_a_stream_fun$) (?v2 B_stream$)) (= (sdrop$b ?v0 (smap$h ?v1 ?v2)) (smap$h ?v1 (sdrop$a ?v0 ?v2)))) :named a36))
+(assert (! (forall ((?v0 Nat$) (?v1 A_b_stream_fun$) (?v2 A_stream$)) (= (sdrop$ ?v0 (smap$i ?v1 ?v2)) (smap$i ?v1 (sdrop$c ?v0 ?v2)))) :named a37))
+(assert (! (forall ((?v0 Nat$) (?v1 A_a_stream_fun$) (?v2 A_stream$)) (= (sdrop$b ?v0 (smap$j ?v1 ?v2)) (smap$j ?v1 (sdrop$c ?v0 ?v2)))) :named a38))
+(assert (! (forall ((?v0 Nat$) (?v1 A_b_fun$) (?v2 A_stream$)) (= (sdrop$a ?v0 (smap$k ?v1 ?v2)) (smap$k ?v1 (sdrop$c ?v0 ?v2)))) :named a39))
+(assert (! (forall ((?v0 Nat$) (?v1 A_a_fun$) (?v2 A_stream$)) (= (sdrop$c ?v0 (fun_app$e (smap$b ?v1) ?v2)) (fun_app$e (smap$b ?v1) (sdrop$c ?v0 ?v2)))) :named a40))
+(assert (! (forall ((?v0 Nat$) (?v1 B_b_fun$) (?v2 B_stream$)) (= (sdrop$a ?v0 (fun_app$c (smap$a ?v1) ?v2)) (fun_app$c (smap$a ?v1) (sdrop$a ?v0 ?v2)))) :named a41))
+(assert (! (forall ((?v0 Nat$) (?v1 B_a_fun$) (?v2 B_stream$)) (= (sdrop$c ?v0 (smap$ ?v1 ?v2)) (smap$ ?v1 (sdrop$a ?v0 ?v2)))) :named a42))
+(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$)) (= (shd$b (smap$g ?v0 ?v1)) (fun_app$ ?v0 (shd$a ?v1)))) :named a43))
+(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$)) (= (shd$d (smap$h ?v0 ?v1)) (fun_app$k ?v0 (shd$a ?v1)))) :named a44))
+(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$)) (= (shd$b (smap$i ?v0 ?v1)) (fun_app$l ?v0 (shd$ ?v1)))) :named a45))
+(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$)) (= (shd$d (smap$j ?v0 ?v1)) (fun_app$a ?v0 (shd$ ?v1)))) :named a46))
+(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$)) (= (shd$a (smap$k ?v0 ?v1)) (fun_app$m ?v0 (shd$ ?v1)))) :named a47))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$)) (= (shd$ (fun_app$e (smap$b ?v0) ?v1)) (fun_app$f ?v0 (shd$ ?v1)))) :named a48))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$)) (= (shd$a (fun_app$c (smap$a ?v0) ?v1)) (fun_app$d ?v0 (shd$a ?v1)))) :named a49))
+(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$)) (= (shd$ (smap$ ?v0 ?v1)) (fun_app$b ?v0 (shd$a ?v1)))) :named a50))
+(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$)) (= (stl$b (smap$g ?v0 ?v1)) (smap$g ?v0 (stl$a ?v1)))) :named a51))
+(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$)) (= (stl$d (smap$h ?v0 ?v1)) (smap$h ?v0 (stl$a ?v1)))) :named a52))
+(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$)) (= (stl$b (smap$i ?v0 ?v1)) (smap$i ?v0 (stl$ ?v1)))) :named a53))
+(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$)) (= (stl$d (smap$j ?v0 ?v1)) (smap$j ?v0 (stl$ ?v1)))) :named a54))
+(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$)) (= (stl$a (smap$k ?v0 ?v1)) (smap$k ?v0 (stl$ ?v1)))) :named a55))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$)) (= (stl$ (fun_app$e (smap$b ?v0) ?v1)) (fun_app$e (smap$b ?v0) (stl$ ?v1)))) :named a56))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$)) (= (stl$a (fun_app$c (smap$a ?v0) ?v1)) (fun_app$c (smap$a ?v0) (stl$a ?v1)))) :named a57))
+(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$)) (= (stl$ (smap$ ?v0 ?v1)) (smap$ ?v0 (stl$a ?v1)))) :named a58))
+(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$) (?v2 B_stream_stream$)) (= (= (smap$g ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$ ?v0 (snth$a ?v1 ?v3)) (snth$ ?v2 ?v3))))) :named a59))
+(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$) (?v2 A_stream_stream$)) (= (= (smap$h ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$k ?v0 (snth$a ?v1 ?v3)) (snth$b ?v2 ?v3))))) :named a60))
+(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$) (?v2 B_stream_stream$)) (= (= (smap$i ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$l ?v0 (snth$c ?v1 ?v3)) (snth$ ?v2 ?v3))))) :named a61))
+(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$) (?v2 A_stream_stream$)) (= (= (smap$j ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$a ?v0 (snth$c ?v1 ?v3)) (snth$b ?v2 ?v3))))) :named a62))
+(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$) (?v2 B_stream$)) (= (= (smap$k ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$m ?v0 (snth$c ?v1 ?v3)) (snth$a ?v2 ?v3))))) :named a63))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$) (?v2 A_stream$)) (= (= (fun_app$e (smap$b ?v0) ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$f ?v0 (snth$c ?v1 ?v3)) (snth$c ?v2 ?v3))))) :named a64))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$) (?v2 B_stream$)) (= (= (fun_app$c (smap$a ?v0) ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$d ?v0 (snth$a ?v1 ?v3)) (snth$a ?v2 ?v3))))) :named a65))
+(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$) (?v2 A_stream$)) (= (= (smap$ ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$b ?v0 (snth$a ?v1 ?v3)) (snth$c ?v2 ?v3))))) :named a66))
+(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_a_fun$) (?v3 A_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$b (fun_app$b ?v2 ?v4) ?v3)))) (member$c (smap$ ?v2 ?v0) (streams$a ?v3)))) :named a67))
+(assert (! (forall ((?v0 A_stream$) (?v1 A_set$) (?v2 A_b_fun$) (?v3 B_set$)) (=> (and (member$c ?v0 (streams$a ?v1)) (forall ((?v4 A$)) (=> (member$b ?v4 ?v1) (member$a (fun_app$m ?v2 ?v4) ?v3)))) (member$ (smap$k ?v2 ?v0) (streams$ ?v3)))) :named a68))
+(assert (! (forall ((?v0 A_stream$) (?v1 A_set$) (?v2 A_a_fun$) (?v3 A_set$)) (=> (and (member$c ?v0 (streams$a ?v1)) (forall ((?v4 A$)) (=> (member$b ?v4 ?v1) (member$b (fun_app$f ?v2 ?v4) ?v3)))) (member$c (fun_app$e (smap$b ?v2) ?v0) (streams$a ?v3)))) :named a69))
+(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_b_fun$) (?v3 B_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$a (fun_app$d ?v2 ?v4) ?v3)))) (member$ (fun_app$c (smap$a ?v2) ?v0) (streams$ ?v3)))) :named a70))
+(assert (! (forall ((?v0 B_stream_stream$) (?v1 B_stream_set$) (?v2 B_stream_b_fun$) (?v3 B_set$)) (=> (and (member$d ?v0 (streams$b ?v1)) (forall ((?v4 B_stream$)) (=> (member$ ?v4 ?v1) (member$a (fun_app$n ?v2 ?v4) ?v3)))) (member$ (smap$l ?v2 ?v0) (streams$ ?v3)))) :named a71))
+(assert (! (forall ((?v0 A_stream_stream$) (?v1 A_stream_set$) (?v2 A_stream_b_fun$) (?v3 B_set$)) (=> (and (member$e ?v0 (streams$c ?v1)) (forall ((?v4 A_stream$)) (=> (member$c ?v4 ?v1) (member$a (fun_app$o ?v2 ?v4) ?v3)))) (member$ (smap$m ?v2 ?v0) (streams$ ?v3)))) :named a72))
+(assert (! (forall ((?v0 B_stream_stream$) (?v1 B_stream_set$) (?v2 B_stream_a_fun$) (?v3 A_set$)) (=> (and (member$d ?v0 (streams$b ?v1)) (forall ((?v4 B_stream$)) (=> (member$ ?v4 ?v1) (member$b (fun_app$p ?v2 ?v4) ?v3)))) (member$c (smap$n ?v2 ?v0) (streams$a ?v3)))) :named a73))
+(assert (! (forall ((?v0 A_stream_stream$) (?v1 A_stream_set$) (?v2 A_stream_a_fun$) (?v3 A_set$)) (=> (and (member$e ?v0 (streams$c ?v1)) (forall ((?v4 A_stream$)) (=> (member$c ?v4 ?v1) (member$b (fun_app$q ?v2 ?v4) ?v3)))) (member$c (smap$o ?v2 ?v0) (streams$a ?v3)))) :named a74))
+(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_b_stream_fun$) (?v3 B_stream_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$ (fun_app$ ?v2 ?v4) ?v3)))) (member$d (smap$g ?v2 ?v0) (streams$b ?v3)))) :named a75))
+(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_a_stream_fun$) (?v3 A_stream_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$c (fun_app$k ?v2 ?v4) ?v3)))) (member$e (smap$h ?v2 ?v0) (streams$c ?v3)))) :named a76))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (shd$a (fun_app$ (siterate$ ?v0) ?v1)) ?v1)) :named a77))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (shd$ (fun_app$a (siterate$a ?v0) ?v1)) ?v1)) :named a78))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (stl$a (fun_app$ (siterate$ ?v0) ?v1)) (fun_app$ (siterate$ ?v0) (fun_app$d ?v0 ?v1)))) :named a79))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (stl$ (fun_app$a (siterate$a ?v0) ?v1)) (fun_app$a (siterate$a ?v0) (fun_app$f ?v0 ?v1)))) :named a80))
+(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (fun_app$ (siterate$ ?v0) ?v1) (sCons$a ?v1 (fun_app$ (siterate$ ?v0) (fun_app$d ?v0 ?v1))))) :named a81))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (fun_app$a (siterate$a ?v0) ?v1) (sCons$ ?v1 (fun_app$a (siterate$a ?v0) (fun_app$f ?v0 ?v1))))) :named a82))
+(check-sat)