From d418467089b139a5087d8006624d13de04b96b54 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Feb 2020 08:26:13 -0800 Subject: [PATCH] can't validate when benchmarks use strict bounds Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 23caf8d93..26bfd0414 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1654,7 +1654,8 @@ namespace opt { case O_MINIMIZE: case O_MAXIMIZE: { inf_eps n = m_optsmt.get_lower(obj.m_index); - if (m_optsmt.objective_is_model_valid(obj.m_index) && + if (false && // theory_lra doesn't produce infinitesimals + m_optsmt.objective_is_model_valid(obj.m_index) && n.get_infinity().is_zero() && n.get_infinitesimal().is_zero() && is_numeral((*m_model)(obj.m_term), r1)) {