--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on January 2011 ---
Dear all, I have Frama-C Boron and Why 2.26 installed (Mac OSX binaries ) on Mac OSX and everything seems to work very well. However it appears that I have an issue with GWhy because it does not detect some provers. There are few different things that happen: 1. I have a translator for a small language called CAO, which translates CAO programs into Jessie input language. Running jessie tool on the output of my CAO2Jessie translator and using the makefile that Jessie generates to run GWhy, the CVC3 (version 2.1) prover works very well and it seems to be detected by Gwhy. 2. On the other hand, running the Jessie plugin (using Frama-C > frama-c -jessie ex.c) on a C file, seems that the CVC3 is not detected by Gwhy. 3. I also have Z3 installed and it seems that Gwhy does not detect it in any case. However, when running why-config, both CVC3 and Z3 are detected. 4. Both provers work very well when they are called directly, e.g.: make -f ex.makefile z3 Does anyone has any idea of what is going wrong? Should I change some configuration file?! It is very helpful to have all the provers working properly on GWhy. Thanks in advance. Best regards, B?rbara Vieira