[YICES-HELP] mk-record question

[Mido]

Dear All,

I was expecting the two formulae below to produce the same solution (i.e.
SAT and x=70). 
That does not happen as formula 2 produces UNSAT.
There is one difference there which is t2 has a mk-record.
Why mk-record changed the behavior of the 2nd formula?

Thanks!

;;Formula 1:
(define-type myrec  (record ix::int idx::int value::int aflag::bool))
(define t::myrec (mk-record ix::100 idx::10 value::20 aflag::true) )
(define t2::myrec )
(define x::int )
(define u::bool (= t2 (update t ix 30)))
(define y::int (+ x (select t2 ix)))
(define b::bool (= (select t ix) y))
(assert+ u)
(assert+ b)
(check)

;;Formula 2:
(define-type myrec  (record ix::int idx::int value::int aflag::bool))
(define t::myrec (mk-record ix::100 idx::10 value::20 aflag::true) )
(define t2::myrec (mk-record ix::100 idx::10 value::20 aflag::true) )
(define x::int )
(define u::bool (= t2 (update t ix 30)))
(define y::int (+ x (select t2 ix)))
(define b::bool (= (select t ix) y))
(assert+ u)
(assert+ b)
(check)