--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on April 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simplify prover instalation problem



Hi everyone,

I've installed Simplify binary in my ubuntu 14.04 and it seems to be
installed ok:

why3 config --debug autodetect --add-prover simplify /usr/local/bin/simplify
Run : (/usr/local/bin/simplify -version) > /tmp/out432f5e 2>&1
Found prover Simplify version 1.5.4 (old version, please consider
upgrading).
Save config to /home/allberson/.why3.conf

or
$ why3 config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
Found prover CVC4 version 1.1, Ok.
Found prover CVC3 version 2.4.1, Ok.
Found prover Simplify version 1.5.4 (old version, please consider
upgrading).
Found prover Coq version 8.4pl3, Ok.
Warning: prover Z3 version 4.3.2 is not known to be supported.
5 provers detected and 1 provers detected with unsupported version
Save config to /home/allberson/.why3.conf


But every time I want to prove something using it, the vc's proof reach
timeout.

How to solve it?

why3 prove -P simplify -a split_goal_wp --extra-config
/home/allberson/.opam/4.01.0/lib/why/why3/why3.conf insert_sort.mlw
insert_sort.mlw Jessie_program WP_parameter insert_sort_ensures_default :
Timeout (4.96s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_ensures_default :
Timeout (4.99s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_ensures_default :
Timeout (4.94s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_ensures_default :
Timeout (4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_ensures_default :
Timeout (4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.99s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.99s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.97s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.99s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.99s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.96s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)
insert_sort.mlw Jessie_program WP_parameter insert_sort_safety : Timeout
(4.98s)

-- 
Allberson Dantas

[Doutorando em Ci?ncia da Computa??o - UFC]
[Analista de Sistemas do Serpro - Servi?o Federal de Processamento de Dados]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150425/5870db3d/attachment.html>