Remove Z3 from simplify

- We only use simplify itself for checking conditions
- Removing recursive rewrite rules
- Reset regression test cases (many case now failed :|)
- Need improve simplify solver!
- Now, we don't add inductive hypothesis when function has precondition
	(can be improved later)
Resolved #15