--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on April 2015 ---
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>