Easier to say than to implement 
The issue is probably almost nobody actually wants to sacrifice the development speed to get a proof of code correctness, like the one SMT-solver provides. In 99% of cases just let it crash works.
2 Likes
