diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/simp-len.smt2')
-rw-r--r-- | test/regress/regress0/quantifiers/simp-len.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
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) |