add interactive choice to add assertion/assumption/eq.cond when an ob…

[danmatichuk]

…servable difference is found

adds an additional priority level for node scheduling to handle assertion propagation that doesn't need to happen immediately