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

added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
replaced unspecific 'error' invocations with raising of specific SMT exceptions,
added annotations to traced SMT problem and solver output

#2 := false
#4 := 0::int
decl ?x2!1 :: int
#91 := ?x2!1
#98 := (<= ?x2!1 0::int)
#99 := (not #98)
#7 := 0::real
decl ?x3!0 :: real
#93 := ?x3!0
#96 := (<= ?x3!0 0::real)
#97 := (not #96)
#111 := (and #97 #99)
#114 := (not #111)
#33 := -1::int
#94 := (<= ?x2!1 -1::int)
#95 := (not #94)
#120 := (or #95 #114)
#125 := (not #120)
#100 := (and #99 #97)
#101 := (not #100)
#102 := (or #101 #95)
#103 := (not #102)
#126 := (iff #103 #125)
#123 := (iff #102 #120)
#117 := (or #114 #95)
#121 := (iff #117 #120)
#122 := [rewrite]: #121
#118 := (iff #102 #117)
#115 := (iff #101 #114)
#112 := (iff #100 #111)
#113 := [rewrite]: #112
#116 := [monotonicity #113]: #115
#119 := [monotonicity #116]: #118
#124 := [trans #119 #122]: #123
#127 := [monotonicity #124]: #126
#5 := (:var 1 int)
#75 := (<= #5 -1::int)
#76 := (not #75)
#8 := (:var 0 real)
#65 := (<= #8 0::real)
#66 := (not #65)
#61 := (<= #5 0::int)
#62 := (not #61)
#69 := (and #62 #66)
#72 := (not #69)
#79 := (or #72 #76)
#82 := (forall (vars (?x2 int) (?x3 real)) #79)
#85 := (not #82)
#104 := (~ #85 #103)
#105 := [sk]: #104
#11 := 1::int
#12 := (- 1::int)
#13 := (< #12 #5)
#9 := (< 0::real #8)
#6 := (< 0::int #5)
#10 := (and #6 #9)
#14 := (implies #10 #13)
#15 := (forall (vars (?x2 int) (?x3 real)) #14)
#16 := (exists (vars (?x1 int)) #15)
#17 := (not #16)
#88 := (iff #17 #85)
#36 := (< -1::int #5)
#42 := (not #10)
#43 := (or #42 #36)
#48 := (forall (vars (?x2 int) (?x3 real)) #43)
#58 := (not #48)
#86 := (iff #58 #85)
#83 := (iff #48 #82)
#80 := (iff #43 #79)
#77 := (iff #36 #76)
#78 := [rewrite]: #77
#73 := (iff #42 #72)
#70 := (iff #10 #69)
#67 := (iff #9 #66)
#68 := [rewrite]: #67
#63 := (iff #6 #62)
#64 := [rewrite]: #63
#71 := [monotonicity #64 #68]: #70
#74 := [monotonicity #71]: #73
#81 := [monotonicity #74 #78]: #80
#84 := [quant-intro #81]: #83
#87 := [monotonicity #84]: #86
#59 := (iff #17 #58)
#56 := (iff #16 #48)
#51 := (exists (vars (?x1 int)) #48)
#54 := (iff #51 #48)
#55 := [elim-unused]: #54
#52 := (iff #16 #51)
#49 := (iff #15 #48)
#46 := (iff #14 #43)
#39 := (implies #10 #36)
#44 := (iff #39 #43)
#45 := [rewrite]: #44
#40 := (iff #14 #39)
#37 := (iff #13 #36)
#34 := (= #12 -1::int)
#35 := [rewrite]: #34
#38 := [monotonicity #35]: #37
#41 := [monotonicity #38]: #40
#47 := [trans #41 #45]: #46
#50 := [quant-intro #47]: #49
#53 := [quant-intro #50]: #52
#57 := [trans #53 #55]: #56
#60 := [monotonicity #57]: #59
#89 := [trans #60 #87]: #88
#32 := [asserted]: #17
#90 := [mp #32 #89]: #85
#108 := [mp~ #90 #105]: #103
#109 := [mp #108 #127]: #125
#128 := [not-or-elim #109]: #111
#130 := [and-elim #128]: #99
#110 := [not-or-elim #109]: #94
#186 := (or #95 #98)
#187 := [th-lemma]: #186
#188 := [unit-resolution #187 #110]: #98
[unit-resolution #188 #130]: false
unsat