mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Remove duplicate initialization of a sort variable.

Browse source
This commit is contained in:
Bruce Mitchener 2018-11-30 23:12:55 +07:00
parent bcfa8045fa
commit c51caad5ad
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_bv.cpp
View file

@ -1083,7 +1083,6 @@ namespace smt {
for (unsigned i = 0; i <= num_args; i++) {
expr* arg = (i == num_args)?n:n->get_arg(i);
sort* s = get_manager().get_sort(arg);
s = get_manager().get_sort(arg);
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) {
if (!m_approximates_large_bvs) {
TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";);