From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Aug 2018 20:57:45 +0000 (-0500)
Subject: Add debug test for sygus subcall verify calls. (#2287)
X-Git-Tag: cvc5-1.0.0~4798
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7489b25e3e50437785e7b739288475e4cdc8626;p=cvc5.git

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 37cfc25f1..31a76d933 100644
--- 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)