diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle index 75a043ab71e0d4b5392bd12ecf2d3fe42a05f8b8..4b93bf2cdabc14eb1c5cafcdce5977f539c35468 100644 --- 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 diff --git a/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json b/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json new file mode 100644 index 0000000000000000000000000000000000000000..ffb25c4ba1ed769df3b84f1d0f9878d0f6555548 --- /dev/null +++ b/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0194, + "steps": 14 } diff --git a/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json b/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json new file mode 100644 index 0000000000000000000000000000000000000000..8256dcea1bc441f80e5f1bc5ffc9ee590a0285ed --- /dev/null +++ b/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" }