mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

eliminated unused variables

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 17:15:07 +01:00
parent 8f388d83a2
commit a07cba72bc
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/fpa/fpa2bv_approx_tactic.cpp
View file

@ -147,7 +147,6 @@ class fpa2bv_approx_tactic: public tactic {
while (to_traverse.size() > 0) { while (to_traverse.size() > 0) {
cur = to_app(to_traverse.front()); cur = to_app(to_traverse.front());
mpf_rounding_mode rm;
#ifdef Z3DEBUG #ifdef Z3DEBUG
std::cout<<"Analyze - traversing: "<<mk_ismt2_pp(cur,m)<<std::endl; std::cout<<"Analyze - traversing: "<<mk_ismt2_pp(cur,m)<<std::endl;
std::cout.flush(); std::cout.flush();
@ -700,7 +699,6 @@ class fpa2bv_approx_tactic: public tactic {
#ifdef Z3DEBUG #ifdef Z3DEBUG
std::cout<<"Increasing precision:"<<std::endl; std::cout<<"Increasing precision:"<<std::endl;
#endif #endif
mpf_rounding_mode rm;
for(std::list<struct pair *>::iterator itp = ranked_terms.begin(); for(std::list<struct pair *>::iterator itp = ranked_terms.begin();
itp != ranked_terms.end(); itp != ranked_terms.end();
itp++) { itp++) {