Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.

86 files changed, 143 insertions, 111 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 697ce6642..2a9202898 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -162,7 +162,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     } else {
       unsigned len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.setInputLanguage(language::input::LANG_SMTLIB_V2_5);
+        opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
         opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
diff --git a/src/options/language.cpp b/src/options/language.cpp
index bbb95f258..86beffd6d 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -114,16 +114,16 @@ InputLanguage toInputLanguage(std::string language) {
   } else if(language == "smtlib1" || language == "smt1" ||
             language == "LANG_SMTLIB_V1") {
     return input::LANG_SMTLIB_V1;
-  } else if(language == "smtlib" || language == "smt" ||
-            language == "smtlib2" || language == "smt2" ||
-            language == "smtlib2.0" || language == "smt2.0" ||
-            language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") {
+  } else if(language == "smtlib2.0" || language == "smt2.0" ||
+            language == "LANG_SMTLIB_V2_0") {
     return input::LANG_SMTLIB_V2_0;
   } else if(language == "smtlib2.5" || language == "smt2.5" ||
             language == "LANG_SMTLIB_V2_5") {
     return input::LANG_SMTLIB_V2_5;
-  } else if(language == "smtlib2.6" || language == "smt2.6" ||
-            language == "LANG_SMTLIB_V2_6") {
+  } else if(language == "smtlib" || language == "smt" ||
+            language == "smtlib2" || language == "smt2" ||
+            language == "smtlib2.6" || language == "smt2.6" ||
+            language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") {
     return input::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c7156635d..86c0b3126 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -3036,15 +3036,15 @@ AS_TOK : 'as';
 CONST_TOK : 'const';
 
 // extended commands
-DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-codatatype';
-DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-datatype';
-DECLARE_DATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-datatypes';
-DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-datatypes';
-DECLARE_CODATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-codatatypes';
-DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-codatatypes';
+DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
+DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype';
+DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes';
+DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
+DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
+DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
 PAR_TOK : { PARSER_STATE->v2_6() }?'par';
-TESTER_TOK : { PARSER_STATE->v2_6() && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
-MATCH_TOK : { PARSER_STATE->v2_6() && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
+TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
+MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
 GET_MODEL_TOK : 'get-model';
 ECHO_TOK : 'echo';
 REWRITE_RULE_TOK : 'assert-rewrite';
diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2
index d5df938a7..2046f4911 100644
--- a/test/regress/regress0/arith/bug716.0.smt2
+++ b/test/regress/regress0/arith/bug716.0.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --lang=smt2.5
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
diff --git a/test/regress/regress0/bug296.smt2 b/test/regress/regress0/bug296.smt2
index 92e540966..3aea7e9c9 100644
--- a/test/regress/regress0/bug296.smt2
+++ b/test/regress/regress0/bug296.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic QF_ALL)
 (set-info :status unsat)
 (declare-datatypes
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2
index 3c73e261c..87a8696b6 100644
--- a/test/regress/regress0/bug484.smt2
+++ b/test/regress/regress0/bug484.smt2
@@ -1,3 +1,6 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+
 ; Preamble  --------------
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress0/bug507.smt2 b/test/regress/regress0/bug507.smt2
index 75a63e328..a20dddfe7 100644
--- a/test/regress/regress0/bug507.smt2
+++ b/test/regress/regress0/bug507.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/bug541.smt2 b/test/regress/regress0/bug541.smt2
index 482823985..771fbed4f 100644
--- a/test/regress/regress0/bug541.smt2
+++ b/test/regress/regress0/bug541.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2
index 37403d8a3..99d7f0302 100644
--- a/test/regress/regress0/bug567.smt2
+++ b/test/regress/regress0/bug567.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL_SUPPORTED)
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --lang=smt2.5
 ; EXPECT: unknown
 ; EXPECT: unsat
 ; EXPECT: unknown
diff --git a/test/regress/regress0/bug681.smt2 b/test/regress/regress0/bug681.smt2
index cc54ab4c2..93d7b88c4 100644
--- a/test/regress/regress0/bug681.smt2
+++ b/test/regress/regress0/bug681.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --lang=smt2.5
 ; EXIT: 1
 ; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/datatypes/bug597-rbt.smt2 b/test/regress/regress0/datatypes/bug597-rbt.smt2
index 45d82a522..078fa59f7 100644
--- a/test/regress/regress0/datatypes/bug597-rbt.smt2
+++ b/test/regress/regress0/datatypes/bug597-rbt.smt2
@@ -2,7 +2,7 @@
 (set-info :status sat)
 
 ; Tree type
-(declare-datatypes () ((Tree (node (data Int) (color Bool) (left Tree) (right Tree)) (nil))))
+(declare-datatypes ((Tree 0)) (((node (data Int) (color Bool) (left Tree) (right Tree)) (nil))))
 
 ; content function
 (declare-fun size (Tree) Int)
diff --git a/test/regress/regress0/datatypes/bug604.smt2 b/test/regress/regress0/datatypes/bug604.smt2
index 15a60c3e3..dfd11001d 100644
--- a/test/regress/regress0/datatypes/bug604.smt2
+++ b/test/regress/regress0/datatypes/bug604.smt2
@@ -1,9 +1,9 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
-(declare-datatypes () ( (PairIntInt (pair (firstPairIntInt Int)
+(declare-datatypes ((PairIntInt 0)) ( ( (pair (firstPairIntInt Int)
 (secondPairIntInt Int)) ) ))
 (declare-fun /ArrayIntOfPair () (Array Int PairIntInt))
-(declare-datatypes () ( (SequenceABC (sequenceABC (a Int) (b Bool) (c Int)) )
+(declare-datatypes ((SequenceABC 0)) ( ( (sequenceABC (a Int) (b Bool) (c Int)) )
 ))
 (declare-fun /ArrayIntOfSequenceABC () (Array Int SequenceABC))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/bug625.smt2 b/test/regress/regress0/datatypes/bug625.smt2
index 3f4312ad4..1e9a18d9d 100644
--- a/test/regress/regress0/datatypes/bug625.smt2
+++ b/test/regress/regress0/datatypes/bug625.smt2
@@ -4,10 +4,10 @@
 (declare-fun x2 () Int)
 (declare-fun y1 () Int)
 (declare-fun y2 () Int)
-(declare-datatypes () ( (type
+(declare-datatypes ((type 0)) ( (
     (constructor1 (f1 Int))
     (constructor2 (f2 Int))
 )))
 (define-fun mktest ((constructor Int) (p1 Int) (p2 Int)) type (ite (= constructor 1) (constructor1 p1) (constructor2 p2)))
 (assert (distinct (mktest x1 x2 x2) (mktest y1 y2 y2)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 b/test/regress/regress0/datatypes/cdt-model-cade15.smt2
index c23a9d594..8ddf7c52a 100644
--- a/test/regress/regress0/datatypes/cdt-model-cade15.smt2
+++ b/test/regress/regress0/datatypes/cdt-model-cade15.smt2
@@ -1,6 +1,6 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
-(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))
+(declare-codatatypes ((Stream 0)) (((C (c Stream)) (D (d Stream)) (E (e Stream)))))
 
 (declare-const z Stream)
 (declare-const x Stream)
@@ -14,4 +14,4 @@
 (assert (= w (E y)))
 (assert (= x (C v)))
 (assert (distinct x y z u v w))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 b/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2
index 4a111b41b..0741b0ff0 100644
--- a/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2
+++ b/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2
@@ -1,6 +1,6 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
-(declare-codatatypes () ((list (cons (head Int) (tail list)))))
+(declare-codatatypes ((list 0)) (((cons (head Int) (tail list)))))
 
 (declare-fun x () list)
 (declare-fun y () list)
diff --git a/test/regress/regress0/datatypes/coda_simp_model.smt2 b/test/regress/regress0/datatypes/coda_simp_model.smt2
index 1e000cecd..3c30021b0 100644
--- a/test/regress/regress0/datatypes/coda_simp_model.smt2
+++ b/test/regress/regress0/datatypes/coda_simp_model.smt2
@@ -2,11 +2,11 @@
 (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 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
+(check-sat)
diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
index 6f82cd842..74b836b47 100644
--- a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
+++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun start!13 () Bool)
diff --git a/test/regress/regress0/datatypes/dt-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-param-2.6.smt2
index a132ce8fc..f6d1cd58d 100644
--- a/test/regress/regress0/datatypes/dt-param-2.6.smt2
+++ b/test/regress/regress0/datatypes/dt-param-2.6.smt2
@@ -1,8 +1,6 @@
-; COMMAND-LINE: --lang=smt2.6
-; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
-(declare-datatypes ( ( Tree 1) ( TreeList 1) ) (
+(declare-datatypes ( (Tree 1) (TreeList 1) ) (
 (par ( X ) ( ( node ( value X ) ( children ( TreeList X )) )))
 (par ( Y ) ( ( empty ) ( insert ( head ( Tree Y )) ( tail ( TreeList Y ))) ))
 ))
diff --git a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
index ca5791ce2..7a0fa30c7 100644
--- a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
+++ b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
diff --git a/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
index 9676745b4..d403cf4ee 100644
--- a/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
+++ b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
diff --git a/test/regress/regress0/datatypes/example-dailler-min.smt2 b/test/regress/regress0/datatypes/example-dailler-min.smt2
index 1698fc3b0..5702cb04b 100644
--- a/test/regress/regress0/datatypes/example-dailler-min.smt2
+++ b/test/regress/regress0/datatypes/example-dailler-min.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-datatypes () ((D (C (R Bool)))))
diff --git a/test/regress/regress0/datatypes/is_test.smt2 b/test/regress/regress0/datatypes/is_test.smt2
index 9c38ffcc8..f13a4f21f 100644
--- a/test/regress/regress0/datatypes/is_test.smt2
+++ b/test/regress/regress0/datatypes/is_test.smt2
@@ -1,6 +1,6 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
-(declare-datatypes () ((Unit (u))))
+(declare-datatypes ((Unit 0)) (((u))))
 (declare-fun x () Unit)
 (assert (not (is-u x)))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/jsat-2.6.smt2 b/test/regress/regress0/datatypes/jsat-2.6.smt2
index 7e7fe4f49..652866136 100644
--- a/test/regress/regress0/datatypes/jsat-2.6.smt2
+++ b/test/regress/regress0/datatypes/jsat-2.6.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --lang=smt2.6
-; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2
index 5d028d723..a4d5ff0ec 100644
--- a/test/regress/regress0/datatypes/pair-real-bool.smt2
+++ b/test/regress/regress0/datatypes/pair-real-bool.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
 ;(set-option :produce-models true)
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/datatypes/sc-cdt1.smt2 b/test/regress/regress0/datatypes/sc-cdt1.smt2
index 672acfa44..3c88c49c0 100644
--- a/test/regress/regress0/datatypes/sc-cdt1.smt2
+++ b/test/regress/regress0/datatypes/sc-cdt1.smt2
@@ -1,11 +1,11 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (declare-sort term 0)
-(declare-codatatypes () (
-    (llist_tree (lnil_tree )
+(declare-codatatypes ((llist_tree 0) (tree 0)) (
+    ( (lnil_tree )
         (lcons_tree (_select_llist_tree_0 tree)
         (_select_llist_tree_1 llist_tree)))
-    (tree (leaf (_select_tree_0 term))
+    ((leaf (_select_tree_0 term))
         (node (_select_tree_1 llist_tree)))
 ))
 (declare-fun nun_sk_2 () term)
@@ -16,4 +16,4 @@
         (node
          (lcons_tree (leaf nun_sk_1)
           (lcons_tree (leaf nun_sk_2) (lcons_tree nun_sk_0 lnil_tree))))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/datatypes/stream-singleton.smt2 b/test/regress/regress0/datatypes/stream-singleton.smt2
index 6884059ca..95d5f0c81 100644
--- a/test/regress/regress0/datatypes/stream-singleton.smt2
+++ b/test/regress/regress0/datatypes/stream-singleton.smt2
@@ -1,11 +1,11 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
-(declare-codatatypes () ((Stream (S (s Stream)))))
+(declare-codatatypes ((Stream 0)) (((S (s Stream)))))
 
 (declare-fun x () Stream)
 (declare-fun y () Stream)
 
 (assert (not (= x y)))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/datatypes/tenum-bug.smt2 b/test/regress/regress0/datatypes/tenum-bug.smt2
index bf82c7b8c..6d25aefd0 100644
--- a/test/regress/regress0/datatypes/tenum-bug.smt2
+++ b/test/regress/regress0/datatypes/tenum-bug.smt2
@@ -1,11 +1,11 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
-(declare-datatypes () ((DNat (dnat (data Nat)))
-                       (Nat (succ (pred DNat)) (zero))))
+(declare-datatypes ((DNat 0) (Nat 0)) (((dnat (data Nat)))
+                                       ((succ (pred DNat)) (zero))))
 
 (declare-fun x () Nat)
 
 (assert (not (= x zero)))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
index 9ef5f14fa..a58e85c0d 100644
--- a/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
+++ b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/agree466.smt2 b/test/regress/regress0/fmf/agree466.smt2
index bfe48195b..d17a663c6 100644
--- a/test/regress/regress0/fmf/agree466.smt2
+++ b/test/regress/regress0/fmf/agree466.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: sat
 ; Preamble  --------------
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/fmf/agree467.smt2 b/test/regress/regress0/fmf/agree467.smt2
index 1bfdb9f83..07180cf4f 100644
--- a/test/regress/regress0/fmf/agree467.smt2
+++ b/test/regress/regress0/fmf/agree467.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: unsat
 ; Preamble  --------------
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/fmf/bug0909.smt2 b/test/regress/regress0/fmf/bug0909.smt2
index 9577e8f57..fc3054c0d 100644
--- a/test/regress/regress0/fmf/bug0909.smt2
+++ b/test/regress/regress0/fmf/bug0909.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: unsat
 ; Preamble  --------------
 (set-option :produce-models true)
@@ -51,4 +51,4 @@
     
     (= (ite (= (x38 (select x62 x63)) x3) (ite (and (=> (= (x40 (select x62 x63)) x69) (=> (= (x41 (select x62 x63)) x71) (=> (= x65 (store x67 x71 (d53 (x46 (x43 (select x62 x63)))))) (=> (= x70 (store x62 x63 (let ((x77 (select x62 x63))) (x44 (x38 x77) (x39 x77) (x40 x77) (x41 x77) (x42 x77) x32)))) (=> (= x68 (store x70 x63 (let ((x78 (select x70 x63))) (x44 x4 (x39 x78) (x40 x78) (x41 x78) (x42 x78) (x43 x78)))))
     (=> (= (store x65 x69 (x51 (let ((x82 (ite (is-x49 (select x65 x69)) (let ((x79 (x48 (select x65 x69)))) (x57 x79)) (ite (is-x51 (select x65 x69)) (let ((x80 (x50 (select x65 x69)))) x80) (let ((x81 (s52 (select x65 x69)))) (x58 x81)))))) (x28 x4 x3 (x25 x82) (x26 x82) (+ (x27 (ite (is-x49 (select x65 x69)) (let ((x83 (x48 (select x65 x69)))) (x57 x83)) (ite (is-x51 (select x65 x69)) (let ((x84 (x50 (select x65 x69)))) x84) (let ((x85 (s52 (select x65 x69)))) (x58 x85))))) 1))))) x64) (forall ((x86 x6)) (=> (and (= x3 (x7 x86)) (= x3 (select x61 x86)) (= (select x66 x86) x16)) (= (ite (is-d53 (select x64 x86)) x3 x4) x3))))))))) (= x3 (x38 (select x62 x63)))) x3 x4) (ite (forall ((x87 x6)) (=> (and (= x3 (select x61 x87)) (= x3 (x7 x87)) (= x16 (select x66 x87))) (= x3 (ite (is-d53 (select x67 x87)) x3 x4)))) x3 x4)) x3))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/bug651.smt2 b/test/regress/regress0/fmf/bug651.smt2
index 9afc47972..bcfeebd69 100644
--- a/test/regress/regress0/fmf/bug651.smt2
+++ b/test/regress/regress0/fmf/bug651.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun --no-check-models --lang=smt2.5
 ; EXPECT: sat
 (set-logic UFDTSLIA)
 (set-info :smt-lib-version 2.5)
diff --git a/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2
index 1a27bf170..e9b748744 100644
--- a/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2
+++ b/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --fmf-fun-rlv --no-check-models --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (define-fun $$isTrue$$ ((b Bool)) Bool b)
diff --git a/test/regress/regress0/fmf/bug764.smt2 b/test/regress/regress0/fmf/bug764.smt2
index d030c3e88..3172fd695 100644
--- a/test/regress/regress0/fmf/bug764.smt2
+++ b/test/regress/regress0/fmf/bug764.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun --no-check-models --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/cons-sets-bounds.smt2 b/test/regress/regress0/fmf/cons-sets-bounds.smt2
index db9788a61..5e3c2952b 100644
--- a/test/regress/regress0/fmf/cons-sets-bounds.smt2
+++ b/test/regress/regress0/fmf/cons-sets-bounds.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --fmf-bound
 ; EXPECT: sat
 (set-logic ALL)
-(declare-datatypes () ((list (cons (head Int) (tail list)) (nil))))
+(declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil))))
 
 (declare-fun P (Int) Bool)
 (declare-fun S () (Set list))
@@ -14,7 +14,7 @@
 
 ; should construct instantiation involving selectors for l 
 (declare-fun l () list)
-(assert (is-cons l))
+(assert ((_ is cons) l))
 (assert (member l S))
 
 ; should not contribute to instantiations
diff --git a/test/regress/regress0/fmf/constr-ground-to.smt2 b/test/regress/regress0/fmf/constr-ground-to.smt2
index c8f6c1d71..bc6d9e948 100644
--- a/test/regress/regress0/fmf/constr-ground-to.smt2
+++ b/test/regress/regress0/fmf/constr-ground-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun
+; COMMAND-LINE: --fmf-fun --lang=smt2.5
 ; EXPECT: sat
 (set-logic UFDTLIA)
 (declare-datatypes () (
diff --git a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
index 3ffc36d05..6b30907ae 100644
--- a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
+++ b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
@@ -8,7 +8,7 @@
 (declare-fun d () U)
 (assert (distinct a b c))
 (declare-sort V 0)
-(declare-datatypes () ((ufin1 (cons1 (s11 U) (s13 ufin2))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-datatypes ((ufin1 0) (ufin2 0)) (((cons1 (s11 U) (s13 ufin2))) ((cons2 (s21 V) (s22 U)) (cons3))))
 (declare-fun P (ufin1 ufin2) Bool)
 (declare-fun Q (ufin1 ufin1) Bool)
 (assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2
index 3564bff8b..a19c8f027 100644
--- a/test/regress/regress0/fmf/datatypes-ufinite.smt2
+++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort U 0)
diff --git a/test/regress/regress0/fmf/dt-proper-model.smt2 b/test/regress/regress0/fmf/dt-proper-model.smt2
index 60a0b6377..0e66db996 100644
--- a/test/regress/regress0/fmf/dt-proper-model.smt2
+++ b/test/regress/regress0/fmf/dt-proper-model.smt2
@@ -3,7 +3,7 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (declare-sort U 0)
-(declare-datatypes () ((D (cons (x Int) (y U)))))
+(declare-datatypes ((D 0)) (((cons (x Int) (y U)))))
 (declare-fun d1 () D)
 (declare-fun d2 () D)
 (declare-fun d3 () D)
@@ -13,4 +13,4 @@
 (declare-fun a () U)
 (declare-fun P (U) Bool)
 (assert (P a))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2
index 813f89732..e4e1f65b4 100644
--- a/test/regress/regress0/fmf/fmc_unsound_model.smt2
+++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2
@@ -4,7 +4,7 @@
 (set-logic ALL_SUPPORTED)
 
 (declare-sort a 0)
-(declare-datatypes () ((tree (Leaf (lab a)))))
+(declare-datatypes ((tree 0)) (((Leaf (lab a)))))
 
 (declare-sort alpha 0)
 (declare-fun alphabet (tree a) Bool)
diff --git a/test/regress/regress0/fmf/forall_unit_data2.smt2 b/test/regress/regress0/fmf/forall_unit_data2.smt2
index 64847d6d2..88f2631c5 100644
--- a/test/regress/regress0/fmf/forall_unit_data2.smt2
+++ b/test/regress/regress0/fmf/forall_unit_data2.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (declare-sort a 0)
-(declare-datatypes () ((prod (Pair (gx a) (gy a)))))
+(declare-datatypes ((prod 0)) (((Pair (gx a) (gy a)))))
 (declare-fun p () prod)
 (assert (forall ((x a) (y a)) (not (= p (Pair x y)))))
 (check-sat)
diff --git a/test/regress/regress0/fmf/fore19-exp2-core.smt2 b/test/regress/regress0/fmf/fore19-exp2-core.smt2
index 9a6e1e270..4b4d57af3 100644
--- a/test/regress/regress0/fmf/fore19-exp2-core.smt2
+++ b/test/regress/regress0/fmf/fore19-exp2-core.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-datatypes () ((St (Block!2236 (body!2237 List!2293)) (For!2238 (init!2239 St) (expr!2240 Ex) (step!2241 St) (body!2242 St)) (IfTE (expr!2244 Ex) (then!2245 St) (elze!2246 St)) (Skip!2250) (While (expr!2252 Ex) (body St)))
diff --git a/test/regress/regress0/fmf/german169.smt2 b/test/regress/regress0/fmf/german169.smt2
index 3558715a8..c88de064c 100644
--- a/test/regress/regress0/fmf/german169.smt2
+++ b/test/regress/regress0/fmf/german169.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/german73.smt2 b/test/regress/regress0/fmf/german73.smt2
index e1d499972..64f551d55 100644
--- a/test/regress/regress0/fmf/german73.smt2
+++ b/test/regress/regress0/fmf/german73.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
diff --git a/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2
index 1f7214232..7012838f9 100644
--- a/test/regress/regress0/fmf/jasmin-cdt-crash.smt2
+++ b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/krs-sat.smt2 b/test/regress/regress0/fmf/krs-sat.smt2
index 22d9e4474..17c6d9748 100644
--- a/test/regress/regress0/fmf/krs-sat.smt2
+++ b/test/regress/regress0/fmf/krs-sat.smt2
@@ -7,10 +7,10 @@
 (declare-fun cowlThing ($$unsorted) Bool)
 (declare-fun xsd_integer ($$unsorted) Bool)
 (declare-fun xsd_string ($$unsorted) Bool)
-(declare-fun is () $$unsorted)
+(declare-fun _is () $$unsorted)
 (assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) )))
 (assert (forall ((X $$unsorted)) (= (xsd_string X) (not (xsd_integer X))) ))
-(assert (and (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) ) (cowlThing is)))
-(assert (cowlThing is))
-(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ) (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) )))
+(assert (and (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X _is)) ) (cowlThing _is)))
+(assert (cowlThing _is))
+(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ) (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X _is)) )))
 (check-sat)
diff --git a/test/regress/regress0/fmf/loopy_coda.smt2 b/test/regress/regress0/fmf/loopy_coda.smt2
index 7c1d30886..519fb17fc 100644
--- a/test/regress/regress0/fmf/loopy_coda.smt2
+++ b/test/regress/regress0/fmf/loopy_coda.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2
index 5e1f3de30..d55e15925 100644
--- a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2
+++ b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel --lang=smt2.5
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil))))
diff --git a/test/regress/regress0/fmf/nun-0208-to.smt2 b/test/regress/regress0/fmf/nun-0208-to.smt2
index f831af1f2..e6b3c2021 100644
--- a/test/regress/regress0/fmf/nun-0208-to.smt2
+++ b/test/regress/regress0/fmf/nun-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: sat
   (set-logic ALL_SUPPORTED)
   (declare-sort b__ 0)
diff --git a/test/regress/regress0/fmf/sc-crash-052316.smt2 b/test/regress/regress0/fmf/sc-crash-052316.smt2
index 2fc86cbed..345d8220e 100644
--- a/test/regress/regress0/fmf/sc-crash-052316.smt2
+++ b/test/regress/regress0/fmf/sc-crash-052316.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: unsat
   (set-logic ALL_SUPPORTED)
   (set-info :status unsat)
diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
index a083e418d..68a4399ca 100644
--- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2
+++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 ; EXPECT: sat
   (set-logic ALL_SUPPORTED)
   (set-info :status sat)
diff --git a/test/regress/regress0/fmf/tail_rec.smt2 b/test/regress/regress0/fmf/tail_rec.smt2
index 87b2d53a6..2651db3f2 100644
--- a/test/regress/regress0/fmf/tail_rec.smt2
+++ b/test/regress/regress0/fmf/tail_rec.smt2
@@ -2,9 +2,9 @@
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort elem 0)
-(declare-datatypes () ((list (Nil) (Cons (hd elem) (tl list)))))
+(declare-datatypes ((list 0)) (((Nil) (Cons (hd elem) (tl list)))))
 (define-fun-rec f ((x list)) elem
-  (ite (is-Nil x) (f x) (hd x))
+  (ite ((_ is Nil) x) (f x) (hd x))
 )
 (declare-fun t () elem)
 (assert (= t (f Nil)))
diff --git a/test/regress/regress0/fmf/with-ind-104-core.smt2 b/test/regress/regress0/fmf/with-ind-104-core.smt2
index a2e3a9ed0..c1d718403 100644
--- a/test/regress/regress0/fmf/with-ind-104-core.smt2
+++ b/test/regress/regress0/fmf/with-ind-104-core.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-datatypes () ((Nat!2409 (succ!2410 (pred!2411 Nat!2409)) (zero!2412))
@@ -30,4 +32,4 @@
 (forall ((?j I_count!263)) (ite (is-nil!2417 (count!263_arg_1_7 ?j)) true (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (ite (= (count!263_arg_0_6 ?j) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (head!2415 (count!263_arg_1_7 ?j)) (head!2415_uf_3 (count!263_arg_1_7 ?j)))) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) )) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) ))) true)) )
 )
 )
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
index d5effc083..229a5e17a 100644
--- a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
+++ b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --incremental --fmf-fun
 (set-logic ALL_SUPPORTED)
