[x] generalize the parser to support multiple conjectures
[x] output one smtlib-encoding of semantics/lemmas/conjecture per conjecture
Advantages:
It is quite natural to formulate multiple conjectures for the same program, so we want to support it.
Currently each conjecture we want to prove requires a copy of the program, which is involved (in particular if one discovers a bug in the program and needs to fix it in each copy).
Advantages: