SMT reconstruction failures

Fabian Huch huch at in.tum.de
Tue Jul 15 17:36:43 CEST 2025


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



More information about the isabelle-dev mailing list