-(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
 (define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l)))))
 
 (declare-fun input () Int)
diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2
index 01c81cdc8..82033e606 100644
--- a/test/regress/regress0/push-pop/bug654-dd.smt2
+++ b/test/regress/regress0/push-pop/bug654-dd.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --fmf-fun --strings-exp
+; COMMAND-LINE: --incremental --fmf-fun --strings-exp --lang=smt2.5
 (set-logic ALL_SUPPORTED)
 (declare-datatypes () (
 (List_T_C (List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C)))
@@ -24,4 +24,4 @@
 ; EXPECT: sat
 (push 1)
 (check-sat)
-(pop 1)
\ No newline at end of file
+(pop 1)
diff --git a/test/regress/regress0/push-pop/bug674.smt2 b/test/regress/regress0/push-pop/bug674.smt2
index 967681ec3..fccde862a 100644
--- a/test/regress/regress0/push-pop/bug674.smt2
+++ b/test/regress/regress0/push-pop/bug674.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
 (set-logic ALL_SUPPORTED)
-(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
 (define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2))))
 (define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil))))
 ; EXPECT: unsat
diff --git a/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2
index 8fdee6f43..7680a7daf 100644
--- a/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2
+++ b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --lang=smt2.5
 ; EXPECT: unsat
 ; EXPECT: sat
 ; EXPECT: sat
