diff --git a/tests/sat/issue40_sat.smt2 b/tests/sat/issue40_sat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..a8b76b52160eacfbdbcba7bedcdbedcf849c86eb
--- /dev/null
+++ b/tests/sat/issue40_sat.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const x Int)
+(declare-const y Int)
+
+;(assert (not (= y 0)))
+
+(assert
+  (not (= (colibri_abs_int (colibri_cdiv x y))
+          (colibri_cdiv (colibri_abs_int x) (colibri_abs_int y)))))
+
+(check-sat)
\ No newline at end of file
diff --git a/tests/sat/issue46.smt2 b/tests/sat/issue46.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..0f7d7471c27ac8f013db355d947eb8eeb3dcdaf9
--- /dev/null
+++ b/tests/sat/issue46.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const modes_on Bool)
+
+(declare-const unit_delay_memory Bool)
+
+(assert (not (= (ite (= unit_delay_memory true) true (ite (= modes_on true) false true)) true)))
+
+(check-sat)
\ No newline at end of file