[isabelle-dev] smt for word

[Sascha Boehme]

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