[YICES-HELP] Type error

[cristia at cifasis-conicet.gov.ar]

Hi!

I'm really new to Yices so forgive me if this is a silly question.

I get "type error: type mismatch 3" with the following script:

(define-type ACCNUM (scalar accnum1 accnum2 accnum3))
(define balances::(tuple d::(-> ACCNUM bool) (-> (subtype (x::ACCNUM) (d
x)) int)))
(define n::ACCNUM)
(define m::int)
(assert ((select balances 1) n))
(assert (= m ((select balances 2) n)))

but I don't see any type mismatch. Is it the subtype used to define
balances? It's strange because the following definition does not end in
type mismatch:

(define aa::int ((select balances 2) n))

Thanks in advance for your help.

All the best,
  Maxi