[YICES] Extrange result

[cristia at cifasis-conicet.gov.ar]

Hi!

I've posted a similar email on September 19 but I had no answer.

I tried to reduce the problem as much as I can so it would be easier for
you to help me.

I'm using Yices 1.0.29 on a Linux machine.

When I load the following script:

(define-type MDATA)
(define mdp::int)
(define memp::(tuple (-> int bool) (-> int MDATA)))
(define r1::(-> int bool) (lambda (i::int) (and (<= 1 i) (<= i 5))))
(assert (= r1 (select memp 1)))
(set-evidence! true)
(check)

I get the following result:

sat
(= (mk-tuple (select memp 1) (select memp 2)) memp)

Is this a complete model? I thought the model should include a "value" for
memp, but the value given by Yices is "circular", isn't it? According to
the assertion "(select memp 1)" should be equal to r1 which in turn is
true of [1..5]. Shouldn't the model include what is the value of "(select
memp 1)" on [1..5]?

Is there something I'm not getting right?

Thank you again for your help.

All the best,
  Maxi