1 2 3 4 5
// RUN: %boogie -proverWarnings:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" type bv; type bv16;