Problem -- hidden bonus
class manager : public employee {
public:
long salary() { return sal + 1000; }
};
Invariant
k =?= (m->salary(k))->salary()
class manager : public employee {
public:
long salary() { return sal + 1000; }
};
k =?= (m->salary(k))->salary()