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

4 files changed, 21 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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 176eb0bf8..418670fa6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1786,8 +1786,10 @@ set(regress_1_tests
   regress1/sygus/issue3514.smt2
   regress1/sygus/issue3507.smt2
   regress1/sygus/issue3580.sy
+  regress1/sygus/issue3633.smt2
   regress1/sygus/issue3634.smt2
   regress1/sygus/issue3635.smt2
+  regress1/sygus/issue3648.smt2
   regress1/sygus/issue3654.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
diff --git a/test/regress/regress1/sygus/issue3633.smt2 b/test/regress/regress1/sygus/issue3633.smt2
new file mode 100644
index 000000000..564a50cca
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3633.smt2
@@ -0,0 +1,6 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () Real)
+(assert (distinct a (sin 2)))
+(check-sat)
diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2
new file mode 100644
index 000000000..e7b7547c4
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3648.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference --no-check-models
+(set-logic ALL)
+(declare-fun a () Real)
+(assert (> a 0.000001))
+(assert (< (- (sin 1) a) 0.000001))
+(check-sat)