mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Eliminated unused variables.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-04 15:22:10 +01:00
parent b20224bc98
commit 32194b3f36
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_model_converter.cpp
View file

@ -179,8 +179,6 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, func_decl * var,
void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
fpa_util fu(m);
bv_util bu(m);
unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)