theory Scratch
  imports "HOL-Word.Word"
begin

declare [[smt_trace]]

lemma "(max_word::1 word) = 1"
  sledgehammer [prover = z3]
  oops

end

...
SMT: Invoking SMT solver "z3" ... 
SMT: Solver: 
SMT: Result:
       unsat
       ((set-logic <null>)
       (proof
       (let (($x43 (= (_ bv1 1) max_word$)))
       (let ((@x94 (monotonicity (rewrite (= (bvneg (_ bv1 1)) (_ bv1 1))) (= (= max_word$ (bvneg (_ bv1 1))) (= max_word$ (_ bv1 1))))))
       (let ((@x96 (trans @x94 (rewrite (= (= max_word$ (_ bv1 1)) $x43)) (= (= max_word$ (bvneg (_ bv1 1))) $x43))))
       (let ((@x97 (mp (asserted (= max_word$ (bvneg (_ bv1 1)))) @x96 $x43)))
       (let ((@x352 (trans (monotonicity @x97 (= $x43 (= (_ bv1 1) (_ bv1 1)))) (rewrite (= (= (_ bv1 1) (_ bv1 1)) true)) (= $x43 true))))
       (let ((@x356 (trans (monotonicity @x352 (= (not $x43) (not true))) (rewrite (= (not true) false)) (= (not $x43) false))))
       (let (($x46 (not $x43)))
       (let ((@x48 (monotonicity (rewrite (= (= max_word$ (_ bv1 1)) $x43)) (= (not (= max_word$ (_ bv1 1))) $x46))))
       (mp (mp (asserted (not (= max_word$ (_ bv1 1)))) @x48 $x46) @x356 false))))))))))) 
SMT: Time (ms):
       11 
"z3": A prover error occurred:
bad SMT term: _