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

12 files changed, 18 insertions, 9 deletions

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)