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/sc-crash-052316.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/sc-crash-052316.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/sc-crash-052316.smt2 | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/test/regress/regress1/fmf/sc-crash-052316.smt2 b/test/regress/regress1/fmf/sc-crash-052316.smt2 index 345d8220e..5c695e482 100644 --- a/test/regress/regress1/fmf/sc-crash-052316.smt2 +++ b/test/regress/regress1/fmf/sc-crash-052316.smt2 @@ -1,29 +1,29 @@ -; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; COMMAND-LINE: --finite-model-find ; EXPECT: unsat - (set-logic ALL_SUPPORTED) - (set-info :status unsat) - (declare-sort g_ 0) - (declare-fun __nun_card_witness_0_ () g_) - (declare-sort f_ 0) - (declare-fun __nun_card_witness_1_ () f_) - (declare-sort e_ 0) - (declare-fun __nun_card_witness_2_ () e_) -(declare-datatypes () - ((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_))))) - (declare-sort d_ 0) - (declare-fun __nun_card_witness_3_ () d_) - (declare-sort c_ 0) - (declare-fun __nun_card_witness_4_ () c_) - (declare-sort b_ 0) - (declare-fun __nun_card_witness_5_ () b_) - (declare-sort a_ 0) - (declare-fun __nun_card_witness_6_ () a_) -(declare-datatypes () - ((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_))))) - (declare-fun f1_ (prod_ c_ d_ prod1_) g_) - (declare-fun g1_ (prod_) c_) - (declare-fun h_ (prod_ d_) prod1_) - (declare-fun nun_sk_0_ () prod_) +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort g_ 0) +(declare-fun __nun_card_witness_0_ () g_) +(declare-sort f_ 0) +(declare-fun __nun_card_witness_1_ () f_) +(declare-sort e_ 0) +(declare-fun __nun_card_witness_2_ () e_) +(declare-datatypes ((prod1_ 0)) + (((Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_))))) +(declare-sort d_ 0) +(declare-fun __nun_card_witness_3_ () d_) +(declare-sort c_ 0) +(declare-fun __nun_card_witness_4_ () c_) +(declare-sort b_ 0) +(declare-fun __nun_card_witness_5_ () b_) +(declare-sort a_ 0) +(declare-fun __nun_card_witness_6_ () a_) +(declare-datatypes ((prod_ 0)) + (((Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_))))) +(declare-fun f1_ (prod_ c_ d_ prod1_) g_) +(declare-fun g1_ (prod_) c_) +(declare-fun h_ (prod_ d_) prod1_) +(declare-fun nun_sk_0_ () prod_) (declare-fun nun_sk_1_ (c_) d_) (assert (not |