Fix two bugs in the base Pintos code: