From 1fca76b0a12ac1a543d9f397c38539b90e640029 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Jul 2019 08:26:23 -0700 Subject: [PATCH] relax restriction on infinitesimal for rdl, #2410 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 6 ------ 1 file changed, 6 deletions(-) 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(opt); - return th.mk_ge(m_fm, v, val); - } - if (typeid(smt::theory_rdl) == typeid(opt)) { smt::theory_rdl& th = dynamic_cast(opt); return th.mk_ge(m_fm, v, val);