diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-04 16:51:35 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-04 16:51:35 +0200 |
commit | 59620e0dcafd8224ce609785c37dd8350c33683f (patch) | |
tree | 1bd882ba00e2716ace9f520bcfc32ac6374f9b38 /test/regress/regress0/quantifiers | |
parent | b539a167fa56deea34472a9725693f45ae325dd8 (diff) |
Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.
Diffstat (limited to 'test/regress/regress0/quantifiers')
12 files changed, 18 insertions, 9 deletions
diff --git a/test/regress/regress0/quantifiers/bug822.smt2 b/test/regress/regress0/quantifiers/bug822.smt2 index fc846b60b..cc1b5ed50 100644 --- a/test/regress/regress0/quantifiers/bug822.smt2 +++ b/test/regress/regress0/quantifiers/bug822.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --lang=smt2.6 -; EXPECT: unsat (set-logic UFDT) (set-info :source | Generated by: Andrew Reynolds diff --git a/test/regress/regress0/quantifiers/bug_743.smt2 b/test/regress/regress0/quantifiers/bug_743.smt2 index 4e3ee0c96..ec5a5149e 100644 --- a/test/regress/regress0/quantifiers/bug_743.smt2 +++ b/test/regress/regress0/quantifiers/bug_743.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat + ;; produced by cvc4_14.drv ;; (set-logic AUFBVDTNIRA) (set-info :source |VC generated by SPARK 2014|) diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index b8b1683a9..fe567f898 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi --dt-rewrite-error-sel +; COMMAND-LINE: --cbqi --dt-rewrite-error-sel --lang=smt2.5 ; EXPECT: unsat (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 b/test/regress/regress0/quantifiers/cdt-0208-to.smt2 index a458cea64..9eff608bb 100644 --- a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 +++ b/test/regress/regress0/quantifiers/cdt-0208-to.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --full-saturate-quant +; COMMAND-LINE: --full-saturate-quant --lang=smt2.5 ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 index 586aa64c7..f44d75195 100644 --- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -2,7 +2,7 @@ ; EXPECT: unknown (set-logic ALL_SUPPORTED) -(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) +(declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil))))) (declare-fun R ((List Real)) Bool) (assert (forall ((x (List Int))) (R x))) diff --git a/test/regress/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2 index c117934f8..c45152d6f 100644 --- a/test/regress/regress0/quantifiers/parametric-lists.smt2 +++ b/test/regress/regress0/quantifiers/parametric-lists.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) (declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil)))) diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 index 0ce96285c..b196ee262 100644 --- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -2,7 +2,7 @@ ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) -(declare-datatypes () ((nat (Suc (pred nat)) (zero)))) +(declare-datatypes ((nat 0)) (( (Suc (pred nat)) (zero)))) (declare-fun y () nat) (assert (forall ((x nat)) (not (= y (Suc x))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2 index 1e29241eb..6c191d688 100644 --- a/test/regress/regress0/quantifiers/rew-to-scala.smt2 +++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) (declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32)))) diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2 index d213e3426..0a736d7b3 100644 --- a/test/regress/regress0/quantifiers/simp-len.smt2 +++ b/test/regress/regress0/quantifiers/simp-len.smt2 @@ -1,9 +1,9 @@ (set-logic ALL_SUPPORTED) (set-info :status unsat) -(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) (define-fun-rec len ((x Lst)) Int (ite (is-cons x) (+ 1 (len (tail x))) 0)) (assert (= (len (cons 0 nil)) 0)) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 index 615d43fe8..9243654b4 100644 --- a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) (declare-sort A$ 0) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 index 42cfb3a11..e3008772d 100644 --- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: +; COMMAND-LINE: --lang=smt2.5 ; EXPECT: unknown ; this will fail if type rule for APPLY_UF requires arguments to be subtypes (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 index a7fe58ac9..42d7a5b60 100644 --- a/test/regress/regress0/quantifiers/subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) |