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: Feb 05 2025 at 16:23 UTC