diff --git a/test/regress/regress0/push-pop/bug765.smt2 b/test/regress/regress0/push-pop/bug765.smt2
index fb4aac85a..2144de060 100644
--- a/test/regress/regress0/push-pop/bug765.smt2
+++ b/test/regress/regress0/push-pop/bug765.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models --lang=smt2.5
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes () (
diff --git a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
index 125d5fcc9..b35c98aa9 100644
--- a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
+++ b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
@@ -1,10 +1,9 @@
 ; COMMAND-LINE: --incremental --fmf-fun --no-check-models
 (set-logic UFDTLIA)
 (set-option :produce-models true)
-(set-info :smt-lib-version 2.5)
-(declare-datatypes () ((List (Nil) (Cons (Cons$head Int) (Cons$tail List)))))
-(define-fun-rec all-z ((x List)) Bool (=> (is-Cons x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x)))))
-(define-fun-rec len ((x List)) Int (ite (is-Nil x) 0 (+ 1 (len (Cons$tail x)))))
+(declare-datatypes ((List 0)) (((Nil) (Cons (Cons$head Int) (Cons$tail List)))))
+(define-fun-rec all-z ((x List)) Bool (=> ((_ is Cons) x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x)))))
+(define-fun-rec len ((x List)) Int (ite ((_ is Nil) x) 0 (+ 1 (len (Cons$tail x)))))
 (declare-fun root() List)
 ; EXPECT: sat
 (assert (and (all-z root) (<= 1 (len root))))
