Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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