SMT reconstruction failures

[Makarius]

On 15/07/2025 17:36, Fabian Huch 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.

I only managed to reproduce the problem by using 
smt_reconstruction_step_timeout=3 instead of the default 10 --- both my local 
test machine and the build cluster are too fast for it.


Doing a bisection, reveals the following result:

changeset:   82837:8aa1c98b948b
user:        wenzelm
date:        Fri Jul 11 14:03:09 2025 +0200
files:       src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML 
src/Provers/classical.ML src/Pure/bires.ML
description:
maintain collective rule declarations via type Bires.decls, with netpair 
operations derived from it;


I've been there many times recently, to sort out remaining omissions in the 
rather delicate treatment of classical rules.

I will sort this out very soon, but not tomorrow.


	Makarius