Possible enhancement: Check for weaker interpolants

[makaimann]

Attached is a simple example that interpolant-based model checking diverges on. It turns out that the generated interpolants are too strong and keep getting expanded with constant values. However, the first interpolant actually contained the "right" interpolant as one of its conjuncts. If we had detected that a subformula was itself an interpolant, this would not happen.

itp_fail_test.tar.gz