add JUMP_OR so we can create disjunctions in Z3
expose or in z3
merged fixed but broken or