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

6 files changed, 85 insertions, 90 deletions

diff --git a/test/regress/regress1/quantifiers/bug_743.smt2 b/test/regress/regress1/quantifiers/bug_743.smt2
index ec5a5149e..1b6b16535 100644
--- a/test/regress/regress1/quantifiers/bug_743.smt2
+++ b/test/regress/regress1/quantifiers/bug_743.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.5
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
 
 ;; produced by cvc4_14.drv ;;
@@ -10,23 +10,22 @@
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
 ;;; SMT-LIB2: integer arithmetic
-(declare-datatypes () ((tuple0 (Tuple0))))
+(declare-datatypes ((tuple0 0)) (((Tuple0))))
 (declare-sort us_private 0)
 
 (declare-fun us_null_ext__ () us_private)
 
 (declare-sort us_type_of_heap 0)
 
-(declare-datatypes ()
-((us_type_of_heap__ref
- (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap)))))
+(declare-datatypes ((us_type_of_heap__ref 0))
+(((mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap)))))
 (declare-sort us_image 0)
 
-(declare-datatypes () ((int__ref (mk_int__ref (int__content Int)))))
-(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool)))))
-(declare-datatypes () ((real__ref (mk_real__ref (real__content Real)))))
-(declare-datatypes ()
-((us_private__ref (mk___private__ref (us_private__content us_private)))))
+(declare-datatypes ((int__ref 0)) (((mk_int__ref (int__content Int)))))
+(declare-datatypes ((bool__ref 0)) (((mk_bool__ref (bool__content Bool)))))
+(declare-datatypes ((real__ref 0)) (((mk_real__ref (real__content Real)))))
+(declare-datatypes ((us_private__ref 0))
+(((mk___private__ref (us_private__content us_private)))))
 (define-fun int__ref___projection ((a int__ref)) Int (int__content a))
 
 (define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
@@ -76,24 +75,24 @@
 
 ;; inversion_axiom
   (assert
-  (forall ((x integer)) (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) 
+  (forall ((x integer)) (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x))
 )))
 
 ;; range_axiom
   (assert
-  (forall ((x integer)) (! (in_range1 (to_rep x)) :pattern ((to_rep x)) 
+  (forall ((x integer)) (! (in_range1 (to_rep x)) :pattern ((to_rep x))
 )))
 
 ;; coerce_axiom
   (assert
   (forall ((x Int))
   (! (=> (in_range1 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep
-                                                            (of_rep x))) 
+                                                            (of_rep x)))
 )))
 
