diff --git a/tests/sat/issue_45.smt2 b/tests/sat/issue_45.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..3ba8848a0e2135ffe926e1795c1ba259df321654
--- /dev/null
+++ b/tests/sat/issue_45.smt2
@@ -0,0 +1,32 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+
+
+(declare-const x Float32)
+
+(declare-const y Float32)
+
+(declare-const z Float32)
+
+;; Assume
+(assert (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) x))
+
+;; Assume
+(assert (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) y))
+
+;; Assume
+(assert (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) z))
+
+;; Assume
+(assert (fp.leq x (fp #b0 #b10010111 #b00000000000000000000000)))
+
+;; Assume
+(assert (fp.leq y (fp #b0 #b10010111 #b00000000000000000000000)))
+
+
+(assert
+  (not (= (ite (fp.lt (fp.neg (fp.mul RNE x y)) z) true false) true)))
+
+(check-sat)