Frama-C-discuss mailing list archives

x_cui at hotmail.com (Xiao-lei Cui) · Thu, 14 Nov 2013 20:52:23 -0500

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>