Add debug test for sygus subcall verify calls. (#2287)

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 37cfc25f11281a26d627ffecb1cc929d43aaf76b..31a76d9333a13390d064441af624671fdc7a230f 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -433,6 +433,17 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
           d_ce_sk_var_mvs.push_back(mv);
         }
         Trace("cegqi-engine") << std::endl;
+#ifdef CVC4_ASSERTIONS
+        // the values for the query should be a complete model
+        Node squery = query.substitute(d_ce_sk_vars.begin(),
+                                       d_ce_sk_vars.end(),
+                                       d_ce_sk_var_mvs.begin(),
+                                       d_ce_sk_var_mvs.end());
+        Trace("cegqi-debug") << "...squery : " << squery << std::endl;
+        squery = Rewriter::rewrite(squery);
+        Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
+        Assert(squery.isConst() && squery.getConst<bool>());
+#endif
         return;
       }
       else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)