It's about SAT-based Bounded Model Checking.
Only 3 functions to implement, but please start ASAP.
The deadline is 9am, 06/11 (Monday).

忘了说，TODO 要 implement induction-based algorithm原来的 spec 没写，以补上! 请重新下载。