From c15f229cfdb7b9a3da21522f957a674b731b943a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 14 Sep 2021 14:34:33 +0200
Subject: [PATCH] Add regression tests for issue 43

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

diff --git a/tests/sat/bug_43.smt2 b/tests/sat/bug_43.smt2
new file mode 100644
index 000000000..2905988c9
--- /dev/null
+++ b/tests/sat/bug_43.smt2
@@ -0,0 +1,20 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(define-fun in_range1 ((x Int)) Bool (and (<= (- 2147483648) x) (<= x 2147483647)))
+
+(declare-const x Int)
+
+(define-fun res () Int (- x (colibri_cdiv (- (* 2 x) 1) 2)))
+
+;; Ensures
+  (assert (in_range1 res))
+
+;; H
+  (assert (<= 0 x))
+
+(assert
+;; defqtvc
+ ;; File "arithmetic.adb", line 291, characters 0-0
+  (not (= res 0)))
+(check-sat)
-- 
GitLab