-(declare-datatypes ()
-((integer__ref (mk_integer__ref (integer__content integer)))))
-(define-fun integer__ref___projection ((a integer__ref)) integer 
+(declare-datatypes ((integer__ref 0))
+(((mk_integer__ref (integer__content integer)))))
+(define-fun integer__ref___projection ((a integer__ref)) integer
 (integer__content
                                                                  a))
 
@@ -124,23 +123,23 @@
 
 ;; range_axiom
   (assert
-  (forall ((x natural)) (! (in_range2 (to_rep1 x)) :pattern ((to_rep1 x)) 
+  (forall ((x natural)) (! (in_range2 (to_rep1 x)) :pattern ((to_rep1 x))
 )))
 
 ;; coerce_axiom
   (assert
   (forall ((x Int))
   (! (=> (in_range2 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1
-                                                              (of_rep1 
+                                                              (of_rep1
 x))) )))
 
-(declare-datatypes ()
-((natural__ref (mk_natural__ref (natural__content natural)))))
-(define-fun natural__ref___projection ((a natural__ref)) natural 
+(declare-datatypes ((natural__ref 0))
+(((mk_natural__ref (natural__content natural)))))
+(define-fun natural__ref___projection ((a natural__ref)) natural
 (natural__content
                                                                  a))
 
-(define-fun dynamic_invariant ((temp___expr_33 Int) (temp___is_init_30 
+(define-fun dynamic_invariant ((temp___expr_33 Int) (temp___is_init_30
 Bool)
   (temp___do_constant_31 Bool)
   (temp___do_toplevel_32 Bool)) Bool (=>
@@ -175,19 +174,19 @@ Bool)
 
 ;; range_axiom
   (assert
-  (forall ((x index)) (! (in_range3 (to_rep2 x)) :pattern ((to_rep2 x)) 
+  (forall ((x index)) (! (in_range3 (to_rep2 x)) :pattern ((to_rep2 x))
 )))
 
 ;; coerce_axiom
   (assert
   (forall ((x Int))
   (! (=> (in_range3 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2
-                                                              (of_rep2 
+                                                              (of_rep2
 x))) )))
 
-(declare-datatypes () ((index__ref (mk_index__ref (index__content 
+(declare-datatypes ((index__ref 0)) (((mk_index__ref (index__content
 index)))))
-(define-fun index__ref___projection ((a index__ref)) index (index__content 
+(define-fun index__ref___projection ((a index__ref)) index (index__content
 a))
 
 (define-fun dynamic_invariant1 ((temp___expr_144 Int)
@@ -197,8 +196,8 @@ a))
                                       (<= 1 100)) (in_range3
                                       temp___expr_144)))
 
-(declare-datatypes ()
-((map__ref (mk_map__ref (map__content (Array Int natural))))))
+(declare-datatypes ((map__ref 0))
+(((mk_map__ref (map__content (Array Int natural))))))
 (declare-fun bool_eq3 ((Array Int natural) Int Int (Array Int natural) Int
   Int) Bool)
 
@@ -214,7 +213,7 @@ a))
      (and (ite (<= af al) (= (+ (- al af) 1) (+ (- bl bf) 1)) (< bl bf))
      (forall ((i Int))
      (! (=> (and (<= af i) (<= i al))
-        (= (select a i) (select b (+ (- bf af) i)))) :pattern ((select a 
+        (= (select a i) (select b (+ (- bf af) i)))) :pattern ((select a
 i)) )))
      (= (bool_eq3 a af al b bf bl) true)) :pattern ((bool_eq3 a af al b bf
                                                     bl)) ))))))))
@@ -233,7 +232,7 @@ i)) )))
   (forall ((old_first Int))
   (forall ((new_first Int))
   (forall ((i Int))
-  (! (= (select (slide a old_first new_first) i) (select a (- i (- 
+  (! (= (select (slide a old_first new_first) i) (select a (- i (-
 new_first old_first)))) :pattern ((select
   (slide a old_first new_first) i)) ))))))
 
@@ -247,10 +246,10 @@ new_first old_first)))) :pattern ((select
   (forall ((i Int))
   (! (and
      (=> (and (<= a_first i) (<= i a_last))
-     (= (select (concat1 a a_first a_last b b_first b_last) i) (select a 
+     (= (select (concat1 a a_first a_last b b_first b_last) i) (select a
 i)))
      (=> (< a_last i)
-     (= (select (concat1 a a_first a_last b b_first b_last) i) (select b 
+     (= (select (concat1 a a_first a_last b b_first b_last) i) (select b
 (+ (- i a_last) (- b_first 1)))))) :pattern ((select
   (concat1 a a_first a_last b b_first b_last) i)) )))))
 
@@ -260,7 +259,7 @@ i)))
   (assert
   (forall ((v natural))
   (forall ((i Int))
-  (! (= (select (singleton v i) i) v) :pattern ((select (singleton v i) 
+  (! (= (select (singleton v i) i) v) :pattern ((select (singleton v i)
 i)) ))))
 
 (declare-fun compare ((Array Int natural) Int Int (Array Int natural) Int
@@ -289,7 +288,7 @@ i)) ))))
      (and (= (bool_eq3 a a_first j b b_first i) true)
      (or (= i b_last)
      (and (< i b_last)
-     (< (to_rep1 (select b (+ i 1))) (to_rep1 (select a (+ j 
+     (< (to_rep1 (select b (+ i 1))) (to_rep1 (select a (+ j
 1))))))))))))) :pattern (
   (compare a a_first a_last b b_first b_last)) ))))
 
