summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r--src/prop/cnf_stream.cpp5
1 files changed, 3 insertions, 2 deletions
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback