(set-logic QF_LIA)
(declare-fun x () Int)
(define-fun d () Int (div x (- 4)))
(assert (> (* (- 4) d) x))
(check-sat)