./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-local-pthread-value-cond.i


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


16:28:12 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp-2024
16:28:12 [INFO ] GitInfo.CreateGitInfo - Git commit ID: 17eeec33cbc9c310519b08551b317469f878ce8c
16:28:12 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
16:28:12 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRIC_LEARNING: FULL
16:28:12 [INFO ] Dartagnan.main - Program path: /mnt/goblint-svcomp/benchexec/tools-pldi24/dartagnan/output/thread-local-pthread-value-cond-opt.ll
16:28:12 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
16:28:12 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type [4 x bv8]. Constant was replaced by zero.
16:28:12 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type [4 x bv8]. Constant was replaced by zero.
16:28:12 [INFO ] Wmm.configureAll - encoding.wmm.reduceAcyclicityEncodeSets: true
16:28:12 [INFO ] LoopFormVerification.run - Detected 2 loops in the program.
16:28:12 [INFO ] Compilation.run - Program compiled to C11
16:28:12 [INFO ] LoopUnrolling.run - Program unrolled 1 times
16:28:12 [INFO ] DynamicPureLoopCutting.run - Found 0 static spin loops and 0 potential spin loops.
16:28:12 [INFO ] ThreadCreation.run - Number of threads (including main): 2
16:28:12 [ERROR] Dartagnan.main - The types of bv32 r4 and bv64(1) do not match.
java.lang.IllegalArgumentException: The types of bv32 r4 and bv64(1) do not match.
	at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445) ~[guava-32.1.2-jre.jar:?]
	at com.dat3m.dartagnan.expression.IExprBin.<init>(IExprBin.java:20) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.expression.ExpressionFactory.makeBinary(ExpressionFactory.java:220) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.expression.ExpressionFactory.makeADD(ExpressionFactory.java:174) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlinePthreadSetSpecific(Intrinsics.java:525) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.replace(Intrinsics.java:306) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlineLate(Intrinsics.java:1051) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlineLate(Intrinsics.java:1041) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.lambda$run$0(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.run(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.ModelChecker.preprocessProgram(ModelChecker.java:71) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.DataRaceSolver.run(DataRaceSolver.java:50) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.DataRaceSolver.run(DataRaceSolver.java:40) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:157) [dartagnan.jar:?]
ERROR
