Yices2-mcsat and converting between Real and Integer

[yav]

The model below illustrates an example where sally (with engine kind) can solve the problem immediately, but if we add --yices2-mcsat Sally fails to find a solution (or is much slower, I didn't wait for too long).

I imagine that this is more of a Yices issue rather than Sally, but I thought it might be of interest here.

(define-state-type S
   ( (ok2 Bool) (ok4 Bool) (init Bool))
   ( (x Real) )
)

(define-transition-system TS S
   (= init true)
   (and (= next.init false)

        (= next.ok2
           (= (= (to_int (- input.x)) (- (to_int input.x)))
              (= input.x (to_real (to_int input.x)))
           )
        )

        (= next.ok4
           (= (to_int (/ (to_real (to_int input.x)) (to_real 5)))
              (to_int (/ input.x 5.0))))))

(query TS (or init ok2))
(query TS (or init ok4))