mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

prevent usage that mixes E/e notation with division / for numerals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-02 23:58:52 -07:00
parent 47b81d2ec0
commit fbb01f3699
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/mpq.cpp
View file

@ -235,6 +235,9 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
SASSERT(str[0] - '0' <= 9); SASSERT(str[0] - '0' <= 9);
exp = (10*exp) + (str[0] - '0'); 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;); TRACE("mpq_set", tout << "[exp]: " << exp << ", str[0]: " << (str[0] - '0') << std::endl;);
++str; ++str;
} }