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>
- Prev by Date: [Frama-c-discuss] Fwd: Jessie umbound symbol problem
- Next by Date: [Frama-c-discuss] Frama-C Jessie, stdlib.h
- Previous by thread: [Frama-c-discuss] Fwd: Jessie umbound symbol problem
- Next by thread: [Frama-c-discuss] Frama-C Jessie, stdlib.h
- Index(es):