Hi Claude,
Thank you for your answer and explanations.
On 28.04.2020 12:23, Claude Marche wrote:
Le 27/04/2020 à 15:47, margarita.capretto a écrit :
Dear colleagues,
We have another issue while using CVC4 to prove some simple code in
WhyML.
For example, for the following code
use int.Int
use list.ListRich
use string.OCaml
predicate post (n: int) (result: int) =
result = 3*n
let f (n: int) : int =
ensures { post n result }
3*n
Why3 shows that the output for CVC4 is
====================> Prover: CVC4 1.7 (counterexamples)
Unknown (sat)
Counterexample suggested by the prover:
File int.mlw:
Line 409:
max_int = {int63'int => 4611686018427387903 (0x3FFFFFFFFFFFFFFF)}
Line 411:
min_int = {int63'int => -4611686018427387904
(-0x4000000000000000)}
File invalid-counterexample.mlw:
Line 10:
n = 0 (0x0)
Line 11:
n = 0 (0x0)
We looked to the input generated by Why3 for CVC4 and it check-sat in
three
different points (two in the middle and one at the end).
This is the case only when looking for counterexamples.
When we pass this
input to CVC4 it returns "sat" for the first two checks and "unsat"
for the
last one, therefore proving that the VC is valid.
Yes, this is the rare situation when, while looking for a CE, the
prover solves the VC.
One clarification, even though in this case CVC4 proves the VC, the
result showed by Why3 is "Unknown (sat)" and the counterexample
suggested corresponds to an intermediate check point.
If we don't use the string.OCaml library we can prove it in Why3 using
CVC4.
The new string theory is raising issues with CVC4. In the master
branch of dev of Why3, the uses of strings by CVC4 is available only
in a CVC4 "alternative".
Hopefully future releases of CVC4 will have those issues fixed.
Of course the main advice is : don't use string.Ocaml if you don't need
it.
The input generated by Why3 for CVC4 in this case is similar to the
previous
one (only removes some assertions related with strings) and the output
generated by CVC4 is also similar to the one in the previous case,
only differ in the models produced.
We will appreciate if someone can help us understand why in the first
case Why3 says that the output for CVC4 is "unknown" and not "valid"
as in the second case.
Not sure I understand the question: if the input file is different,
even slightly, why would you think the answer must be the same ?
If you think : "If I give a prover more things in the context, but
these things are not needed, the prover will answer the same" then you
are simply wrong.
Don't hesitate to ask more questions, we will try to answer our best.
Maybe an extra advice : use more provers. CVC4 and Z3 and Alt-Ergo is
a minimum. I recommend E prover too, it sometimes nicely solves VCs
which are not solved by others.
- Claude
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
