Skip to content
Snippets Groups Projects
Commit f4a26236 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[WP] updates json script files

parent 858caa17
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 8 additions and 8 deletions
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+ 2
− 2
View file @ f4a26236
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"verdict": "valid", "time": 0.0072,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0148,
"verdict": "valid", "time": 0.0051,
"steps": 22 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+ 2
− 2
View file @ f4a26236
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"verdict": "valid", "time": 0.0072,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0148,
"verdict": "valid", "time": 0.0051,
"steps": 22 } ] } } ]
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 @ f4a26236
......@@ -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$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0241,
"verdict": "valid", "time": 0.0151,
"steps": 41 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.025,
"verdict": "valid", "time": 0.0147,
"steps": 41 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+ 2
− 2
View file @ f4a26236
......@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0199,
"verdict": "valid", "time": 0.0115,
"steps": 29 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0241,
"verdict": "valid", "time": 0.0117,
"steps": 29 } ] } } ]
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