Use Z3 for non-determinism check
Use Z3 for non-determinism check.
After redesign of formal verification in AF3, non-determinism check ended up being implemented using NuSMV.
Consider implementing it using Z3.
#2 Updated by Anonymous over 2 years ago
- Assignee changed from Anonymous to Anonymous
I think the only case where this could make sense is for BIG models and only if the current implementation is slow for such cases (SMT is probably way faster than a model checker but this will be only observable in huge models).