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 沒寫，以補上! 請重新下載。