(set-logic QF_NIA)
(assert (= (div 1 (- 1)) (- 1)))
(set-info :status sat)
(check-sat)