diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/quantifiers_preprocess.cpp | 5 | ||||
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 7 |
2 files changed, 9 insertions, 3 deletions
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index 3052e9629..cda7ad67a 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -39,9 +39,10 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( for (size_t i = 0; i < size; ++i) { Node prev = (*assertionsToPreprocess)[i]; - Node next = quantifiers::QuantifiersRewriter::preprocess(prev); - if (next != prev) + TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev); + if (!trn.isNull()) { + Node next = trn.getNode(); assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-preprocess") diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d44321a35..82515c6a4 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -24,6 +24,7 @@ using namespace std; using namespace CVC4::kind; +using namespace CVC4::theory; namespace CVC4 { namespace preprocessing { @@ -135,7 +136,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, if (pas.getKind() == FORALL) { // preprocess the quantified formula - pas = theory::quantifiers::QuantifiersRewriter::preprocess(pas); + TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas); + if (!trn.isNull()) + { + pas = trn.getNode(); + } Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl; } if (pas.getKind() == FORALL) |