From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 11 Mar 2010 06:15:32 +0000 (+0000)
Subject: Boolean variables were marked as theory literals by mistake. Fixed, should give us... 
X-Git-Tag: cvc5-1.0.0~9185
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7ccddcad95d7b6534a83a873c522b115530a553;p=cvc5.git

Boolean variables were marked as theory literals by mistake. Fixed, should give us back the SAT performance we had before the theory stuff.
---

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 634ba00d4..a5924a544 100644
--- 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: