From 8b4e1c120993d34357764e5e02145332a7078d7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Aug 2018 18:13:26 -0700 Subject: [PATCH] fix #1793 Signed-off-by: Nikolaj Bjorner --- src/api/api_numeral.cpp | 5 ++--- src/tactic/arith/card2bv_tactic.cpp | 6 +++--- src/util/mpq.cpp | 4 ++++ 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 2b77294d5..2891e8cc4 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -68,11 +68,10 @@ extern "C" { ('/' == *m) || ('-' == *m) || (' ' == *m) || ('\n' == *m) || ('.' == *m) || ('e' == *m) || - ('E' == *m) || + ('E' == *m) || ('+' == *m) || (is_float && (('p' == *m) || - ('P' == *m) || - ('+' == *m))))) { + ('P' == *m))))) { SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr); RETURN_Z3(nullptr); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 97649cc2f..65b8d8bf3 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -80,10 +80,10 @@ public: } expr_ref_vector fmls(m); rw2.flush_side_constraints(fmls); - for (unsigned i = 0; !g->inconsistent() && i < fmls.size(); ++i) { - g->assert_expr(fmls[i].get()); + for (expr* e : fmls) { + g->assert_expr(e); } - + func_decl_ref_vector const& fns = rw2.fresh_constants(); if (!fns.empty()) { generic_model_converter* filter = alloc(generic_model_converter, m, "card2bv"); diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index 207614ee0..b126f4c5d 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -230,6 +230,10 @@ void mpq_manager::set(mpq & a, char const * val) { exp_sign = true; ++str; } + else if (str[0] == '+') { + exp_sign = false; + ++str; + } while (str[0]) { if ('0' <= str[0] && str[0] <= '9') { SASSERT(str[0] - '0' <= 9);