From ef0c5838612b7095522520fe9c91ae48f6c20708 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 9 Sep 2021 09:50:00 +0200
Subject: [PATCH] Tests issue #40 with hypothesis

---
 tests/sat/issue_40_with_hyp.smt2 | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 tests/sat/issue_40_with_hyp.smt2

diff --git a/tests/sat/issue_40_with_hyp.smt2 b/tests/sat/issue_40_with_hyp.smt2
new file mode 100644
index 000000000..811fde090
--- /dev/null
+++ b/tests/sat/issue_40_with_hyp.smt2
@@ -0,0 +1,9 @@
+(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)
-- 
GitLab