From 823fe6df074d568432592fc0ca85abf88f849d18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Aug 2013 10:41:00 -0700
Subject: [PATCH] Move test from lean.cpp

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/numerics/mpq.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/tests/util/numerics/mpq.cpp b/src/tests/util/numerics/mpq.cpp
index 2507f9582..ca09f1db5 100644
--- a/src/tests/util/numerics/mpq.cpp
+++ b/src/tests/util/numerics/mpq.cpp
@@ -9,6 +9,12 @@ Author: Leonardo de Moura
 #include "mpq.h"
 using namespace lean;
 
+static void tst0() {
+    lean::mpq n1("10000000000000000000000000000000000000000");
+    lean::mpq n2(317, 511);
+    std::cout << n1*n2 << "\n";
+}
+
 static void tst1() {
     mpq a(2,3), b(4,3);
     b = a / b;
@@ -128,6 +134,7 @@ static void tst5() {
 }
 
 int main() {
+    tst0();
     tst1();
     tst2();
     tst3();