SAT solvers will also be also be applied in traditional compilers soon.
The remaining problem with formal verification and compilation is proof of termination, which is not a SAT problem.
Running all test cases via cbcm is magnitudes faster than writing 100% coverage (only line cov, not covered values) tests. It's like one day vs one month. And I've never seen code with full value test coverage.
For guaranteed timing you need special tests, not a SAT solvers. The solver just helps with the proofs.
Even if everything you say is true, it's true the first time. Then I make a change to the code. Now if I have unit tests, I have to fix a test (maybe minutes, maybe an hour) and re-run the tests (minutes). Or I have to re-run the formal verification (a day).
SAT solvers will also be also be applied in traditional compilers soon.
The remaining problem with formal verification and compilation is proof of termination, which is not a SAT problem.
Running all test cases via cbcm is magnitudes faster than writing 100% coverage (only line cov, not covered values) tests. It's like one day vs one month. And I've never seen code with full value test coverage.
For guaranteed timing you need special tests, not a SAT solvers. The solver just helps with the proofs.