// This is an example from p.500 (the buggy version of the program)

// To obtain a (partial) proof for this problem:
//
// With KeY 1.2
// ============
//
// Use the DefOps arithmetics strategy.
//
//
// With KeY version prior to 1.2
// =============================
//
// Apart from the obvious bug in the program, there is one difficulty in
// doing the proof: reasoning about the Java division. It is necessary
// to do a case distinction whether x>0 and then manually apply the
// taclets jdivToDiv and divSame. A saved proof is included for
// reference.


\problem {

    \<{
        int x;
        int res;
        res=x/x;
    }\> res=1

}