#lang ivy1.7

# include order

type foo
interpret foo -> bv[3]


parameter max : foo = 3

action a (s:foo) returns (r:foo) = {
    require s < max;
    r := s + 1
}

action b returns (r:foo) = {
    r := 0
}

export a
export b