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/push-pop/fmf-fun-dbu.smt2 | |
| 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/push-pop/fmf-fun-dbu.smt2')
| -rw-r--r-- | test/regress/regress0/push-pop/fmf-fun-dbu.smt2 | 7 |
1 files changed, 3 insertions, 4 deletions
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)))) |