--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] z3 failure




On 10/09/2013 05:00 AM, Stephen Siegel wrote:
> I am happy to assume that the inputs to the function are not NaNs (Jessie's default interpretation), so the contract should hold, right?

Yes

>  Then it is just a question of why Z3 can't prove it.  Is there a way to see the actual query that is submitted to Z3 (or any other prover)?

select the corresponding line of the tree view of why3ide, then click on
"Edit" button. The file sent to Z3 will show up in your selected editor.

> As to Claude's comment that he has seen many VCs that Z3 could not discharge, I have seen this too, but only when using Frama-C+Jessie+Why.   When I have used Z3, CVC3, etc., by hand, it is usually the opposite -- Z3 wins.  Also Z3 wins many competitions. 

I recommend to be very cautious when drawing conclusions from such
"competitions". Moreover, as far as I know, the AUFNIRA category of the
SMT competition was not run for several years now.

> So it makes me wonder if there is a problem in the way the translation to Z3 is done. 

Sure there could be problems in that translation, and volunteers to
investigate are warmly welcome, this is not a trivial task, and a
time-consuming one. I assure that the Why3 developers do want to provide
the most powerful usage of external provers as possible.

> If it is really a shortcoming of Z3, it would be interesting to understand why.

I agree.

- Claude