Split termination failure message into two dedicates messages

[mschwerhoff]

import <decreases/int.vpr>

function foo1(n: Int): Int
  decreases n
{ 0 < n ? foo1(n) : 123 } // n does not decrease (but is bounded)

function foo2(n: Int): Int
  decreases n
{ 0 < n ? 456 : foo2(n - 1) } // n is not bounded (but decreases)

Both functions are rejected with the error Function might not terminate. Termination measure might not decrease or might not be bounded.. It would be better, if dedicated messages were generated. This should be straight-forward in Carbon, but potentially not in Silicon, which (if I'm not mistaken), does not point out which conjunct of assert A && B failed, if both A and B are pure.