fdupress Jan 5, 2010 at 3:56 PM Hi all, I am running into a bit of a problem here: in some cases, unwrapping a wrapped structure does not entail that structure's invariants in the resulting state. The code I am working on involves huge numbers of invariants, and I have failed so far to reproduce the problem with a smaller version, so I am not attaching any code, but it would probably help to know if there are cases where such a situation (invariant not holding immediately after unwrap) is possible. Cheers, Francois MarkHillebrand Jan 12, 2010 at 8:50 AM Asserting quantified formulae may sometimes not work "out-of-box" due to trigger / Z3 behavior -- are quantifiers involved in your example? Best, Mark fdupress Jan 18, 2010 at 8:37 AM I indeed have a lot of quantifiers (including a few forall/exists alternations, which is probably the worst thing I could do, from what I understand), and it looks like it is indeed a triggering issue. Thanks for pointing me there, I tend to forget that Z3 is not perfect, and to have way too much confidence in it. Francois fdupress Jan 25, 2010 at 12:25 PM Hi again, list. I finally took the time to look into this matter a bit more, and identified the faulty invariants. Since I cannot get rid of some of them, I investigated further and realised that it might not something I can fix with source-level triggers. The following code is an example of one of the invariants that goes wrong, and more specifically, when it goes wrong:   #include struct preds1 { int dummy; spec(bool P1[mathint];) spec(bool P2[mathint][mathint];) spec(bool P3[mathint];) invariant(forall(mathint a; P1[a] && forall(mathint b; P2[a][b]) ==> P3[a])) }; void testInvInv1(spec(struct preds1 ^P)) requires(inv(P)) { assert(inv(P)); } void testInvInd1(spec(struct preds1 ^P)) requires(inv(P)) { assert(forall(mathint a; P->P1[a] && forall(mathint b; P->P2[a][b]) ==> P->P3[a])); } void testWrappedInv1(spec(struct preds1 ^P)) requires(wrapped(P)) writes(P) { assert(inv(P)); speconly(unwrap(P);) assert(inv(P)); } void testWrappedInd1(spec(struct preds1 ^P)) requires(wrapped(P)) writes(P) { assert(inv(P)); speconly(unwrap(P);) assert(forall(mathint a; P->P1[a] && forall(mathint b; P->P2[a][b]) ==> P->P3[a])); }     ```#include struct preds { int dummy; spec(bool P1[mathint];) spec(bool P2[mathint][mathint];) spec(bool P3[mathint];) invariant(forall(mathint a; P1[a] && forall(mathint b; P2[a][b]) ==> P3[a])) }; void testInv(spec(struct preds ^P)) requires(inv(P)) { assert(inv(P)); // (1) Succeeds``` ```} void testWrapped(spec(struct preds ^P)) requires(wrapped(P)) writes(P) { assert(inv(P)); // (2) Succeeds speconly(unwrap(P);) assert(inv(P)); // (3) Fails } ``` The problem seems to come from the unwrapping, that may indeed cause triggering issues in Z3, but is there anything I can do on the code above itself to make it go through? (without changing the shape of the invariant: I may not be able to do so in all instances of P1, P2 and P3.) fdupress Jan 28, 2010 at 4:47 PM Here is an extra example, with a call to wrap() failing because of the invariant "not holding" when it is asserted both using inv(P) and the actual formula. I guess my question is: what, in the encoding of wrap() and unwrap() (or static_wrap and static_unwrap, since they are the corresponding boogie calls), prevents the triggers that applied previously from being applied?   ```#include struct preds { int dummy; spec(bool P1[mathint];) spec(bool P2[mathint][mathint];) spec(bool P3[mathint];) invariant(forall(mathint a; P1[a] && forall(mathint b; P2[a][b]) ==> P3[a])) }; void test(spec(struct preds ^P)) requires(inv(P)) requires(!closed(P)) writes(P) { assert(inv(P)); assert(forall(mathint a; P->P1[a] && forall(mathint b; P->P2[a][b]) ==> P->P3[a])); speconly(wrap(P);) }``` MarkHillebrand Mar 24, 2011 at 8:25 AM Hi Francois,   this last example can be made working like this: ```#include spec(ispure bool match_mathint(mathint x) returns(true);) struct preds { int dummy; spec(bool P1[mathint];) spec(bool P2[mathint][mathint];) spec(bool P3[mathint];) invariant(forall(mathint a; P1[a] && forall(mathint b; {sk_hack(match_mathint(b))} {match_mathint(b)} P2[a][b]) ==> P3[a])) }; void test(spec(struct preds ^P)) requires(inv(P)) requires(!closed(P)) writes(P) { assert(inv(P)); assert(forall(mathint a; P->P1[a] && forall(mathint b; {sk_hack(match_mathint(b))} {match_mathint(b)} P->P2[a][b]) ==> P->P3[a])); wrap(P); } ```   Hope that helps,   Mark