Comment Comment by jimsimmons What exactly do SMT systems "solve" in cases like this?If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle.I am surprised people prefer having a dependency of something like Z3 at compiler level. parent jimsimmons 2 years ago
If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle.
I am surprised people prefer having a dependency of something like Z3 at compiler level.