Support for more examples

[edenfrenkel]

After adding more examples converted from mypyvy (currently on the qalpha branch), I've encountered the following issues:

• There appears to be no support for if-then-else parsing, even though such terms are implemented. This is relevant for the following examples, which currently cannot be parsed: bosco_3t_safety, hybrid_reliable_broadcast_cisa, raft, ring_id_not_dead, ring_id, ticket, as well as all stoppable_paxos variants.
• Definitions do not behave correctly, at least when appearing in proofs. Specifically, the defined relations aren't substituted when calling the solver, yielding an unknown constant error when running verify. This can be seen in all the choosable variants of paxos, where derived relations are currently defined via def.

[tchajed]

I fixed the bug with defined relations. Now:

• fast_paxos_forall_choosable.fly times out in the solver
• flexible_paxos_forall_choosable.fly verifies
• paxos_forall_choosable.fly verifies
• stoppable_paxos_forall_choosable.fly has an if ... then ... else
• vertical_paxos_forall_choosable.fly verifies

[tchajed]

All of the examples now run, although stoppable_paxos_forall_choosable.fly and bosco_3t_safety.fly run into the 10-minute timeout. I've now made that timeout configurable easily with --timeout so if it's just a matter of running for a really long time you should be able to try that out.