diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 08d4cd50a..753fd0582 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1155,6 +1155,14 @@ public:
         auto op1 = getExpr(b->op1);
         auto op2 = getExpr(b->op2);
 
+        // floating point promotion
+        if (b->binop != "&&" && b->binop != "||" && b->binop != "<<" && b->binop != ">>") {
+            if (z3_is_fp(op1) || z3_is_fp(op2)) {
+                z3_to_fp(op1);
+                z3_to_fp(op2);
+            }
+        }
+
         if (b->binop == "+")
             return op1 + op2;
         if (b->binop == "-")
@@ -1298,6 +1306,13 @@ public:
 #endif
     }
 
+    int floatSymbol = 0;
+    void z3_to_fp(z3::expr &e) {
+        if (e.is_int())
+            // TODO: Is there a better way to promote e?
+            e = z3_fp_const("f" + std::to_string(++floatSymbol));
+    }
+
     z3::expr z3_int_val(int128_t value) {
 #if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
         return context.int_val(int64_t(value));
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 3ea4d2b99..469a16a6a 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -103,6 +103,7 @@ private:
         TEST_CASE(floatValue2);
         TEST_CASE(floatValue3);
         TEST_CASE(floatValue4);
+        TEST_CASE(floatValue5);
 
         TEST_CASE(functionCall1);
         TEST_CASE(functionCall2);
@@ -835,6 +836,12 @@ private:
         ASSERT_EQUALS(expected, expr(code, ">"));
     }
 
+    void floatValue5() { // float < int
+        const char code[] = "void foo(float f) { if (f < 1){} }";
+        const char expected[] = "(< $1 f1)\n" // TODO: The "f1" should be something like (float)1
+                                "z3::sat\n";
+        ASSERT_EQUALS(expected, expr(code, "<"));
+    }
 
     void functionCall1() {
         ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));