JKind does not support the following program, because the If then else expression assigning output1,output2 contains node call expressions. Current workaround is done by lifting the expressions.
node test_call(a : int) returns (x : int; y : int);
let
x = a + 1;
y = a - 1;
tel ;
node main (input : int; x : bool) returns (output1 : int; output2 : int);
let
output1,output2 =
if x
then test_call(input+1)
else test_call(input-1) ;
tel ;
JKind does not support the following program, because the If then else expression assigning output1,output2 contains node call expressions. Current workaround is done by lifting the expressions.
node test_call(a : int) returns (x : int; y : int); let x = a + 1; y = a - 1; tel ;
node main (input : int; x : bool) returns (output1 : int; output2 : int); let output1,output2 = if x then test_call(input+1) else test_call(input-1) ; tel ;