mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

Bugfix for FP API

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-04 21:01:01 +00:00
parent 677ff221f8
commit 05b29df2cb
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_fpa.cpp
View file

@ -268,7 +268,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig) { Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_fp(c, sgn, sig, exp); LOG_Z3_mk_fpa_fp(c, sgn, exp, sig);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) { if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
@ -1072,7 +1072,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) { Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_to_fp_int_real(c, rm, sig, exp, s); LOG_Z3_mk_fpa_to_fp_int_real(c, rm, exp, sig, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil(); fpa_util & fu = ctx->fpautil();
@ -1083,7 +1083,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp)); expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(exp), to_expr(sig));
ctx->save_ast_trail(a); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a)); RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);

4
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -760,8 +760,8 @@ br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & res
unsigned bvsz_sgn, bvsz_exp, bvsz_sig; unsigned bvsz_sgn, bvsz_exp, bvsz_sig;
if (bu.is_numeral(sgn, rsgn, bvsz_sgn) && if (bu.is_numeral(sgn, rsgn, bvsz_sgn) &&
bu.is_numeral(sig, rsig, bvsz_exp) && bu.is_numeral(sig, rsig, bvsz_sig) &&
bu.is_numeral(exp, rexp, bvsz_sig)) { bu.is_numeral(exp, rexp, bvsz_exp)) {
SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); SASSERT(mpzm.is_one(rexp.to_mpq().denominator()));
SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); SASSERT(mpzm.is_one(rsig.to_mpq().denominator()));
scoped_mpf v(m_fm); scoped_mpf v(m_fm);