Resolve "why3 prove raises Not_found when called on a DIMACS file"

This MR catches the exception Not_found that was raised when calling why3 prove on programs that are parsed directly to a theory, skipping the module. The exception is now just caught (I haven't found a function to check if a module can be restored from a theory).

Additionally, this MR adds a check if there are actually any prover models before selecting one. (This doesn't change behaviour but avoids setting up the model selection in this case).

Closes #524 (closed)