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

fix unused-but-set-variable warnings reported in #579

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-18 11:03:31 -07:00
parent 3a6e6df4f5
commit d2622da747
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/mpn.cpp
View file

@ -274,7 +274,7 @@ void mpn_manager::div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom,
bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom, bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
mpn_digit * quot) const { mpn_digit * quot) const {
mpn_double_digit q_hat, temp, r_hat, ms; mpn_double_digit q_hat, temp, ms;
mpn_digit borrow; mpn_digit borrow;
for (size_t j = numer.size()-1; j > 0; j--) { for (size_t j = numer.size()-1; j > 0; j--) {
@ -294,7 +294,7 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
numer[j] = numer[j-1] + denom; numer[j] = numer[j-1] + denom;
} }
TRACE("mpn_div1", TRACE("mpn_div1",
r_hat = temp % (mpn_double_digit) denom; mpn_double_digit r_hat = temp % (mpn_double_digit) denom;
tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat; tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
tout << " ms=" << ms; tout << " ms=" << ms;
tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size()); tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());