Support offline SMT-Lib provers

Setting the prover to "offline" now triggers generation of an SMT-Lib file without invoking a prover on it. If the setting "smtfile" has its default value of "-", the script is printed to standard output. If it has any other value, the value taken as the name of the file to write to. If "smtfile" is set to anything other than "-" during a normal, online proof, the script is saved in the given file after the proof completes, rather than being saved in a temporary file that's subsequently deleted. This behavior can be useful for debugging.