test/coq/pass/while_MP_terminating.sail


1
2
3
4
5
6
7
8
9
10
11
12
13

default Order dec

$include <prelude.sail>

register INT : bool

function test () -> int = {
  count : int = 0;
  while not_bool(INT) & count < 5 do count = count + 1;
  return(count)
}

termination_measure test while 5 - count