Solver error invoking node with quantified variable

[xaaronc]

This input:

node istrue(x: bool) returns (y: bool) let y = x; tel

node A(x: bool) returns (y: bool)
let
    y = x;
    --%PROPERTY forall(i:bool) istrue(i) => y;
tel

gives the following error output:

Runtime failure in bounded model checking: SMT solver failed: line 30 column 10: unknown constant __C2
Runtime failure in inductive step: SMT solver failed: line 44 column 10: unknown constant __C2
Child process 65582 (2-induction) exited with return code 2
Child process 65581 (inductive step) exited with return code 2
Terminating useless bounded model checking (PID 65580)
Child process 65583 (property directed reachability) exited with return code 2
Terminating useless bounded model checking (PID 65580)
Child process 65580 (bounded model checking) exited with return code 2
Runtime failure in property directed reachability: SMT solver failed: line 40 column 11: unknown constant __C2
Caught exception Failure("SMT solver failed: line 36 column 10: unknown constant __C2")
Caught exception Failure("SMT solver failed: line 36 column 10: unknown constant __C2")
Caught exception Failure("SMT solver failed: line 36 column 10: unknown constant __C2")
Runtime failure in 2-induction: SMT solver failed: line 43 column 10: unknown constant __C2
Caught exception Failure("SMT solver failed: line 36 column 10: unknown constant __C2")

Replacing istrue(i) with istrue(x) does the expected thing.

kind2 --version
kind2 v1.2.0-521-g445b0439

[daniel-larraz]

Quantified variables are currently not allowed in arguments to node calls. The new front-end (enabled in PR #843) rejects this input and reports the problem.