5 files changed, 22 insertions, 22 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c063245a5..bb6dfe40b 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -516,7 +516,7 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_PLUS &&
          res.size() == 0);
 
@@ -537,7 +537,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
 
 
 void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_SUB &&
          node.getNumChildren() == 2 &&
          bits.size() == 0);
@@ -555,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
   
   Bits a;
@@ -633,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 }
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UDIV &&  q.size() == 0);
 
   Bits a, b;
@@ -649,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UREM &&  rem.size() == 0);
 
   Bits a, b;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index a5a9b9a7e..24d6b300b 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bv_subtheory_eq_bitblast.cpp
+/*! \file bv_subtheory_bitblast.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: dejan
+ ** Original author: dejan
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 0a8f046b7..324921f9a 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bv_subtheory_eq_bitblast.h
+/*! \file bv_subtheory_bitblast.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: dejan
+ ** Original author: dejan
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 8cbf99ae9..005be88a8 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_bv_rewrite_rules_core.h
+/*! \file theory_bv_rewrite_rules_constant_evaluation.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Major contributors: barrett
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 506570ed2..48df9492d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_bv_rewrite_rules_core.h
+/*! \file theory_bv_rewrite_rules_operator_elimination.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Major contributors: barrett
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -65,7 +65,7 @@ bool RewriteRule<SgtEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SgtEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);