[csanadtelbisz]

LTS-based XCFA analyses now support NORMAL and RECURSIVE mutexes. Mutex attribute initialization/type changes and mutex initialization remain library InvokeLabels, while an immutable MutexState tracks attribute snapshots and acquisition counts per process. A recursive mutex stays held until its owner performs the final matching unlock.

Update state coverage, POR owner lookups, witnesses, and JSON serialization to preserve the mutex state. Count repeated read-lock acquisitions and retain existing atomic-block semantics. MutexToVarPass continues to support NORMAL mutexes and explicitly rejects recursive types.

Validation:

• XCFA model and analysis module test suites passed; focused mutex, LTS, and serialization tests passed again after the final review change.
• All six recursive-mutex tasks in sv-benchmarks/c/pthread-locked-creation matched their expected verdicts with CEGAR/PRED_CART, SEQ_ITP, DFS, and SPOR (two safe, four unsafe). Bitvector safe/unsafe checks also passed.
• All 268 frontend canaries passed. The fixture gate's only failure was the existing compound_bitwise_encoding.c timeout, reproduced on the baseline with MathSAT 5.6.12 missing.
• Spotless and copyright checks passed.

[github-actions]

Release Preview

Version: 8.3.6
Tag: v8.3.6

Release Notes:
Add recursive mutex support

LTS-based XCFA analyses now support NORMAL and RECURSIVE mutexes. Mutex attribute initialization/type changes and mutex initialization remain library InvokeLabels, while an immutable MutexState tracks attribute snapshots and acquisition counts per process. A recursive mutex stays held until its owner performs the final matching unlock.

Update state coverage, POR owner lookups, witnesses, and JSON serialization to preserve the mutex state. Count repeated read-lock acquisitions and retain existing atomic-block semantics. MutexToVarPass continues to support NORMAL mutexes and explicitly rejects recursive types.

Validation:

• XCFA model and analysis module test suites passed; focused mutex, LTS, and serialization tests passed again after the final review change.
• All six recursive-mutex tasks in sv-benchmarks/c/pthread-locked-creation matched their expected verdicts with CEGAR/PRED_CART, SEQ_ITP, DFS, and SPOR (two safe, four unsafe). Bitvector safe/unsafe checks also passed.
• All 268 frontend canaries passed. The fixture gate's only failure was the existing compound_bitwise_encoding.c timeout, reproduced on the baseline with MathSAT 5.6.12 missing.
• Spotless and copyright checks passed.

Modified subprojects (since v8.3.5):
xcfa/xcfa
xcfa/xcfa-analysis
xcfa/xcfa-cli

Files to be uploaded:

• theta-cfa-cli.jar (from ThetaJars)
• theta-xsts-cli.jar (from ThetaJars)
• theta-xta-cli.jar (from ThetaJars)
• theta-xcfa-cli.jar (from ThetaJars)
• theta-solver-smtlib-cli.jar (from ThetaJars)
• theta-sts-cli.jar (from ThetaJars)
• EmergenTheta-svcomp.zip (from release-EmergenTheta-svcomp)
• SymbolicTheta-svcomp.zip (from release-SymbolicTheta-svcomp)
• Theta-sts.zip (from release-Theta-sts)
• Theta-xta.zip (from release-Theta-xta)
• Theta-xsts.zip (from release-Theta-xsts)
• Thorn-svcomp.zip (from release-Thorn-svcomp)
• Theta-cfa.zip (from release-Theta-cfa)
• Theta-chccomp.zip (from release-Theta-chccomp)
• Theta-svcomp.zip (from release-Theta-svcomp)

[github-actions]

Benchexec test report for a selection of benchmarks (correct / incorrect / all):

Rundefinition	Correct	Incorrect	All	Status
CHC-COMP_Portfolio	147	0	195	✅
Hardware_CEGAR	47	0	54	✅
PLC_CEGAR	9	0	9	✅
PetriNet_MDD	58	0	122	✅
PetriNet_PN_MDD	70	0	122	✅
SV-COMP_Portfolio_Emergent	142	0	168	✅
SV-COMP_Portfolio_Horn	140	0	168	✅
SV-COMP_Portfolio_Stable	164	0	168	✅
SV-COMP_Portfolio_Symbolic	120	0	168	✅
Statechart_CEGAR	110	0	126	✅

📦 Download the results - extract the zip and open the *.html files.

[marian-lingsch]

IMO this mostly seems good ^^ (even though I'm not too familiar with the Theta codebase 😅)

Just two small comments on code-style ^^
(Have not yet read the Theta codestyle guidelines so please ignore them if my suggestions contradict them)