janhaag/PSE2011 — Issue #13: Empty programs are always correct in runtime checker
Author: danielbruns
Created: 2012-02-15 10:36:59+00:00
State: open

Try the following program. Verification fails, right so. But letting it run does not report the failed postcondition.
main (){}
ensure false;