diff options
Diffstat (limited to 'test/regress/regress0/push-pop')
6 files changed, 9 insertions, 10 deletions
diff --git a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 index d5effc083..229a5e17a 100644 --- a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 +++ b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --incremental --fmf-fun (set-logic ALL_SUPPORTED) -(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) (define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l))))) (declare-fun input () Int) diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2 index 01c81cdc8..82033e606 100644 --- a/test/regress/regress0/push-pop/bug654-dd.smt2 +++ b/test/regress/regress0/push-pop/bug654-dd.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --fmf-fun --strings-exp +; COMMAND-LINE: --incremental --fmf-fun --strings-exp --lang=smt2.5 (set-logic ALL_SUPPORTED) (declare-datatypes () ( (List_T_C (List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C))) @@ -24,4 +24,4 @@ ; EXPECT: sat (push 1) (check-sat) -(pop 1)
\ No newline at end of file +(pop 1) diff --git a/test/regress/regress0/push-pop/bug674.smt2 b/test/regress/regress0/push-pop/bug674.smt2 index 967681ec3..fccde862a 100644 --- a/test/regress/regress0/push-pop/bug674.smt2 +++ b/test/regress/regress0/push-pop/bug674.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --quant-ind --incremental --rewrite-divk (set-logic ALL_SUPPORTED) -(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) (define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2)))) (define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil)))) ; EXPECT: unsat diff --git a/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 index 8fdee6f43..7680a7daf 100644 --- a/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 +++ b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --lang=smt2.5 ; EXPECT: unsat ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/regress0/push-pop/bug765.smt2 b/test/regress/regress0/push-pop/bug765.smt2 index fb4aac85a..2144de060 100644 --- a/test/regress/regress0/push-pop/bug765.smt2 +++ b/test/regress/regress0/push-pop/bug765.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models +; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models --lang=smt2.5 (set-logic ALL_SUPPORTED) (declare-datatypes () ( diff --git a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 index 125d5fcc9..b35c98aa9 100644 --- a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 +++ b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 @@ -1,10 +1,9 @@ ; COMMAND-LINE: --incremental --fmf-fun --no-check-models (set-logic UFDTLIA) (set-option :produce-models true) -(set-info :smt-lib-version 2.5) -(declare-datatypes () ((List (Nil) (Cons (Cons$head Int) (Cons$tail List))))) -(define-fun-rec all-z ((x List)) Bool (=> (is-Cons x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x))))) -(define-fun-rec len ((x List)) Int (ite (is-Nil x) 0 (+ 1 (len (Cons$tail x))))) +(declare-datatypes ((List 0)) (((Nil) (Cons (Cons$head Int) (Cons$tail List))))) +(define-fun-rec all-z ((x List)) Bool (=> ((_ is Cons) x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x))))) +(define-fun-rec len ((x List)) Int (ite ((_ is Nil) x) 0 (+ 1 (len (Cons$tail x))))) (declare-fun root() List) ; EXPECT: sat (assert (and (all-z root) (<= 1 (len root)))) |