added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML)
#2 := false
#11 := 4::real
decl uf_2 :: real
#8 := uf_2
#7 := 7::real
#9 := (* 7::real uf_2)
decl uf_1 :: real
#5 := uf_1
#4 := 3::real
#6 := (* 3::real uf_1)
#10 := (+ #6 #9)
#41 := (>= #10 4::real)
#39 := (not #41)
#12 := (< #10 4::real)
#40 := (iff #12 #39)
#37 := [rewrite]: #40
#34 := [asserted]: #12
#38 := [mp #34 #37]: #39
#13 := 2::real
#14 := (* 2::real uf_1)
#43 := (<= #14 3::real)
#44 := (not #43)
#15 := (< 3::real #14)
#45 := (iff #15 #44)
#46 := [rewrite]: #45
#35 := [asserted]: #15
#47 := [mp #35 #46]: #44
#16 := 0::real
#51 := (>= uf_2 0::real)
#17 := (< uf_2 0::real)
#18 := (not #17)
#58 := (iff #18 #51)
#49 := (not #51)
#53 := (not #49)
#56 := (iff #53 #51)
#57 := [rewrite]: #56
#54 := (iff #18 #53)
#50 := (iff #17 #49)
#52 := [rewrite]: #50
#55 := [monotonicity #52]: #54
#59 := [trans #55 #57]: #58
#36 := [asserted]: #18
#60 := [mp #36 #59]: #51
[th-lemma #60 #47 #38]: false
unsat