diff --git a/tests/sat/bug_43.smt2 b/tests/sat/bug_43.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..2905988c9f797998f9bf72ea3de88c14c8868d98
--- /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)