(declare-fun MIN () Int)
(declare-fun MAX () Int)

(assert (= MAX 2147483647))
(assert (or
  ;; 2s complement
  (= (+ MIN 1) (- MAX))
  ;; 1s complement / signed zero
  (= MIN (- MAX))
))

(define-fun truncdiv ((x Int) (y Int)) Int
  (ite (or (= (mod x y) 0) (>= x 0))
       (div x y)
       (ite (>= y 0)
            (+ (div x y) 1)
            (- (div x y) 1))))
(define-fun truncmod ((x Int) (y Int)) Int
  (- x (* (truncdiv x y) y)))

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(declare-fun q2 () Int)
(declare-fun r2 () Int)

(assert
 (and

  (>= x MIN) (<= x MAX)
  (>= y MIN) (<= y MAX)
  (>= q MIN) (<= q MAX)
  (>= r MIN) (<= r MAX)

  ;; search for integer overflow
  (not (and

  (>= q2 MIN) (<= q2 MAX)
  (>= r2 MIN) (<= r2 MAX)

  ))

  ;; preconditions
  (not (= y 0)) (not (and (not (= (- MAX) MIN)) (= x MIN) (= y -1)))

  ;; perform division
  (= q (truncdiv x y))
  (= r (truncmod x y))

  ;; sub-precondition: r && (x < 0) != (y < 0)
  (not (= r 0)) (not (= (< x 0) (< y 0)))

  (= q2 (- q 1))
  (= r2 (+ r y))

 )
)

(check-sat)
(get-model)

(exit)