Add regression test for #30

tests/sat/div_zero.smt2

+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-sort tuple0 0)
+
+;;  uncomment to pass the VC to cvc4 or z3
+;; (define-fun colibri_cdiv ((x Int) (y Int)) Int (div x y))
+;; (define-fun colibri_crem ((x Int) (y Int)) Int (mod x y))
+;; (define-fun colibri_abs_int ((x Int)) Int (abs x))
+
+;; Abs_le
+  (assert
+  (forall ((x Int) (y Int))
+  (= (<= (colibri_abs_int x) y) (and (<= (- y) x) (<= x y)))))
+
+;; Abs_pos
+  (assert (forall ((x Int)) (<= 0 (colibri_abs_int x))))
+
+;; Div_bound
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< 0 y))
+  (and (<= 0 (colibri_cdiv x y)) (<= (colibri_cdiv x y) x)))))
+
+;; Div_sign_pos
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< 0 y)) (<= 0 (colibri_cdiv x y)))))
+
+;; Div_sign_neg
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= x 0) (< 0 y)) (<= (colibri_cdiv x y) 0))))
+
+;; Mod_sign_pos
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (not (= y 0))) (<= 0 (colibri_crem x y)))))
+
+;; Mod_sign_neg
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= x 0) (not (= y 0))) (<= (colibri_crem x y) 0))))
+
+;; Rounds_toward_zero
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (not (= y 0))
+  (<= (colibri_abs_int (* (colibri_cdiv x y) y)) (colibri_abs_int x)))))
+
+;; Div_inf
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< x y)) (= (colibri_cdiv x y) 0))))
+
+;; Mod_inf
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< x y)) (= (colibri_crem x y) x))))
+
+;; Div_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
+     (= (colibri_cdiv (+ (* x y) z) x) (+ y (colibri_cdiv z x)))) :pattern ((colibri_cdiv (+ (* x y) z) x)) )))
+
+;; Mod_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
+     (= (colibri_crem (+ (* x y) z) x) (colibri_crem z x))) :pattern ((colibri_crem (+ (* x y) z) x)) )))
+
+;; Div_unique
+  (assert
+  (forall ((x Int) (y Int) (q Int))
+  (=> (< 0 y) (=> (and (<= (* q y) x) (< x (+ (* q y) y))) (= (div x y) q)))))
+
+;; Div_bound
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div x y)) (<= (div x y) x)))))
+
+;; Div_inf
+  (assert
+  (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div x y) 0))))
+
+;; Div_inf_neg
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (< 0 x) (<= x y)) (= (div (- x) y) (- 1)))))
+
+;; Mod_0
+  (assert (forall ((y Int)) (=> (not (= y 0)) (= (mod 0 y) 0))))
+
+;; Div_1_left
+  (assert (forall ((y Int)) (=> (< 1 y) (= (div 1 y) 0))))
+
+;; Div_minus1_left
+  (assert (forall ((y Int)) (=> (< 1 y) (= (div (- 1) y) (- 1)))))
+
+;; Mod_1_left
+  (assert (forall ((y Int)) (=> (< 1 y) (= (mod 1 y) 1))))
+
+;; Mod_minus1_left
+  (assert
+  (forall ((y Int))
+  (! (=> (< 1 y) (= (mod (- 1) y) (- y 1))) :pattern ((mod (- 1) y)) )))
+
+;; Div_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (< 0 x) (= (div (+ (* x y) z) x) (+ y (div z x)))) :pattern ((div (+ (* x y) z) x)) )))
+
+;; Mod_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (< 0 x) (= (mod (+ (* x y) z) x) (mod z x))) :pattern ((mod (+ (* x y) z) x)) )))
+
+(define-fun mod1 ((x Int)
+  (y Int)) Int (ite (< 0 y) (mod x y) (+ (mod x y) y)))
+
+(declare-sort integer 0)
+
+(define-fun in_range ((x Int)) Bool (and (<= (- 2147483648) x)
+                                    (<= x 2147483647)))
+
+
+(define-fun dynamic_invariant ((temp___expr_18 Int) (temp___is_init_14 Bool)
+  (temp___skip_constant_15 Bool) (temp___do_toplevel_16 Bool)
+  (temp___do_typ_inv_17 Bool)) Bool (=>
+                                    (or (= temp___is_init_14 true)
+                                    (<= (- 2147483648) 2147483647)) (in_range
+                                    temp___expr_18)))
+
+(declare-const x Int)
+
+(declare-const y Int)
+
+(declare-const z Int)
+
+(declare-const tmp1 Int)
+
+(declare-const tmp2 Int)
+
+;; Assume
+  (assert (dynamic_invariant x true false true true))
+
+;; Assume
+  (assert (dynamic_invariant y true false true true))
+
+;; Assume
+  (assert (dynamic_invariant z true false true true))
+
+;; Assume
+  (assert (dynamic_invariant tmp1 false false true true))
+
+;; Assume
+  (assert (dynamic_invariant tmp2 false false true true))
+
+(define-fun o () Int (+ x y))
+
+;; Ensures
+  (assert (in_range o))
+
+;; Ensures
+  (assert (in_range (+ o z)))
+
+(define-fun o1 () Int (+ x y))
+
+;; Ensures
+  (assert (in_range o1))
+
+;; Ensures
+  (assert (in_range (- o1 z)))
+
+(define-fun o2 () Int (+ x y))
+
+;; Ensures
+  (assert (in_range o2))
+
+;; Ensures
+  (assert (in_range (+ o2 z)))
+
+(define-fun o3 () Int (- y z))
+
+;; Ensures
+  (assert (in_range o3))
+
+;; Ensures
+  (assert (in_range (+ x o3)))
+
+;; Assert
+  (assert (or (not (= x (- 2147483648))) (not (= y (- 1)))))
+
+;; Ensures
+  (assert (in_range (* x y)))
+
+;; Uncomment to prove VC in z3 and cvc4
+;;  (assert (distinct y 0))
+
+(assert
+;; defqtvc
+ ;; File "arith.adb", line 1, characters 0-0
+  (not (in_range (colibri_cdiv x y))))
+(check-sat)