Le 21/05/2019 à 09:48, Raphael Rieu-Helft a écrit :
Dear Evgeny,
With the following change to your program, both invariants are proved
instantly by Alt-Ergo. The reason why the invariants are true is that
the contents of the matrix above the diagonal are unchanged. My change
makes this explicit. In general, as a user I prefer doing this kind of
change to fiddling with the auto strategies. I don't really understand
why the change is needed for the second invariant but not the first.
As always with SMT solvers, it is just a matter of triggers. The first
invariant contains "j + d", which the SMT solvers turn into a trigger
that then matches the goal. The second invariant does not. That is why
the first invariant is proved automatically, while the second is not.
By making the second invariant stronger, you are giving a new
opportunity for a useful trigger. Similarly, when Evgeny unfolds the
definition of "get" by inlining, SMT solvers also generate a useful trigger.
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
