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 >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
