Separate solving for invariants (abduction) and postconditions (disjunction elimination), main commit. Converge numerical part of postconditions.