--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on April 2016 ---
Em 2016-04-05 04:26, Loïc Correnson escreveu: >> //@ assert A3: v[i] == \at( v[i], Pre ); > > The \at( _ , Pre ) scope applies also to variable i, which is > undefined in pre-state and different from \at( i , Here ). > L. Oh, indeed... I'm sorry I didn't realize that myself, but I'm happy everything works now. Thanks a lot! --Pablo.