This program takes old Scott Adams text adventure games, and checks that they can be solved by executing them symbolically and feeding it to an SMT solver.
See https://gergo.erdi.hu/blog/2020-08-01-solving_text_adventure_games_via_symbolic_execution/ where I write about the why and the how.