FV does not work when array index is a variable
If the model contains an expression of the form Output = Input[(Input[0])]; then the file generated for the model checker is incorrect.
To reproduce:
- Open the attached model
- Try to run OCRA constraints
Expected: the status of checking the contract should be true
Actual: An error is logged in the console.
(from redmine: issue id 3497, created on 2018-08-28)
- Relations:
- relates #1756 (closed)
- Uploads: