WP now supports terminates

a45a5957 · Allan Blanchard · Virgile Prevosto · 66133a7b · a45a5957 · a45a5957
Commit a45a5957 authored 3 years ago by Allan Blanchard Committed by Virgile Prevosto 3 years ago
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -3,11 +3,6 @@
 Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/bugs/term.cpp:11: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:17: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:43: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:26: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:34: Warning: Terminates not implemented yet (skipped).
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_Z2m2_ensures : Valid
 [wp] [Qed] Goal typed_Z2m3_c_ensures : Valid

--- a/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json
+++ b/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json
+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0194,
+  "steps": 14 }
--- a/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json
+++ b/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json
+{ "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" }