diff options
author | ajreynol <ajreynol@r-lnx214.cs.uiowa.edu> | 2016-01-19 12:21:50 -0600 |
---|---|---|
committer | ajreynol <ajreynol@r-lnx214.cs.uiowa.edu> | 2016-01-19 12:21:50 -0600 |
commit | bbcf8ccc012caf6ad54b7ec2b91a9886fb6021e6 (patch) | |
tree | aaf3b3f944f193eba28ad3962801f481fc69f2bb /test | |
parent | 4d3e24e52765b03d8e6f36afe7de6168e8740693 (diff) |
Bug fixes for model construction with codatatypes, add regressions.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/coda_simp_model.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/fmf/jasmin-cdt-crash.smt2 | 100 | ||||
-rw-r--r-- | test/regress/regress0/fmf/loopy_coda.smt2 | 38 |
5 files changed, 155 insertions, 2 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index d06fb1b9b..1759d2924 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -68,7 +68,8 @@ TESTS = \ bug625.smt2 \ cdt-model-cade15.smt2 \ sc-cdt1.smt2 \ - conqueue-dt-enum-iloop.smt2 + conqueue-dt-enum-iloop.smt2 \ + coda_simp_model.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/coda_simp_model.smt2 b/test/regress/regress0/datatypes/coda_simp_model.smt2 new file mode 100644 index 000000000..1e000cecd --- /dev/null +++ b/test/regress/regress0/datatypes/coda_simp_model.smt2 @@ -0,0 +1,12 @@ +(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 s () llist_) +(declare-fun a () a_) +(declare-fun b () a_) +(assert (= s (LCons_ a (LCons_ b s)))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index ff2591a5b..d262d624f 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -45,7 +45,9 @@ TESTS = \ sc_bad_model_1221.smt2 \ dt-proper-model.smt2 \ fd-false.smt2 \ - tail_rec.smt2 + tail_rec.smt2 \ + jasmin-cdt-crash.smt2 \ + loopy_coda.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 new file mode 100644 index 000000000..1f7214232 --- /dev/null +++ b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 @@ -0,0 +1,100 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone +; 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-datatypes () ((_nat (_succ (_select__succ_0 _nat)) (_zero )))) +(declare-fun decr_lprefix_ () _nat) +(declare-sort G_lprefix__neg 0) +(declare-fun __nun_card_witness_1 () G_lprefix__neg) +(declare-fun lprefix__- (_nat llist_ llist_) Bool) +(declare-fun proj_G_lprefix__neg_0 (G_lprefix__neg) _nat) +(declare-fun proj_G_lprefix__neg_1 (G_lprefix__neg) llist_) +(declare-fun proj_G_lprefix__neg_2 (G_lprefix__neg) llist_) +(assert + (forall ((a/60 G_lprefix__neg)) + (=> + (or (= (proj_G_lprefix__neg_0 a/60) _zero) + (and (is-_succ (proj_G_lprefix__neg_0 a/60)) + (= (proj_G_lprefix__neg_1 a/60) LNil_)) + (and + (=> + (exists ((a/68 G_lprefix__neg)) + (and + (= (_select_LCons__1 (proj_G_lprefix__neg_2 a/60)) + (proj_G_lprefix__neg_2 a/68)) + (= (_select_LCons__1 (proj_G_lprefix__neg_1 a/60)) + (proj_G_lprefix__neg_1 a/68)) + (= (_select__succ_0 (proj_G_lprefix__neg_0 a/60)) + (proj_G_lprefix__neg_0 a/68)))) + (lprefix__- (_select__succ_0 (proj_G_lprefix__neg_0 a/60)) + (_select_LCons__1 (proj_G_lprefix__neg_1 a/60)) + (_select_LCons__1 (proj_G_lprefix__neg_2 a/60)))) + (is-_succ (proj_G_lprefix__neg_0 a/60)) + (is-LCons_ (proj_G_lprefix__neg_1 a/60)) + (is-LCons_ (proj_G_lprefix__neg_2 a/60)) + (= (_select_LCons__0 (proj_G_lprefix__neg_2 a/60)) + (_select_LCons__0 (proj_G_lprefix__neg_1 a/60))))) + (lprefix__- (proj_G_lprefix__neg_0 a/60) (proj_G_lprefix__neg_1 a/60) + (proj_G_lprefix__neg_2 a/60))))) +(declare-sort G_lprefix__pos 0) +(declare-fun __nun_card_witness_2 () G_lprefix__pos) +(declare-fun lprefix__+ (llist_ llist_) Bool) +(declare-fun proj_G_lprefix__pos_0 (G_lprefix__pos) llist_) +(declare-fun proj_G_lprefix__pos_1 (G_lprefix__pos) llist_) +(assert + (forall ((a/69 G_lprefix__pos)) + (=> + (lprefix__+ (proj_G_lprefix__pos_0 a/69) (proj_G_lprefix__pos_1 a/69)) + (or (= (proj_G_lprefix__pos_0 a/69) LNil_) + (and + (lprefix__+ (_select_LCons__1 (proj_G_lprefix__pos_0 a/69)) + (_select_LCons__1 (proj_G_lprefix__pos_1 a/69))) + (exists ((a/77 G_lprefix__pos)) + (and + (= (_select_LCons__1 (proj_G_lprefix__pos_1 a/69)) + (proj_G_lprefix__pos_1 a/77)) + (= (_select_LCons__1 (proj_G_lprefix__pos_0 a/69)) + (proj_G_lprefix__pos_0 a/77)))) + (is-LCons_ (proj_G_lprefix__pos_0 a/69)) + (is-LCons_ (proj_G_lprefix__pos_1 a/69)) + (= (_select_LCons__0 (proj_G_lprefix__pos_1 a/69)) + (_select_LCons__0 (proj_G_lprefix__pos_0 a/69)))))))) +(declare-fun nun_sk_0 () llist_) +(assert + (or + (and + (not + (=> + (exists ((a/109 G_lprefix__neg)) + (and (= (LCons_ y_ ys_) (proj_G_lprefix__neg_2 a/109)) + (= xs_ (proj_G_lprefix__neg_1 a/109)) + (= decr_lprefix_ (proj_G_lprefix__neg_0 a/109)))) + (lprefix__- decr_lprefix_ xs_ (LCons_ y_ ys_)))) + (or (= xs_ LNil_) + (and (= xs_ (LCons_ y_ nun_sk_0)) (lprefix__+ xs_ ys_) + (exists ((a/113 G_lprefix__pos)) + (and (= ys_ (proj_G_lprefix__pos_1 a/113)) + (= xs_ (proj_G_lprefix__pos_0 a/113))))))) + (and (not (= xs_ LNil_)) + (forall ((xs_H_/120 llist_)) + (or (not (= xs_ (LCons_ y_ xs_H_/120))) + (not + (=> + (exists ((a/124 G_lprefix__neg)) + (and (= ys_ (proj_G_lprefix__neg_2 a/124)) + (= xs_ (proj_G_lprefix__neg_1 a/124)) + (= decr_lprefix_ (proj_G_lprefix__neg_0 a/124)))) + (lprefix__- decr_lprefix_ xs_ ys_))))) + (lprefix__+ xs_ (LCons_ y_ ys_)) + (exists ((a/125 G_lprefix__pos)) + (and (= (LCons_ y_ ys_) (proj_G_lprefix__pos_1 a/125)) + (= xs_ (proj_G_lprefix__pos_0 a/125))))))) +(check-sat) diff --git a/test/regress/regress0/fmf/loopy_coda.smt2 b/test/regress/regress0/fmf/loopy_coda.smt2 new file mode 100644 index 000000000..7c1d30886 --- /dev/null +++ b/test/regress/regress0/fmf/loopy_coda.smt2 @@ -0,0 +1,38 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone +; 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) |