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
88 stars 29 forks source link

Filter updates on properties that are not in the system #1073

Closed daniel-larraz closed 5 months ago

daniel-larraz commented 6 months ago

The IC3IA engine slices the transition system based on the property to be checked. This PR filters out notifications for properties that are not in the sliced transition system.