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;