diff options
Diffstat (limited to 'src/preprocessing/passes/theory_preprocess.cpp')
-rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 641cab162..2f9d12637 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -44,19 +44,17 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; - std::vector<TrustNode> newAsserts; - std::vector<Node> newSkolems; - TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems); + std::vector<SkolemLemma> newAsserts; + TrustNode trn = propEngine->preprocess(assertion, newAsserts); if (!trn.isNull()) { // process assertions->replaceTrusted(i, trn); } - Assert(newSkolems.size() == newAsserts.size()); - for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + for (const SkolemLemma& lem : newAsserts) { - imap[assertions->size()] = newSkolems[j]; - assertions->pushBackTrusted(newAsserts[j]); + imap[assertions->size()] = lem.d_skolem; + assertions->pushBackTrusted(lem.d_lemma); } } |