Remove the forall form div_zero so that colibri answers sat

tests/sat/div_zero.smt2

@@ -8,114 +8,6 @@
 ;; (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)))