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 := 0::int
decl uf_2 :: int
#7 := uf_2
#42 := -1::int
#45 := (* -1::int uf_2)
decl uf_1 :: int
#5 := uf_1
#46 := (+ uf_1 #45)
#63 := (>= #46 0::int)
#83 := (iff #63 false)
#44 := -4::int
#79 := (>= -4::int 0::int)
#81 := (iff #79 false)
#82 := [rewrite]: #81
#77 := (iff #63 #79)
#47 := (= #46 -4::int)
#8 := 4::int
#9 := (+ uf_1 4::int)
#10 := (= uf_2 #9)
#49 := (iff #10 #47)
#32 := (+ 4::int uf_1)
#39 := (= uf_2 #32)
#43 := (iff #39 #47)
#48 := [rewrite]: #43
#40 := (iff #10 #39)
#37 := (= #9 #32)
#38 := [rewrite]: #37
#41 := [monotonicity #38]: #40
#50 := [trans #41 #48]: #49
#31 := [asserted]: #10
#51 := [mp #31 #50]: #47
#80 := [monotonicity #51]: #77
#84 := [trans #80 #82]: #83
#12 := (- uf_2 uf_1)
#13 := (< 0::int #12)
#14 := (not #13)
#74 := (iff #14 #63)
#53 := (* -1::int uf_1)
#54 := (+ #53 uf_2)
#57 := (< 0::int #54)
#60 := (not #57)
#72 := (iff #60 #63)
#64 := (not #63)
#67 := (not #64)
#70 := (iff #67 #63)
#71 := [rewrite]: #70
#68 := (iff #60 #67)
#65 := (iff #57 #64)
#66 := [rewrite]: #65
#69 := [monotonicity #66]: #68
#73 := [trans #69 #71]: #72
#61 := (iff #14 #60)
#58 := (iff #13 #57)
#55 := (= #12 #54)
#56 := [rewrite]: #55
#59 := [monotonicity #56]: #58
#62 := [monotonicity #59]: #61
#75 := [trans #62 #73]: #74
#52 := [asserted]: #14
#76 := [mp #52 #75]: #63
[mp #76 #84]: false
unsat