diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index eaafc298f..08d4cd50a 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1278,12 +1278,14 @@ public:
 #endif
     }
 
-    z3::expr z3_fp_val(long double value, const std::string &name) {
+    z3::expr z3_fp_val(long double value, std::string name) {
 #if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
         (void)name;
         return context.fpa_val(static_cast<double>(value));
 #else
         (void)value;
+        while (name.size() > 1 && (name.back() == 'f' || name.back() == 'F' || name.back() == 'l' || name.back() == 'L'))
+            name.erase(name.size() - 1);
         return context.real_val(name.c_str());
 #endif
     }
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 06b3eae34..3ea4d2b99 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -102,6 +102,7 @@ private:
         TEST_CASE(floatValue1);
         TEST_CASE(floatValue2);
         TEST_CASE(floatValue3);
+        TEST_CASE(floatValue4);
 
         TEST_CASE(functionCall1);
         TEST_CASE(functionCall2);
@@ -827,6 +828,13 @@ private:
         ASSERT_EQUALS(expected, expr(code, ">"));
     }
 
+    void floatValue4() {
+        const char code[] = "void foo(float f) { return f > 12.3f; }";
+        const char expected[] = "(> $1 12.3)\n"
+                                "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"));