summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes/theory_preprocess.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes/theory_preprocess.cpp')
-rw-r--r--src/preprocessing/passes/theory_preprocess.cpp7
1 files changed, 0 insertions, 7 deletions
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 90a4b8240..1eb21cd96 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -20,7 +20,6 @@
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
#include "prop/prop_engine.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
@@ -58,12 +57,6 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
{
imap[assertions->size()] = newSkolems[j];
assertions->pushBackTrusted(newAsserts[j]);
- // new assertions have a dependence on the node (old pf architecture)
- if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
- {
- ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
- assertion);
- }
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback