Underapproximate unfolding

[vkuncak]

Postconditions are not needed to ensure that counterexamples are real, so we don't need them for under-approximation check. When these postconditions contain recursive functions, the size of trees may increase unnecessarily. Tools like the KIND2 model checker therefore construct separate under-approximating and over-approximating sequences. Consider developing a counterexample-only solver in Inox that does not inline postconditions.