Added Rational constructors that only take a numerator. The const char* Rational and Integer constructors are now explicit. This means that 'Integer = 3;' and so on are no longer permitted. This closes bug 121.

2 files changed, 3 insertions, 3 deletions

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 0e1e09178..6ff2b64e0 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -167,13 +167,13 @@ public:
 
 
   void testMkConstInt() {
-    Integer i = "3";
+    Integer i("3");
     Node n = d_nodeManager->mkConst(i);
     TS_ASSERT_EQUALS(n.getConst<Integer>(),i);
   }
 
   void testMkConstRat() {
-    Rational r = "3/2";
+    Rational r("3/2");
     Node n = d_nodeManager->mkConst(r);
     TS_ASSERT_EQUALS(n.getConst<Rational>(),r);
   }
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index af38c790b..7f0115922 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -48,7 +48,7 @@ public:
   }
 
   void testMkConstInt() {
-    Integer i = "3";
+    Integer i("3");
     Node n = d_nm->mkConst(i);
     Node m = d_nm->mkConst(i);
     TS_ASSERT_EQUALS(n.getId(), m.getId());