Test/test15/NullInModel.bpl


1
2
3
4
5
6
7

// RUN: %boogie -printModel:2 %s > %t
// RUN: %diff %s.expect %t
procedure M (s: ref) {
  assert s != null;
}
type ref;
const null: ref;