[YICES-HELP] works with -tc, crashes without

[Johannes Waldmann]

sorry, this is the program:


(define-type max-plus
             (record is_minus_infinite :: bool
                     contents :: nat))

(define max :: (-> nat nat nat)
     ( lambda (x :: nat y :: nat) (if (>= x y) x y)))

(define times :: (-> max-plus max-plus max-plus)
   (lambda (x :: max-plus y :: max-plus)
       (if (or (select x is_minus_infinite)
               (select y is_minus_infinite))
           (mk-record is_minus_infinite :: true
                      contents :: 0)
           (mk-record is_minus_infinite :: false
                      contents :: (+ (select x contents)
                                     (select y contents))))))

(define gt  :: ( -> max-plus max-plus bool )
     ( lambda (x :: max-plus y :: max-plus)
              (or (and (not (select x is_minus_infinite ))
                       (select y is_minus_infinite ))
                  (and (not (select x is_minus_infinite))
                       (not (select y is_minus_infinite))
                       (> (select x contents) ( select y contents))))))

(define a :: max-plus)
(define b :: max-plus)

(assert (gt (times a a) (times b (times b b))))
(assert (gt (times b b) a))

(check)