diff options
Diffstat (limited to 'src/preprocessing/passes/sygus_inference.cpp')
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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) |