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
#43 := 0::int
decl ?x1!0 :: int
#78 := ?x1!0
#56 := -2::int
#113 := (* -2::int ?x1!0)
decl uf_1 :: int
#6 := uf_1
#8 := 2::int
#10 := (* 2::int uf_1)
#114 := (+ #10 #113)
#115 := (<= #114 0::int)
#120 := (not #115)
#41 := -1::int
#100 := (* -1::int ?x1!0)
#101 := (+ uf_1 #100)
#102 := (<= #101 0::int)
#123 := (or #102 #120)
#126 := (not #123)
#59 := (* -2::int uf_1)
#79 := (* 2::int ?x1!0)
#80 := (+ #79 #59)
#81 := (>= #80 0::int)
#82 := (not #81)
#45 := (* -1::int uf_1)
#83 := (+ ?x1!0 #45)
#84 := (>= #83 0::int)
#85 := (or #84 #82)
#86 := (not #85)
#127 := (iff #86 #126)
#124 := (iff #85 #123)
#121 := (iff #82 #120)
#118 := (iff #81 #115)
#107 := (+ #59 #79)
#110 := (>= #107 0::int)
#116 := (iff #110 #115)
#117 := [rewrite]: #116
#111 := (iff #81 #110)
#108 := (= #80 #107)
#109 := [rewrite]: #108
#112 := [monotonicity #109]: #111
#119 := [trans #112 #117]: #118
#122 := [monotonicity #119]: #121
#105 := (iff #84 #102)
#94 := (+ #45 ?x1!0)
#97 := (>= #94 0::int)
#103 := (iff #97 #102)
#104 := [rewrite]: #103
#98 := (iff #84 #97)
#95 := (= #83 #94)
#96 := [rewrite]: #95
#99 := [monotonicity #96]: #98
#106 := [trans #99 #104]: #105
#125 := [monotonicity #106 #122]: #124
#128 := [monotonicity #125]: #127
#4 := (:var 0 int)
#5 := (pattern #4)
#9 := (* 2::int #4)
#60 := (+ #9 #59)
#58 := (>= #60 0::int)
#57 := (not #58)
#46 := (+ #4 #45)
#44 := (>= #46 0::int)
#63 := (or #44 #57)
#66 := (forall (vars (?x1 int)) (:pat #5) #63)
#69 := (not #66)
#87 := (~ #69 #86)
#88 := [sk]: #87
#11 := (< #9 #10)
#7 := (< #4 uf_1)
#12 := (implies #7 #11)
#13 := (forall (vars (?x1 int)) (:pat #5) #12)
#14 := (not #13)
#72 := (iff #14 #69)
#31 := (not #7)
#32 := (or #31 #11)
#35 := (forall (vars (?x1 int)) (:pat #5) #32)
#38 := (not #35)
#70 := (iff #38 #69)
#67 := (iff #35 #66)
#64 := (iff #32 #63)
#61 := (iff #11 #57)
#62 := [rewrite]: #61
#54 := (iff #31 #44)
#42 := (not #44)
#49 := (not #42)
#52 := (iff #49 #44)
#53 := [rewrite]: #52
#50 := (iff #31 #49)
#47 := (iff #7 #42)
#48 := [rewrite]: #47
#51 := [monotonicity #48]: #50
#55 := [trans #51 #53]: #54
#65 := [monotonicity #55 #62]: #64
#68 := [quant-intro #65]: #67
#71 := [monotonicity #68]: #70
#39 := (iff #14 #38)
#36 := (iff #13 #35)
#33 := (iff #12 #32)
#34 := [rewrite]: #33
#37 := [quant-intro #34]: #36
#40 := [monotonicity #37]: #39
#73 := [trans #40 #71]: #72
#30 := [asserted]: #14
#74 := [mp #30 #73]: #69
#91 := [mp~ #74 #88]: #86
#92 := [mp #91 #128]: #126
#130 := [not-or-elim #92]: #115
#93 := (not #102)
#129 := [not-or-elim #92]: #93
[th-lemma #129 #130]: false
unsat