cleanup

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1055 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -490,7 +490,8 @@ Function: boolbvt::convert_symbol
 
 void boolbvt::convert_symbol(const exprt &expr, bvt &bv)
 {
-  unsigned width=boolbv_width(expr.type());
+  const typet &type=expr.type();
+  unsigned width=boolbv_width(type);
 
   bv.resize(width);
 
@@ -502,7 +503,7 @@ void boolbvt::convert_symbol(const exprt &expr, bvt &bv)
   if(width==0)
   {
     // just put in map
-    map.get_map_entry(identifier, expr.type());
+    map.get_map_entry(identifier, type);
   }
   else
   {

src/solvers/flattening/boolbv_map.cpp

@@ -90,14 +90,15 @@ literalt boolbv_mapt::get_literal(
   map_entryt &map_entry=get_map_entry(identifier, type);
 
   assert(bit<map_entry.literal_map.size());
+  map_bitt &mb=map_entry.literal_map[bit];
 
-  if(map_entry.literal_map[bit].is_set)
-    return map_entry.literal_map[bit].l;
+  if(mb.is_set)
+    return mb.l;
 
   literalt l=prop.new_variable();
 
-  map_entry.literal_map[bit].is_set=true;
-  map_entry.literal_map[bit].l=l;
+  mb.is_set=true;
+  mb.l=l;
 
   #ifdef DEBUG
   std::cout << "NEW: " << identifier << ":" << bit
@@ -130,14 +131,15 @@ void boolbv_mapt::set_literal(
 
   map_entryt &map_entry=get_map_entry(identifier, type);
   assert(bit<map_entry.literal_map.size());
+  map_bitt &mb=map_entry.literal_map[bit];
 
-  if(map_entry.literal_map[bit].is_set)
+  if(mb.is_set)
   {
-    prop.set_equal(map_entry.literal_map[bit].l, literal);
+    prop.set_equal(mb.l, literal);
     return;
   }
 
-  map_entry.literal_map[bit].is_set=true;
-  map_entry.literal_map[bit].l=literal;
+  mb.is_set=true;
+  mb.l=literal;
 }
 

src/solvers/flattening/bv_utils.cpp

@@ -680,10 +680,8 @@ literalt bv_utilst::overflow_negate(const bvt &bv)
   // a overflow on unary- can only happen with the smallest
   // representable number 100....0
 
-  bvt zeros;
-
-  for(unsigned i=0; i<bv.size()-1; i++)
-    zeros.push_back(bv[i]);
+  bvt zeros(bv);
+  zeros.erase(--zeros.end());
 
   return prop.land(bv[bv.size()-1], prop.lnot(prop.lor(zeros)));
 }