<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><blockquote type="cite">This is both in the build and interactive session; declaring [[smt_reconstruction_step_timeout=0]] helps. Can the SMT situation be improved so we don't have these timeout issues even if things are slightly slower?<br></blockquote><div><br></div>The obvious fix is to disable the timeout or crank it up very high. But since it's "smt_reconstruction_step_timeout" and not "smt_timeout", I'm wondering if there might be some nonmonotonic aspects to consider. E.g. is there any code of the form "try reconstruction step A for smt_reconstruction_step_timeout seconds; if this fails, try reconstruction step B". I guess the best way to find out is to try it out.<div><div><br></div><div>Note that I (like you) have inherited this situation. I didn't invent this timeout and am generally suspicious of tactic-specific timeouts.</div><div><br></div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science and Theorem Proving<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9341<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 15. Jul 2025, at 17:36, Fabian Huch <huch@in.tum.de> wrote:</div><br class="Apple-interchange-newline"><div><div>As of Isabelle/3e1521dc095d and AFP/8851801a38e0, I am getting SMT failures:<br><br>>isabelle build -A: Modular_arithmetic_LLL_and_HNF_algorithms<br>Running Modular_arithmetic_LLL_and_HNF_algorithms ...<br>Modular_arithmetic_LLL_and_HNF_algorithms FAILED (see also "isabelle build_log -H Error Modular_arithmetic_LLL_and_HNF_algorithms")<br>*** Failed to apply initial proof method (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"):<br>*** goal (1 subgoal):<br>*** 1. A $$ (0, 0) =<br>*** A'' $$<br>*** (0, 0)<br>*** At command "by" (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy")<br>Unfinished session(s): Modular_arithmetic_LLL_and_HNF_algorithms<br>0:15:36 elapsed time, 1:39:03 cpu time, factor 6.35<br><br>This is both in the build and interactive session; declaring [[smt_reconstruction_step_timeout=0]] helps. Can the SMT situation be improved so we don't have these timeout issues even if things are slightly slower?<br><br>The problem appears after the merge in Isabelle/1e39653de974. But I have the suspicion that those changes only uncovered an existing problem, which otherwise manifests as spurious SMT failures during scheduled build.<br><br><br>Fabian<br><br></div></div></blockquote></div><br></div></div></body></html>