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