--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on November 2013 ---
Hi David, I have alt-ergo prover installed (version 0.93). It is fast and efficient. I also installed Simplify-1.5.4 recently, but it is timed out for almost every proof obligation. Eventhough I set the timeout limit to 10 seconds, still it cannot prove anything. Not sure what went wrong:) cheers, xiaolei > From: abiao.yang at gmail.com > Date: Mon, 11 Nov 2013 10:03:12 +0000 > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] adding new provers to why3 > > Hi, xiao lei, > > I suggest you also to install the Alt-Ergo prover. > > It seems that the Alt-Ergo prover is really fast... > > -david > > On 11 November 2013 02:20, Xiao-lei Cui <x_cui at hotmail.com> wrote: > > Hello David, > > Thanks for the tip. I copied the simplify-executable to usr/local/bin/ > > as you suggested. And renamed that file to "simplify" as Virgile said in > > another thread. It is working well now. It seems why3 cannot recognize > > namings like Simplify-1.5.5.linux. > > > > cuix at berkhoff:~/Downloads/why3-0.81$ why3config --add-prover simplify > > /usr/local/bin/simplify > > cuix at berkhoff:~/Downloads/why3-0.81$ why3config --detect-proversFound prover > > Alt-Ergo version 0.93 (it is an old version that is less tested than the > > current one). > > > > Found prover CVC3 version 2.4.1, Ok. > > Found prover Simplify version 1.5.4 (it is an old version that is less > > tested than the current one). > > Found prover Coq version 8.3pl4, Ok. > > 4 provers detected and 0 provers detected with unsupported version > > Save config to /home/cuix/.why3.conf > > > > cheers, > > xiaolei > > > >> From: dmentre at linux-france.org > >> Date: Fri, 8 Nov 2013 08:31:45 +0100 > >> To: frama-c-discuss at lists.gforge.inria.fr > >> Subject: Re: [Frama-c-discuss] adding new provers to why3 > > > >> > >> Hello Xiao-lei, > >> > >> 2013/11/8 Xiao-lei Cui <x_cui at hotmail.com>: > >> > I am trying to add Simplify-1.5.4 to why3 prover list. > >> > I copied Simplify-1.5.4.linux to /usr/sbin/ directory, and run the > >> > commands as it follows: > >> > >> The prover should be in your regular user PATH. I doubt /usr/sbin/ is > >> in your PATH (it is a special path for administrators). I would put > >> the Simplify binary into /usr/local/bin/. The general habit is to > >> never put anything outside /usr/local/. > >> > >> > cuix at berkhoff:~/Downloads/why3-0.81$ why3config --add-prover simplify > >> > /usr/sbin/Simplify-1.5.4.linux > >> > Found prover Simplify version 1.5.4 (it is an old version that is less > >> > tested than the current one). > >> > Save config to /home/cuix/.why3.conf > >> > >> What print "why3 --list-provers" after that step? > >> > >> > cuix at berkhoff:~/Downloads/why3-0.81$ why3config --detect-provers > >> > Found prover Alt-Ergo version 0.93 (it is an old version that is less > >> > tested > >> > than the current one). > >> > Found prover CVC3 version 2.4.1, Ok. > >> > Found prover Coq version 8.3pl4, Ok. > >> > 3 provers detected and 0 provers detected with unsupported version > >> > Save config to /home/cuix/.why3.conf > >> > >> Option --detect-provers re-initialize your /home/cuix/.why3.conf > >> configuration file, therefore I guess your previous --add-prover > >> configuration is lost. > >> > >> Best regards, > >> david > >> > > > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131114/bb117528/attachment-0001.html>