Truncated integer division in Z3

integer-division.z3

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

;; (assert (= a (div -7 -3)))
;; (assert (= b (div  7 -3)))
;; (assert (= c (div -7  3)))
;; (assert (= a (mod -7 -3)))
;; (assert (= b (mod  7 -3)))
;; (assert (= c (mod -7  3)))

;; C-style truncated division/modulus
(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)))

;; (assert (= a (truncdiv -7 -3)))
;; (assert (= b (truncdiv  7 -3)))
;; (assert (= c (truncdiv -7  3)))
(assert (= a (truncmod -7 -3)))
(assert (= b (truncmod  7 -3)))
(assert (= c (truncmod -7  3)))

(check-sat)
(get-model)

(exit)

overflow-checker-template.z3

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

(assert
 (and

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

  ;; unsigned integer
  ;; (= MAX 4294967295)
  ;; (= MIN 0)

))


(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)

(assert
 (and

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

  ;; search for integer overflow
  (not (and

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

  ))

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

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

 )
)

(check-sat)
(get-model)

(exit)

undefined-behavior-floordiv.z3

(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)