diff options
Diffstat (limited to 'src/preprocessing/passes/miplib_trick.cpp')
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index f64fce118..3a8bbdb70 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -522,8 +522,10 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node n = Rewriter::rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); - PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); - + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(n, Node::null()); + } SubstitutionMap nullMap(&fakeContext); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions status = te->solve(geq, nullMap); @@ -591,9 +593,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( Debug("miplib") << " " << newAssertion << endl; assertionsToPreprocess->push_back(newAssertion); - PROOF(ProofManager::currentPM()->addDependence(newAssertion, - Node::null())); - + 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(); |