Commit fead0320 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] use only command-line provers when replaying scripts

parent dff46c11
......@@ -130,7 +130,8 @@ struct
let tree env = env.tree
let play env res =
let play env prv res =
List.mem prv env.provers &&
if VCS.is_valid res then env.valid else env.failed
let progress env msg = env.progress (ProofEngine.main env.tree) msg
......@@ -332,7 +333,7 @@ let rec crawl env on_child node = function
| Prover( prv , res ) :: alternative ->
begin
let task =
if Env.play env res then
if Env.play env prv res then
let wpo = Env.goal env node in
let config = VCS.configure res in
Env.prove env wpo ~config prv
......
......@@ -8,14 +8,14 @@
"occur": 0,
"target": "(to_uint64 (2*x_1))",
"pattern": "to_uint64.2$x" },
"children": { "In-Range": [ { "prover": "CVC4:1.7",
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
"time": 0.04,
"steps": 9937 } ],
"No-Overflow": [ { "prover": "CVC4:1.7",
"time": 4.6879,
"steps": 46 } ],
"No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
"time": 0.05,
"steps": 9890 } ] } } ],
"time": 4.8895,
"steps": 47 } ] } } ],
"Value 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
......@@ -23,14 +23,14 @@
"occur": 0,
"target": "(to_uint64 (a_1*b_1))",
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "CVC4:1.7",
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
"time": 0.03,
"steps": 8691 } ],
"No-Overflow": [ { "prover": "CVC4:1.7",
"time": 4.7487,
"steps": 40 } ],
"No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
"time": 1.15,
"steps": 65987 } ] } } ],
"time": 4.7716,
"steps": 183 } ] } } ],
"Value 1": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
......@@ -38,14 +38,14 @@
"occur": 0,
"target": "(to_uint64 (a_1*b_1))",
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "CVC4:1.7",
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
"time": 0.04,
"steps": 8794 } ],
"No-Overflow": [ { "prover": "CVC4:1.7",
"time": 4.7262,
"steps": 44 } ],
"No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
"time": 0.33,
"steps": 54186 } ] } } ],
"time": 4.7611,
"steps": 221 } ] } } ],
"Upper 1": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 6.2835,
"steps": 48 } ] } } ]
Supports Markdown
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