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

6 files changed, 9 insertions, 10 deletions

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