Page MenuHomeIsabelle/Phabricator

Sledgehammer/z3: "bad SMT term: _"
Open, WishlistPublic


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):


theory Scratch
  imports "HOL-Word.Word"

declare [[smt_trace]]

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



SMT: Invoking SMT solver "z3" ... 
SMT: Solver: 
SMT: Result:
       ((set-logic <null>)
       (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):
"z3": A prover error occurred:
bad SMT term: _

The final error message stems from the following exception:

Event Timeline

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

Maybe a spurious dummy abstraction λ_. bthat is not translated properly?

The same happens for sledgehammer [provers = cvc4].

The heart of the problem is that reconstruction for bit vectors isn't supported (despite the completely wrong and misleading claims made by a certain CPP 2011 papers, due to magical thinking on the part of its authors). We could try to have nicer error messages for that case but it's a bit tricky to do cleanly and without breaking anything. I'll wait to see if it emerges again on the mailing list first.

makarius lowered the priority of this task from Normal to Wishlist.May 1 2020, 10:54 PM

OK, so this is now on "Wishlist".