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

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 697ce6642f4290f5ed5aff435f0a56492f62315f..2a9202898d2d67bab0ff321de2c9f041e7c7a5e1 100644 (file)
--- 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 bbb95f2582842c920d01998c3acbb4f68119102a..86beffd6d35e11ee685068094cfdcad51fb92b41 100644 (file)
--- 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 c7156635dc8e24378501d3abeac4b17838e80307..86c0b31265e58a61460916bd536e9c2e8d46710e 100644 (file)
--- 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 d5df938a729a799d949807d7f1f8aa02b4049e1e..2046f491163cda1363fb7c9e669da5181360a4f8 100644 (file)
--- 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 92e54096664be254c1874a444d85a2bd6661d37a..3aea7e9c9759cf0a8fcf970580269f68efcd64ea 100644 (file)
--- 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 3c73e261c314eada96cc9396b48ae06db43f7c44..87a8696b6b343e4f12fac557ab7a834b365159d1 100644 (file)
--- 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 75a63e328a0060937ffb4485d571555cf452a036..a20dddfe730e3b8cb6c7bc37e6c56ea55fbec136 100644 (file)
--- 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 482823985f987f230a02665fa155aa4ba35eec45..771fbed4fb479f25e2cb8e2684c648d354502b68 100644 (file)
--- 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 37403d8a30dc718f4a3b4884ff9ce188293f6a2d..99d7f0302e740870ff6fe652549fc0826f2e3ac2 100644 (file)
--- 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 cc54ab4c265489440ebf86681f27fa3f1a72d23e..93d7b88c4691a1337d7069547a28b7f02cb8866f 100644 (file)
--- 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 45d82a522a9c25f4e73a76ef357fa85e9c3ceb43..078fa59f7b3afa56fc75d3d9d30cfff394ace4fc 100644 (file)
--- 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 15a60c3e389e62f32fce39e4facdf8d4c98e3319..dfd11001dce237a0a8fc73398defc313f6188766 100644 (file)
--- 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 3f4312ad4871d0d8b443cab58ea25448c65048d2..1e9a18d9d66efcdef08511ddea51e825b00609f6 100644 (file)
--- 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 c23a9d594af88837f1c4c50e5161cd7fcf24e46a..8ddf7c52ab35ed65c10ffad94ef2fa587e86df1e 100644 (file)
--- 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 4a111b41bbb3b60aa80f46ce77fada8b9cd02dda..0741b0ff00e17ad134890c8a5da6a72487ea2605 100644 (file)
--- 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 1e000cecda65370d0c0f649b660fdbab064e740d..3c30021b04b83ec9f73ec11b08c128d061778647 100644 (file)
--- 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 6f82cd842f4a91d034359838d1571bffc17e8a82..74b836b47302c464a3ebf0a7fc5262c11ffec756 100644 (file)
--- 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 a132ce8fcfdb92e59fece7a65eb61f4830aa35a7..f6d1cd58db1dd12754b9b0a4ab46a249207cba56 100644 (file)
--- 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 ca5791ce26951189ef1cf08fcb7a5141f931d6fc..7a0fa30c718758ce653cd7118290ed952adea4b1 100644 (file)
--- 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 9676745b4760cbc916465ceb165b043d7271c8df..d403cf4eeb9c5f2ab92e654ab82bbc0c9dc51b46 100644 (file)
--- 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 1698fc3b094e749e82a85ce7963e18cda1e5e358..5702cb04b1b64e4a51b8c8a3460ce40a3e105daf 100644 (file)
--- 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 9c38ffcc8a43ae86dbe4d05309647fdd98ff56c6..f13a4f21f0a6b9571a38ac575cf97598fca9da79 100644 (file)
--- 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 7e7fe4f492e47ef75fe1897f544ba760e04c45c4..6528661366518ab4b3f04d0beaa747354b0cef85 100644 (file)
--- 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 5d028d72351e482b52a6ffa235f7125ce765a010..a4d5ff0eccf2aad74a825bf8de31dcc09593f941 100644 (file)
--- 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 672acfa44987e2cc51aec0daf649f7e52b0ea304..3c88c49c011519419bf2885df18c8c966a38d871 100644 (file)
--- 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 6884059caef4f63100bf948d900070b6b080942b..95d5f0c81653a8c3e7bf8ba1cf567a35f5cc23e4 100644 (file)
--- 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 bf82c7b8ce0f9bae79cc1dd6a97edfc196ba3f4d..6d25aefd0d16ed59b2a5cfe4c6a1b173e2c65b6d 100644 (file)
--- 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 9ef5f14fa799581445e6b49e7240be64b644a66f..a58e85c0d38b3f887c3d82ccca9b4d872cc7b297 100644 (file)
--- 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 bfe48195b780c9ddb8e6b01895fb9682c8e4f631..d17a663c6dd0a445c720e8ebd753335bb561bbd9 100644 (file)
--- 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 1bfdb9f833facd1d3397d3e092d37ccdeeec6591..07180cf4fb43334992104d952cf18ffe3782a8c0 100644 (file)
--- 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 9577e8f57608304f3849d39a121227bd705d7a77..fc3054c0d7456190c7a8be33b0666a3b512ecb95 100644 (file)
--- 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 9afc47972ed1081bc919e57e608ceccff4edd1d4..bcfeebd691228bc159fe7fd96c7d0378e5ab946f 100644 (file)
--- 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 1a27bf1702223c8211b089ff4973bb3c77aed54a..e9b748744232684b080c356447e0b64f8d2aa643 100644 (file)
--- 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 d030c3e8836bfe63f08fc3034efb4495bb9fe2f6..3172fd6951fe382ca073c36a0168a7d6ff2db1e4 100644 (file)
--- 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 db9788a6145e401f1899b7a390d9cbfeaedc71e6..5e3c2952b7b58ffc0b66c2bb2027973671dc96c5 100644 (file)
--- 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 c8f6c1d718f6122734d67286f6f1a11c1defed69..bc6d9e9486b0a2fde15582ab2e8192231448425a 100644 (file)
--- 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 3ffc36d0549d5ea4cc92dee10a6e52db901e5a8b..6b30907aec9f04a5c9be721d3b57d328f2642514 100644 (file)
--- 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 3564bff8be1072efb20aa6e95a0b3a08c356635f..a19c8f027647208e5bbd978d566ce1a56fb134f7 100644 (file)
--- 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 60a0b63771cb8baaccc6f329e7f2b477156f7ec9..0e66db9964617dc7ad2decb75c2528b8ea83718f 100644 (file)
--- 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 813f897323d09fd755c678d1911628290d7fb088..e4e1f65b48d3a8fd4414a6e75648262fd88ebff7 100644 (file)
--- 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 64847d6d20d7d03cf4b04bd054189d1266b20c62..88f2631c5d59cad65c09cbfcffc7480456a05771 100644 (file)
--- 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 9a6e1e270276775ca256831fd7b8abdceb42cbab..4b4d57af3f11cf20fcbb501df30dda6dfc330da6 100644 (file)
--- 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 3558715a8a14267c854cb4450c8b1d580ae5fd95..c88de064c9f92539b2ca56796ee8ed9a8cd22bd6 100644 (file)
--- 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 e1d49997230f9a1982730c900211d2e8206dfd66..64f551d55c029bcdd74659104352fb646c31103e 100644 (file)
--- 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 1f7214232af3e7086b1392b51aa5262d45d39ed7..7012838f9e460c62809204a04bb47f83a421f59a 100644 (file)
--- 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 22d9e447498afcc8f2dea8b7d73be231a85c6a40..17c6d974872fc3da74b3c27bb011909c9f643c70 100644 (file)
--- 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 7c1d30886bdbe213f1c2fa626958873bd3aa6c49..519fb17fc16e3699d2597f566d44145c2b475845 100644 (file)
--- 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 5e1f3de30e32d7a8541504b55380c1e86de7739d..d55e15925fff65251517e4fb6fb3f2f0a95b9d1f 100644 (file)
--- 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 f831af1f2e79735d216507b5926c92deb80e12e7..e6b3c2021f14f18782eb3f2f1aeeca042eaef94d 100644 (file)
--- 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 2fc86cbed9e7e26267f21512475de9162382bd9a..345d8220e4b591bbaa269e6db71748264b1d61e7 100644 (file)
--- 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 a083e418d28b6d62af3b5197be3a64c5610cfc3e..68a4399caa9e7f47823cc4d00bbd76063f94e484 100644 (file)
--- 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 87b2d53a65c0c20f4589f171f159c36bebc10743..2651db3f2f181454813239b9b31b8db68f95da43 100644 (file)
--- 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 a2e3a9ed0b51ef4a043869d413aae28f2d9b1d1d..c1d718403919dfaa8731c4d4058aee351e9714e7 100644 (file)
--- 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 d5effc08312fd3652d1225f59dd750912a62416d..229a5e17a1d96c88959490cce6fb2f10c861a01c 100644 (file)
--- 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 01c81cdc8d3df0fe48cd2d94e59ea591827d9099..82033e606ed38a57b4b5f38c1bbf1c3d0a70c844 100644 (file)
--- 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 967681ec36c1781fde40f5422cd55d39aba4b51d..fccde862a13f431edeafede1283dc8d36c784432 100644 (file)
--- 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 8fdee6f430e80067a3c8706407acdc183b64c890..7680a7daf551b374bc2e8f9729596c6c98c5bac5 100644 (file)
--- 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 fb4aac85adc025c4dd91650727fedccb7ad79e7b..2144de0607b0c5fa1b824fcee2dc198904be47a4 100644 (file)
--- 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 125d5fcc9a37382cfbd1936e8ef380e22196584d..b35c98aa955ad5936d7c1dd8959122cef93067e7 100644 (file)
--- 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 fc846b60bc093509fb25d8cba1923302922f7efc..cc1b5ed50182526c3abcd74acd5df5ffa76a2ee4 100644 (file)
--- 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 4e3ee0c96ffecd4da633ea67ab36f57bdcb4dcaf..ec5a5149e28e483cbd23d84bcd5043c58c6d7789 100644 (file)
--- 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 b8b1683a95e2588668e8f14d4152223a1bbced6a..fe567f898154f9006e322368c43ee9c18c9119b5 100644 (file)
--- 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 a458cea646f26a485d457ece1bafbdce56c710a0..9eff608bb0fac7486d3b1b434a7e2ef9fb5977f1 100644 (file)
--- 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 586aa64c73e93d29957c0f72a74236064ebd379d..f44d751957182bebf7fc60300222ab44c44daf40 100644 (file)
--- 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 c117934f8abdba6f7a64ada0af241b3ba9b5cc61..c45152d6f8da76ba90ff5b3852995b1338148073 100644 (file)
--- 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 0ce96285c45de17b0621ab17d7f1a65f8e7d537b..b196ee262c120cafc7d5a177246645e37ce2cd6b 100644 (file)
--- 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 1e29241ebbc16102a70bc17d716b8fd88d5e07ac..6c191d688d9fea0ba4d50d32491dd30283082491 100644 (file)
--- 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 d213e34264c75afba0d45f9b9d1a054d0688bdc9..0a736d7b3b9b942758a9a3533d13c7c1e9b4a6b9 100644 (file)
--- 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 615d43fe842632ff350747cbab94c4b36a2dabd0..9243654b4dd9f9b371f796e1ade48c1354de867a 100644 (file)
--- 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 42cfb3a1133f6c95179d87ac94a790859863d8cc..e3008772d7336f51669894b96ac686c3279a98ca 100644 (file)
--- 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 a7fe58ac94ca14ffebdbd761144cec228a858fba..42d7a5b6030844246e3602c1b629cb7d5dcb96bb 100644 (file)
--- 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 f5d53e3d5185ba5ee96073ac2b2d4e22d4f21fa8..c3c4aad73da3b36c7a83477bccd496e5972c0aac 100644 (file)
--- 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 4a719fb8523ef23f71046c9c7ce754165bfc1a3b..f19e5097bbb7d6426dc9835b044f968e4048c36c 100644 (file)
--- 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 3fa0d0555caef6bcbff8a3a5322677a007d32b92..e0ccee04919d7f746c2684073326a15b615af435 100644 (file)
--- 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 a38544aa2f0a0a3a270e183c984aa8533b58123d..51400a05ae0ac48e073820fd0ef18024f0a14f48 100644 (file)
--- 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 688cecec15d540310718d04ae614b394b6379c77..7c923654d64800f36a63b00f74ae07d52bb34a73 100644 (file)
--- 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 3519319bd11a25fd5f1c49b7032b148ed9eb5693..2409b82d266a2d7eddf9b409b5abade22f83aa8b 100644 (file)
--- 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 42382ac91fd13c2a74d074c932704309039010f3..0a9fb9112ce57f74be10ed5de18fd7d6d528d92a 100644 (file)
--- 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 0520650614a2f22b05bb55c8dec0792d2451dc41..0c28769b2e0cd553da207b07e6702e5cb8b2f96c 100644 (file)
--- 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 21362dc2cfd4ee25f569c7d2ae2df53b5098a0a0..8d209a9a00d341134717a645d3a3e1e4f3ea3a0d 100644 (file)
--- 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 97c223e16066164e88d1bc235f3f7d4dc4a6a1c6..ab2d4de056766b395784fc0142a37aa40cfb8c58 100644 (file)
--- 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 be67491399fe37e7e9e849d8985cdddb750a129b..59560ed61f838673f1f38de6b60da12713bc8faf 100644 (file)
--- 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 4ade71151ea5f2987ae621d6266883ea3086c0dd..771f40dec8c2c30a2eed26be6c20ce9f3cf948c7 100644 (file)
--- 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 36bb915f42f293078b49bff1b4c341b59c4b322a..e8a784fc751b23515fd2c0712fbc3b36592a5162 100644 (file)
--- 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 076150dc319fc11ddddf8dd1440f2eac8ae3ef62..9c8bc1d3e08e438114a5382efd51f79c639f3795 100644 (file)
--- 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 209cbb3f99b35eda0124382c041dc6846908f1a7..3bf47ed61fd17d48f4725a9b47172708b40f0b81 100644 (file)
--- 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)