# Re: [isabelle] SMT and bound variables.

```Hey Lars.

```
I'm not sure if proof reconstruction is now available for bitvectors. Sascha and I looked at the problem a few years ago, and the conclusion was it was doable but the performance was a tad disappointing.
```
```
The tactic we implemented to help discharge the theory-lemmas appearing in bitvector proofs *is* available, and should be in your context under the name word_bitwise. It does the bitwise expansion of your problem and some minor simplification. Together with real simplification it solves both of these problems, although a bit slowly.
```
Thomas.

On 06/07/13 03:21, Lars Noschinski wrote:
```
```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

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.