1 2 3 4 5 6 7 8 9 10 11
function {:inline true} foo3(x:int, y:bool) returns(bool) { foo3(x,y) } axiom foo3(1,false); procedure baz1() requires foo3(2,false); { assume foo3(1,true); }