Ant S. (May 06 2026 at 12:39): Ant S. (May 06 2026 at 12:39):Sorry, meant to make a new thread
Ant S. (May 06 2026 at 12:40):Ant S. said in #Beginner Questions > Getting value of a configuration parameter:
A follow-up from this thread|
I've had to recently downgrade my machine, and so one SMT query will complete nondeterministically -- sometimes it times out and sometimes it doesn't. This problem is a whole lot more persistent on my weaker machine. Setting
declare [[ smt_timeout = 0 ]]does nothing, nor do big numbers like 10000 or -1. What do I do?
Mathias Fleury (May 06 2026 at 18:08):There is an reconstruction_step_timeout which might help
Mathias Fleury (May 06 2026 at 18:09):but you can also call sledgehammer again and try to find another faster proof
Ant S. (May 06 2026 at 18:10):sledgehammer can't :(
But I'll try reconstruction ty
Mathias Fleury (May 06 2026 at 18:11):try replacing the by (smt ....) by sledgehammer(add: ....) or even sledgehammer (...)
Ant S. (May 06 2026 at 18:11):what does that do
Ant S. (May 06 2026 at 18:12):Is that not what putting facts in a using clause is for
Mathias Fleury (May 06 2026 at 18:12):that will force sledgehammer to use that facts (with add:) or only those facts
Ant S. (May 06 2026 at 18:12):oh
Ant S. (May 06 2026 at 18:12):whoa
Mathias Fleury (May 06 2026 at 18:12):otherwise sledgehammer will use its own heuristics to select facts
Last updated: May 17 2026 at 06:46 UTC