(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (and (<= (* (- 4) y) x)
	     (<  x (+ 4 (* (- 4) y)))
	     (not (= y (div x (- 4))))))
(check-sat)
(get-model)
(get-value (x y (div x (- 4))))