Hi,

`I'm getting annoyed by the tediousness required to discharge seemingly
``trivial problems on words and thought I would try the "smt" method on
``them.
`
(BTW: Is proof reconstruction available for Bitvectors?)

`I found a strange behaviour (in 2012, 2013 and ffc3f1659a25): Consider
``the two goals stated below. They are equivalent, the only difference is
``between free and bound variables. Yet "smt" can only solve the second
``goal and suggests a possibly spurious counter-example for the first one.
`

`--------------------------------------------------------------------------
``
`theory Scratch imports "~~/src/HOL/Word/Word" begin
lemma "⋀degree k. (degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
using [[smt_oracle=true]]
apply smt (* Fails, talks about possibly spurious counter-example *)
oops
lemma "(degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
using [[smt_oracle=true]]
apply smt (* Succeeds *)
done

`--------------------------------------------------------------------------
``
`
Is this some known limitation or a bug in the preprocessing?
Best regards,
Lars