From fbb01f369959cfd35ea16495bf64c96728376353 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Oct 2014 23:58:52 -0700
Subject: [PATCH] prevent usage that mixes E/e notation with division / for
 numerals

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/mpq.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp
index eda937029..df4d207a6 100644
--- a/src/util/mpq.cpp
+++ b/src/util/mpq.cpp
@@ -235,6 +235,9 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
                     SASSERT(str[0] - '0' <= 9);
                     exp = (10*exp) + (str[0] - '0');
                 }
+                else if ('/' == str[0]) {
+                    throw default_exception("mixing rational/scientific notation");
+                }
                 TRACE("mpq_set", tout << "[exp]: " << exp << ", str[0]: " << (str[0] - '0') << std::endl;);
                 ++str;
             }