Revision 4174a469
Added by Guillaume Davy over 8 years ago
| tcm_benchmarks/ALT2/ALT2_proof/makefile | ||
|---|---|---|
| 1 | 1 |
NAME=ALT_2.lustrec |
| 2 | 2 |
NODE=AltitudeControl |
| 3 | 3 |
PAR=1 |
| 4 |
LAUNCHPROVER=-wp-prover CVC4,alt-ergo,z3,coq |
|
| 4 |
LAUNCHPROVER=-wp-prover CVC3,CVC4,alt-ergo,z3,coq
|
|
| 5 | 5 |
ARGS=$(NAME).c -wp-par $(PAR) -wp-rte -wp-model ref -wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" -wp-script $(NAME).coq -wp-no-let |
| 6 | 6 |
gen: |
| 7 | 7 |
make -C ../../../ |
Also available in: Unified diff
Correct some problem related to new bool encoding