Simplifier does not modify out-of-bounds access

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

Author: kroening

src/solvers/flattening/boolbv_index.cpp

@@ -339,6 +339,12 @@ void boolbvt::convert_index(
      offset+width<=mp_integer(tmp.size()))
   {
     // in bounds
+
+    // Expression simplification should remove these cases
+    assert(array.id()!=ID_array_of &&
+           array.id()!=ID_array);
+    // If not there are large improvements possible as above
+
     for(unsigned i=0; i<width; i++)
       bv[i]=tmp[integer2long(offset+i)];
   }