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
decl uf_4 :: int
#9 := uf_4
decl uf_5 :: int
#13 := uf_5
decl uf_3 :: int
#8 := uf_3
#24 := (+ uf_3 uf_5)
#25 := (+ #24 uf_4)
decl uf_2 :: int
#6 := uf_2
#5 := 1::int
#7 := (+ 1::int uf_2)
#26 := (* #7 #25)
#21 := (* uf_5 uf_2)
#19 := (* #7 uf_5)
#10 := (+ uf_3 uf_4)
#16 := 2::int
#17 := (* 2::int #7)
#18 := (* #17 #10)
#20 := (+ #18 #19)
#22 := (+ #20 #21)
decl uf_1 :: int
#4 := uf_1
#23 := (+ uf_1 #22)
#27 := (- #23 #26)
#14 := (* uf_2 uf_5)
#11 := (* #7 #10)
#12 := (+ uf_1 #11)
#15 := (+ #12 #14)
#28 := (= #15 #27)
#29 := (not #28)
#149 := (iff #29 false)
#1 := true
#144 := (not true)
#147 := (iff #144 false)
#148 := [rewrite]: #147
#145 := (iff #29 #144)
#142 := (iff #28 true)
#47 := (* uf_2 uf_4)
#46 := (* uf_2 uf_3)
#48 := (+ #46 #47)
#59 := (+ #14 #48)
#60 := (+ uf_4 #59)
#61 := (+ uf_3 #60)
#62 := (+ uf_1 #61)
#136 := (= #62 #62)
#140 := (iff #136 true)
#141 := [rewrite]: #140
#135 := (iff #28 #136)
#138 := (= #27 #62)
#123 := (+ uf_5 #59)
#124 := (+ uf_4 #123)
#125 := (+ uf_3 #124)
#77 := (* 2::int #47)
#75 := (* 2::int #46)
#78 := (+ #75 #77)
#104 := (* 2::int #14)
#105 := (+ #104 #78)
#106 := (+ uf_5 #105)
#76 := (* 2::int uf_4)
#107 := (+ #76 #106)
#74 := (* 2::int uf_3)
#108 := (+ #74 #107)
#113 := (+ uf_1 #108)
#130 := (- #113 #125)
#133 := (= #130 #62)
#139 := [rewrite]: #133
#131 := (= #27 #130)
#128 := (= #26 #125)
#116 := (+ uf_4 uf_5)
#117 := (+ uf_3 #116)
#120 := (* #7 #117)
#126 := (= #120 #125)
#127 := [rewrite]: #126
#121 := (= #26 #120)
#118 := (= #25 #117)
#119 := [rewrite]: #118
#122 := [monotonicity #119]: #121
#129 := [trans #122 #127]: #128
#114 := (= #23 #113)
#111 := (= #22 #108)
#91 := (+ #14 #78)
#92 := (+ uf_5 #91)
#93 := (+ #76 #92)
#94 := (+ #74 #93)
#101 := (+ #94 #14)
#109 := (= #101 #108)
#110 := [rewrite]: #109
#102 := (= #22 #101)
#99 := (= #21 #14)
#100 := [rewrite]: #99
#97 := (= #20 #94)
#85 := (+ uf_5 #14)
#79 := (+ #76 #78)
#80 := (+ #74 #79)
#88 := (+ #80 #85)
#95 := (= #88 #94)
#96 := [rewrite]: #95
#89 := (= #20 #88)
#86 := (= #19 #85)
#87 := [rewrite]: #86
#83 := (= #18 #80)
#67 := (* 2::int uf_2)
#68 := (+ 2::int #67)
#71 := (* #68 #10)
#81 := (= #71 #80)
#82 := [rewrite]: #81
#72 := (= #18 #71)
#69 := (= #17 #68)
#70 := [rewrite]: #69
#73 := [monotonicity #70]: #72
#84 := [trans #73 #82]: #83
#90 := [monotonicity #84 #87]: #89
#98 := [trans #90 #96]: #97
#103 := [monotonicity #98 #100]: #102
#112 := [trans #103 #110]: #111
#115 := [monotonicity #112]: #114
#132 := [monotonicity #115 #129]: #131
#137 := [trans #132 #139]: #138
#65 := (= #15 #62)
#49 := (+ uf_4 #48)
#50 := (+ uf_3 #49)
#53 := (+ uf_1 #50)
#56 := (+ #53 #14)
#63 := (= #56 #62)
#64 := [rewrite]: #63
#57 := (= #15 #56)
#54 := (= #12 #53)
#51 := (= #11 #50)
#52 := [rewrite]: #51
#55 := [monotonicity #52]: #54
#58 := [monotonicity #55]: #57
#66 := [trans #58 #64]: #65
#134 := [monotonicity #66 #137]: #135
#143 := [trans #134 #141]: #142
#146 := [monotonicity #143]: #145
#150 := [trans #146 #148]: #149
#45 := [asserted]: #29
[mp #45 #150]: false
unsat