Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 51ae695cf..a245eb469 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -359,6 +359,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
     }
 
     if(somethingChanged) {
+
       rewrite = nodeManager->mkNode(node.getKind(), newChildren);
       nodeManager->setAttribute(node, IteRewriteAttr(), rewrite);
       return rewrite;
@@ -399,7 +400,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
   case AND:
     return handleAnd(node);
   default:
-    return handleAtom(handleNonAtomicNode(node));
+    {
+      Node atomic = handleNonAtomicNode(node);
+      AlwaysAssert(isCached(atomic) || atomic.isAtomic());
+      return toCNF(atomic);
+    }
   }
 }