search

kind2-mc / kind2

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
https://kind.cs.uiowa.edu
Apache License 2.0
85 stars 29 forks source link

Solver error invoking node with quantified variable #673

Open xaaronc opened 4 years ago

xaaronc commented 4 years ago

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 commented 2 years ago

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.