Add regression tests for #33 #35 #36 #37

tests/sat/bug36.smt2

+;; produced by colibri.drv ;;
+(set-logic ALL)
+
+(declare-fun bool_eq (Real Real) Bool)
+(declare-const x Int)
+(declare-fun to_big_real (Int) Real)
+
+(assert
+  (not
+  (= (bool_eq (to_big_real x) (fp.to_real ((_ to_fp 11 53) RNE (to_real x)))) true)))
+(check-sat)

tests/unsat/issue33.smt2

+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (= b 0)))
+(assert (not (= (colibri_cdiv (- a) b) (- (colibri_cdiv a b)))))
+(check-sat)

tests/unsat/issue35.smt2

+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(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))))
+
+(define-fun same_sign ((x Int) (y Int)) Bool
+  (or (and (<= 0 x) (<= 0 y)) (and (<= x 0) (<= y 0))))
+
+(assert (not (= b 0)))
+(assert (not (= (same_sign (mod1 a b) b) true)))
+(check-sat)