Boolean variables were marked as theory literals by mistake. Fixed, should give us...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 634ba00d45452c2a6d35c61fe8c71e3dee98ff6d..a5924a54416caa6a83ea4d26bd77721d17cb4f42 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -109,8 +109,9 @@ SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
   Assert(!isCached(node), "atom already mapped!");
 
   Debug("cnf") << "handleAtom(" << node << ")" << endl;
-
-  SatLiteral lit = newLiteral(node, true);
+ 
+   bool theoryLiteral = node.getKind() != kind::VARIABLE;
+   SatLiteral lit = newLiteral(node, theoryLiteral);
 
   switch(node.getKind()) {
   case TRUE: