Imported node sometimes prevents refinement

[xaaronc]

Given the following:

function imported imp(x: int) returns (y: int);

function min(x,y:int) returns (z: int)
(*@contract
    assume true;
*)
let
    z = if x < y then x else y;
tel

function main(x:int) returns (y:int)
let
    y = min(imp(2),10);
    --%PROPERTY y <= 10;
tel

Running kind2 with --compositional true --modular true, it fails to prove the (obviously correct) property of main because it does not attempt to refine min, seemingly due to the presence of abstract imp.

Either removing min’s contract, or giving imp a concrete implementation, causes kind2 to verify the property as expected.

This behavior seems to be somewhat order-dependent. For example, replacing:
y = min(imp(2),10);
with
y = foo(min(2,10));
does result in refinement of min, though of course the property does not verify since it’s false.

kind2 nightly-68-g48a0a6fd

[daniel-larraz]

Thank you for reporting this bug. #599 fixes this issue.