--- layout: fc_discuss_archives title: Message 103 from Frama-C-discuss on November 2013 ---
Hi xiao-lei, I also installed Simplify under Nanci Naomi's instructions: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-November/004083.html "why3config --debug autodetect --add-prover simplify /usr/local/bin/simplify" I used it to verify some of those examples in this website: http://proval.lri.fr/gallery/jessieplugin.en.html It seems simplify works fine for me. What kind of code you try to prove? What happened if you increase the value of timeout to a bigger one? Regards, -david On 15 November 2013 01:52, Xiao-lei Cui <x_cui at hotmail.com> wrote: > 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 > > _______________________________________________ > 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