summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/simp-len.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/quantifiers/simp-len.smt2')
-rw-r--r--test/regress/regress0/quantifiers/simp-len.smt24
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback