diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-04-22 07:06:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-22 07:06:24 -0500 |
commit | da73f99910a25fca342c0ba1d8ec19de6c3cefda (patch) | |
tree | 724e6b2b3061b2eb57f0814537bfb2d687947e40 /test/regress/regress1/fmf/jasmin-cdt-crash.smt2 | |
parent | 2a38d482462fdf30376c984e7a82c99d08e75f92 (diff) |
Convert V2.5 SMT regressions to V2.6. (#4319)
This commit converts all v2.5 smt2 regressions to v2.6 (except for regress/regress0/lang_opts_2_5.smt2).
Diffstat (limited to 'test/regress/regress1/fmf/jasmin-cdt-crash.smt2')
-rw-r--r-- | test/regress/regress1/fmf/jasmin-cdt-crash.smt2 | 75 |
1 files changed, 37 insertions, 38 deletions
diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 index 7012838f9..7f3a5b28f 100644 --- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 +++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 @@ -1,16 +1,15 @@ -; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone --lang=smt2.5 +; 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-codatatypes ((llist_ 0)) + (((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-datatypes ((_nat 0)) (((_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) @@ -21,28 +20,28 @@ (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_)) + (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)) + (proj_G_lprefix__neg_2 a/68)) (= (_select_LCons__1 (proj_G_lprefix__neg_1 a/60)) - (proj_G_lprefix__neg_1 a/68)) + (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)) + (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) + (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) @@ -53,18 +52,18 @@ (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_) + (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))) + (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)) + (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)) + (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_) @@ -74,27 +73,27 @@ (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)) + (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_) + (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_)) + (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))) + (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)) + (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_)) + (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)) + (and (= (LCons_ y_ ys_) (proj_G_lprefix__pos_1 a/125)) (= xs_ (proj_G_lprefix__pos_0 a/125))))))) (check-sat) |