From 02b7f980b03c10fafa3f6085583fda7d1214110f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Aug 2014 08:18:07 -0700 Subject: [PATCH] fix(library/num): bug in to_pos_num, missing test Signed-off-by: Leonardo de Moura --- src/library/num.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/library/num.cpp b/src/library/num.cpp index 231ada991..665944b46 100644 --- a/src/library/num.cpp +++ b/src/library/num.cpp @@ -54,12 +54,14 @@ expr from_num(mpz const & n) { optional to_pos_num(expr const & e) { if (e == g_one) { return some(mpz(1)); - } else if (app_fn(e) == g_bit0) { - if (auto r = to_pos_num(app_arg(e))) - return some(2*(*r)); - } else if (app_fn(e) == g_bit1) { - if (auto r = to_pos_num(app_arg(e))) - return some(2*(*r) + 1); + } else if (is_app(e)) { + if (app_fn(e) == g_bit0) { + if (auto r = to_pos_num(app_arg(e))) + return some(2*(*r)); + } else if (app_fn(e) == g_bit1) { + if (auto r = to_pos_num(app_arg(e))) + return some(2*(*r) + 1); + } } return optional(); }