diff options
Diffstat (limited to 'test/regress/regress0')
79 files changed, 122 insertions, 94 deletions
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)) |