Merging CAV14 paper bit-vector work.

1 files changed, 0 insertions, 6 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 47d352949..3d2c29798 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -228,12 +228,6 @@ SatLiteral CnfStream::convertAtom(TNode node) {
     theoryLiteral = true;
     canEliminate = false;
     preRegister = true;
-
-    if (options::bitvectorEagerBitblast() && theory::Theory::theoryOf(node) == theory::THEORY_BV) {
-      // All BV atoms are treated as boolean except for equality
-      theoryLiteral = false;
-      canEliminate = true;
-    }
   }
 
   // Make a new literal (variables are not considered theory literals)