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

[wp] scripts cleanup

parent 5b0b8ae4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 22 additions and 22 deletions
src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+ 4
− 4
View file @ 4b054873
......@@ -10,8 +10,8 @@
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
"children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid",
"time": 0.0205,
"steps": 14 } ],
"time": 0.021,
"steps": 12 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
"params":
......@@ -27,6 +27,6 @@
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid",
"time": 0.0201,
"steps": 14 } ] } } ],
"time": 0.0189,
"steps": 12 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+ 1
− 1
View file @ 4b054873
......@@ -3,7 +3,7 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.1131,
"verdict": "valid", "time": 0.0876,
"steps": 51 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+ 1
− 1
View file @ 4b054873
......@@ -3,7 +3,7 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.1131,
"verdict": "valid", "time": 0.0876,
"steps": 51 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+ 2
− 2
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.7529,
"steps": 75 } ],
"verdict": "valid", "time": 0.8178,
"steps": 88 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+ 3
− 3
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.0324,
"verdict": "valid", "time": 0.0318,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.4933,
"steps": 404 } ] } } ]
"verdict": "valid", "time": 0.562,
"steps": 414 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+ 2
− 2
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.5313,
"steps": 65 } ],
"verdict": "valid", "time": 0.6393,
"steps": 63 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+ 2
− 2
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.4321,
"steps": 57 } ],
"verdict": "valid", "time": 0.4508,
"steps": 55 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+ 2
− 2
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.4321,
"steps": 57 } ],
"verdict": "valid", "time": 0.4508,
"steps": 55 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+ 3
− 3
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.0324,
"verdict": "valid", "time": 0.0318,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.4933,
"steps": 404 } ] } } ]
"verdict": "valid", "time": 0.562,
"steps": 414 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+ 2
− 2
View file @ 4b054873
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid", "time": 0.3617,
"steps": 72 } ],
"verdict": "valid", "time": 0.3477,
"steps": 70 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment