In order for splitting on demand to be able to retract clauses every translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b9fbd3ce6..16881f9e4 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -77,14 +77,14 @@ void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(node);
+  d_cnfStream->convertAndAssert(node, false, false);
 }
 
 void PropEngine::assertLemma(TNode node) {
   Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as removable
-  d_cnfStream->convertAndAssert(node);
+  d_cnfStream->convertAndAssert(node, false, false);
 }