simplify_exprt::bits2expr is now independent of bitvector representation

kroening · kroening · commit c6baef2a94e0 · 2018-10-18T14:41:04.000+01:00
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -1458,7 +1458,9 @@ exprt simplify_exprt::bits2expr(
       tmp[i]=bits[map.map_bit(i)];
 
     std::reverse(tmp.begin(), tmp.end());
-    return constant_exprt(tmp, type);
+
+    mp_integer i = binary2integer(tmp, false);
+    return constant_exprt(integer2bv(i, bits.size()), type);
   }
   else if(type.id()==ID_c_enum)
   {

Original file line number	Diff line number	Diff line change
`@@ -1458,7 +1458,9 @@ exprt simplify_exprt::bits2expr(`
`1458`	`1458`	`tmp[i]=bits[map.map_bit(i)];`
`1459`	`1459`
`1460`	`1460`	`std::reverse(tmp.begin(), tmp.end());`
`1461`		`- return constant_exprt(tmp, type);`
	`1461`	`+`
	`1462`	`+ mp_integer i = binary2integer(tmp, false);`
	`1463`	`+ return constant_exprt(integer2bv(i, bits.size()), type);`
`1462`	`1464`	`}`
`1463`	`1465`	`else if(type.id()==ID_c_enum)`
`1464`	`1466`	`{`