SMT reconstruction failures

[Jasmin Blanchette]

> 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?

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.

Note that I (like you) have inherited this situation. I didn't invent this timeout and am generally suspicious of tactic-specific timeouts.

Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 15. Jul 2025, at 17:36, Fabian Huch <huch at in.tum.de> wrote:
> 
> As of Isabelle/3e1521dc095d and AFP/8851801a38e0, I am getting SMT failures:
> 
> >isabelle build -A: Modular_arithmetic_LLL_and_HNF_algorithms
> Running Modular_arithmetic_LLL_and_HNF_algorithms ...
> Modular_arithmetic_LLL_and_HNF_algorithms FAILED (see also "isabelle build_log -H Error Modular_arithmetic_LLL_and_HNF_algorithms")
> *** Failed to apply initial proof method (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"):
> *** goal (1 subgoal):
> ***  1. A $$ (0, 0) =
> ***     A'' $$
> ***     (0, 0)
> *** At command "by" (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy")
> Unfinished session(s): Modular_arithmetic_LLL_and_HNF_algorithms
> 0:15:36 elapsed time, 1:39:03 cpu time, factor 6.35
> 
> 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?
> 
> 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.
> 
> 
> Fabian
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250715/57833285/attachment.htm>