--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on November 2013 ---
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