diff --git a/test/regress/regress0/quantifiers/bug822.smt2 b/test/regress/regress0/quantifiers/bug822.smt2
index fc846b60b..cc1b5ed50 100644
--- a/test/regress/regress0/quantifiers/bug822.smt2
+++ b/test/regress/regress0/quantifiers/bug822.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --lang=smt2.6
-; EXPECT: unsat
 (set-logic UFDT)
 (set-info :source |
 Generated by: Andrew Reynolds
diff --git a/test/regress/regress0/quantifiers/bug_743.smt2 b/test/regress/regress0/quantifiers/bug_743.smt2
index 4e3ee0c96..ec5a5149e 100644
--- a/test/regress/regress0/quantifiers/bug_743.smt2
+++ b/test/regress/regress0/quantifiers/bug_743.smt2
@@ -1,3 +1,6 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
+
 ;; produced by cvc4_14.drv ;;
 (set-logic AUFBVDTNIRA)
 (set-info :source |VC generated by SPARK 2014|)
diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
index b8b1683a9..fe567f898 100644
--- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
+++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi --dt-rewrite-error-sel
+; COMMAND-LINE: --cbqi --dt-rewrite-error-sel --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 b/test/regress/regress0/quantifiers/cdt-0208-to.smt2
index a458cea64..9eff608bb 100644
--- a/test/regress/regress0/quantifiers/cdt-0208-to.smt2
+++ b/test/regress/regress0/quantifiers/cdt-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --full-saturate-quant
+; COMMAND-LINE: --full-saturate-quant --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
index 586aa64c7..f44d75195 100644
--- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2
+++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: unknown
 (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/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2
index c117934f8..c45152d6f 100644
--- a/test/regress/regress0/quantifiers/parametric-lists.smt2
+++ b/test/regress/regress0/quantifiers/parametric-lists.smt2
@@ -1,3 +1,5 @@
+; 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))))
diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
index 0ce96285c..b196ee262 100644
--- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
-(declare-datatypes () ((nat (Suc (pred nat)) (zero))))
+(declare-datatypes ((nat 0)) (( (Suc (pred nat)) (zero))))
 (declare-fun y () nat)
 (assert (forall ((x nat)) (not (= y (Suc x)))))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2
