(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x (+ y (* (- 5) (div x (- 5))))))
(assert (not (= y (mod x (- 5)))))
(check-sat)