Commit a960dc7c authored by François Bobot's avatar François Bobot

relativize path for the benchs of frocos

parent e8e0dc51
......@@ -4,8 +4,8 @@ The result of this bench can be reproduce using Why3 in the following way:
- You need to come back to version acbaa9b711b41e10d3815e3 with
git checkout acbaa9b711b41e10d3815e3, and
- You need to configure and install why3.
- After that you should run why3config and set in ~/.why.conf in the
- You need to configure with --enable-local and compile why3.
- After that you should set in ./why.conf in the
section [main] the variable "running_provers_max" to your own
number of core. You need CVC3, Z3 and Yices.
- Run ./gen_allbench.sh generates one file, bench, by possible set of parameters
......
......@@ -4,4 +4,3 @@ Inst_nothing_Kept_nothing_Lskept_nothing_Product_nothing_Kept_twin_Poly_explict
Inst_goal_Kept_goal_Lskept_nothing_Product_some_kept_Kept_twin_Poly_explicit
Inst_nothing_Kept_nothing_Lskept_nothing_Product_nothing_Kept_twin_Poly_deco
Inst_goal_Kept_goal_Lskept_nothing_Product_some_kept_Kept_twin_Poly_deco
......@@ -4,4 +4,3 @@ Inst_nothing_Kept_nothing_Lskept_nothing_Product_nothing_Kept_twin_Poly_explict
Inst_goal_Kept_nothing_Lskept_nothing_Product_some_kept_Kept_twin_Poly_explicit
Inst_nothing_Kept_nothing_Lskept_nothing_Product_nothing_Kept_twin_Poly_deco
Inst_goal_Kept_nothing_Lskept_nothing_Product_some_kept_Kept_twin_Poly_deco
#!/bin/sh
WHY3BENCH="../../bin/why3bench -C why.conf"
echo "With Z3"
for bench in $(cat benchs); do
echo $bench
why3bench -B z3_$bench.rc "$@"
$WHY3BENCH -B z3_$bench.rc $ARGS
echo
done
echo "With CVC3"
for bench in $(cat benchs); do
echo $bench
why3bench -B cvc3_$bench.rc "$@"
$WHY3BENCH -B cvc3_$bench.rc $ARGS
echo
done
echo "With Yices"
for $bench in $(cat benchs_yices); do
echo bench
why3bench -B yices_$bench.rc "$@"
for bench in $(cat benchs_yices); do
echo $bench
$WHY3BENCH -B yices_$bench.rc
echo
done
\ No newline at end of file
[tools @BENCH_NAME@]
prover = "@PROVER@"
timelimit = 60
memlimit = 2048
loadpath = "."
use = "meta.@SELECT_INST@"
use = "meta.@SELECT_KEPT@"
......
[main ]
loadpath = "../../share/theories"
magic = 5
memlimit = 2048
running_provers_max = 7
timelimit = 60
[prover z3]
command = "../../bin/why3-cpulimit %t %m -s z3 -smt2 %f"
driver = "../../share/drivers/z3_smtv2.drv"
editor = ""
name = "Z3"
version = "..."
[prover yices]
command = "../../bin/why3-cpulimit %t %m -s yices -smt %f"
driver = "../../share/drivers/yices.drv"
editor = ""
name = "Yices"
version = "..."
[prover cvc3]
command = "../../bin/why3-cpulimit 0 %m -s cvc3 -timeout %t %f"
driver = "../../share/drivers/cvc3.drv"
editor = ""
name = "CVC3"
version = "..."
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