index 1e29241eb..6c191d688 100644
--- a/test/regress/regress0/quantifiers/rew-to-scala.smt2
+++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32))))
diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2
index d213e3426..0a736d7b3 100644
--- a/test/regress/regress0/quantifiers/simp-len.smt2
+++ b/test/regress/regress0/quantifiers/simp-len.smt2
@@ -1,9 +1,9 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 
-(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
 
 (define-fun-rec len ((x Lst)) Int (ite (is-cons x) (+ 1 (len (tail x))) 0))
 
 (assert (= (len (cons 0 nil)) 0))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2
index 615d43fe8..9243654b4 100644
--- a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2
+++ b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-sort A$ 0)
diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
index 42cfb3a11..e3008772d 100644
--- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2
+++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: 
+; COMMAND-LINE: --lang=smt2.5
 ; EXPECT: unknown
 ; this will fail if type rule for APPLY_UF requires arguments to be subtypes
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2
index a7fe58ac9..42d7a5b60 100644
--- a/test/regress/regress0/quantifiers/subtype-param.smt2
+++ b/test/regress/regress0/quantifiers/subtype-param.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 
diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2
index f5d53e3d5..c3c4aad73 100644
--- a/test/regress/regress0/rewriterules/native_datatypes.smt2
+++ b/test/regress/regress0/rewriterules/native_datatypes.smt2
@@ -3,9 +3,9 @@
 
 (set-info :status unsat)
 
