Dear Claude,
thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
(couldn’t find opam upgrade to 1.2.0!)
Now I’m facing a new problem with strange ‘ghost’ error.
-
module AAA
use list.List
use map.Map
let rec set_1000 (s : list 'a)(f : map 'a int) =
Dear JJ,
As you remark, Why3 0.88 is now quite outdated and my answer may not be
very accurate. As far as I remember, the former "Inline" button was
applying the transformation "inline_goal" which has the effect of
inlining the defined function symbols appearing in an outermost position
in