@@ -306,17 +305,17 @@ i)) ))))
   (forall ((f Int) (l Int))
   (! (=> (in_range1 f)
      (=> (in_range1 l)
-     (and (= (to_rep (first (mk f l))) f) (= (to_rep (last (mk f l))) 
+     (and (= (to_rep (first (mk f l))) f) (= (to_rep (last (mk f l)))
 l)))) :pattern (
   (mk f l)) )))
 
 (define-fun dynamic_property ((range_first Int) (range_last Int) (low Int)
   (high Int)) Bool (and (in_range1 low)
                    (and (in_range1 high)
-                   (=> (<= low high) (and (in_range3 low) (in_range3 
+                   (=> (<= low high) (and (in_range3 low) (in_range3
 high))))))
 
-(declare-datatypes () ((us_t (mk___t (elts (Array Int natural))(rt t)))))
+(declare-datatypes ((us_t 0)) (((mk___t (elts (Array Int natural)) (rt t)))))
 (define-fun to_array ((a us_t)) (Array Int natural) (elts a))
 
 (define-fun of_array ((a (Array Int natural)) (f Int)
@@ -369,16 +368,16 @@ high))))))
 
 (declare-fun dummy3 () us_t)
 
-(declare-datatypes ()
-((nat_array__ref (mk_nat_array__ref (nat_array__content us_t)))))
-(define-fun nat_array__ref___projection ((a nat_array__ref)) us_t 
+(declare-datatypes ((nat_array__ref 0))
+(((mk_nat_array__ref (nat_array__content us_t)))))
+(define-fun nat_array__ref___projection ((a nat_array__ref)) us_t
 (nat_array__content
                                                                   a))
 
 (define-fun dynamic_invariant2 ((temp___expr_150 us_t)
   (temp___is_init_147 Bool) (temp___do_constant_148 Bool)
   (temp___do_toplevel_149 Bool)) Bool (=>
-                                      (not (= temp___do_constant_148 
+                                      (not (= temp___do_constant_148
 true))
                                       (dynamic_property 1 100
                                       (first1 temp___expr_150)
@@ -405,9 +404,9 @@ true))
 
 (declare-fun dummy4 () integer)
 
-(declare-datatypes () ((t15s__ref (mk_t15s__ref (t15s__content 
+(declare-datatypes ((t15s__ref 0)) (((mk_t15s__ref (t15s__content
 integer)))))
-(define-fun t15s__ref___projection ((a t15s__ref)) integer (t15s__content 
+(define-fun t15s__ref___projection ((a t15s__ref)) integer (t15s__content
 a))
 
 (declare-sort t1 0)
@@ -423,11 +422,11 @@ a))
   (forall ((f Int) (l Int))
   (! (=> (in_range1 f)
      (=> (in_range1 l)
-     (and (= (to_rep (first3 (mk1 f l))) f) (= (to_rep (last3 (mk1 f l))) 
+     (and (= (to_rep (first3 (mk1 f l))) f) (= (to_rep (last3 (mk1 f l)))
 l)))) :pattern (
   (mk1 f l)) )))
 
-(define-fun dynamic_property2 ((range_first Int) (range_last Int) (low 
+(define-fun dynamic_property2 ((range_first Int) (range_last Int) (low
 Int)
   (high Int)) Bool (and (in_range1 low)
                    (and (in_range1 high)
@@ -435,8 +434,8 @@ Int)
                    (and (dynamic_property1 range_first range_last low)
                    (dynamic_property1 range_first range_last high))))))
 
-(declare-datatypes ()
-((us_t1 (mk___t1 (elts1 (Array Int natural))(rt1 t1)))))
+(declare-datatypes ((us_t1 0))
+(((mk___t1 (elts1 (Array Int natural)) (rt1 t1)))))
 (define-fun to_array1 ((a us_t1)) (Array Int natural) (elts1 a))
 
 (define-fun of_array1 ((a (Array Int natural)) (f Int)
@@ -478,7 +477,7 @@ Int)
   (assert (<= 0 value__alignment1))
 
 ;; object__alignment_axiom
-  (assert (forall ((a (Array Int natural))) (<= 0 (object__alignment1 
+  (assert (forall ((a (Array Int natural))) (<= 0 (object__alignment1
 a))))
 
 (define-fun bool_eq6 ((x us_t1)
@@ -490,8 +489,8 @@ a))))
 
 (declare-fun dummy5 () us_t1)
 
-(declare-datatypes () ((t16s__ref (mk_t16s__ref (t16s__content us_t1)))))
-(define-fun t16s__ref___projection ((a t16s__ref)) us_t1 (t16s__content 
+(declare-datatypes ((t16s__ref 0)) (((mk_t16s__ref (t16s__content us_t1)))))
+(define-fun t16s__ref___projection ((a t16s__ref)) us_t1 (t16s__content
 a))
 
 ;; remove_last__post_axiom
@@ -505,15 +504,15 @@ a))
   (assert
   (forall ((a us_t))
   (! (=> (dynamic_invariant2 a true true true)
-     (= (remove_last a) (let ((temp___163 (let ((temp___162 (- (last1 a) 
+     (= (remove_last a) (let ((temp___163 (let ((temp___162 (- (last1 a)
 1)))
                                           (let ((temp___161 (first1 a)))
-                                          (of_array1 (to_array a) 
+                                          (of_array1 (to_array a)
 temp___161
                                           temp___162)))))
-                        (of_array (to_array1 temp___163) (first4 
+                        (of_array (to_array1 temp___163) (first4
 temp___163)
-                        (last4 temp___163))))) :pattern ((remove_last a)) 
+                        (last4 temp___163))))) :pattern ((remove_last a))
 )))
 
 (declare-fun occ (us_t Int) Int)
@@ -545,19 +544,19 @@ temp___163)
 
 ;; range_axiom
   (assert
-  (forall ((x nb_occ)) (! (in_range4 (to_rep3 x)) :pattern ((to_rep3 x)) 
+  (forall ((x nb_occ)) (! (in_range4 (to_rep3 x)) :pattern ((to_rep3 x))
 )))
 
 ;; coerce_axiom
   (assert
   (forall ((x Int))
   (! (=> (in_range4 x) (= (to_rep3 (of_rep3 x)) x)) :pattern ((to_rep3
-                                                              (of_rep3 
+                                                              (of_rep3
 x))) )))
 
-(declare-datatypes ()
-((nb_occ__ref (mk_nb_occ__ref (nb_occ__content nb_occ)))))
-(define-fun nb_occ__ref___projection ((a nb_occ__ref)) nb_occ 
+(declare-datatypes ((nb_occ__ref 0))
+(((mk_nb_occ__ref (nb_occ__content nb_occ)))))
+(define-fun nb_occ__ref___projection ((a nb_occ__ref)) nb_occ
 (nb_occ__content
                                                               a))
 
@@ -576,7 +575,7 @@ x))) )))
   (forall ((e Int))
   (! (=> (and (dynamic_invariant2 a true true true) (in_range2 e))
      (let ((result (occ a e)))
-     (and (<= result (length a)) (dynamic_invariant3 result true false 
+     (and (<= result (length a)) (dynamic_invariant3 result true false
 true)))) :pattern (
   (occ a e)) ))))
 
@@ -600,7 +599,7 @@ true)))) :pattern (
      (forall ((j Int))
      (=> (and (<= (first1 a) j) (<= j (last1 a)))
      (=> (not (= i j))
-     (= (to_rep1 (select (to_array r) j)) (to_rep1 (select (to_array a) 
+     (= (to_rep1 (select (to_array r) j)) (to_rep1 (select (to_array a)
 j)))))))) :pattern (
   (is_set a i v r)) ))))
 
@@ -630,7 +629,7 @@ j)))))))) :pattern (
 
 (declare-fun attr__ATTRIBUTE_ADDRESS5 () Int)
 
-(define-fun dynamic_invariant4 ((temp___expr_15 Int) (temp___is_init_12 
+(define-fun dynamic_invariant4 ((temp___expr_15 Int) (temp___is_init_12
 Bool)
   (temp___do_constant_13 Bool)
   (temp___do_toplevel_14 Bool)) Bool (=>
@@ -644,12 +643,12 @@ Bool)
   (forall ((e1 Int))
   (! (=> (and (dynamic_invariant2 a1 true true true) (in_range2 e1))
      (= (occ_def a1 e1) (ite (= (length a1) 0) 0
-                        (ite (= (to_rep1 (select (to_array a1) (last1 
+                        (ite (= (to_rep1 (select (to_array a1) (last1
 a1))) e1)
                         (+ (occ_def (remove_last a1) e1) 1)
-                        (occ_def (remove_last a1) e1))))) :pattern 
+                        (occ_def (remove_last a1) e1))))) :pattern
 ((occ_def
-                                                                    a1 
+                                                                    a1
 e1)) ))))
 
 (declare-fun b () (Array Int natural))
@@ -721,7 +720,7 @@ e1)) ))))
   (assert (= b1 perm__occ_set__b__assume))
 
 ;; H
-  (assert (= (to_rep b__first) (to_rep (first 
+  (assert (= (to_rep b__first) (to_rep (first
 perm__occ_set__b__assume1))))
 
 ;; H
@@ -774,4 +773,3 @@ perm__occ_set__b__assume1))))
      (to_rep (first (mk (to_rep b__first) (to_rep b__last))))
      (to_rep (last (mk (to_rep b__first) (to_rep b__last))))) true)))
 (check-sat)
