[isabelle-dev] smt for word

[Gerwin Klein]

Thanks, that explains things.

Gerwin

On 05/10/2011, at 4:42 PM, Sascha Boehme wrote:

> Hi Gerwin,
> 
> This is because by default the smt method tries to reconstruct the
> proof of Z3.  For bitvectors, however, there is currently no Z3 proof
> reconstruction.  You might want to invoke the smt method as an oracle:
> 
>  lemma "(x :: 8 word) + x  = 2 * x"
>    using [[smt_oracle]]
>    by smt
> 
> Cheers,
> Sascha
> 
> 
> Gerwin Klein wrote:
>> I'm getting 
>> 
>> lemma "(x :: 8 word) + x  = 2 * x"
>> apply smt
>> 
>> Solver z3: Z3 proof parser (line 2): unknown sort: "bv" 
>> 
>> I was trying remote Z3 from a Mac.
>> 
>> This is on isabelle 20b3377b08d7, but I don't think anything relevant has changed since Sep 26.
>> 
>> Am I doing something wrong? Sounds like Z3 responds with something the smt method doesn't know about.
>> 
>> Cheers,
>> Gerwin
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>