Improve intersect_source_invariant option in hybrid solve

[schillic]

The option intersect_source_invariant in the hybrid solve is not fully used.

1. Once the intersection is empty, the flowpipe should be shortened (all later reach sets are unreachable).
2. When intersecting with the guard, the invariant is ignored.