-
diff --git a/test/regress/regress1/quantifiers/cdt-0208-to.smt2 b/test/regress/regress1/quantifiers/cdt-0208-to.smt2
index 9eff608bb..8f0312616 100644
--- a/test/regress/regress1/quantifiers/cdt-0208-to.smt2
+++ b/test/regress/regress1/quantifiers/cdt-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --full-saturate-quant --lang=smt2.5
+; COMMAND-LINE: --full-saturate-quant
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
@@ -102,11 +102,12 @@
 (declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$ 0)
 (declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
 (declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
-(declare-codatatypes () ((A_llist$ (lNil$) (lCons$ (lhd$ A$) (ltl$ A_llist$)))))
-(declare-datatypes () ((A_llist_a_llist_prod$ (pair$ (fst$ A_llist$) (snd$ A_llist$)))))
-(declare-codatatypes () ((A_llist_a_llist_prod_llist$ (lNil$a) (lCons$a (lhd$a A_llist_a_llist_prod$) (ltl$a A_llist_a_llist_prod_llist$)))))
-(declare-datatypes () ((A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod$ (pair$a (fst$a A_llist_a_llist_prod_llist$) (snd$a A_llist_a_llist_prod_llist$)))
-  (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$ (pair$b (fst$b A_llist_a_llist_prod$) (snd$b A_llist_a_llist_prod$)))))
+(declare-codatatypes ((A_llist$ 0)) (((lNil$) (lCons$ (lhd$ A$) (ltl$ A_llist$)))))
+(declare-datatypes ((A_llist_a_llist_prod$ 0)) (((pair$ (fst$ A_llist$) (snd$ A_llist$)))))
+(declare-codatatypes ((A_llist_a_llist_prod_llist$ 0)) (((lNil$a) (lCons$a (lhd$a A_llist_a_llist_prod$) (ltl$a A_llist_a_llist_prod_llist$)))))
+(declare-datatypes ((A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod$ 0) (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$ 0)) (
+  ((pair$a (fst$a A_llist_a_llist_prod_llist$) (snd$a A_llist_a_llist_prod_llist$)))
+  ((pair$b (fst$b A_llist_a_llist_prod$) (snd$b A_llist_a_llist_prod$)))))
 (declare-fun p$ () A_llist_a_llist_bool_fun_fun$)
 (declare-fun uu$ (Bool) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
 (declare-fun xs$ () A_llist$)
diff --git a/test/regress/regress1/quantifiers/parametric-lists.smt2 b/test/regress/regress1/quantifiers/parametric-lists.smt2
index c45152d6f..f236c1ec7 100644
--- a/test/regress/regress1/quantifiers/parametric-lists.smt2
+++ b/test/regress/regress1/quantifiers/parametric-lists.smt2
@@ -1,9 +1,8 @@
-; COMMAND-LINE: --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
-(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil))))
-(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair
+(declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil)))))
+(declare-datatypes ((KV 0)) (((kv (key Int) (value Int)) (nilKV))))
 (declare-fun mapper ((List Int)) (List KV))
 (assert
   (forall
@@ -13,7 +12,7 @@
         (= (as nil (List KV)) (mapper input))
         (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input))
      )
