From 4a570503808007f8f31a11b298d3d91fb8cd4a32 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Jan 2013 15:26:48 -0800
Subject: [PATCH] Fix rcf test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/test/rcf.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/rcf.cpp b/src/test/rcf.cpp
index 5bef0dfef..d6cfd8b86 100644
--- a/src/test/rcf.cpp
+++ b/src/test/rcf.cpp
@@ -32,7 +32,7 @@ static void tst1() {
 #endif
 
     scoped_rcnumeral eps(m);
-    m.mk_infinitesimal("eps", eps);
+    m.mk_infinitesimal(eps);
     mpq aux;
     qm.set(aux, 1, 3);
     m.set(a, aux);
@@ -151,7 +151,7 @@ static void tst_denominators() {
     scoped_rcnumeral eps(m);
     m.mk_pi(a);
     m.inv(a);
-    m.mk_infinitesimal("eps", eps);
+    m.mk_infinitesimal(eps);
     t = (a - eps*2) / (a*eps + 1);
     // t = t + a * 2;
     scoped_rcnumeral n(m), d(m);