On 08/25/2017 06:38 PM, Andrei Paskevich wrote: > normally, when r is a larger term, it is abstracted via a let-in: let > z = r in mk_record ..., and the let-in terms are not inlined for the > SMT solvers.
Hi Andrei, thanks for your quick reply. Indeed, I also noticed the optimization using let-in when having a look at the code in the type checker, but for some reason, no such let-in terms are introduced, or they get eliminated by some other transformation. The trouble with let-in expressions is that you almost always have to unfold them in order to be able to prove anything meaningful about them, at least in Isabelle, which I have used for my application :-( > Could you please share an example of input, where > the blowup happens? That's a bit difficult, since the blowup occurred in some large Why3 file generated by gnatprove. I'll try to send you the files off-list next week. Do you have an idea how I could tweak my contract_record_updates transformation, so that the introduced update function symbols end up in the right theories? Greetings, Stefan _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