-  )                                                                                                                            
+  )
 )
 (declare-fun reduce ((List KV)) Int)
 (assert
@@ -41,4 +40,3 @@
   (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int)))))))
 )
 (check-sat)
-
diff --git a/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2
index 9243654b4..fe593e8c0 100644
--- a/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2
+++ b/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
@@ -28,13 +27,14 @@
 (declare-sort B_stream_stream_b_stream_stream_fun$ 0)
 (declare-sort A_stream_stream_stream_a_stream_stream_stream_fun$ 0)
 (declare-sort B_stream_stream_stream_b_stream_stream_stream_fun$ 0)
-(declare-datatypes () ((Nat$ (zero$) (suc$ (pred$ Nat$)))))
-(declare-codatatypes () ((A_stream$ (sCons$ (shd$ A$) (stl$ A_stream$)))
-  (B_stream$ (sCons$a (shd$a B$) (stl$a B_stream$)))
-  (B_stream_stream$ (sCons$b (shd$b B_stream$) (stl$b B_stream_stream$)))
-  (B_stream_stream_stream$ (sCons$c (shd$c B_stream_stream$) (stl$c B_stream_stream_stream$)))
-  (A_stream_stream$ (sCons$d (shd$d A_stream$) (stl$d A_stream_stream$)))
-  (A_stream_stream_stream$ (sCons$e (shd$e A_stream_stream$) (stl$e A_stream_stream_stream$)))))
+(declare-datatypes ((Nat$ 0)) (((zero$) (suc$ (pred$ Nat$)))))
+(declare-codatatypes ((A_stream$ 0) (B_stream$ 0) (B_stream_stream$ 0) (B_stream_stream_stream$ 0) (A_stream_stream$ 0) (A_stream_stream_stream$ 0)) (
+  ((sCons$ (shd$ A$) (stl$ A_stream$)))
+  ((sCons$a (shd$a B$) (stl$a B_stream$)))
+  ((sCons$b (shd$b B_stream$) (stl$b B_stream_stream$)))
+  ((sCons$c (shd$c B_stream_stream$) (stl$c B_stream_stream_stream$)))
+  ((sCons$d (shd$d A_stream$) (stl$d A_stream_stream$)))
+  ((sCons$e (shd$e A_stream_stream$) (stl$e A_stream_stream_stream$)))))
 (declare-fun f$ () B_a_fun$)
 (declare-fun x$ () B$)
 (declare-fun id$ () B_b_fun$)
