diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index e69ced63f..44f03d99c 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -401,12 +401,6 @@ namespace opt {
             return th.mk_ge(m_fm, v, val);
         }
 
-        if (typeid(smt::theory_rdl) == typeid(opt) &&
-            val.get_infinitesimal().is_zero()) {
-            smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
-            return th.mk_ge(m_fm, v, val);
-        }
-
         if (typeid(smt::theory_rdl) == typeid(opt)) {
             smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
             return th.mk_ge(m_fm, v, val);