MDD libvsync optimizations

[mondokm]

Optimizations to allow solving the libvsync tasks with GSAT:

• Handling variable values outside of an int's 32 bits by reserving a range (2^16 possible values) for them. As we give up at 1000 edges by default, this should be enough. Values that were originally in the range also get one from there using the same process.
• Introducing separate variables for dynamic array addresses that are used like a variable. This is done using a best effort value analysis (start from the initial states and keep appling all writes until a fixpoint without considering control flow).

We can solve 6 of the 12 libvsync tasks with this

[github-actions]

❗ Please modify build.gradle.kts to contain a later version than 8.3.5. Current version is 8.3.5.
You can add a new comment with /version-bump <patch|minor|major> to let the bot do it for you.

[github-actions]

Release Preview

Version: 8.3.5
Tag: v8.3.5

Release Notes:
MDD libvsync optimizations

Optimizations to allow solving the libvsync tasks with GSAT:

• Handling variable values outside of an int's 32 bits by reserving a range (2^16 possible values) for them. As we give up at 1000 edges by default, this should be enough. Values that were originally in the range also get one from there using the same process.
• Introducing separate variables for dynamic array addresses that are used like a variable. This is done using a best effort value analysis (start from the initial states and keep appling all writes until a fixpoint without considering control flow).

We can solve 6 of the 12 libvsync tasks with this

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

Files to be uploaded:

• theta-cfa-cli.jar (from ThetaJars)
• theta-xcfa-cli.jar (from ThetaJars)
• theta-solver-smtlib-cli.jar (from ThetaJars)
• theta-xsts-cli.jar (from ThetaJars)
• theta-xta-cli.jar (from ThetaJars)
• theta-sts-cli.jar (from ThetaJars)
• Theta-cfa.zip (from release-Theta-cfa)
• Theta-chccomp.zip (from release-Theta-chccomp)
• EmergenTheta-svcomp.zip (from release-EmergenTheta-svcomp)
• Theta-xta.zip (from release-Theta-xta)
• Theta-svcomp.zip (from release-Theta-svcomp)
• Theta-sts.zip (from release-Theta-sts)
• Theta-xsts.zip (from release-Theta-xsts)
• SymbolicTheta-svcomp.zip (from release-SymbolicTheta-svcomp)
• Thorn-svcomp.zip (from release-Thorn-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	72	0	122	✅
SV-COMP_Portfolio_Emergent	138	0	168	✅
SV-COMP_Portfolio_Horn	140	0	168	✅
SV-COMP_Portfolio_Stable	164	0	168	✅
SV-COMP_Portfolio_Symbolic	112	0	168	✅
Statechart_CEGAR	110	0	126	✅

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