diff --git a/test/regress/regress1/quantifiers/subtype-param-unk.smt2 b/test/regress/regress1/quantifiers/subtype-param-unk.smt2
index f3ee6a86a..1828a68b2 100644
--- a/test/regress/regress1/quantifiers/subtype-param-unk.smt2
+++ b/test/regress/regress1/quantifiers/subtype-param-unk.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --lang=smt2.5
 ; EXPECT: (error "argument type is not a subtype of the function's argument type:
 ; EXPECT: argument:  x
 ; EXPECT: has type:  (List Int)
@@ -9,7 +8,7 @@
 ; this will fail if type rule for APPLY_UF requires arguments to be subtypes
 (set-logic ALL_SUPPORTED)
 
-(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+(declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil)))))
 
 (declare-fun R ((List Real)) Bool)
 (assert (forall ((x (List Int))) (R x)))
diff --git a/test/regress/regress1/quantifiers/subtype-param.smt2 b/test/regress/regress1/quantifiers/subtype-param.smt2
index 860c03b6f..c4cdfb244 100644
--- a/test/regress/regress1/quantifiers/subtype-param.smt2
+++ b/test/regress/regress1/quantifiers/subtype-param.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --lang=smt2.5
 ; EXPECT: (error "argument type is not a subtype of the function's argument type:
 ; EXPECT: argument:  x
 ; EXPECT: has type:  (Array Int Int)
@@ -9,7 +8,7 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 
-(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+(declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil)))))
 
 (declare-fun R ((List Real)) Bool)
 (assert (forall ((x (List Real))) (R x)))