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

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
custom-made (top-down) atomize_conv,
store predicate and function symbols in a table instead of a list for faster lookup,
updated certificates

#2 := false
decl uf_1 :: int
#4 := uf_1
decl uf_3 :: int
#6 := uf_3
#9 := (+ uf_3 uf_1)
decl uf_2 :: int
#5 := uf_2
#10 := (+ uf_2 #9)
#7 := (+ uf_2 uf_3)
#8 := (+ uf_1 #7)
#11 := (= #8 #10)
#12 := (not #11)
#51 := (iff #12 false)
#1 := true
#46 := (not true)
#49 := (iff #46 false)
#50 := [rewrite]: #49
#47 := (iff #12 #46)
#44 := (iff #11 true)
#39 := (= #8 #8)
#42 := (iff #39 true)
#43 := [rewrite]: #42
#40 := (iff #11 #39)
#37 := (= #10 #8)
#29 := (+ uf_1 uf_3)
#32 := (+ uf_2 #29)
#35 := (= #32 #8)
#36 := [rewrite]: #35
#33 := (= #10 #32)
#30 := (= #9 #29)
#31 := [rewrite]: #30
#34 := [monotonicity #31]: #33
#38 := [trans #34 #36]: #37
#41 := [monotonicity #38]: #40
#45 := [trans #41 #43]: #44
#48 := [monotonicity #45]: #47
#52 := [trans #48 #50]: #51
#28 := [asserted]: #12
[mp #28 #52]: false
unsat