--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on November 2013 ---
On 08/11/2013 13:26, Virgile Prevosto wrote: > Hello, > > 2013/11/8 Nanci Naomi <nnarai at gmail.com>: > >> 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 > > Rename the file to Simplify or simplify. If I'm not mistaken, why3 > does not search for an executable whose name begins with Simplify, but > is exactly Simplify, With option "--add-prover", why3 does not care about the name of the executable; it only checks that the program has the expected version string. (Just to be sure, I renamed one of my provers 'toto' and it worked fine.) You can pass option "--debug autodetect" in addition to "--add-prover" in order to see which part of the detection failed. Best regards, Guillaume