--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on November 2013 ---
Hello, We have problem with the MAC OS version of simplify. The simplify binary file was in the /private/var/root/.opam/4.01.0/bin directory with the other provers (alt-ergo, cvc3, z3, gappa, yices, coq) The command why3config --detect-provers shows all the provers, but simplify. As suggested by David we moved the simplify binary file to /usr/local/bin. The command why3config --add-prover simplify /usr/local/bin/Simplify-1.5.4.macosx shows the following error: Error: File /usr/local/bin/Simplify-1.5.4.macosx does not correspond to the prover id simplify How to solve it? Best regards Nanci Naomi ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Treat the Earth well. It was not given to you by your parents, it was loaned to you by your children. (Kenyan proverb) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ On Fri, Nov 8, 2013 at 5:31 AM, David MENTRE <dmentre at linux-france.org>wrote: > 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 > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131108/b9ded529/attachment.html>