8 files changed, 16 insertions, 14 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index d568f8c1f..007378528 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Tianyi Liang
+ ** Minor contributors (to current version): Kshitij Bansal, Tianyi Liang
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
index d867ef7fa..8097220ad 100644
--- a/test/unit/theory/stacking_map_black.h
+++ b/test/unit/theory/stacking_map_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index c99c66fff..58bbe7a2b 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -103,6 +103,7 @@ public:
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
+    d_smt->setOption("incremental", false);
     d_ctxt = d_smt->d_context;
     d_uctxt = d_smt->d_userContext;
     d_scope = new SmtScope(d_smt);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 4644d3385..bafd572c3 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index 4999ec3d4..eed173366 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -21,7 +21,8 @@
 #include "theory/theory.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-#include "theory/bv/eager_bitblaster.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/bitblaster_template.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "context/context.h"
@@ -59,7 +60,7 @@ public:
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
     d_smt->setOption("bitblast", SExpr("eager"));
-    d_bb = new EagerBitblaster();
+    d_bb = new EagerBitblaster(NULL);
     
   }
   void tearDown() {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index e32e49801..7440de350 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: Dejan Jovanovic
  ** Minor contributors (to current version): Andrew Reynolds, Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 3259381ad..08447b86d 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: Tim King
  ** Minor contributors (to current version): Dejan Jovanovic, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index 4e80b7d20..3dcb2db85 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **