Make bounded checkers' arguments more uniform

flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.

BSD 2-Clause "Simplified" License

14 stars 1 forks source link

Make bounded checkers' arguments more uniform #88

Closed wilcoxjay closed 1 year ago

wilcoxjay commented 1 year ago

Support unbounded depth in the BDD checker
Report that unbounded depth is not supported in the SAT checker
Clean up code in command.rs for collecting bounds on universe sizes

wilcoxjay commented 1 year ago

Fixes #85