From ca81e803cbd2524741be48ea9d27d1cb647842dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 21:33:42 +0000 Subject: [PATCH] Bugfix for Z3_fpa_get_numeral_sign. Relates to #570. --- src/api/api_fpa.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index a039de63c..8e122ff01 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -909,6 +909,10 @@ extern "C" { Z3_TRY; LOG_Z3_fpa_get_numeral_sign(c, t, sgn); RESET_ERROR_CODE(); + if (sgn == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());