diff options
Diffstat (limited to 'test/regress/regress0/fmf/tail_rec.smt2')
| -rw-r--r-- | test/regress/regress0/fmf/tail_rec.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/fmf/tail_rec.smt2 b/test/regress/regress0/fmf/tail_rec.smt2 index 87b2d53a6..2651db3f2 100644 --- a/test/regress/regress0/fmf/tail_rec.smt2 +++ b/test/regress/regress0/fmf/tail_rec.smt2 @@ -2,9 +2,9 @@ ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-sort elem 0) -(declare-datatypes () ((list (Nil) (Cons (hd elem) (tl list))))) +(declare-datatypes ((list 0)) (((Nil) (Cons (hd elem) (tl list))))) (define-fun-rec f ((x list)) elem - (ite (is-Nil x) (f x) (hd x)) + (ite ((_ is Nil) x) (f x) (hd x)) ) (declare-fun t () elem) (assert (= t (f Nil))) |