; EXIT: 0
(set-logic QF_LRA)
(define-fun x () Real (+ 4 1))