Fixing failures in minisat

1 files changed, 6 insertions, 18 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 5d88a9240..5f8eb12b9 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -94,12 +94,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 }
 
 Node CnfStream::getNode(const SatLiteral& literal) {
-  Node node;
   NodeCache::iterator find = d_nodeCache.find(literal);
-  if(find != d_nodeCache.end()) {
-    node = find->second;
-  }
-  return node;
+  Assert(find != d_nodeCache.end());
+  return find->second;
 }
 
 SatLiteral CnfStream::convertAtom(TNode node) {
@@ -121,20 +118,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
   return lit;
 }
 
-SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) {
+SatLiteral CnfStream::getLiteral(TNode node) {
   TranslationCache::iterator find = d_translationCache.find(node);
-  SatLiteral literal;
-  if(create) {
-    if(find == d_translationCache.end()) {
-      literal = convertAtom(node);
-    } else {
-      literal = find->second;
-    }
-  } else {
-    Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
-    literal = find->second;
-  }
-  Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl;
+  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+  SatLiteral literal = find->second;
+  Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
 }