Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simplify prover instalation problem

  • Subject: [Frama-c-discuss] Simplify prover instalation problem
  • From: allberson85 at gmail.com (Allberson Dantas)
  • Date: Sat, 25 Apr 2015 15:14:32 -0300
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>