Empty ADT causes "unsoundness"

[JonasAlaif]

The following fails to verify:

adt Test {}
method foo() {
  refute false
}

This is not an unsoundess per-se, but rather a imo surprising meaning of empty (uninhabitable) adt definitions. What I would expect is that if I have a x: Test then I can prove false, but not that I immediately get false from just defining such a type. I think we should either change the encoding or at least report a warning in such a case.

[marcoeilers]

Fixed in PR #696 by adding a consistency check that forbids empty ADTs (since they're never useful and cause the problem you described).