diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 6d597ec1c5e..f6438834896 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -660,17 +660,16 @@ void boolbvt::print_assignment(std::ostream &out) const out << pair.first << "=" << pair.second.get_value(prop) << '\n'; } -void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest) +boolbvt::offset_mapt boolbvt::build_offset_map(const struct_typet &src) { - const struct_typet::componentst &components= - src.components(); - - dest.resize(components.size()); - std::size_t offset=0; - for(std::size_t i=0; i offset_mapt; - void build_offset_map(const struct_typet &src, offset_mapt &dest); + offset_mapt build_offset_map(const struct_typet &src); // strings numbering string_numbering; diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 838c8df84ac..724b59b6a78 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -530,10 +530,8 @@ bool boolbvt::type_conversion( op_struct.components(); // build offset maps - offset_mapt op_offsets, dest_offsets; - - build_offset_map(op_struct, op_offsets); - build_offset_map(dest_struct, dest_offsets); + const offset_mapt op_offsets = build_offset_map(op_struct); + const offset_mapt dest_offsets = build_offset_map(dest_struct); // build name map typedef std::map op_mapt;