diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 012661081..c910b3f99 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -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_TRY; - LOG_Z3_mk_fpa_fp(c, sgn, sig, exp); + LOG_Z3_mk_fpa_fp(c, sgn, exp, sig); RESET_ERROR_CODE(); if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) { 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_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(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1083,7 +1083,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); 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); RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 2d1166ee8..cd096d6a5 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -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; if (bu.is_numeral(sgn, rsgn, bvsz_sgn) && - bu.is_numeral(sig, rsig, bvsz_exp) && - bu.is_numeral(exp, rexp, bvsz_sig)) { + bu.is_numeral(sig, rsig, bvsz_sig) && + bu.is_numeral(exp, rexp, bvsz_exp)) { SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); scoped_mpf v(m_fm);