It is like contract checking, but all the checks are done statically (at compile time) and automatically by the solver. Also, we allow the checks to only expre

It is like contract checking, but all the checks are done statically (at compile time) and automatically by the solver. Also, we allow the checks to only express things that the SMT solvers can decide fast (eg linear arithmetic). So, checking will definitely terminate and it will terminate fast.