Allow repeated calls to the same debug solver.

In such a way that debug output is appended to the given file, rather than
overwriting the file.
Give default values for lookupVar instead of requiring an explicit value.

In preparation for lazy declaration of SMT variables.
Declare SMT variables lazily.

Simplifies the code a little, and makes sense from a performance standpoint.