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).

1 files changed, 32 insertions, 32 deletions

diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
index 68a4399ca..d951e6c50 100644
--- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2
+++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
@@ -1,33 +1,33 @@
-; COMMAND-LINE: --finite-model-find --lang=smt2.5
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
-  (set-logic ALL_SUPPORTED)
-  (set-info :status sat)
-  (declare-sort a 0)
-  (declare-fun __nun_card_witness_0 () a)
-  (declare-datatypes () ((prod (Pair (_select_Pair_0 a) (_select_Pair_1 a)))))
-  (declare-sort G_snd 0)
-  (declare-fun __nun_card_witness_1 () G_snd)
-  (declare-fun snd (prod) a)
-  (declare-fun proj_G_snd_0 (G_snd) prod)
-  (assert
-   (forall ((a/32 G_snd))
-      (and
-       (= (snd (proj_G_snd_0 a/32)) (_select_Pair_1 (proj_G_snd_0 a/32))) 
-       true)))
-  (declare-fun p () prod)
-  (declare-datatypes () ((pd (Pd (_select_Pd_0 prod)))))
-  (declare-sort G_fs 0)
-  (declare-fun __nun_card_witness_2 () G_fs)
-  (declare-fun fs (pd) a)
-  (declare-fun proj_G_fs_0 (G_fs) pd)
-  (assert
-   (forall ((a/33 G_fs))
-      (and
-       (= (fs (proj_G_fs_0 a/33))
-        (_select_Pair_0 (_select_Pd_0 (proj_G_fs_0 a/33)))) 
-       true)))
-  (assert
-   (and (not (= (fs (Pd p)) (snd p))) 
-    (exists ((a/34 G_fs)) (= (Pd p) (proj_G_fs_0 a/34))) 
-    (exists ((a/35 G_snd)) (= p (proj_G_snd_0 a/35)))))
-  (check-sat)
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort a 0)
+(declare-fun __nun_card_witness_0 () a)
+(declare-datatypes ((prod 0)) (((Pair (_select_Pair_0 a) (_select_Pair_1 a)))))
+(declare-sort G_snd 0)
+(declare-fun __nun_card_witness_1 () G_snd)
+(declare-fun snd (prod) a)
+(declare-fun proj_G_snd_0 (G_snd) prod)
+(assert
+ (forall ((a/32 G_snd))
+    (and
+     (= (snd (proj_G_snd_0 a/32)) (_select_Pair_1 (proj_G_snd_0 a/32)))
+     true)))
+(declare-fun p () prod)
+(declare-datatypes ((pd 0)) (((Pd (_select_Pd_0 prod)))))
+(declare-sort G_fs 0)
+(declare-fun __nun_card_witness_2 () G_fs)
+(declare-fun fs (pd) a)
+(declare-fun proj_G_fs_0 (G_fs) pd)
+(assert
+ (forall ((a/33 G_fs))
+    (and
+     (= (fs (proj_G_fs_0 a/33))
+      (_select_Pair_0 (_select_Pd_0 (proj_G_fs_0 a/33))))
+     true)))
+(assert
+ (and (not (= (fs (Pd p)) (snd p)))
+  (exists ((a/34 G_fs)) (= (Pd p) (proj_G_fs_0 a/34)))
+  (exists ((a/35 G_snd)) (= p (proj_G_snd_0 a/35)))))
+(check-sat)