diff options
Diffstat (limited to 'src/preprocessing/passes/quantifiers_preprocess.cpp')
| -rw-r--r-- | src/preprocessing/passes/quantifiers_preprocess.cpp | 5 |
1 files changed, 3 insertions, 2 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") |