If TPA was queried with a transition system that has empty bad states, it ran into an assertion that the interpolant is not logical true. This assertion is, in general, useful to detect incorrect behaviour of the algorithm, so we would like to keep it, even though in this special case of query == false such interpolant is correct. Instead, we check for these special cases beforehand.
For now we only make syntactic check. It is possible we should do proper SMT check on the initial and query states.
If TPA was queried with a transition system that has empty bad states, it ran into an assertion that the interpolant is not logical true. This assertion is, in general, useful to detect incorrect behaviour of the algorithm, so we would like to keep it, even though in this special case of
query == falsesuch interpolant is correct. Instead, we check for these special cases beforehand.For now we only make syntactic check. It is possible we should do proper SMT check on the initial and query states.