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
#9 := 1::int
decl uf_1 :: int
#5 := uf_1
#10 := (< uf_1 1::int)
#6 := 3::int
#7 := (+ uf_1 3::int)
#4 := 4::int
#8 := (<= 4::int #7)
#11 := (or #8 #10)
#12 := (not #11)
#66 := (iff #12 false)
#29 := (+ 3::int uf_1)
#32 := (<= 4::int #29)
#38 := (or #10 #32)
#43 := (not #38)
#64 := (iff #43 false)
#1 := true
#59 := (not true)
#62 := (iff #59 false)
#63 := [rewrite]: #62
#60 := (iff #43 #59)
#57 := (iff #38 true)
#48 := (>= uf_1 1::int)
#46 := (not #48)
#52 := (or #46 #48)
#55 := (iff #52 true)
#56 := [rewrite]: #55
#53 := (iff #38 #52)
#50 := (iff #32 #48)
#51 := [rewrite]: #50
#47 := (iff #10 #46)
#49 := [rewrite]: #47
#54 := [monotonicity #49 #51]: #53
#58 := [trans #54 #56]: #57
#61 := [monotonicity #58]: #60
#65 := [trans #61 #63]: #64
#44 := (iff #12 #43)
#41 := (iff #11 #38)
#35 := (or #32 #10)
#39 := (iff #35 #38)
#40 := [rewrite]: #39
#36 := (iff #11 #35)
#33 := (iff #8 #32)
#30 := (= #7 #29)
#31 := [rewrite]: #30
#34 := [monotonicity #31]: #33
#37 := [monotonicity #34]: #36
#42 := [trans #37 #40]: #41
#45 := [monotonicity #42]: #44
#67 := [trans #45 #65]: #66
#28 := [asserted]: #12
[mp #28 #67]: false
unsat