Skip to content

make the way iMod solves side-conditions consistent with iInv

Ralf Jung requested to merge ralf/side-condition into gen_proofmode

Also, always split conjunctions in side-conditions to make sure we don't have some silly True /\ _ left.

Merge request reports