cvc4 example

overflow_checking.smt2

;; overflow checking words vs. checking explicit bounds
;; x * y / y == x     <==>
;; x * y does not overflow


;; max value of (_ BitVec 256)
(define-fun pow256 () Int
  115792089237316195423570985008687907853269984665640564039457584007913129639936)

;; x * y / y == x
(define-fun divinv ((x (_ BitVec 256)) (y (_ BitVec 256))) Bool
   (= (bvudiv (bvmul x y) y) y))


(declare-fun x () (_ BitVec 256))
(declare-fun y () (_ BitVec 256))
(declare-fun xnat () Int)
(declare-fun ynat () Int)

(assert (not (= ynat 0)))

(assert (= (bv2nat x) xnat))
(assert (= (bv2nat y) ynat))

(assert (not
 (and
  (=> (< (* xnat ynat) pow256)
      (divinv x y))
  (=> (divinv x y)
      (< (* xnat ynat) pow256)))
 ))
  

(check-sat)
(get-model)