Regression tests for #41 #42

tests/sat/issue_42.smt2

+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const a Int)
+(assert (and (< 1 a) (< a 100)))
+
+(assert (= (colibri_crem 100 a) 0))
+(check-sat)

tests/sat/issue_42_bis.smt2

+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(assert (not (= (colibri_crem (- 1) (- 1)) (- 1))))
+(check-sat)

tests/unsat/issue_41.smt2

+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+;;; SMT-LIB2: integer arithmetic
+(declare-sort string 0)
+
+(declare-fun match_bool (par (a) (Bool a a) a))
+
+;; match_bool_True
+  (assert (par (a) (forall ((z a) (z1 a)) (= (match_bool true z z1) z))))
+
+;; match_bool_False
+  (assert (par (a) (forall ((z a) (z1 a)) (= (match_bool false z z1) z1))))
+
+(declare-fun index_bool (Bool) Int)
+
+;; index_bool_True
+  (assert (= (index_bool true) 0))
+
+;; index_bool_False
+  (assert (= (index_bool false) 1))
+
+;; bool_inversion
+  (assert (forall ((u Bool)) (or (= u true) (= u false))))
+
+(declare-sort tuple0 0)
+
+(declare-const Tuple0 tuple0)
+
+;; tuple0_inversion
+  (assert (forall ((u tuple0)) (= u Tuple0)))
+
+(declare-sort us_private 0)
+
+(declare-fun private__bool_eq (us_private us_private) Bool)
+
+(declare-const us_null_ext__ us_private)
+
+(declare-sort us_type_of_heap 0)
+
+(declare-sort us_type_of_heap__ref 0)
+
+(declare-fun us_type_of_heap__refqtmk (us_type_of_heap) us_type_of_heap__ref)
+
+(declare-fun us_type_of_heap__content (us_type_of_heap__ref) us_type_of_heap)
+
+;; __type_of_heap__content'def
+  (assert
+  (forall ((u us_type_of_heap))
+  (= (us_type_of_heap__content (us_type_of_heap__refqtmk u)) u)))
+
+;; __type_of_heap__ref_inversion
+  (assert
+  (forall ((u us_type_of_heap__ref))
+  (! (= u (us_type_of_heap__refqtmk (us_type_of_heap__content u))) :pattern (
+  (us_type_of_heap__content u)) )))
+
+(declare-sort us_image 0)
+
+(declare-sort int__ref 0)
+
+(declare-fun int__refqtmk (Int) int__ref)
+
+(declare-fun int__content (int__ref) Int)
+
+;; int__content'def
+  (assert (forall ((u Int)) (= (int__content (int__refqtmk u)) u)))
+
+;; int__ref_inversion
+  (assert
+  (forall ((u int__ref))
+  (! (= u (int__refqtmk (int__content u))) :pattern ((int__content u)) )))
+
+(declare-sort bool__ref 0)
+
+(declare-fun bool__refqtmk (Bool) bool__ref)
+
+(declare-fun bool__content (bool__ref) Bool)
+
+;; bool__content'def
+  (assert (forall ((u Bool)) (= (bool__content (bool__refqtmk u)) u)))
+
+;; bool__ref_inversion
+  (assert
+  (forall ((u bool__ref))
+  (! (= u (bool__refqtmk (bool__content u))) :pattern ((bool__content u)) )))
+
+(declare-sort us_fixed__ref 0)
+
+(declare-fun us_fixed__refqtmk (Int) us_fixed__ref)
+
+(declare-fun us_fixed__content (us_fixed__ref) Int)
+
+;; __fixed__content'def
+  (assert (forall ((u Int)) (= (us_fixed__content (us_fixed__refqtmk u)) u)))
+
+;; __fixed__ref_inversion
+  (assert
+  (forall ((u us_fixed__ref))
+  (! (= u (us_fixed__refqtmk (us_fixed__content u))) :pattern ((us_fixed__content
+                                                               u)) )))
+
+(declare-sort real__ref 0)
+
+(declare-fun real__refqtmk (Real) real__ref)
+
+(declare-fun real__content (real__ref) Real)
+
+;; real__content'def
+  (assert (forall ((u Real)) (= (real__content (real__refqtmk u)) u)))
+
+;; real__ref_inversion
+  (assert
+  (forall ((u real__ref))
+  (! (= u (real__refqtmk (real__content u))) :pattern ((real__content u)) )))
+
+(declare-sort us_private__ref 0)
+
+(declare-fun us_private__refqtmk (us_private) us_private__ref)
+
+(declare-fun us_private__content (us_private__ref) us_private)
+
+;; __private__content'def
+  (assert
+  (forall ((u us_private))
+  (= (us_private__content (us_private__refqtmk u)) u)))
+
+;; __private__ref_inversion
+  (assert
+  (forall ((u us_private__ref))
+  (! (= u (us_private__refqtmk (us_private__content u))) :pattern ((us_private__content
+                                                                   u)) )))
+
+(define-fun int__ref___projection ((a1 int__ref)) Int (int__content a1))
+
+(define-fun us_fixed__ref___projection ((a1 us_fixed__ref)) Int (us_fixed__content
+                                                                a1))
+
+(define-fun bool__ref___projection ((a1 bool__ref)) Bool (bool__content a1))
+
+(define-fun real__ref___projection ((a1 real__ref)) Real (real__content a1))
+
+(define-fun us_private__ref___projection ((a1 us_private__ref)) us_private 
+  (us_private__content a1))
+
+(define-fun length ((x Int) (y Int)) Int (ite (<= x y) (+ (- y x) 1) 0))
+
+;; 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 (or (and (< 0 x) (< 0 y)) (and (< x 0) (< y 0)))
+               (colibri_crem x y)
+               (ite (= (colibri_crem x y) 0) 0 (+ (colibri_crem x y) y))))
+
+(declare-fun bool_eq (Int Int) Bool)
+
+(declare-const value__size Int)
+
+(declare-const object__size Int)
+
+(declare-const alignment Int)
+
+;; value__size_axiom
+  (assert (<= 0 value__size))
+
+;; object__size_axiom
+  (assert (<= 0 object__size))
+
+;; alignment_axiom
+  (assert (<= 0 alignment))
+
+(declare-fun user_eq (Int Int) Bool)
+
+(declare-const dummy Int)
+
+(declare-sort big_integer__ref 0)
+
+(declare-fun big_integer__refqtmk (Int) big_integer__ref)
+
+(declare-fun big_integer__content (big_integer__ref) Int)
+
+;; big_integer__content'def
+  (assert
+  (forall ((u Int)) (= (big_integer__content (big_integer__refqtmk u)) u)))
+
+;; big_integer__ref_inversion
+  (assert
+  (forall ((u big_integer__ref))
+  (! (= u (big_integer__refqtmk (big_integer__content u))) :pattern (
+  (big_integer__content u)) )))
+
+(define-fun big_integer__ref_big_integer__content__projection ((a1 big_integer__ref)) Int 
+  (big_integer__content a1))
+
+(declare-sort valid_big_integer__ref 0)
+
+(declare-fun valid_big_integer__refqtmk (Int) valid_big_integer__ref)
+
+(declare-fun valid_big_integer__content (valid_big_integer__ref) Int)
+
+;; valid_big_integer__content'def
+  (assert
+  (forall ((u Int))
+  (= (valid_big_integer__content (valid_big_integer__refqtmk u)) u)))
+
+;; valid_big_integer__ref_inversion
+  (assert
+  (forall ((u valid_big_integer__ref))
+  (! (= u (valid_big_integer__refqtmk (valid_big_integer__content u))) :pattern (
+  (valid_big_integer__content u)) )))
+
+(define-fun valid_big_integer__ref_valid_big_integer__content__projection ((a1 valid_big_integer__ref)) Int 
+  (valid_big_integer__content a1))
+
+(declare-const x Int)
+
+(declare-const y Int)
+
+(define-fun dynamic_invariant ((temp___expr_227 Int)
+  (temp___is_init_223 Bool) (temp___skip_constant_224 Bool)
+  (temp___do_toplevel_225 Bool) (temp___do_typ_inv_226 Bool)) Bool true)
+
+(define-fun dynamic_predicate ((temp___231 Int)) Bool true)
+
+;; Assume
+  (assert (not (= (= y 0) true)))
+
+(assert
+;; defqtvc
+  (not (= (= (colibri_crem x y) (colibri_crem x (- y))) true)))
+(check-sat)