diff options
Diffstat (limited to 'test/regress/regress1/fmf/loopy_coda.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/loopy_coda.smt2 | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2 new file mode 100644 index 000000000..519fb17fc --- /dev/null +++ b/test/regress/regress1/fmf/loopy_coda.smt2 @@ -0,0 +1,38 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone --lang=smt2.5 +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort a 0) +(declare-fun __nun_card_witness_0 () a) +(declare-codatatypes () + ((llist (LCons (_select_LCons_0 a) (_select_LCons_1 llist)) (LNil )))) +(declare-fun xs () llist) +(declare-fun y () a) +(declare-fun ys () llist) +(declare-sort G_lappend 0) +(declare-fun __nun_card_witness_1 () G_lappend) +(declare-fun lappend (llist llist) llist) +(declare-fun proj_G_lappend_0 (G_lappend) llist) +(declare-fun proj_G_lappend_1 (G_lappend) llist) +(assert + (forall ((a/33 G_lappend)) + (and + (= (lappend (proj_G_lappend_0 a/33) (proj_G_lappend_1 a/33)) + (ite (is-LCons (proj_G_lappend_0 a/33)) + (LCons (_select_LCons_0 (proj_G_lappend_0 a/33)) + (lappend (_select_LCons_1 (proj_G_lappend_0 a/33)) + (proj_G_lappend_1 a/33))) + (proj_G_lappend_1 a/33))) + (=> (is-LCons (proj_G_lappend_0 a/33)) + (exists ((a/35 G_lappend)) + (and (= (proj_G_lappend_1 a/33) (proj_G_lappend_1 a/35)) + (= (_select_LCons_1 (proj_G_lappend_0 a/33)) + (proj_G_lappend_0 a/35)))))))) +(assert + (not + (=> + (exists ((a/37 G_lappend)) + (and (= (LCons y ys) (proj_G_lappend_1 a/37)) + (= xs (proj_G_lappend_0 a/37)))) + (= (lappend xs (LCons y ys)) xs)))) +(check-sat) |