diff options
Diffstat (limited to 'test/regress/regress1/fmf/nun-0208-to.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/nun-0208-to.smt2 | 180 |
1 files changed, 180 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2 new file mode 100644 index 000000000..e6b3c2021 --- /dev/null +++ b/test/regress/regress1/fmf/nun-0208-to.smt2 @@ -0,0 +1,180 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: sat + (set-logic ALL_SUPPORTED) + (declare-sort b__ 0) + (declare-fun __nun_card_witness_0_ () b__) + (declare-sort a__ 0) + (declare-fun __nun_card_witness_1_ () a__) + (declare-datatypes () + ((prod__ (Pair__ (_select_Pair___0 a__) (_select_Pair___1 b__))))) + (declare-datatypes () + ((list2__ + (Cons2__ (_select_Cons2___0 prod__) (_select_Cons2___1 list2__)) + (Nil2__ )))) + (declare-datatypes () + ((list__ (Cons__ (_select_Cons___0 a__) (_select_Cons___1 list__)) + (Nil__ )))) + (declare-datatypes () + ((list1__ (Cons1__ (_select_Cons1___0 b__) (_select_Cons1___1 list1__)) + (Nil1__ )))) + (declare-sort G_zip__ 0) + (declare-fun __nun_card_witness_2_ () G_zip__) + (declare-fun zip__ (list__ list1__) list2__) + (declare-fun proj_G_zip__0_ (G_zip__) list__) + (declare-fun proj_G_zip__1_ (G_zip__) list1__) + (assert + (forall ((a/166 G_zip__)) + (and + (= (zip__ (proj_G_zip__0_ a/166) (proj_G_zip__1_ a/166)) + (ite (is-Cons1__ (proj_G_zip__1_ a/166)) + (ite (is-Cons__ (proj_G_zip__0_ a/166)) + (Cons2__ + (Pair__ (_select_Cons___0 (proj_G_zip__0_ a/166)) + (_select_Cons1___0 (proj_G_zip__1_ a/166))) + (zip__ (_select_Cons___1 (proj_G_zip__0_ a/166)) + (_select_Cons1___1 (proj_G_zip__1_ a/166)))) + Nil2__) + Nil2__)) + (=> (is-Cons1__ (proj_G_zip__1_ a/166)) + (=> (is-Cons__ (proj_G_zip__0_ a/166)) + (exists ((a/168 G_zip__)) + (and + (= (_select_Cons1___1 (proj_G_zip__1_ a/166)) + (proj_G_zip__1_ a/168)) + (= (_select_Cons___1 (proj_G_zip__0_ a/166)) + (proj_G_zip__0_ a/168))))))))) + (declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ )))) + (declare-sort G_replicate__ 0) + (declare-fun __nun_card_witness_3_ () G_replicate__) + (declare-fun replicate__ (nat__ a__) list__) + (declare-fun proj_G_replicate__0_ (G_replicate__) nat__) + (declare-fun proj_G_replicate__1_ (G_replicate__) a__) + (assert + (forall ((a/169 G_replicate__)) + (and + (= + (replicate__ (proj_G_replicate__0_ a/169) + (proj_G_replicate__1_ a/169)) + (ite (is-Suc__ (proj_G_replicate__0_ a/169)) + (Cons__ (proj_G_replicate__1_ a/169) + (replicate__ (_select_Suc___0 (proj_G_replicate__0_ a/169)) + (proj_G_replicate__1_ a/169))) + Nil__)) + (=> (is-Suc__ (proj_G_replicate__0_ a/169)) + (exists ((a/171 G_replicate__)) + (and + (= (proj_G_replicate__1_ a/169) (proj_G_replicate__1_ a/171)) + (= (_select_Suc___0 (proj_G_replicate__0_ a/169)) + (proj_G_replicate__0_ a/171)))))))) + (declare-fun j__ () nat__) + (declare-fun x__ () a__) + (declare-sort G_replicate1__ 0) + (declare-fun __nun_card_witness_4_ () G_replicate1__) + (declare-fun replicate1__ (nat__ b__) list1__) + (declare-fun proj_G_replicate1__0_ (G_replicate1__) nat__) + (declare-fun proj_G_replicate1__1_ (G_replicate1__) b__) + (assert + (forall ((a/172 G_replicate1__)) + (and + (= + (replicate1__ (proj_G_replicate1__0_ a/172) + (proj_G_replicate1__1_ a/172)) + (ite (is-Suc__ (proj_G_replicate1__0_ a/172)) + (Cons1__ (proj_G_replicate1__1_ a/172) + (replicate1__ (_select_Suc___0 (proj_G_replicate1__0_ a/172)) + (proj_G_replicate1__1_ a/172))) + Nil1__)) + (=> (is-Suc__ (proj_G_replicate1__0_ a/172)) + (exists ((a/174 G_replicate1__)) + (and + (= (proj_G_replicate1__1_ a/172) (proj_G_replicate1__1_ a/174)) + (= (_select_Suc___0 (proj_G_replicate1__0_ a/172)) + (proj_G_replicate1__0_ a/174)))))))) + (declare-fun y__ () b__) + (declare-sort G_replicate2__ 0) + (declare-fun __nun_card_witness_5_ () G_replicate2__) + (declare-fun replicate2__ (nat__ prod__) list2__) + (declare-fun proj_G_replicate2__0_ (G_replicate2__) nat__) + (declare-fun proj_G_replicate2__1_ (G_replicate2__) prod__) + (assert + (forall ((a/175 G_replicate2__)) + (and + (= + (replicate2__ (proj_G_replicate2__0_ a/175) + (proj_G_replicate2__1_ a/175)) + (ite (is-Suc__ (proj_G_replicate2__0_ a/175)) + (Cons2__ (proj_G_replicate2__1_ a/175) + (replicate2__ (_select_Suc___0 (proj_G_replicate2__0_ a/175)) + (proj_G_replicate2__1_ a/175))) + Nil2__)) + (=> (is-Suc__ (proj_G_replicate2__0_ a/175)) + (exists ((a/177 G_replicate2__)) + (and + (= (proj_G_replicate2__1_ a/175) (proj_G_replicate2__1_ a/177)) + (= (_select_Suc___0 (proj_G_replicate2__0_ a/175)) + (proj_G_replicate2__0_ a/177)))))))) + (declare-sort G_less__eq__ 0) + (declare-fun __nun_card_witness_6_ () G_less__eq__) + (declare-fun less__eq__ (nat__ nat__) Bool) + (declare-fun proj_G_less__eq__0_ (G_less__eq__) nat__) + (declare-fun proj_G_less__eq__1_ (G_less__eq__) nat__) + (assert + (forall ((a/178 G_less__eq__)) + (and + (= + (less__eq__ (proj_G_less__eq__0_ a/178) (proj_G_less__eq__1_ a/178)) + (=> (is-Suc__ (proj_G_less__eq__0_ a/178)) + (and (is-Suc__ (proj_G_less__eq__1_ a/178)) + (less__eq__ (_select_Suc___0 (proj_G_less__eq__0_ a/178)) + (_select_Suc___0 (proj_G_less__eq__1_ a/178)))))) + (exists ((a/182 G_less__eq__)) + (and + (= (_select_Suc___0 (proj_G_less__eq__1_ a/178)) + (proj_G_less__eq__1_ a/182)) + (= (_select_Suc___0 (proj_G_less__eq__0_ a/178)) + (proj_G_less__eq__0_ a/182))))))) + (declare-sort G_min__ 0) + (declare-fun __nun_card_witness_7_ () G_min__) + (declare-fun min__ (nat__ nat__) nat__) + (declare-fun proj_G_min__0_ (G_min__) nat__) + (declare-fun proj_G_min__1_ (G_min__) nat__) + (assert + (forall ((a/183 G_min__)) + (and + (= (min__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183)) + (ite (less__eq__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183)) + (proj_G_min__0_ a/183) (proj_G_min__1_ a/183))) + (exists ((a/184 G_less__eq__)) + (and (= (proj_G_min__1_ a/183) (proj_G_less__eq__1_ a/184)) + (= (proj_G_min__0_ a/183) (proj_G_less__eq__0_ a/184))))))) + (declare-fun i__ () nat__) + (assert + (not + (=> + (and + (exists ((a/212 G_min__)) + (and (= i__ (proj_G_min__1_ a/212)) (= i__ (proj_G_min__0_ a/212)))) + (exists ((a/208 G_replicate2__)) + (and (= (Pair__ x__ y__) (proj_G_replicate2__1_ a/208)) + (= (min__ i__ i__) (proj_G_replicate2__0_ a/208)) + (exists ((a/210 G_min__)) + (and (= i__ (proj_G_min__1_ a/210)) + (= i__ (proj_G_min__0_ a/210)))))) + (exists ((a/199 G_zip__)) + (and (= (replicate1__ j__ y__) (proj_G_zip__1_ a/199)) + (exists ((a/202 G_replicate1__)) + (and (= y__ (proj_G_replicate1__1_ a/202)) + (= j__ (proj_G_replicate1__0_ a/202)))) + (= (replicate__ j__ x__) (proj_G_zip__0_ a/199)) + (exists ((a/203 G_replicate__)) + (and (= x__ (proj_G_replicate__1_ a/203)) + (= j__ (proj_G_replicate__0_ a/203)))))) + (exists ((a/207 G_replicate1__)) + (and (= y__ (proj_G_replicate1__1_ a/207)) + (= j__ (proj_G_replicate1__0_ a/207)))) + (exists ((a/206 G_replicate__)) + (and (= x__ (proj_G_replicate__1_ a/206)) + (= j__ (proj_G_replicate__0_ a/206))))) + (= (replicate2__ (min__ i__ i__) (Pair__ x__ y__)) + (zip__ (replicate__ j__ x__) (replicate1__ j__ y__)))))) + (check-sat) |