summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes/ite_simp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes/ite_simp.cpp')
-rw-r--r--src/preprocessing/passes/ite_simp.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 9a6a8ec61..388c5742d 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -16,7 +16,6 @@
#include <vector>
-#include "options/proof_options.h"
#include "smt/smt_statistics_registry.h"
#include "smt_util/nary_builder.h"
#include "theory/arith/arith_ite_utils.h"
@@ -118,7 +117,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
// This pass does not support dependency tracking yet
// (learns substitutions from all assertions so just
// adding addDependence is not enough)
- if (options::unsatCores() || options::fewerPreprocessingHoles())
+ if (options::unsatCores())
{
return true;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback