blob: 13748eeeaf8ebadca418a9efacc45677afc6da71 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
(set-logic UFDTSLIA)
(set-info :smt-lib-version 2.5)
(set-option :produce-models true)
(declare-datatypes () (
(List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
) )
(define-funs-rec
(
(f4208$lengthList_boolean((x List_boolean)) Int)
)
(
(ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x))))
)
)
(declare-const boolean Bool)
(check-sat)
|
