handle let expressions inside terms by unfolding (instead of raising an exception),
added examples to test this feature
#2 := false
#55 := 0::int
#7 := 2::int
decl uf_1 :: int
#4 := uf_1
#8 := (mod uf_1 2::int)
#9 := (* 2::int #8)
#56 := (>= #9 0::int)
#51 := (not #56)
#5 := 1::int
#10 := (+ #9 1::int)
#11 := (+ uf_1 #10)
#6 := (+ uf_1 1::int)
#12 := (<= #6 #11)
#13 := (not #12)
#58 := (iff #13 #51)
#39 := (+ uf_1 #9)
#40 := (+ 1::int #39)
#30 := (+ 1::int uf_1)
#45 := (<= #30 #40)
#48 := (not #45)
#52 := (iff #48 #51)
#53 := (iff #45 #56)
#54 := [rewrite]: #53
#57 := [monotonicity #54]: #52
#49 := (iff #13 #48)
#46 := (iff #12 #45)
#43 := (= #11 #40)
#33 := (+ 1::int #9)
#36 := (+ uf_1 #33)
#41 := (= #36 #40)
#42 := [rewrite]: #41
#37 := (= #11 #36)
#34 := (= #10 #33)
#35 := [rewrite]: #34
#38 := [monotonicity #35]: #37
#44 := [trans #38 #42]: #43
#31 := (= #6 #30)
#32 := [rewrite]: #31
#47 := [monotonicity #32 #44]: #46
#50 := [monotonicity #47]: #49
#59 := [trans #50 #57]: #58
#29 := [asserted]: #13
#60 := [mp #29 #59]: #51
#107 := (>= #8 0::int)
#1 := true
#28 := [true-axiom]: true
#135 := (or false #107)
#136 := [th-lemma]: #135
#137 := [unit-resolution #136 #28]: #107
[th-lemma #137 #60]: false
unsat