1 files changed, 2 insertions, 16 deletions
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 7ace55c0a..656822299 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -66,7 +66,8 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult NonClausalSimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(!options::unsatCores());
+  Assert(!options::unsatCores() || isProofEnabled())
+      << "Unsat cores with non-clausal simp only supported with new proofs";
 
   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
@@ -111,13 +112,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
     // If in conflict, just return false
     Trace("non-clausal-simplify")
         << "conflict in non-clausal propagation" << std::endl;
-    Assert(!options::unsatCores());
     assertionsToPreprocess->clear();
     assertionsToPreprocess->pushBackTrusted(conf);
-    if (options::unsatCores())
-    {
-      ProofManager::currentPM()->addDependence(conf.getNode(), Node::null());
-    }
     propagator->setNeedsFinish(true);
     return PreprocessingPassResult::CONFLICT;
   }
@@ -177,14 +173,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         // If the learned literal simplifies to false, we're in conflict
         Trace("non-clausal-simplify")
             << "conflict with " << learned_literals[i].getNode() << std::endl;
-        Assert(!options::unsatCores());
         assertionsToPreprocess->clear();
         Node n = NodeManager::currentNM()->mkConst<bool>(false);
         assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
-        if (options::unsatCores())
-        {
-          ProofManager::currentPM()->addDependence(n, Node::null());
-        }
         propagator->setNeedsFinish(true);
         return PreprocessingPassResult::CONFLICT;
       }
@@ -216,14 +207,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         // If in conflict, we return false
         Trace("non-clausal-simplify")
             << "conflict while solving " << learnedLiteral << std::endl;
-        Assert(!options::unsatCores());
         assertionsToPreprocess->clear();
         Node n = NodeManager::currentNM()->mkConst<bool>(false);
         assertionsToPreprocess->push_back(n);
-        if (options::unsatCores())
-        {
-          ProofManager::currentPM()->addDependence(n, Node::null());
-        }
         propagator->setNeedsFinish(true);
         return PreprocessingPassResult::CONFLICT;
       }