Do not insist on bound values being constant in arithmetic instantiation (#3643)

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 0a3775807..2984c23be 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -236,9 +236,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
           // since the quantifier-free arithmetic solver may pass full
           // effort with no lemmas even when we are not guaranteed to have a
           // model. By convention, we use GEQ to compare the values here.
+          // It also may be the case that cmp is non-constant, in the case
+          // where lhs or rhs contains a transcendental function. We consider
+          // the bound to be an upper bound in this case.
           Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value);
           cmp = Rewriter::rewrite(cmp);
-          Assert(cmp.isConst());
           is_upper = !cmp.isConst() || !cmp.getConst<bool>();
         }
       }
@@ -466,8 +468,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
               cmp_bound = Rewriter::rewrite(cmp_bound);
               // Should be comparing two constant values which should rewrite
               // to a constant. If a step failed, we assume that this is not
-              // the new best bound.
-              Assert(cmp_bound.isConst());
+              // the new best bound. We might not be comparing constant
+              // values (for instance if transcendental functions are
+              // involved), in which case we do update the best bound value.
               if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>())
               {
                 new_best = false;