diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 1f08c0332..ebd7c00c5 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -788,6 +788,10 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
     const Data *data = dynamic_cast<Data *>(dataBase);
     if (data->constraints.empty())
         return true;
+    if (MathLib::isFloat(name)) {
+        float f = MathLib::toDoubleNumber(name);
+        return value >= f - 0.00001 && value <= f + 0.00001;
+    }
 #ifdef USE_Z3
     // Check the value against the constraints
     ExprData exprData;
@@ -797,7 +801,7 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
         for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
             solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
-        solver.add(e == value);
+        solver.add(e >= value && e <= value);
         return solver.check() != z3::unsat;
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
@@ -817,6 +821,8 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
     const Data *data = dynamic_cast<Data *>(dataBase);
     if (data->constraints.empty())
         return true;
+    if (MathLib::isFloat(name))
+        return value > MathLib::toDoubleNumber(name);
 #ifdef USE_Z3
     // Check the value against the constraints
     ExprData exprData;
@@ -846,6 +852,8 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
     const Data *data = dynamic_cast<Data *>(dataBase);
     if (data->constraints.empty())
         return true;
+    if (MathLib::isFloat(name))
+        return value < MathLib::toDoubleNumber(name);
 #ifdef USE_Z3
     // Check the value against the constraints
     ExprData exprData;
diff --git a/test/verify/juliet.py b/test/verify/juliet.py
index a313c0082..8c34554ed 100644
--- a/test/verify/juliet.py
+++ b/test/verify/juliet.py
@@ -61,8 +61,7 @@ def check(tc:str, warning_id:str):
 
 
 final_report = ''
-final_report += check('C/testcases/CWE369_Divide_by_Zero/s*/*_int_*.c', 'verificationDivByZero')
-#final_report += check('C/testcases/CWE476_*/*.c', 'verificationNullPointerDereference')
+final_report += check('C/testcases/CWE369_Divide_by_Zero/s*/*.c', 'verificationDivByZero')
 
 print(final_report)