Models for relevant regular expression operations

[shigoel]

Description of changes:

• Reorganize the Python-specific Boogie prelude.
• Add PyFactory, a Python-specific Lambda factory that -- for now -- contains a candidate model for Python's re.compile.
• Turn on elimination of irrelevant axioms for Python analyses.
• Suppress any counterexample parsing errors from a SAT solver.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[atomb]

Looks good!