Stream: Mirror: Isabelle Users Mailing List

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

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: Jan 04 2025 at 20:18 UTC