bug with exceptions

bench/bench

@@ -113,13 +113,18 @@ test_prover () {
     fi
 }
 
+echo "=== Checking drivers ==="
+drivers drivers
+echo ""
+
+echo "=== Checking valid goals ==="
+valid_goals bench/valid
+echo ""
 
-# 1. Syntax
 echo "=== Parsing good files  ==="
 goods bench/typing/bad --parse-only
 echo ""
 
-# 2. Typing
 echo "=== Type-checking bad files ==="
 bads bench/typing/bad --type-only
 echo ""
@@ -150,12 +155,10 @@ programs bench/programs/good
 programs examples/programs
 echo ""
 
-echo "=== Checking drivers ==="
-drivers drivers
-echo ""
-
-echo "=== Checking valid goals ==="
-valid_goals bench/valid
+echo "=== VC generation on good programs ==="
+pgml_options=
+programs bench/programs/good
+programs examples/programs
 echo ""
 
 echo "=== Checking provers ==="

bench/programs/good/exceptions.mlw

+exception Break
+
+let f (n : int) : int  =
+  { true }
+  let i = ref n in 
+  try
+    while (!i > 0) do
+      invariant { true }
+      variant { !i }
+      if (!i <= 10) then raise Break;
+      i := !i - 1
+    done
+  with Break -> ()
+  end;
+  !i
+  { result <= 10 }