diff options
Diffstat (limited to 'src/preprocessing/passes/miplib_trick.cpp')
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 4ed2aede9..0bb386697 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -180,6 +180,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Assert(assertionsToPreprocess->getRealAssertionsEnd() == assertionsToPreprocess->size()); Assert(!options::incrementalSolving()); + Assert(!options::unsatCores()); context::Context fakeContext; TheoryEngine* te = d_preprocContext->getTheoryEngine(); @@ -527,10 +528,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node n = Rewriter::rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, Node::null()); - } TrustSubstitutionMap tnullMap(&fakeContext, nullptr); CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get(); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions @@ -599,11 +596,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( Debug("miplib") << " " << newAssertion << endl; assertionsToPreprocess->push_back(newAssertion); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(newAssertion, - Node::null()); - } Debug("miplib") << " assertions to remove: " << endl; for (vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); |