./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-3.i


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


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