#include "limits.h"

/*@ ensures \result == a/b;
*/
int div(int a, int b);