src/HOL/SMT/Examples/cert/z3_linarith_12.proof

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
#16 := (not false)
decl uf_2 :: int
#8 := uf_2
#4 := 0::int
#12 := (<= 0::int uf_2)
#13 := (not #12)
#14 := (or #13 #12)
#6 := 1::int
#7 := (- 1::int)
#9 := (* #7 uf_2)
decl uf_1 :: int
#5 := uf_1
#10 := (+ uf_1 #9)
#11 := (<= 0::int #10)
#15 := (or #11 #14)
#17 := (iff #15 #16)
#18 := (not #17)
#70 := (iff #18 false)
#1 := true
#65 := (not true)
#68 := (iff #65 false)
#69 := [rewrite]: #68
#66 := (iff #18 #65)
#63 := (iff #17 true)
#58 := (iff true true)
#61 := (iff #58 true)
#62 := [rewrite]: #61
#59 := (iff #17 #58)
#56 := (iff #16 true)
#57 := [rewrite]: #56
#54 := (iff #15 true)
#35 := -1::int
#38 := (* -1::int uf_2)
#41 := (+ uf_1 #38)
#44 := (<= 0::int #41)
#49 := (or #44 true)
#52 := (iff #49 true)
#53 := [rewrite]: #52
#50 := (iff #15 #49)
#47 := (iff #14 true)
#48 := [rewrite]: #47
#45 := (iff #11 #44)
#42 := (= #10 #41)
#39 := (= #9 #38)
#36 := (= #7 -1::int)
#37 := [rewrite]: #36
#40 := [monotonicity #37]: #39
#43 := [monotonicity #40]: #42
#46 := [monotonicity #43]: #45
#51 := [monotonicity #46 #48]: #50
#55 := [trans #51 #53]: #54
#60 := [monotonicity #55 #57]: #59
#64 := [trans #60 #62]: #63
#67 := [monotonicity #64]: #66
#71 := [trans #67 #69]: #70
#34 := [asserted]: #18
[mp #34 #71]: false
unsat