  We present a case study on using program verification tools, specifically
model-checkers for C programs, to solve simple interactive fiction games from
around 1980. Off-the-shelf model-checking tools are unable to handle the games
in their original form. In order to work around this, we apply a series of
program transformations that do not change the behaviour of the program. An
interesting aspect of these games is that they use a simple, interpreted
language to script in-game events. This turns out to be the most difficult part
of the program for verification tools to handle; we tackle this using partial
evaluation. Our case study thus provides some insights that are applicable more
generally to verification and analysis of programs that interpret scripting
languages.
  To the best of our knowledge, this is the first example of a commercially
released game being solved by application of a program model-checker to the
game's code.
