// Here, since we first do an unconditional assignment inside the 
// transaction, the value of b[0] should be reverted back to 
// that assigned value

\javaSource "code/";

\withOptions transactions:transactionsOn,transactionAbort:abortOn,intRules:arithmeticSemanticsIgnoringOF;

\programVariables {
  MyClass self;
}

\problem {
javacard.framework.JCSystem._transactionDepth = 0 &
!self = null & !self.b = null & self.b.length = 2 
& self.b.<transient> = 0 ->
\<{
   self.b[0] = 0;
   javacard.framework.JCSystem.beginTransaction();
     javacard.framework.Util.arrayFillNonAtomic(self.b, (short)0, (short)1, (byte)2);
     self.b[0] = 3;
   javacard.framework.JCSystem.abortTransaction();
}\> (self.b[0] = 2)

}