1 2 3 4 5 6 7 8 9 10
; EXPECT: sat ; EXPECT: (model ; EXPECT: (define-fun x () Int 5) ; EXPECT: ) ; EXIT: 10 (set-option :produce-models true) (set-logic QF_UFLIA) (define-fun x () Int 5) (check-sat) (get-model)