./Dartagnan-SVCOMP.sh /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-array-const-race.i


--------------------------------------------------------------------------------


12:23:56 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp-2024
12:23:56 [INFO ] GitInfo.CreateGitInfo - Git commit ID: 17eeec33cbc9c310519b08551b317469f878ce8c
12:23:56 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
12:23:56 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRIC_LEARNING: FULL
12:23:56 [INFO ] Dartagnan.main - Program path: /mnt/goblint-svcomp/benchexec/tools-pldi24/dartagnan/output/thread-join-array-const-race-opt.ll
12:23:56 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
12:23:56 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type [4 x bv8]. Constant was replaced by zero.
12:23:56 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type [4 x bv8]. Constant was replaced by zero.
12:23:56 [INFO ] Wmm.configureAll - encoding.wmm.reduceAcyclicityEncodeSets: true
12:23:57 [INFO ] LoopFormVerification.run - Detected 0 loops in the program.
12:23:57 [INFO ] Compilation.run - Program compiled to C11
12:23:57 [INFO ] LoopUnrolling.run - Program unrolled 1 times
12:23:57 [INFO ] DynamicPureLoopCutting.run - Found 0 static spin loops and 0 potential spin loops.
12:23:57 [INFO ] ThreadCreation.run - Number of threads (including main): 5
12:23:57 [INFO ] LogThreadStatistics.run - 
======== Program statistics ========
#Threads: 5
#Events: 351
	#Annotations: 30
	#Stores: 24
	#Loads: 28
	#Inits: 52
	#Others: 0
#Allocated bytes: 72
	Statically allocated: 40
	Dynamically allocated: 32
========================================
12:23:57 [INFO ] Dependency.fromConfig - Analyze dependencies
12:23:57 [INFO ] AliasAnalysis.fromConfig - Selected alias analysis: FIELD_SENSITIVE
12:23:57 [INFO ] AliasAnalysis.fromConfig - Finished alias analysis in 7ms
12:23:57 [INFO ] RelationAnalysis.fromConfig - 
	wmm.analysis.relationAnalysis: true
	wmm.analysis.mustSets: true
	wmm.analysis.extendedRelationAnalysis: true
12:23:57 [INFO ] RelationAnalysis.fromConfig - Finished regular analysis in 43ms
12:23:57 [INFO ] RelationAnalysis.fromConfig - Finished extended analysis in 13ms
12:23:57 [INFO ] RelationAnalysis.fromConfig - 
======== RelationAnalysis summary ======== 
	#Relations: 16
	#Axioms: 1
	#may-edges removed (extended): 64
	#must-edges added (extended): 0
	total #must|may|exclusive edges: 11852|13050|0
	#must|may rf edges: 4|92
	#must|may co edges: 28|96
===========================================
12:23:57 [INFO ] EncodingContext.of - encoding.wmm.idl2sat: false
12:23:57 [INFO ] EncodingContext.of - encoding.mergeCFVars: true
12:23:57 [INFO ] Acyclic.getEncodeGraph - Computing encodeGraph for acyclic hb
12:23:57 [INFO ] Acyclic.getEncodeGraph - encodeGraph size: 542
12:23:57 [INFO ] Acyclic.getEncodeGraph - reduced encodeGraph size: 255
12:23:57 [INFO ] EncodingContext.of - Number of encoded edges for acyclicity: 192
12:23:57 [INFO ] ProgramEncoder.withContext - encoding.initializeRegisters: false
12:23:57 [INFO ] WmmEncoder.withContext - encoding.activeSets: true
12:23:57 [INFO ] Acyclic.getEncodeGraph - Computing encodeGraph for acyclic hb
12:23:57 [INFO ] Acyclic.getEncodeGraph - encodeGraph size: 542
12:23:57 [INFO ] Acyclic.getEncodeGraph - reduced encodeGraph size: 255
12:23:57 [INFO ] WmmEncoder.withContext - Finished active sets in 20ms
12:23:57 [INFO ] WmmEncoder.withContext - Number of unknown edges: 1198
12:23:57 [INFO ] WmmEncoder.withContext - Number of encoded edges: 1086
12:23:57 [INFO ] SymmetryEncoder.<init> - Symmetry breaking disabled.
12:23:57 [INFO ] DataRaceSolver.run - Starting encoding using Z3 4.12.2.0
12:23:57 [INFO ] ProgramEncoder.encodeMemory - Encoding fixed memory
12:23:57 [INFO ] ProgramEncoder.encodeControlFlow - Encoding program control flow
12:23:57 [INFO ] ProgramEncoder.encodeFinalRegisterValues - Skipping encoding of final register values: C-Code has no assertions over those values.
12:23:57 [INFO ] ProgramEncoder.encodeDependencies - Encoding dependencies
12:23:57 [INFO ] WmmEncoder.encodeRelations - Encoding relations
12:23:57 [INFO ] WmmEncoder.encodeConsistency - Encoding consistency
12:23:57 [INFO ] Acyclic.getEncodeGraph - Computing encodeGraph for acyclic hb
12:23:57 [INFO ] Acyclic.getEncodeGraph - encodeGraph size: 542
12:23:57 [INFO ] Acyclic.getEncodeGraph - reduced encodeGraph size: 255
12:23:57 [INFO ] PropertyEncoder.encodeDataRaces - Encoding data races
12:23:57 [INFO ] DataRaceSolver.run - Starting first solver.check()
12:23:57 [INFO ] DataRaceSolver.run - Verification finished with result FAIL
FAIL
