Merge branch '1.3.x'

Conflicts:
	NEWS

2 files changed, 21 insertions, 4 deletions

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 7f6385d36..4a9d73cb7 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -30,6 +30,8 @@ using namespace std;
 class ExprPublic : public CxxTest::TestSuite {
 private:
 
+  Options opts;
+
   ExprManager* d_em;
 
   Expr* a_bool;
@@ -51,7 +53,14 @@ public:
 
   void setUp() {
     try {
-      d_em = new ExprManager;
+      char *argv[2];
+      argv[0] = strdup("");
+      argv[1] = strdup("--output-language=ast");
+      opts.parseOptions(2, argv);
+      free(argv[0]);
+      free(argv[1]);
+
+      d_em = new ExprManager(opts);
 
       a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
@@ -61,7 +70,7 @@ public:
       fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
       fun_op = new Expr(d_em->mkVar("f", *fun_type));
       d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
-      null = new Expr;
+      null = new Expr();
 
       i1 = new Expr(d_em->mkConst(Rational("0")));
       i2 = new Expr(d_em->mkConst(Rational(23)));
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 8e8263fe7..6cf85fb7e 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -34,6 +34,7 @@ using namespace std;
 class NodeBlack : public CxxTest::TestSuite {
 private:
 
+  Options opts;
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
@@ -43,8 +44,15 @@ private:
 public:
 
   void setUp() {
-    d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt, NULL);
+    char *argv[2];
+    argv[0] = strdup("");
+    argv[1] = strdup("--output-language=ast");
+    opts.parseOptions(2, argv);
+    free(argv[0]);
+    free(argv[1]);
+
+    d_ctxt = new Context();
+    d_nodeManager = new NodeManager(d_ctxt, NULL, opts);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());