-(declare-datatypes (
-(nat  (succ (pred nat)) (zero ) )
-(list  (cons (car nat)(cdr list)) (nil ) )
+(declare-datatypes ((nat 0) (list 0)) (
+((succ (pred nat)) (zero ) )
+((cons (car nat)(cdr list)) (nil ) )
 
 ))
 
diff --git a/test/regress/regress0/rewriterules/native_datatypes2.smt2 b/test/regress/regress0/rewriterules/native_datatypes2.smt2
index 4a719fb85..f19e5097b 100644
--- a/test/regress/regress0/rewriterules/native_datatypes2.smt2
+++ b/test/regress/regress0/rewriterules/native_datatypes2.smt2
@@ -3,9 +3,9 @@
 
 (set-info :status unsat)
 
-(declare-datatypes (
-(nat  (succ (pred nat)) (zero ) )
-(list  (cons (car nat)(cdr list)) (nil ) )
+(declare-datatypes ((nat 0) (list 0)) (
+((succ (pred nat)) (zero ) )
+((cons (car nat)(cdr list)) (nil ) )
 
 ))
 
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 3fa0d0555..e0ccee049 100644
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -4,7 +4,7 @@
 (declare-sort Loc 0)
 (declare-const loc0 Loc)
 
-(declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc)))))
+(declare-datatypes ((Node 0)) (((node (data Int) (left Loc) (right Loc)))))
 
 (declare-fun data0 () Node)
 
diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2
index a38544aa2..51400a05a 100644
--- a/test/regress/regress0/sets/dt-simp-mem.smt2
+++ b/test/regress/regress0/sets/dt-simp-mem.smt2
@@ -1,6 +1,6 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
-(declare-datatypes () ((D (A (a Int)))))
+(declare-datatypes ((D 0)) (((A (a Int)))))
 (declare-fun x1 () D)
 (declare-fun S () (Set D))
 (declare-fun P (D) Bool)
diff --git a/test/regress/regress0/strings/bug686dd.smt2 b/test/regress/regress0/strings/bug686dd.smt2
index 688cecec1..7c923654d 100644
--- a/test/regress/regress0/strings/bug686dd.smt2
+++ b/test/regress/regress0/strings/bug686dd.smt2
@@ -1,7 +1,7 @@
 (set-logic UFDTSLIA)
 (set-info :status sat)
 
-(declare-datatypes () ( (T (TC (TCb String))) ) )
+(declare-datatypes ((T 0)) ( ((TC (TCb String))) ) )
 
 (declare-fun root5 () String)
 (declare-fun root6 () T)
diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
index 3519319bd..2409b82d2 100644
--- a/test/regress/regress0/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -5,7 +5,7 @@
 (declare-var m Int)
 (declare-var s Int)
 (declare-var inc Int)
-(declare-datatypes () ( (tuple2 (tuple2 (_m Int) (_s Int))) ))
+(declare-datatypes ((tuple2 0)) ( ((tuple2 (_m Int) (_s Int))) ))
 
 (synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2)
 (constraint (=> 
diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
index 42382ac91..0a9fb9112 100644
--- a/test/regress/regress0/sygus/dt-no-syntax.sy
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -2,7 +2,7 @@
 ; EXPECT: unsat
 (set-logic LIA)
 
-(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
 
 (synth-fun f ((x Int)) List)
 
diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
index 052065061..0c28769b2 100644
--- a/test/regress/regress0/sygus/dt-test-ns.sy
+++ b/test/regress/regress0/sygus/dt-test-ns.sy
@@ -2,7 +2,7 @@
 ; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 
-(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
 
 (synth-fun f ((x Int)) List)
 
diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy
index 21362dc2c..8d209a9a0 100644
--- a/test/regress/regress0/sygus/list-head-x.sy
+++ b/test/regress/regress0/sygus/list-head-x.sy
@@ -2,7 +2,7 @@
 ; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic ALL_SUPPORTED)
 
-(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
 
 (synth-fun f ((x Int)) List)
 
diff --git a/test/regress/regress0/sygus/max.smt2 b/test/regress/regress0/sygus/max.smt2
index 97c223e16..ab2d4de05 100644
--- a/test/regress/regress0/sygus/max.smt2
+++ b/test/regress/regress0/sygus/max.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --lang=smt2.5
 
 (set-logic UFDTLIA)
 
diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
index be6749139..59560ed61 100644
--- a/test/regress/regress0/sygus/sygus-dt.sy
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -3,7 +3,7 @@
 
 (set-logic LIA)
 
-(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
 (define-fun g ((x Int)) List (cons (+ x 1) nil))
 (define-fun i () List (cons 3 nil))
 
diff --git a/test/regress/regress1/datatypes/manos-model.smt2 b/test/regress/regress1/datatypes/manos-model.smt2
index 4ade71151..771f40dec 100644
--- a/test/regress/regress1/datatypes/manos-model.smt2
+++ b/test/regress/regress1/datatypes/manos-model.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-datatypes () ( (tuple2!879 (tuple2!879!880 (_1!881 Int) (_2!882 Int))) ))
diff --git a/test/regress/regress1/fmf/ForElimination-scala-9.smt2 b/test/regress/regress1/fmf/ForElimination-scala-9.smt2
index 36bb915f4..e8a784fc7 100644
--- a/test/regress/regress1/fmf/ForElimination-scala-9.smt2
+++ b/test/regress/regress1/fmf/ForElimination-scala-9.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
+; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes () ((Statement!1556 (Assign!1557 (varID!1558 (_ BitVec 32)) (expr!1559 Expression!1578)) (Block!1560 (body!1561 List!1617)) (For!1562 (init!1563 Statement!1556) (expr!1564 Expression!1578) (step!1565 Statement!1556) (body!1566 Statement!1556)) (IfThenElse!1567 (expr!1568 Expression!1578) (then!1569 Statement!1556) (elze!1570 Statement!1556)) (Print!1571 (msg!1572 (_ BitVec 32)) (varID!1573 (_ BitVec 32))) (Skip!1574) (While!1575 (expr!1576 Expression!1578) (body!1577 Statement!1556)))
diff --git a/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2 b/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2
index 076150dc3..9c8bc1d3e 100644
--- a/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2
+++ b/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ ))))
diff --git a/test/regress/regress1/strings/cmu-dis-0707-3.smt2 b/test/regress/regress1/strings/cmu-dis-0707-3.smt2
index 209cbb3f9..3bf47ed61 100644
--- a/test/regress/regress1/strings/cmu-dis-0707-3.smt2
+++ b/test/regress/regress1/strings/cmu-dis-0707-3.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --lang=smt2.0
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (set-option :strings-exp true)