// This example 2 from Chapter 9 of the KeY book, NOTE it's not provable

\javaSource "code/";

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

\programVariables { MyClass o; }

\problem {

!o = null & o.x + o.y = 100 ->
\[[{
   de.uka.ilkd.key.javacard.KeYJCSystem.jvmBeginTransaction();
     o.x = 60;
     o.y = 40;
   de.uka.ilkd.key.javacard.KeYJCSystem.jvmCommitTransaction();
   int t = o.x;
   o.x = o.y;
   o.y = t;
}\]] (o.x + o.y = 100)

}