Require that used model values are constant in CEGQI (#8528)

Fixes #8520.

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index f10e59540cecd88de9f1f42c05f9657314de2db4..50623285d0b42758adc4db4015e8432c4516a3d5 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -643,25 +643,31 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     // - the instantiator uses model values at this effort or
     //   if we are solving for a subfield of a datatype (is_sv), and
     // - the instantiator allows model values.
+    // Furthermore, we only permit the value if it is constant, since the model
+    // may contain internal-only expressions, e.g. RANs.
     if ((options().quantifiers.cegqiMultiInst || !hasTriedInstantiation(pv))
         && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
       Node mv = getModelValue( pv );
-      TermProperties pv_prop_m;
-      Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
-      d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
-      CegInstEffort prev = d_effort;
-      if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
+      if (mv.isConst())
       {
-        // update the effort level to indicate we have used a model value
-        d_effort = CEG_INST_EFFORT_STANDARD_MV;
-      }
-      if (constructInstantiationInc(pv, mv, pv_prop_m, sf))
-      {
-        return true;
+        TermProperties pv_prop_m;
+        Trace("cegqi-inst-debug")
+            << "[4] " << i << "...try model value " << mv << std::endl;
+        d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
+        CegInstEffort prev = d_effort;
+        if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
+        {
+          // update the effort level to indicate we have used a model value
+          d_effort = CEG_INST_EFFORT_STANDARD_MV;
+        }
+        if (constructInstantiationInc(pv, mv, pv_prop_m, sf))
+        {
+          return true;
+        }
+        d_effort = prev;
       }
-      d_effort = prev;
     }
 
     Trace("cegqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index f06d6a91316a6b413cb0bbbdf439693f7f29315a..8fda24a13d7dfd90ed761e69c446ad02e3cb0e68 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2229,6 +2229,7 @@ set(regress_1_tests
   regress1/quantifiers/issue8456-2-syqi-ic.smt2
   regress1/quantifiers/issue8456-syqi-ic.smt2
   regress1/quantifiers/issue8497-syqi-str-fmf.smt2
+  regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2

diff --git a/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 b/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
new file mode 100644 (file)
index 0000000..561e03d
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: poly
+; COMMAND-LINE: --nl-cov
+; EXPECT: unknown
+(set-logic ALL)
+(declare-fun e () Real)
+(assert (forall ((x Real)) (distinct (* e e) (+ 1 (* x x (- 1))))))
+(check-sat)