Commit 6c1e5397 authored by François Bobot's avatar François Bobot

cpu_limit : a new_cpu_limit which print the time spent in the prover.

parent b6131a75
......@@ -622,18 +622,22 @@ clean::
# tools
#######
TOOLS = bin/why3-cpulimit
TOOLS = bin/why3-cpulimit bin/why3-cpulimit_time
byte opt: $(TOOLS)
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
$(CC) -Wall -o $@ $^
bin/why3-cpulimit_time: src/tools/@CPULIMIT@_time.c
$(CC) -Wall -o $@ $^
clean::
rm -f bin/why3-cpulimit src/tools/*~
install_no_local::
cp -f bin/why3-cpulimit $(BINDIR)
cp -f bin/why3-cpulimit_time $(BINDIR)
########
# bench
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.smt"
valid "unsat"
unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.sx"
valid "\\bValid\\b"
unknown "\\bInvalid\\b" "Unknown"
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -21,7 +21,7 @@ version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.2"
version_old = "2.1"
command = "why3-cpulimit 0 %m %e -timeout %t -lang smt %f 2>&1"
command = "why3-cpulimit_time 0 %m %e -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"
[ATP yices]
......@@ -67,7 +67,7 @@ version_switch = "-version"
version_regexp = "Simplify version \\([^ \n,]+\\)"
version_ok = "1.5.5"
version_ok = "1.5.4"
command = "why3-cpulimit %t %m %e %f 2>&1"
command = "why3-cpulimit_time %t %m %e %f 2>&1"
driver = "drivers/simplify.drv"
[ATP spass]
......@@ -96,7 +96,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
command = "why3-cpulimit %t %m %e -smt %f 2>&1"
command = "why3-cpulimit_time %t %m %e -smt %f 2>&1"
driver = "drivers/z3.drv"
[ITP coq]
......
Markdown is supported
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