# Sledgehammer/z3: "bad SMT term: _"Open, WishlistPublicActions

Assigned To
None
Authored By
 makarius Apr 5 2020, 12:38 PM2020-04-05 12:38:09 (UTC+2)
Tags
None
Subscribers

# Description

The following problem with sledgehammer and z3 has been reported by Peter Lammich (isabelle-users 05-Apr-2020 00:22) and happens in Isabelle2019 (also in Isabelle2018 or Isabelle2014):

Input:

```theory Scratch
imports "HOL-Word.Word"
begin

declare [[smt_trace]]

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

end```

Output:

```...
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:

The final error message stems from the following exception: https://isabelle.sketis.net/repos/isabelle/file/Isabelle2019/src/HOL/Tools/SMT/smtlib_proof.ML#l248

### Event Timeline

makarius triaged this task as Normal priority.Apr 5 2020, 12:38 PM