summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes/non_clausal_simp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes/non_clausal_simp.cpp')
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp6
1 files changed, 0 insertions, 6 deletions
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index d88e901d7..921442f0e 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -69,12 +69,6 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
PreprocessingPassResult NonClausalSimp::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
- || isProofEnabled())
- << "Unsat cores with non-clausal simp only supported with new proofs. "
- "Cores mode is "
- << options::unsatCoresMode() << "\n";
-
d_preprocContext->spendResource(Resource::PreprocessStep);
theory::booleans::CircuitPropagator* propagator =
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback