Constant input passed to non-constant formal input

[AdrienChampion]

The bug happens when a node has a constant input and passes it through a call to a subnode accepting non-constant inputs.

node count (in: bool) returns (cnt: int) ;
let
  cnt = (if in then 1 else 0) + (0 -> pre cnt) ;
tel

node top (const in: bool) returns (cnt: int) ;
(*@contract
  guarantee cnt >= 0 ;
*)
let
  cnt = count(in) ;
tel

The actual problem is an arity mismatch at SMT-level between the signature of the subnode and the way the caller uses it. That's because the constant state variable is only passed once since it's constant, where as the subnodes expects to see the previous and current versions.