Skip to content
Snippets Groups Projects
Commit 58aebd88 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[qed+wp] fix typo in inductive types for native coq

parent 42cff6de
No related branches found
No related tags found
No related merge requests found
...@@ -4,8 +4,9 @@ ...@@ -4,8 +4,9 @@
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 1 goal scheduled [wp] 1 goal scheduled
[wp] [Failed] Goal typed_foo_assert_ko [wp] [Alt-Ergo 2.0.0] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1 [wp] Proved goals: 0 / 1
Alt-Ergo 2.0.0: 0 (unsuccess: 1)
[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2471.0.report.json' [wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2471.0.report.json'
[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.0.report.json' [wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 1. }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment