1 2 3 4 5 6
; EXPECT: unsat (set-logic ALL) (set-option :incremental false) (define-fun-rec five () Int 5) (assert (= five 6)) (check-sat)