Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] smt (z3): Replaying the proof trace produced b...


view this post on Zulip Email Gateway (Jul 19 2022 at 11:53):

From: Peter Lammich <lammich@in.tum.de>
And another sledgehammer related problem. I bumped into this during
sledgehammering, and stripped it down to Z3. Example for reproduction
attached.
Bug2.thy


Last updated: Apr 24 2024 at 01:07 UTC