Comment by MWil

the author seems unaware of the SAT/SMT solver/analysis ecosystem