Constraint builder should implement branching model

[JSAbrahams]

Summary of current issue

We want a system where

• The builder allows us to diverge paths, which are disjoint.
• Allow us to only add to one such disjoint path if we are checking disjoint paths of execution.
• Allow us to add to all disjoint if we are in sequential code.

For the last two, we therefore need a system which changes the internal state of the builder to:

• Only add to a select set of paths.
• Add to all paths.

If we want to generalize this as far as possible, we need to continue using some sort of level system. We should then:

• Be able to mark at what level we start to create diverging paths
• Return to this mark when we wish to add to all paths

Proposed change

Been trying to draw this out on paper. Causing a bit of a headache.