From b3c36648bf72c368e880a68f8ac6a672e7be5378 Mon Sep 17 00:00:00 2001 From: Jaewoo Kim Date: Fri, 4 Oct 2024 05:11:23 +0000 Subject: [PATCH] Add why3 warning for step size. --- assets/why3/assignment05/README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/assets/why3/assignment05/README.md b/assets/why3/assignment05/README.md index 7d9e695de..3f687d353 100644 --- a/assets/why3/assignment05/README.md +++ b/assets/why3/assignment05/README.md @@ -9,6 +9,7 @@ * You may use [Why3 in your browser](https://www.why3.org/try/). * Clicking `Verify` button at the top will open a panel on the right side. * For each task in the panel (e.g. `loop invariant preservation`), you can right-click it and run the prover. + * Important: The prover might not be able to verify the correct solution if the number of steps is too small. Make sure to test with 1000~5000 steps. * Fill in `TODO`s until the prover can verify all tasks, notified with green check-marks. * To submit your solution, run `./scripts/submit.sh` and submit `assignment05.zip` in the `target` directory to gg.