speed up construction of values for large bitvector types

This commit improves the complexity of boolbvt::get(...) from quadratic to
linear.  The difference is noticeable when using very large bitvectors,
e.g., for encoding unions with large array members.

E.g., the time taken for regression/cbmc/union/union_large_array.c when using
--cprover-smt2 improves from 12s to 0.2s.

Author: kroening

regression/cbmc/bounds_check1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-z3-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$

regression/cbmc/union/union_large_array.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-z3-smt-backend
 union_large_array.c
 
 ^EXIT=10$

src/solvers/flattening/boolbv_get.cpp

@@ -199,8 +199,8 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
   const std::size_t width = boolbv_width(type);
   PRECONDITION(bv.size() >= offset + width);
 
-  // most significant bit first
   std::string value;
+  value.reserve(width);
 
   for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
   {
@@ -214,9 +214,13 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
     }
     // clang-format on
 
-    value=ch+value;
+    value += ch;
   }
 
+  // The above collects bits starting with the least significant bit,
+  // but we need the most significant bit first.
+  std::reverse(value.begin(), value.end());
+
   switch(bvtype)
   {
   case bvtypet::IS_UNKNOWN: