fix for non-byte operands

kroening · kroening · commit cd0e4f23c039 · 2014-06-02T22:09:27.000Z
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3908 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -29,6 +29,9 @@ Function: map_bv
 
 bvt map_bv(const endianness_mapt &map, const bvt &src)
 {
+  // don't do anything for a byte or less
+  if(src.size()<=8) return src;
+
   assert(map.size()*8==src.size());
 
   bvt result;

Original file line number	Diff line number	Diff line change
`@@ -29,6 +29,9 @@ Function: map_bv`
`29`	`29`
`30`	`30`	`bvt map_bv(const endianness_mapt &map, const bvt &src)`
`31`	`31`	`{`
	`32`	`+ // don't do anything for a byte or less`
	`33`	`+ if(src.size()<=8) return src;`
	`34`	`+`
`32`	`35`	`assert(map.size()*8==src.size());`
`33`	`36`
`34`	`37`	`bvt result;`