janhaag/PSE2011 — Issue #14: Translation of % to prover broken
Author: danielbruns
Created: 2012-02-15 10:50:57+00:00
State: open

The expression -1%2 is equal to -1 according to the definition of %. This is respected in runtime checking, but for the prover it is translated to 1. Check the following program:
main (){
int x = -1%2;
}
ensure x==-1;