9 files changed, 34 insertions, 25 deletions
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 00ebc8b8d..df7e263d2 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,18 +18,18 @@
 
 #include <string>
 
-#include "expr/node_value.h"
+#include "base/cvc4_assert.h"
+#include "expr/attribute.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
-#include "expr/node.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
-#include "util/cvc4_assert.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 727abe984..040bd7161 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -21,7 +21,7 @@
 
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "util/exception.h"
+#include "base/exception.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index b70c51276..a83e53780 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -19,9 +19,10 @@
 #include <sstream>
 #include <string>
 
+#include "base/exception.h"
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "util/exception.h"
+#include "smt/smt_options_handler.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -31,6 +32,7 @@ class ExprPublic : public CxxTest::TestSuite {
 private:
 
   Options opts;
+  smt::SmtOptionsHandler* d_handler;
 
   ExprManager* d_em;
 
@@ -53,10 +55,12 @@ public:
 
   void setUp() {
     try {
+      d_handler = new smt::SmtOptionsHandler(NULL);
+
       char *argv[2];
       argv[0] = strdup("");
       argv[1] = strdup("--output-language=ast");
-      opts.parseOptions(2, argv);
+      opts.parseOptions(2, argv, d_handler);
       free(argv[0]);
       free(argv[1]);
 
@@ -98,6 +102,7 @@ public:
       delete c_bool_and;
       delete b_bool;
       delete a_bool;
+      delete d_handler;
 
       delete d_em;
     } catch(Exception e) {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 7d6ee523a..3a24057b2 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -25,6 +25,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node.h"
+#include "smt/smt_options_handler.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -34,6 +35,7 @@ class NodeBlack : public CxxTest::TestSuite {
 private:
 
   Options opts;
+  smt::SmtOptionsHandler* d_handler;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
   TypeNode* d_booleanType;
@@ -42,10 +44,13 @@ private:
 public:
 
   void setUp() {
+#warning "TODO: Discuss the effects of this change with Clark."
+    d_handler = new smt::SmtOptionsHandler(NULL);
+
     char *argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-language=ast");
-    opts.parseOptions(2, argv);
+    opts.parseOptions(2, argv, d_handler);
     free(argv[0]);
     free(argv[1]);
 
@@ -59,6 +64,7 @@ public:
     delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;
+    delete d_handler;
   }
 
   bool imp(bool a, bool b) const {
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 9bac0d818..a7ebea2fe 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -20,12 +20,12 @@
 #include <limits.h>
 #include <sstream>
 
-#include "expr/node_builder.h"
+#include "base/cvc4_assert.h"
 #include "expr/convenience_node_builders.h"
-#include "expr/node_manager.h"
-#include "expr/node.h"
 #include "expr/kind.h"
-#include "util/cvc4_assert.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
 #include "util/rational.h"
 
 using namespace CVC4;
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index b94e6a691..781829e36 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -21,9 +21,8 @@
 
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
-
-#include "util/rational.h"
 #include "util/integer.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::expr;
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index aaa3256dd..fa44b837a 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,9 +19,8 @@
 #include <string>
 
 #include "expr/node_manager.h"
-
-#include "util/rational.h"
 #include "util/integer.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::expr;
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 8a68db269..594a981c8 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -18,11 +18,11 @@
 
 #include <string>
 
-#include "expr/node_value.h"
+#include "base/cvc4_assert.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
-#include "util/cvc4_assert.h"
+#include "expr/node_value.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 2acd1ebae..2b26ad745 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -19,13 +19,13 @@
 #include <sstream>
 #include <string>
 
+#include "base/cvc4_assert.h"
+#include "base/exception.h"
 #include "context/context.h"
-#include "expr/symbol_table.h"
-#include "expr/expr_manager.h"
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/symbol_table.h"
 #include "expr/type.h"
-#include "util/cvc4_assert.h"
-#include "util/exception.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;