From cef27ce318880117e076543a7d8c030da059fc13 Mon Sep 17 00:00:00 2001
From: bruno <bruno.marre@cea.fr>
Date: Thu, 7 Oct 2021 12:42:56 +0200
Subject: [PATCH] ok

---
 tests/sat/issue40_sat.smt2 | 12 ++++++++++++
 tests/sat/issue46.smt2     | 10 ++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 tests/sat/issue40_sat.smt2
 create mode 100644 tests/sat/issue46.smt2

diff --git a/tests/sat/issue40_sat.smt2 b/tests/sat/issue40_sat.smt2
new file mode 100644
index 000000000..a8b76b521
--- /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 000000000..0f7d7471c
--- /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
-- 
GitLab