Current status: Fix typo in property (1 min) → rerun verification (50 min) → fix typo in property (3 min) → rerun verification (90 min) → fix typo in property (1 min) → rerun verification (45 min) → ⋯
-
Yes. More like 120-180 minutes if you don't accidentally add a bug that the solver can find quickly. Luckily that's what the typos did..
SAT/SMT solvers are inherently hard to parallelize. The best method so far is to run multiple solver instances on the same problem with slightly different tuning parameters and hope that one of those will finish slightly sooner than the others.
