From c7489b25e3e50437785e7b739288475e4cdc8626 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Aug 2018 15:57:45 -0500 Subject: [PATCH] Add debug test for sygus subcall verify calls. (#2287) --- src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) 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& 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()); +#endif return; } else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) -- 2.30.2