./Ultimate.py --spec /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp --file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i --full-output --architecture 32bit


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


Checking for data races
Using default analysis
Version 2329fc70
Calling Ultimate with: /usr/lib/jvm/java-11-openjdk-amd64/bin/java -Dosgi.configuration.area=/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data -tc /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/AutomizerReach.xml -i /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i -s /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf --cacsl2boogietranslator.entry.function main --witnessprinter.witness.directory /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux --witnessprinter.witness.filename witness.graphml --witnessprinter.write.witness.besides.input.file false --witnessprinter.graph.data.specification CHECK( init(main()), LTL(G ! data-race) )

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 32bit --witnessprinter.graph.data.programhash 9322697277eb986511a36781229ce42b45829e13f79f269b044b747bd925b9c9
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2023-10-27 12:50:17,486 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2023-10-27 12:50:17,488 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2023-10-27 12:50:17,531 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2023-10-27 12:50:17,540 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2023-10-27 12:50:17,543 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2023-10-27 12:50:17,544 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2023-10-27 12:50:17,550 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2023-10-27 12:50:17,551 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2023-10-27 12:50:17,553 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2023-10-27 12:50:17,555 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2023-10-27 12:50:17,556 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2023-10-27 12:50:17,569 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2023-10-27 12:50:17,575 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2023-10-27 12:50:17,577 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2023-10-27 12:50:17,578 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2023-10-27 12:50:17,580 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2023-10-27 12:50:17,581 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2023-10-27 12:50:17,582 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2023-10-27 12:50:17,587 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2023-10-27 12:50:17,588 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2023-10-27 12:50:17,589 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2023-10-27 12:50:17,591 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2023-10-27 12:50:17,591 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2023-10-27 12:50:17,593 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2023-10-27 12:50:17,593 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2023-10-27 12:50:17,594 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2023-10-27 12:50:17,595 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2023-10-27 12:50:17,595 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2023-10-27 12:50:17,596 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2023-10-27 12:50:17,609 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2023-10-27 12:50:17,610 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2023-10-27 12:50:17,611 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2023-10-27 12:50:17,611 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2023-10-27 12:50:17,612 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2023-10-27 12:50:17,612 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2023-10-27 12:50:17,612 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2023-10-27 12:50:17,613 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2023-10-27 12:50:17,613 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2023-10-27 12:50:17,613 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2023-10-27 12:50:17,614 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2023-10-27 12:50:17,614 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2023-10-27 12:50:17,656 INFO  L113        SettingsManager]: Loading preferences was successful
[2023-10-27 12:50:17,657 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2023-10-27 12:50:17,657 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2023-10-27 12:50:17,657 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2023-10-27 12:50:17,658 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2023-10-27 12:50:17,658 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2023-10-27 12:50:17,658 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2023-10-27 12:50:17,659 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2023-10-27 12:50:17,659 INFO  L138        SettingsManager]:  * Use SBE=true
[2023-10-27 12:50:17,659 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2023-10-27 12:50:17,660 INFO  L138        SettingsManager]:  * sizeof long=4
[2023-10-27 12:50:17,660 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2023-10-27 12:50:17,660 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2023-10-27 12:50:17,660 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2023-10-27 12:50:17,660 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2023-10-27 12:50:17,660 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * sizeof long double=12
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2023-10-27 12:50:17,661 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2023-10-27 12:50:17,662 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2023-10-27 12:50:17,662 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2023-10-27 12:50:17,662 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2023-10-27 12:50:17,662 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-10-27 12:50:17,662 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2023-10-27 12:50:17,663 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2023-10-27 12:50:17,663 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2023-10-27 12:50:17,663 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2023-10-27 12:50:17,673 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2023-10-27 12:50:17,674 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2023-10-27 12:50:17,674 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2023-10-27 12:50:17,674 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2023-10-27 12:50:17,674 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2023-10-27 12:50:17,674 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2023-10-27 12:50:17,675 INFO  L138        SettingsManager]:  * Looper check in Petri net analysis=SEMANTIC
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1 (file:/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/com.sun.xml.bind_2.2.0.v201505121915.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int)
WARNING: Please consider reporting this to the maintainers of com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
Applying setting for plugin de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: Entry function -> main
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness directory -> /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness filename -> witness.graphml
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Write witness besides input file -> false
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data specification -> CHECK( init(main()), LTL(G ! data-race) )


Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data producer -> Automizer
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data architecture -> 32bit
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data programhash -> 9322697277eb986511a36781229ce42b45829e13f79f269b044b747bd925b9c9
[2023-10-27 12:50:17,999 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2023-10-27 12:50:18,028 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2023-10-27 12:50:18,030 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2023-10-27 12:50:18,034 INFO  L271        PluginConnector]: Initializing CDTParser...
[2023-10-27 12:50:18,034 INFO  L275        PluginConnector]: CDTParser initialized
[2023-10-27 12:50:18,035 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i
[2023-10-27 12:50:19,747 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2023-10-27 12:50:20,087 INFO  L351              CDTParser]: Found 1 translation units.
[2023-10-27 12:50:20,097 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i
[2023-10-27 12:50:20,114 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/19215712e/b6f27424cf8744639f0a70b11e711927/FLAGa7caae0e0
[2023-10-27 12:50:20,128 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/19215712e/b6f27424cf8744639f0a70b11e711927
[2023-10-27 12:50:20,131 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2023-10-27 12:50:20,146 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2023-10-27 12:50:20,147 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2023-10-27 12:50:20,157 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2023-10-27 12:50:20,160 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2023-10-27 12:50:20,160 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,163 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@2f86b609 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20, skipping insertion in model container
[2023-10-27 12:50:20,163 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,168 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2023-10-27 12:50:20,249 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2023-10-27 12:50:20,701 WARN  L623        FunctionHandler]: Unknown extern function pthread_detach
[2023-10-27 12:50:20,706 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-10-27 12:50:20,729 INFO  L203         MainTranslator]: Completed pre-run
[2023-10-27 12:50:20,791 WARN  L623        FunctionHandler]: Unknown extern function pthread_detach
[2023-10-27 12:50:20,813 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-10-27 12:50:20,853 INFO  L208         MainTranslator]: Completed translation
[2023-10-27 12:50:20,862 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20 WrapperNode
[2023-10-27 12:50:20,863 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2023-10-27 12:50:20,864 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2023-10-27 12:50:20,864 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2023-10-27 12:50:20,864 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2023-10-27 12:50:20,884 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,910 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,943 INFO  L138                Inliner]: procedures = 159, calls = 37, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 95
[2023-10-27 12:50:20,948 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2023-10-27 12:50:20,948 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2023-10-27 12:50:20,949 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2023-10-27 12:50:20,949 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2023-10-27 12:50:20,964 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,964 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,974 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,982 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:20,996 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:21,010 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:21,012 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:21,019 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:21,021 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2023-10-27 12:50:21,028 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2023-10-27 12:50:21,028 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2023-10-27 12:50:21,028 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2023-10-27 12:50:21,029 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (1/1) ...
[2023-10-27 12:50:21,033 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-10-27 12:50:21,053 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-10-27 12:50:21,072 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2023-10-27 12:50:21,107 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2023-10-27 12:50:21,112 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2023-10-27 12:50:21,112 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2023-10-27 12:50:21,112 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexLock
[2023-10-27 12:50:21,112 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2023-10-27 12:50:21,112 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2023-10-27 12:50:21,118 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2023-10-27 12:50:21,123 INFO  L130     BoogieDeclarations]: Found specification of procedure pthread_detach
[2023-10-27 12:50:21,123 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2023-10-27 12:50:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2023-10-27 12:50:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2023-10-27 12:50:21,129 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2023-10-27 12:50:21,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2023-10-27 12:50:21,130 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2023-10-27 12:50:21,321 INFO  L235             CfgBuilder]: Building ICFG
[2023-10-27 12:50:21,326 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2023-10-27 12:50:21,678 INFO  L276             CfgBuilder]: Performing block encoding
[2023-10-27 12:50:21,684 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2023-10-27 12:50:21,701 INFO  L300             CfgBuilder]: Removed 2 assume(true) statements.
[2023-10-27 12:50:21,704 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 27.10 12:50:21 BoogieIcfgContainer
[2023-10-27 12:50:21,704 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2023-10-27 12:50:21,711 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2023-10-27 12:50:21,711 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2023-10-27 12:50:21,714 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2023-10-27 12:50:21,714 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 27.10 12:50:20" (1/3) ...
[2023-10-27 12:50:21,715 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6df0682c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 27.10 12:50:21, skipping insertion in model container
[2023-10-27 12:50:21,715 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:50:20" (2/3) ...
[2023-10-27 12:50:21,716 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6df0682c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 27.10 12:50:21, skipping insertion in model container
[2023-10-27 12:50:21,716 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 27.10 12:50:21" (3/3) ...
[2023-10-27 12:50:21,717 INFO  L112   eAbstractionObserver]: Analyzing ICFG thread-join-counter-outer-race-2.i
[2023-10-27 12:50:21,726 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2023-10-27 12:50:21,736 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2023-10-27 12:50:21,736 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 8 error locations.
[2023-10-27 12:50:21,736 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2023-10-27 12:50:21,848 INFO  L144    ThreadInstanceAdder]: Constructed 0 joinOtherThreadTransitions.
[2023-10-27 12:50:21,912 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 135 places, 136 transitions, 277 flow
[2023-10-27 12:50:22,042 INFO  L130       PetriNetUnfolder]: 7/176 cut-off events.
[2023-10-27 12:50:22,043 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:50:22,047 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 181 conditions, 176 events. 7/176 cut-off events. For 0/0 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 220 event pairs, 0 based on Foata normal form. 0/155 useless extension candidates. Maximal degree in co-relation 88. Up to 4 conditions per place. 
[2023-10-27 12:50:22,061 INFO  L82        GeneralOperation]: Start removeDead. Operand has 135 places, 136 transitions, 277 flow
[2023-10-27 12:50:22,069 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 135 places, 136 transitions, 277 flow
[2023-10-27 12:50:22,072 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-27 12:50:22,098 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 135 places, 136 transitions, 277 flow
[2023-10-27 12:50:22,102 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 135 places, 136 transitions, 277 flow
[2023-10-27 12:50:22,102 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 135 places, 136 transitions, 277 flow
[2023-10-27 12:50:22,165 INFO  L130       PetriNetUnfolder]: 7/176 cut-off events.
[2023-10-27 12:50:22,165 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:50:22,167 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 181 conditions, 176 events. 7/176 cut-off events. For 0/0 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 220 event pairs, 0 based on Foata normal form. 0/155 useless extension candidates. Maximal degree in co-relation 88. Up to 4 conditions per place. 
[2023-10-27 12:50:22,184 INFO  L119        LiptonReduction]: Number of co-enabled transitions 3304
[2023-10-27 12:50:26,422 INFO  L134        LiptonReduction]: Checked pairs total: 12522
[2023-10-27 12:50:26,422 INFO  L136        LiptonReduction]: Total number of compositions: 98
[2023-10-27 12:50:26,443 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-27 12:50:26,452 INFO  L357      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mHoare=true, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=LoopsAndPotentialCycles, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@5229e3b6, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-27 12:50:26,452 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 12 error locations.
[2023-10-27 12:50:26,472 INFO  L130       PetriNetUnfolder]: 0/6 cut-off events.
[2023-10-27 12:50:26,473 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:50:26,473 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:26,473 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1]
[2023-10-27 12:50:26,474 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2023-10-27 12:50:26,482 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:26,482 INFO  L85        PathProgramCache]: Analyzing trace with hash 13815242, now seen corresponding path program 1 times
[2023-10-27 12:50:26,503 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:26,503 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [429435394]
[2023-10-27 12:50:26,504 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:26,504 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:26,678 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:26,850 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:26,850 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:26,851 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [429435394]
[2023-10-27 12:50:26,851 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [429435394] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:26,851 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:26,852 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:26,853 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [519937042]
[2023-10-27 12:50:26,870 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:26,876 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:26,876 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:26,909 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:26,911 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:26,947 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 121 out of 234
[2023-10-27 12:50:26,951 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 46 places, 45 transitions, 95 flow. Second operand  has 3 states, 3 states have (on average 122.33333333333333) internal successors, (367), 3 states have internal predecessors, (367), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:26,951 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:26,965 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 121 of 234
[2023-10-27 12:50:26,966 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:27,166 INFO  L130       PetriNetUnfolder]: 216/619 cut-off events.
[2023-10-27 12:50:27,167 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:50:27,183 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1096 conditions, 619 events. 216/619 cut-off events. For 0/0 co-relation queries the response was YES. Maximal size of possible extension queue 39. Compared 3533 event pairs, 78 based on Foata normal form. 0/561 useless extension candidates. Maximal degree in co-relation 1044. Up to 255 conditions per place. 
[2023-10-27 12:50:27,187 INFO  L137   encePairwiseOnDemand]: 221/234 looper letters, 45 selfloop transitions, 8 changer transitions 0/67 dead transitions.
[2023-10-27 12:50:27,188 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 47 places, 67 transitions, 245 flow
[2023-10-27 12:50:27,188 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:27,190 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:27,200 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 423 transitions.
[2023-10-27 12:50:27,215 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6025641025641025
[2023-10-27 12:50:27,216 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 423 transitions.
[2023-10-27 12:50:27,217 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 423 transitions.
[2023-10-27 12:50:27,218 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:27,220 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 423 transitions.
[2023-10-27 12:50:27,229 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 141.0) internal successors, (423), 3 states have internal predecessors, (423), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,233 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,233 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,234 INFO  L175             Difference]: Start difference. First operand has 46 places, 45 transitions, 95 flow. Second operand 3 states and 423 transitions.
[2023-10-27 12:50:27,247 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 47 places, 67 transitions, 245 flow
[2023-10-27 12:50:27,249 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 47 places, 67 transitions, 245 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-27 12:50:27,250 INFO  L231             Difference]: Finished difference. Result has 49 places, 51 transitions, 161 flow
[2023-10-27 12:50:27,252 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=234, PETRI_DIFFERENCE_MINUEND_FLOW=91, PETRI_DIFFERENCE_MINUEND_PLACES=45, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=43, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=35, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=161, PETRI_PLACES=49, PETRI_TRANSITIONS=51}
[2023-10-27 12:50:27,254 INFO  L288   CegarLoopForPetriNet]: 46 programPoint places, 3 predicate places.
[2023-10-27 12:50:27,269 INFO  L495      AbstractCegarLoop]: Abstraction has has 49 places, 51 transitions, 161 flow
[2023-10-27 12:50:27,270 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 122.33333333333333) internal successors, (367), 3 states have internal predecessors, (367), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,270 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:27,270 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:27,271 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2023-10-27 12:50:27,271 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2023-10-27 12:50:27,273 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:27,273 INFO  L85        PathProgramCache]: Analyzing trace with hash -1672456406, now seen corresponding path program 1 times
[2023-10-27 12:50:27,276 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:27,276 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [461646930]
[2023-10-27 12:50:27,277 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:27,277 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:27,309 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:27,384 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:27,384 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:27,385 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [461646930]
[2023-10-27 12:50:27,385 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [461646930] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:27,385 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:27,385 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:27,386 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1025225835]
[2023-10-27 12:50:27,386 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:27,387 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:27,387 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:27,401 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:27,402 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:27,428 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 122 out of 234
[2023-10-27 12:50:27,428 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 49 places, 51 transitions, 161 flow. Second operand  has 3 states, 3 states have (on average 124.0) internal successors, (372), 3 states have internal predecessors, (372), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,429 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:27,429 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 122 of 234
[2023-10-27 12:50:27,429 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:27,573 INFO  L130       PetriNetUnfolder]: 185/530 cut-off events.
[2023-10-27 12:50:27,573 INFO  L131       PetriNetUnfolder]: For 171/174 co-relation queries the response was YES.
[2023-10-27 12:50:27,574 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1131 conditions, 530 events. 185/530 cut-off events. For 171/174 co-relation queries the response was YES. Maximal size of possible extension queue 41. Compared 2978 event pairs, 108 based on Foata normal form. 2/491 useless extension candidates. Maximal degree in co-relation 1071. Up to 345 conditions per place. 
[2023-10-27 12:50:27,575 INFO  L137   encePairwiseOnDemand]: 228/234 looper letters, 35 selfloop transitions, 7 changer transitions 0/64 dead transitions.
[2023-10-27 12:50:27,575 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 51 places, 64 transitions, 281 flow
[2023-10-27 12:50:27,576 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:27,576 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:27,577 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 403 transitions.
[2023-10-27 12:50:27,578 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5740740740740741
[2023-10-27 12:50:27,578 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 403 transitions.
[2023-10-27 12:50:27,578 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 403 transitions.
[2023-10-27 12:50:27,579 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:27,580 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 403 transitions.
[2023-10-27 12:50:27,585 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 134.33333333333334) internal successors, (403), 3 states have internal predecessors, (403), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,588 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,589 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,589 INFO  L175             Difference]: Start difference. First operand has 49 places, 51 transitions, 161 flow. Second operand 3 states and 403 transitions.
[2023-10-27 12:50:27,589 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 51 places, 64 transitions, 281 flow
[2023-10-27 12:50:27,608 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 49 places, 64 transitions, 261 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:27,609 INFO  L231             Difference]: Finished difference. Result has 51 places, 56 transitions, 201 flow
[2023-10-27 12:50:27,609 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=234, PETRI_DIFFERENCE_MINUEND_FLOW=145, PETRI_DIFFERENCE_MINUEND_PLACES=47, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=51, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=44, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=201, PETRI_PLACES=51, PETRI_TRANSITIONS=56}
[2023-10-27 12:50:27,610 INFO  L288   CegarLoopForPetriNet]: 46 programPoint places, 5 predicate places.
[2023-10-27 12:50:27,610 INFO  L495      AbstractCegarLoop]: Abstraction has has 51 places, 56 transitions, 201 flow
[2023-10-27 12:50:27,610 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 124.0) internal successors, (372), 3 states have internal predecessors, (372), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,611 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:27,611 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:27,611 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2023-10-27 12:50:27,611 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2023-10-27 12:50:27,613 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:27,613 INFO  L85        PathProgramCache]: Analyzing trace with hash 326858899, now seen corresponding path program 1 times
[2023-10-27 12:50:27,614 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:27,614 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [522314482]
[2023-10-27 12:50:27,614 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:27,614 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:27,656 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:27,703 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:27,703 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:27,704 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [522314482]
[2023-10-27 12:50:27,704 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [522314482] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:27,705 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:27,705 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:27,706 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [543595493]
[2023-10-27 12:50:27,706 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:27,706 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:27,706 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:27,707 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:27,708 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:27,716 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 128 out of 234
[2023-10-27 12:50:27,716 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 51 places, 56 transitions, 201 flow. Second operand  has 3 states, 3 states have (on average 129.33333333333334) internal successors, (388), 3 states have internal predecessors, (388), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,716 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:27,716 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 128 of 234
[2023-10-27 12:50:27,718 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:27,854 INFO  L130       PetriNetUnfolder]: 192/567 cut-off events.
[2023-10-27 12:50:27,855 INFO  L131       PetriNetUnfolder]: For 216/248 co-relation queries the response was YES.
[2023-10-27 12:50:27,855 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1233 conditions, 567 events. 192/567 cut-off events. For 216/248 co-relation queries the response was YES. Maximal size of possible extension queue 41. Compared 3255 event pairs, 88 based on Foata normal form. 9/539 useless extension candidates. Maximal degree in co-relation 1172. Up to 324 conditions per place. 
[2023-10-27 12:50:27,857 INFO  L137   encePairwiseOnDemand]: 230/234 looper letters, 39 selfloop transitions, 3 changer transitions 2/68 dead transitions.
[2023-10-27 12:50:27,869 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 53 places, 68 transitions, 319 flow
[2023-10-27 12:50:27,869 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:27,870 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:27,870 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 421 transitions.
[2023-10-27 12:50:27,871 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5997150997150997
[2023-10-27 12:50:27,871 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 421 transitions.
[2023-10-27 12:50:27,871 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 421 transitions.
[2023-10-27 12:50:27,871 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:27,871 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 421 transitions.
[2023-10-27 12:50:27,872 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 140.33333333333334) internal successors, (421), 3 states have internal predecessors, (421), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,873 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,874 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,874 INFO  L175             Difference]: Start difference. First operand has 51 places, 56 transitions, 201 flow. Second operand 3 states and 421 transitions.
[2023-10-27 12:50:27,874 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 53 places, 68 transitions, 319 flow
[2023-10-27 12:50:27,878 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 51 places, 68 transitions, 305 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:27,880 INFO  L231             Difference]: Finished difference. Result has 53 places, 58 transitions, 209 flow
[2023-10-27 12:50:27,880 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=234, PETRI_DIFFERENCE_MINUEND_FLOW=187, PETRI_DIFFERENCE_MINUEND_PLACES=49, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=56, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=53, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=209, PETRI_PLACES=53, PETRI_TRANSITIONS=58}
[2023-10-27 12:50:27,881 INFO  L288   CegarLoopForPetriNet]: 46 programPoint places, 7 predicate places.
[2023-10-27 12:50:27,883 INFO  L495      AbstractCegarLoop]: Abstraction has has 53 places, 58 transitions, 209 flow
[2023-10-27 12:50:27,884 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 129.33333333333334) internal successors, (388), 3 states have internal predecessors, (388), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:27,884 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:27,884 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:27,884 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2023-10-27 12:50:27,885 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2023-10-27 12:50:27,885 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:27,885 INFO  L85        PathProgramCache]: Analyzing trace with hash 832391173, now seen corresponding path program 1 times
[2023-10-27 12:50:27,885 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:27,886 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [177126794]
[2023-10-27 12:50:27,886 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:27,886 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:27,923 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:28,089 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:28,089 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:28,089 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [177126794]
[2023-10-27 12:50:28,090 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [177126794] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:28,090 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:28,090 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:28,090 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1844664836]
[2023-10-27 12:50:28,090 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:28,090 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:28,090 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:28,091 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:28,091 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:28,118 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 123 out of 234
[2023-10-27 12:50:28,118 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 53 places, 58 transitions, 209 flow. Second operand  has 3 states, 3 states have (on average 127.0) internal successors, (381), 3 states have internal predecessors, (381), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:28,119 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:28,119 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 123 of 234
[2023-10-27 12:50:28,119 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:28,249 INFO  L130       PetriNetUnfolder]: 223/623 cut-off events.
[2023-10-27 12:50:28,251 INFO  L131       PetriNetUnfolder]: For 216/251 co-relation queries the response was YES.
[2023-10-27 12:50:28,252 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1415 conditions, 623 events. 223/623 cut-off events. For 216/251 co-relation queries the response was YES. Maximal size of possible extension queue 52. Compared 3564 event pairs, 104 based on Foata normal form. 3/573 useless extension candidates. Maximal degree in co-relation 1347. Up to 397 conditions per place. 
[2023-10-27 12:50:28,254 INFO  L137   encePairwiseOnDemand]: 227/234 looper letters, 41 selfloop transitions, 11 changer transitions 0/75 dead transitions.
[2023-10-27 12:50:28,254 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 55 places, 75 transitions, 369 flow
[2023-10-27 12:50:28,255 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:28,255 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:28,255 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 407 transitions.
[2023-10-27 12:50:28,256 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5797720797720798
[2023-10-27 12:50:28,256 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 407 transitions.
[2023-10-27 12:50:28,257 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 407 transitions.
[2023-10-27 12:50:28,259 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:28,260 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 407 transitions.
[2023-10-27 12:50:28,261 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 135.66666666666666) internal successors, (407), 3 states have internal predecessors, (407), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:28,267 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:28,268 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 234.0) internal successors, (936), 4 states have internal predecessors, (936), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:28,268 INFO  L175             Difference]: Start difference. First operand has 53 places, 58 transitions, 209 flow. Second operand 3 states and 407 transitions.
[2023-10-27 12:50:28,268 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 55 places, 75 transitions, 369 flow
[2023-10-27 12:50:28,269 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 53 places, 75 transitions, 363 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:28,271 INFO  L231             Difference]: Finished difference. Result has 55 places, 65 transitions, 291 flow
[2023-10-27 12:50:28,271 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=234, PETRI_DIFFERENCE_MINUEND_FLOW=203, PETRI_DIFFERENCE_MINUEND_PLACES=51, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=58, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=47, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=291, PETRI_PLACES=55, PETRI_TRANSITIONS=65}
[2023-10-27 12:50:28,272 INFO  L288   CegarLoopForPetriNet]: 46 programPoint places, 9 predicate places.
[2023-10-27 12:50:28,273 INFO  L495      AbstractCegarLoop]: Abstraction has has 55 places, 65 transitions, 291 flow
[2023-10-27 12:50:28,273 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 127.0) internal successors, (381), 3 states have internal predecessors, (381), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:28,273 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:28,273 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1]
[2023-10-27 12:50:28,273 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2023-10-27 12:50:28,273 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2023-10-27 12:50:28,285 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:28,286 INFO  L85        PathProgramCache]: Analyzing trace with hash -402211179, now seen corresponding path program 1 times
[2023-10-27 12:50:28,286 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:28,286 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1038595414]
[2023-10-27 12:50:28,286 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:28,287 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:28,336 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:50:28,337 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-27 12:50:28,368 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:50:28,401 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-27 12:50:28,415 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-27 12:50:28,416 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (11 of 12 remaining)
[2023-10-27 12:50:28,418 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (10 of 12 remaining)
[2023-10-27 12:50:28,418 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (9 of 12 remaining)
[2023-10-27 12:50:28,418 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (8 of 12 remaining)
[2023-10-27 12:50:28,418 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (7 of 12 remaining)
[2023-10-27 12:50:28,419 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (6 of 12 remaining)
[2023-10-27 12:50:28,419 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (5 of 12 remaining)
[2023-10-27 12:50:28,419 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (4 of 12 remaining)
[2023-10-27 12:50:28,419 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (3 of 12 remaining)
[2023-10-27 12:50:28,419 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 12 remaining)
[2023-10-27 12:50:28,419 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (1 of 12 remaining)
[2023-10-27 12:50:28,420 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (0 of 12 remaining)
[2023-10-27 12:50:28,420 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2023-10-27 12:50:28,420 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2023-10-27 12:50:28,422 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-10-27 12:50:28,422 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2023-10-27 12:50:28,456 INFO  L144    ThreadInstanceAdder]: Constructed 0 joinOtherThreadTransitions.
[2023-10-27 12:50:28,467 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 166 places, 165 transitions, 342 flow
[2023-10-27 12:50:28,519 INFO  L130       PetriNetUnfolder]: 10/263 cut-off events.
[2023-10-27 12:50:28,519 INFO  L131       PetriNetUnfolder]: For 2/2 co-relation queries the response was YES.
[2023-10-27 12:50:28,520 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 273 conditions, 263 events. 10/263 cut-off events. For 2/2 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 374 event pairs, 0 based on Foata normal form. 0/230 useless extension candidates. Maximal degree in co-relation 177. Up to 6 conditions per place. 
[2023-10-27 12:50:28,520 INFO  L82        GeneralOperation]: Start removeDead. Operand has 166 places, 165 transitions, 342 flow
[2023-10-27 12:50:28,521 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 166 places, 165 transitions, 342 flow
[2023-10-27 12:50:28,521 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-27 12:50:28,521 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 166 places, 165 transitions, 342 flow
[2023-10-27 12:50:28,522 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 166 places, 165 transitions, 342 flow
[2023-10-27 12:50:28,522 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 166 places, 165 transitions, 342 flow
[2023-10-27 12:50:28,559 INFO  L130       PetriNetUnfolder]: 10/263 cut-off events.
[2023-10-27 12:50:28,560 INFO  L131       PetriNetUnfolder]: For 2/2 co-relation queries the response was YES.
[2023-10-27 12:50:28,560 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 273 conditions, 263 events. 10/263 cut-off events. For 2/2 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 374 event pairs, 0 based on Foata normal form. 0/230 useless extension candidates. Maximal degree in co-relation 177. Up to 6 conditions per place. 
[2023-10-27 12:50:28,564 INFO  L119        LiptonReduction]: Number of co-enabled transitions 8232
[2023-10-27 12:50:32,403 INFO  L134        LiptonReduction]: Checked pairs total: 37075
[2023-10-27 12:50:32,404 INFO  L136        LiptonReduction]: Total number of compositions: 109
[2023-10-27 12:50:32,405 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-27 12:50:32,416 INFO  L357      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mHoare=true, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=LoopsAndPotentialCycles, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@5229e3b6, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-27 12:50:32,416 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 15 error locations.
[2023-10-27 12:50:32,417 INFO  L130       PetriNetUnfolder]: 0/6 cut-off events.
[2023-10-27 12:50:32,418 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:50:32,418 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:32,418 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1]
[2023-10-27 12:50:32,418 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:32,418 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:32,418 INFO  L85        PathProgramCache]: Analyzing trace with hash 23137701, now seen corresponding path program 1 times
[2023-10-27 12:50:32,418 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:32,418 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1770835433]
[2023-10-27 12:50:32,418 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:32,419 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:32,438 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:32,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:32,464 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:32,467 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1770835433]
[2023-10-27 12:50:32,467 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1770835433] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:32,467 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:32,467 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:32,467 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1007720518]
[2023-10-27 12:50:32,467 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:32,468 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:32,468 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:32,469 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:32,469 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:32,495 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 145 out of 274
[2023-10-27 12:50:32,496 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 66 places, 63 transitions, 138 flow. Second operand  has 3 states, 3 states have (on average 146.33333333333334) internal successors, (439), 3 states have internal predecessors, (439), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:32,496 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:32,496 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 145 of 274
[2023-10-27 12:50:32,496 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:34,329 INFO  L130       PetriNetUnfolder]: 6897/13150 cut-off events.
[2023-10-27 12:50:34,333 INFO  L131       PetriNetUnfolder]: For 75/75 co-relation queries the response was YES.
[2023-10-27 12:50:34,361 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 24191 conditions, 13150 events. 6897/13150 cut-off events. For 75/75 co-relation queries the response was YES. Maximal size of possible extension queue 511. Compared 106541 event pairs, 2899 based on Foata normal form. 0/12061 useless extension candidates. Maximal degree in co-relation 10367. Up to 5879 conditions per place. 
[2023-10-27 12:50:34,468 INFO  L137   encePairwiseOnDemand]: 257/274 looper letters, 67 selfloop transitions, 11 changer transitions 0/97 dead transitions.
[2023-10-27 12:50:34,468 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 67 places, 97 transitions, 367 flow
[2023-10-27 12:50:34,469 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:34,469 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:34,470 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 521 transitions.
[2023-10-27 12:50:34,470 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6338199513381995
[2023-10-27 12:50:34,470 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 521 transitions.
[2023-10-27 12:50:34,470 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 521 transitions.
[2023-10-27 12:50:34,470 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:34,471 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 521 transitions.
[2023-10-27 12:50:34,472 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 173.66666666666666) internal successors, (521), 3 states have internal predecessors, (521), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:34,473 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:34,473 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:34,473 INFO  L175             Difference]: Start difference. First operand has 66 places, 63 transitions, 138 flow. Second operand 3 states and 521 transitions.
[2023-10-27 12:50:34,474 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 67 places, 97 transitions, 367 flow
[2023-10-27 12:50:34,474 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 67 places, 97 transitions, 365 flow, removed 1 selfloop flow, removed 0 redundant places.
[2023-10-27 12:50:34,476 INFO  L231             Difference]: Finished difference. Result has 69 places, 72 transitions, 228 flow
[2023-10-27 12:50:34,493 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=132, PETRI_DIFFERENCE_MINUEND_PLACES=65, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=61, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=50, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=228, PETRI_PLACES=69, PETRI_TRANSITIONS=72}
[2023-10-27 12:50:34,497 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 3 predicate places.
[2023-10-27 12:50:34,497 INFO  L495      AbstractCegarLoop]: Abstraction has has 69 places, 72 transitions, 228 flow
[2023-10-27 12:50:34,500 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 146.33333333333334) internal successors, (439), 3 states have internal predecessors, (439), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:34,501 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:34,501 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:34,501 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2023-10-27 12:50:34,501 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:34,501 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:34,502 INFO  L85        PathProgramCache]: Analyzing trace with hash 1933570323, now seen corresponding path program 1 times
[2023-10-27 12:50:34,502 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:34,502 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [19190611]
[2023-10-27 12:50:34,502 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:34,502 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:34,510 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:34,537 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:34,537 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:34,537 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [19190611]
[2023-10-27 12:50:34,537 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [19190611] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:34,538 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:34,538 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:34,539 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [445640848]
[2023-10-27 12:50:34,539 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:34,540 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:34,542 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:34,542 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:34,542 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:34,551 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 155 out of 274
[2023-10-27 12:50:34,552 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 69 places, 72 transitions, 228 flow. Second operand  has 3 states, 3 states have (on average 156.33333333333334) internal successors, (469), 3 states have internal predecessors, (469), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:34,552 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:34,552 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 155 of 274
[2023-10-27 12:50:34,552 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:36,154 INFO  L130       PetriNetUnfolder]: 6163/12024 cut-off events.
[2023-10-27 12:50:36,154 INFO  L131       PetriNetUnfolder]: For 2641/2786 co-relation queries the response was YES.
[2023-10-27 12:50:36,175 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 25283 conditions, 12024 events. 6163/12024 cut-off events. For 2641/2786 co-relation queries the response was YES. Maximal size of possible extension queue 512. Compared 100210 event pairs, 3703 based on Foata normal form. 8/11279 useless extension candidates. Maximal degree in co-relation 7057. Up to 7537 conditions per place. 
[2023-10-27 12:50:36,259 INFO  L137   encePairwiseOnDemand]: 269/274 looper letters, 60 selfloop transitions, 4 changer transitions 0/97 dead transitions.
[2023-10-27 12:50:36,260 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 71 places, 97 transitions, 424 flow
[2023-10-27 12:50:36,260 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:36,260 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:36,262 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 523 transitions.
[2023-10-27 12:50:36,262 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6362530413625304
[2023-10-27 12:50:36,262 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 523 transitions.
[2023-10-27 12:50:36,262 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 523 transitions.
[2023-10-27 12:50:36,263 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:36,263 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 523 transitions.
[2023-10-27 12:50:36,264 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 174.33333333333334) internal successors, (523), 3 states have internal predecessors, (523), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:36,265 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:36,266 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:36,266 INFO  L175             Difference]: Start difference. First operand has 69 places, 72 transitions, 228 flow. Second operand 3 states and 523 transitions.
[2023-10-27 12:50:36,266 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 71 places, 97 transitions, 424 flow
[2023-10-27 12:50:36,272 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 69 places, 97 transitions, 396 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:36,287 INFO  L231             Difference]: Finished difference. Result has 71 places, 75 transitions, 236 flow
[2023-10-27 12:50:36,287 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=206, PETRI_DIFFERENCE_MINUEND_PLACES=67, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=72, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=68, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=236, PETRI_PLACES=71, PETRI_TRANSITIONS=75}
[2023-10-27 12:50:36,289 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 5 predicate places.
[2023-10-27 12:50:36,289 INFO  L495      AbstractCegarLoop]: Abstraction has has 71 places, 75 transitions, 236 flow
[2023-10-27 12:50:36,289 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 156.33333333333334) internal successors, (469), 3 states have internal predecessors, (469), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:36,289 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:36,289 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:36,289 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2023-10-27 12:50:36,290 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:36,290 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:36,290 INFO  L85        PathProgramCache]: Analyzing trace with hash 707870376, now seen corresponding path program 1 times
[2023-10-27 12:50:36,290 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:36,290 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [63333649]
[2023-10-27 12:50:36,290 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:36,291 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:36,297 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:36,320 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:36,320 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:36,320 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [63333649]
[2023-10-27 12:50:36,320 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [63333649] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:36,320 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:36,320 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:36,321 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [251165348]
[2023-10-27 12:50:36,321 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:36,321 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:36,321 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:36,321 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:36,321 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:36,358 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 148 out of 274
[2023-10-27 12:50:36,360 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 71 places, 75 transitions, 236 flow. Second operand  has 3 states, 3 states have (on average 150.0) internal successors, (450), 3 states have internal predecessors, (450), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:36,360 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:36,360 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 148 of 274
[2023-10-27 12:50:36,360 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:37,990 INFO  L130       PetriNetUnfolder]: 6394/12647 cut-off events.
[2023-10-27 12:50:37,990 INFO  L131       PetriNetUnfolder]: For 2400/2499 co-relation queries the response was YES.
[2023-10-27 12:50:38,006 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 27002 conditions, 12647 events. 6394/12647 cut-off events. For 2400/2499 co-relation queries the response was YES. Maximal size of possible extension queue 541. Compared 107470 event pairs, 4163 based on Foata normal form. 25/11602 useless extension candidates. Maximal degree in co-relation 22451. Up to 8963 conditions per place. 
[2023-10-27 12:50:38,119 INFO  L137   encePairwiseOnDemand]: 266/274 looper letters, 57 selfloop transitions, 12 changer transitions 0/101 dead transitions.
[2023-10-27 12:50:38,119 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 73 places, 101 transitions, 444 flow
[2023-10-27 12:50:38,119 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:38,119 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:38,121 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 502 transitions.
[2023-10-27 12:50:38,121 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.610705596107056
[2023-10-27 12:50:38,121 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 502 transitions.
[2023-10-27 12:50:38,121 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 502 transitions.
[2023-10-27 12:50:38,122 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:38,122 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 502 transitions.
[2023-10-27 12:50:38,123 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 167.33333333333334) internal successors, (502), 3 states have internal predecessors, (502), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:38,125 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:38,126 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:38,126 INFO  L175             Difference]: Start difference. First operand has 71 places, 75 transitions, 236 flow. Second operand 3 states and 502 transitions.
[2023-10-27 12:50:38,126 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 73 places, 101 transitions, 444 flow
[2023-10-27 12:50:38,148 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 71 places, 101 transitions, 436 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:38,150 INFO  L231             Difference]: Finished difference. Result has 73 places, 85 transitions, 334 flow
[2023-10-27 12:50:38,151 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=228, PETRI_DIFFERENCE_MINUEND_PLACES=69, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=75, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=63, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=334, PETRI_PLACES=73, PETRI_TRANSITIONS=85}
[2023-10-27 12:50:38,152 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 7 predicate places.
[2023-10-27 12:50:38,152 INFO  L495      AbstractCegarLoop]: Abstraction has has 73 places, 85 transitions, 334 flow
[2023-10-27 12:50:38,152 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 150.0) internal successors, (450), 3 states have internal predecessors, (450), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:38,152 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:38,152 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:38,153 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2023-10-27 12:50:38,153 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:38,153 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:38,153 INFO  L85        PathProgramCache]: Analyzing trace with hash -1492693568, now seen corresponding path program 1 times
[2023-10-27 12:50:38,153 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:38,153 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1709215321]
[2023-10-27 12:50:38,154 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:38,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:38,172 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:38,211 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:38,212 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:38,212 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1709215321]
[2023-10-27 12:50:38,212 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1709215321] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:38,212 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:38,212 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:38,212 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [619093778]
[2023-10-27 12:50:38,212 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:38,213 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:38,213 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:38,213 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:38,213 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:38,246 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 149 out of 274
[2023-10-27 12:50:38,247 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 73 places, 85 transitions, 334 flow. Second operand  has 3 states, 3 states have (on average 153.33333333333334) internal successors, (460), 3 states have internal predecessors, (460), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:38,247 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:38,247 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 149 of 274
[2023-10-27 12:50:38,247 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:39,836 INFO  L130       PetriNetUnfolder]: 7449/14345 cut-off events.
[2023-10-27 12:50:39,837 INFO  L131       PetriNetUnfolder]: For 9104/9923 co-relation queries the response was YES.
[2023-10-27 12:50:39,852 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 34391 conditions, 14345 events. 7449/14345 cut-off events. For 9104/9923 co-relation queries the response was YES. Maximal size of possible extension queue 626. Compared 122396 event pairs, 4147 based on Foata normal form. 115/13029 useless extension candidates. Maximal degree in co-relation 21305. Up to 10066 conditions per place. 
[2023-10-27 12:50:39,923 INFO  L137   encePairwiseOnDemand]: 265/274 looper letters, 67 selfloop transitions, 19 changer transitions 0/118 dead transitions.
[2023-10-27 12:50:39,937 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 75 places, 118 transitions, 643 flow
[2023-10-27 12:50:39,937 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:39,938 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:39,938 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 506 transitions.
[2023-10-27 12:50:39,939 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6155717761557178
[2023-10-27 12:50:39,939 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 506 transitions.
[2023-10-27 12:50:39,939 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 506 transitions.
[2023-10-27 12:50:39,939 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:39,939 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 506 transitions.
[2023-10-27 12:50:39,941 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 168.66666666666666) internal successors, (506), 3 states have internal predecessors, (506), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:39,954 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:39,954 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:39,955 INFO  L175             Difference]: Start difference. First operand has 73 places, 85 transitions, 334 flow. Second operand 3 states and 506 transitions.
[2023-10-27 12:50:39,955 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 75 places, 118 transitions, 643 flow
[2023-10-27 12:50:40,001 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 73 places, 118 transitions, 605 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:40,010 INFO  L231             Difference]: Finished difference. Result has 75 places, 100 transitions, 492 flow
[2023-10-27 12:50:40,010 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=310, PETRI_DIFFERENCE_MINUEND_PLACES=71, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=85, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=66, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=492, PETRI_PLACES=75, PETRI_TRANSITIONS=100}
[2023-10-27 12:50:40,012 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 9 predicate places.
[2023-10-27 12:50:40,012 INFO  L495      AbstractCegarLoop]: Abstraction has has 75 places, 100 transitions, 492 flow
[2023-10-27 12:50:40,012 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 153.33333333333334) internal successors, (460), 3 states have internal predecessors, (460), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:40,012 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:40,012 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:40,012 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2023-10-27 12:50:40,013 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:40,013 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:40,013 INFO  L85        PathProgramCache]: Analyzing trace with hash -683117820, now seen corresponding path program 1 times
[2023-10-27 12:50:40,013 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:40,013 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1232480052]
[2023-10-27 12:50:40,013 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:40,014 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:40,040 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:40,168 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2023-10-27 12:50:40,168 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:40,168 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1232480052]
[2023-10-27 12:50:40,171 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1232480052] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:40,171 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:40,171 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [3] imperfect sequences [] total 3
[2023-10-27 12:50:40,171 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2076616727]
[2023-10-27 12:50:40,171 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:40,172 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:40,172 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:40,173 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:40,173 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:40,212 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 147 out of 274
[2023-10-27 12:50:40,212 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 75 places, 100 transitions, 492 flow. Second operand  has 3 states, 3 states have (on average 151.0) internal successors, (453), 3 states have internal predecessors, (453), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:40,212 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:40,213 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 147 of 274
[2023-10-27 12:50:40,213 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:40,891 INFO  L130       PetriNetUnfolder]: 2137/5080 cut-off events.
[2023-10-27 12:50:40,891 INFO  L131       PetriNetUnfolder]: For 2188/2277 co-relation queries the response was YES.
[2023-10-27 12:50:40,906 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 11650 conditions, 5080 events. 2137/5080 cut-off events. For 2188/2277 co-relation queries the response was YES. Maximal size of possible extension queue 260. Compared 42259 event pairs, 856 based on Foata normal form. 296/5119 useless extension candidates. Maximal degree in co-relation 7132. Up to 2054 conditions per place. 
[2023-10-27 12:50:40,925 INFO  L137   encePairwiseOnDemand]: 262/274 looper letters, 66 selfloop transitions, 14 changer transitions 0/123 dead transitions.
[2023-10-27 12:50:40,940 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 77 places, 123 transitions, 687 flow
[2023-10-27 12:50:40,941 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:40,941 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:40,942 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 505 transitions.
[2023-10-27 12:50:40,943 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6143552311435523
[2023-10-27 12:50:40,943 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 505 transitions.
[2023-10-27 12:50:40,943 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 505 transitions.
[2023-10-27 12:50:40,943 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:40,943 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 505 transitions.
[2023-10-27 12:50:40,944 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 168.33333333333334) internal successors, (505), 3 states have internal predecessors, (505), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:40,946 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:40,946 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:40,946 INFO  L175             Difference]: Start difference. First operand has 75 places, 100 transitions, 492 flow. Second operand 3 states and 505 transitions.
[2023-10-27 12:50:40,946 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 77 places, 123 transitions, 687 flow
[2023-10-27 12:50:40,951 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 75 places, 123 transitions, 661 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:50:40,954 INFO  L231             Difference]: Finished difference. Result has 76 places, 99 transitions, 466 flow
[2023-10-27 12:50:40,955 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=380, PETRI_DIFFERENCE_MINUEND_PLACES=73, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=90, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=5, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=76, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=466, PETRI_PLACES=76, PETRI_TRANSITIONS=99}
[2023-10-27 12:50:40,955 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 10 predicate places.
[2023-10-27 12:50:40,968 INFO  L495      AbstractCegarLoop]: Abstraction has has 76 places, 99 transitions, 466 flow
[2023-10-27 12:50:40,969 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 151.0) internal successors, (453), 3 states have internal predecessors, (453), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:40,969 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:40,969 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:40,969 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2023-10-27 12:50:40,969 INFO  L420      AbstractCegarLoop]: === Iteration 6 === Targeting threadErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:40,969 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:40,970 INFO  L85        PathProgramCache]: Analyzing trace with hash 381404354, now seen corresponding path program 1 times
[2023-10-27 12:50:40,971 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:40,971 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [5528926]
[2023-10-27 12:50:40,971 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:40,971 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:40,980 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:41,018 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:50:41,018 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:41,018 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [5528926]
[2023-10-27 12:50:41,019 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [5528926] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:41,019 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:41,019 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:41,019 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1826173999]
[2023-10-27 12:50:41,019 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:41,019 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:41,019 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:41,020 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:41,020 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:41,030 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 153 out of 274
[2023-10-27 12:50:41,030 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 76 places, 99 transitions, 466 flow. Second operand  has 3 states, 3 states have (on average 158.33333333333334) internal successors, (475), 3 states have internal predecessors, (475), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:41,030 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:41,030 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 153 of 274
[2023-10-27 12:50:41,030 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:41,576 INFO  L130       PetriNetUnfolder]: 2743/5888 cut-off events.
[2023-10-27 12:50:41,576 INFO  L131       PetriNetUnfolder]: For 3668/3931 co-relation queries the response was YES.
[2023-10-27 12:50:41,582 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 15496 conditions, 5888 events. 2743/5888 cut-off events. For 3668/3931 co-relation queries the response was YES. Maximal size of possible extension queue 285. Compared 46598 event pairs, 1891 based on Foata normal form. 119/5601 useless extension candidates. Maximal degree in co-relation 7486. Up to 4358 conditions per place. 
[2023-10-27 12:50:41,592 INFO  L137   encePairwiseOnDemand]: 269/274 looper letters, 78 selfloop transitions, 6 changer transitions 0/127 dead transitions.
[2023-10-27 12:50:41,592 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 78 places, 127 transitions, 760 flow
[2023-10-27 12:50:41,592 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:41,592 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:41,594 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 516 transitions.
[2023-10-27 12:50:41,609 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6277372262773723
[2023-10-27 12:50:41,609 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 516 transitions.
[2023-10-27 12:50:41,609 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 516 transitions.
[2023-10-27 12:50:41,610 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:41,610 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 516 transitions.
[2023-10-27 12:50:41,611 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 172.0) internal successors, (516), 3 states have internal predecessors, (516), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:41,612 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:41,621 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:41,621 INFO  L175             Difference]: Start difference. First operand has 76 places, 99 transitions, 466 flow. Second operand 3 states and 516 transitions.
[2023-10-27 12:50:41,621 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 78 places, 127 transitions, 760 flow
[2023-10-27 12:50:41,627 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 77 places, 127 transitions, 739 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-10-27 12:50:41,628 INFO  L231             Difference]: Finished difference. Result has 78 places, 103 transitions, 494 flow
[2023-10-27 12:50:41,642 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=452, PETRI_DIFFERENCE_MINUEND_PLACES=75, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=99, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=93, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=494, PETRI_PLACES=78, PETRI_TRANSITIONS=103}
[2023-10-27 12:50:41,644 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 12 predicate places.
[2023-10-27 12:50:41,644 INFO  L495      AbstractCegarLoop]: Abstraction has has 78 places, 103 transitions, 494 flow
[2023-10-27 12:50:41,644 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 158.33333333333334) internal successors, (475), 3 states have internal predecessors, (475), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:41,644 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:41,645 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:41,645 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2023-10-27 12:50:41,645 INFO  L420      AbstractCegarLoop]: === Iteration 7 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:41,645 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:41,645 INFO  L85        PathProgramCache]: Analyzing trace with hash 1121615732, now seen corresponding path program 1 times
[2023-10-27 12:50:41,646 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:41,646 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1983397742]
[2023-10-27 12:50:41,646 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:41,646 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:41,657 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:50:41,694 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2023-10-27 12:50:41,695 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:50:41,696 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1983397742]
[2023-10-27 12:50:41,697 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1983397742] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:50:41,697 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:50:41,697 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:50:41,697 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1032805223]
[2023-10-27 12:50:41,697 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:50:41,697 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:50:41,697 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:50:41,698 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:50:41,698 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:50:41,723 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 149 out of 274
[2023-10-27 12:50:41,724 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 78 places, 103 transitions, 494 flow. Second operand  has 3 states, 3 states have (on average 153.66666666666666) internal successors, (461), 3 states have internal predecessors, (461), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:41,724 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:50:41,724 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 149 of 274
[2023-10-27 12:50:41,724 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:50:42,444 INFO  L130       PetriNetUnfolder]: 2495/5558 cut-off events.
[2023-10-27 12:50:42,444 INFO  L131       PetriNetUnfolder]: For 4957/5203 co-relation queries the response was YES.
[2023-10-27 12:50:42,450 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 15347 conditions, 5558 events. 2495/5558 cut-off events. For 4957/5203 co-relation queries the response was YES. Maximal size of possible extension queue 275. Compared 44466 event pairs, 1665 based on Foata normal form. 8/5225 useless extension candidates. Maximal degree in co-relation 7874. Up to 4035 conditions per place. 
[2023-10-27 12:50:42,458 INFO  L137   encePairwiseOnDemand]: 267/274 looper letters, 79 selfloop transitions, 12 changer transitions 0/128 dead transitions.
[2023-10-27 12:50:42,458 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 80 places, 128 transitions, 789 flow
[2023-10-27 12:50:42,458 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:50:42,459 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:50:42,472 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 501 transitions.
[2023-10-27 12:50:42,473 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6094890510948905
[2023-10-27 12:50:42,473 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 501 transitions.
[2023-10-27 12:50:42,473 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 501 transitions.
[2023-10-27 12:50:42,479 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:50:42,479 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 501 transitions.
[2023-10-27 12:50:42,480 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 167.0) internal successors, (501), 3 states have internal predecessors, (501), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:42,481 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:42,481 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 274.0) internal successors, (1096), 4 states have internal predecessors, (1096), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:42,482 INFO  L175             Difference]: Start difference. First operand has 78 places, 103 transitions, 494 flow. Second operand 3 states and 501 transitions.
[2023-10-27 12:50:42,482 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 80 places, 128 transitions, 789 flow
[2023-10-27 12:50:42,492 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 79 places, 128 transitions, 780 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-10-27 12:50:42,506 INFO  L231             Difference]: Finished difference. Result has 81 places, 111 transitions, 598 flow
[2023-10-27 12:50:42,506 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=274, PETRI_DIFFERENCE_MINUEND_FLOW=488, PETRI_DIFFERENCE_MINUEND_PLACES=77, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=103, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=91, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=598, PETRI_PLACES=81, PETRI_TRANSITIONS=111}
[2023-10-27 12:50:42,507 INFO  L288   CegarLoopForPetriNet]: 66 programPoint places, 15 predicate places.
[2023-10-27 12:50:42,507 INFO  L495      AbstractCegarLoop]: Abstraction has has 81 places, 111 transitions, 598 flow
[2023-10-27 12:50:42,507 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 153.66666666666666) internal successors, (461), 3 states have internal predecessors, (461), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:50:42,507 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:50:42,508 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:42,508 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2023-10-27 12:50:42,508 INFO  L420      AbstractCegarLoop]: === Iteration 8 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-10-27 12:50:42,508 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:50:42,508 INFO  L85        PathProgramCache]: Analyzing trace with hash 1095061694, now seen corresponding path program 1 times
[2023-10-27 12:50:42,508 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:50:42,514 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1384860343]
[2023-10-27 12:50:42,514 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:50:42,514 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:50:42,543 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:50:42,557 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-27 12:50:42,570 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:50:42,578 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-27 12:50:42,578 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-27 12:50:42,579 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (14 of 15 remaining)
[2023-10-27 12:50:42,579 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (13 of 15 remaining)
[2023-10-27 12:50:42,579 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (12 of 15 remaining)
[2023-10-27 12:50:42,579 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (11 of 15 remaining)
[2023-10-27 12:50:42,593 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (10 of 15 remaining)
[2023-10-27 12:50:42,593 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (9 of 15 remaining)
[2023-10-27 12:50:42,593 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (8 of 15 remaining)
[2023-10-27 12:50:42,593 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (7 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (6 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (5 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (4 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (3 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (1 of 15 remaining)
[2023-10-27 12:50:42,594 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (0 of 15 remaining)
[2023-10-27 12:50:42,594 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2023-10-27 12:50:42,595 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:50:42,599 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 2 thread instances
[2023-10-27 12:50:42,599 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2023-10-27 12:50:42,681 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 27.10 12:50:42 BasicIcfg
[2023-10-27 12:50:42,682 INFO  L132        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2023-10-27 12:50:42,682 INFO  L113        PluginConnector]: ------------------------Witness Printer----------------------------
[2023-10-27 12:50:42,682 INFO  L271        PluginConnector]: Initializing Witness Printer...
[2023-10-27 12:50:42,682 INFO  L275        PluginConnector]: Witness Printer initialized
[2023-10-27 12:50:42,683 INFO  L185        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 27.10 12:50:21" (3/4) ...
[2023-10-27 12:50:42,685 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2023-10-27 12:50:42,685 INFO  L132        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2023-10-27 12:50:42,685 INFO  L158              Benchmark]: Toolchain (without parser) took 22539.21ms. Allocated memory was 45.7MB in the beginning and 160.5MB in the end (delta: 114.8MB). Free memory was 15.1MB in the beginning and 56.6MB in the end (delta: -41.5MB). Peak memory consumption was 73.3MB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,685 INFO  L158              Benchmark]: CDTParser took 2.08ms. Allocated memory is still 40.8MB. Free memory was 15.7MB in the beginning and 15.6MB in the end (delta: 1.6kB). Peak memory consumption was 1.6kB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,686 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 716.13ms. Allocated memory is still 45.7MB. Free memory was 14.9MB in the beginning and 18.0MB in the end (delta: -3.1MB). Peak memory consumption was 3.8MB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,686 INFO  L158              Benchmark]: Boogie Procedure Inliner took 83.89ms. Allocated memory is still 45.7MB. Free memory was 18.0MB in the beginning and 15.8MB in the end (delta: 2.2MB). Peak memory consumption was 2.2MB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,686 INFO  L158              Benchmark]: Boogie Preprocessor took 79.01ms. Allocated memory is still 45.7MB. Free memory was 15.8MB in the beginning and 14.2MB in the end (delta: 1.6MB). Peak memory consumption was 1.6MB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,687 INFO  L158              Benchmark]: RCFGBuilder took 676.17ms. Allocated memory is still 45.7MB. Free memory was 14.2MB in the beginning and 10.7MB in the end (delta: 3.4MB). Peak memory consumption was 3.7MB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,687 INFO  L158              Benchmark]: TraceAbstraction took 20970.74ms. Allocated memory was 45.7MB in the beginning and 160.5MB in the end (delta: 114.8MB). Free memory was 22.2MB in the beginning and 56.6MB in the end (delta: -34.4MB). Peak memory consumption was 80.3MB. Max. memory is 15.6GB.
[2023-10-27 12:50:42,687 INFO  L158              Benchmark]: Witness Printer took 2.71ms. Allocated memory is still 160.5MB. Free memory is still 56.6MB. There was no memory consumed. Max. memory is 15.6GB.
[2023-10-27 12:50:42,689 INFO  L339   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 2.08ms. Allocated memory is still 40.8MB. Free memory was 15.7MB in the beginning and 15.6MB in the end (delta: 1.6kB). Peak memory consumption was 1.6kB. Max. memory is 15.6GB.
 * CACSL2BoogieTranslator took 716.13ms. Allocated memory is still 45.7MB. Free memory was 14.9MB in the beginning and 18.0MB in the end (delta: -3.1MB). Peak memory consumption was 3.8MB. Max. memory is 15.6GB.
 * Boogie Procedure Inliner took 83.89ms. Allocated memory is still 45.7MB. Free memory was 18.0MB in the beginning and 15.8MB in the end (delta: 2.2MB). Peak memory consumption was 2.2MB. Max. memory is 15.6GB.
 * Boogie Preprocessor took 79.01ms. Allocated memory is still 45.7MB. Free memory was 15.8MB in the beginning and 14.2MB in the end (delta: 1.6MB). Peak memory consumption was 1.6MB. Max. memory is 15.6GB.
 * RCFGBuilder took 676.17ms. Allocated memory is still 45.7MB. Free memory was 14.2MB in the beginning and 10.7MB in the end (delta: 3.4MB). Peak memory consumption was 3.7MB. Max. memory is 15.6GB.
 * TraceAbstraction took 20970.74ms. Allocated memory was 45.7MB in the beginning and 160.5MB in the end (delta: 114.8MB). Free memory was 22.2MB in the beginning and 56.6MB in the end (delta: -34.4MB). Peak memory consumption was 80.3MB. Max. memory is 15.6GB.
 * Witness Printer took 2.71ms. Allocated memory is still 160.5MB. Free memory is still 56.6MB. There was no memory consumed. Max. memory is 15.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator:
  - GenericResult: Unfinished Backtranslation
    The program execution was not completely translated back.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 4.3s, 135 PlacesBefore, 46 PlacesAfterwards, 136 TransitionsBefore, 45 TransitionsAfterwards, 3304 CoEnabledTransitionPairs, 6 FixpointIterations, 47 TrivialSequentialCompositions, 43 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 3 ConcurrentYvCompositions, 2 ChoiceCompositions, 98 TotalNumberOfCompositions, 12522 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 5115, independent: 4657, independent conditional: 0, independent unconditional: 4657, dependent: 458, dependent conditional: 0, dependent unconditional: 458, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 1620, independent: 1560, independent conditional: 0, independent unconditional: 1560, dependent: 60, dependent conditional: 0, dependent unconditional: 60, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 5115, independent: 3097, independent conditional: 0, independent unconditional: 3097, dependent: 398, dependent conditional: 0, dependent unconditional: 398, unknown: 1620, unknown conditional: 0, unknown unconditional: 1620] , Statistics on independence cache: Total cache size (in pairs): 297, Positive cache size: 262, Positive conditional cache size: 0, Positive unconditional cache size: 262, Negative cache size: 35, Negative conditional cache size: 0, Negative unconditional cache size: 35, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 3.9s, 166 PlacesBefore, 66 PlacesAfterwards, 165 TransitionsBefore, 63 TransitionsAfterwards, 8232 CoEnabledTransitionPairs, 7 FixpointIterations, 47 TrivialSequentialCompositions, 54 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 3 ConcurrentYvCompositions, 2 ChoiceCompositions, 109 TotalNumberOfCompositions, 37075 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 9452, independent: 8700, independent conditional: 0, independent unconditional: 8700, dependent: 752, dependent conditional: 0, dependent unconditional: 752, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 3556, independent: 3465, independent conditional: 0, independent unconditional: 3465, dependent: 91, dependent conditional: 0, dependent unconditional: 91, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 9452, independent: 5235, independent conditional: 0, independent unconditional: 5235, dependent: 661, dependent conditional: 0, dependent unconditional: 661, unknown: 3556, unknown conditional: 0, unknown unconditional: 3556] , Statistics on independence cache: Total cache size (in pairs): 452, Positive cache size: 401, Positive conditional cache size: 0, Positive unconditional cache size: 401, Negative cache size: 51, Negative conditional cache size: 0, Negative unconditional cache size: 51, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - DataRaceFoundResult [Line: 708]: Data race detected
    Data race detected
The following path leads to a data race: 
[L678]               0  int threads_alive = 0;
[L679]               0  pthread_mutex_t threads_alive_mutex = { { 0, 0, 0, PTHREAD_MUTEX_TIMED_NP, 0, { { 0, 0 } } } };
[L680]               0  pthread_cond_t threads_alive_cond = { { {0}, {0}, {0, 0}, {0, 0}, 0, 0, {0, 0} } };
[L681]               0  int data = 0;
[L682]               0  pthread_mutex_t data_mutex = { { 0, 0, 0, PTHREAD_MUTEX_TIMED_NP, 0, { { 0, 0 } } } };
[L694]               0  int threads_total = __VERIFIER_nondet_int();
[L695]  CALL         0  assume_abort_if_not(threads_total >= 0)
[L675]  COND FALSE   0  !(!cond)
[L695]  RET          0  assume_abort_if_not(threads_total >= 0)
[L696]               0  int i = 0;
        VAL             [data=0, data_mutex={3:0}, i=0, threads_alive=0, threads_alive_cond={2:0}, threads_alive_mutex={1:0}, threads_total=1]
[L696]  COND TRUE    0  i < threads_total
[L698]               0  threads_alive++
[L700]               0  pthread_t tid;
[L701]  FCALL, FORK  0  pthread_create(&tid, ((void *)0), &thread, ((void *)0))
        VAL             [arg={0:0}, data=0, data_mutex={3:0}, i=0, pthread_create(&tid, ((void *)0), &thread, ((void *)0))=-1, threads_alive=1, threads_alive_cond={2:0}, threads_alive_mutex={1:0}, threads_total=1, tid={5:0}]
[L702]  EXPR         0  \read(tid)
[L702]               0  pthread_detach(tid)
[L696]               0  i++
[L685]               1  threads_alive--
[L696]  COND FALSE   0  !(i < threads_total)
[L705]  COND FALSE   0  !(\read(threads_alive))
        VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={3:0}, i=1, threads_alive=0, threads_alive_cond={2:0}, threads_alive_mutex={1:0}, threads_total=1]
[L708]               0  return data;
        VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={3:0}, i=1, threads_alive=0, threads_alive_cond={2:0}, threads_alive_mutex={1:0}, threads_total=1]
[L689]               1  data = __VERIFIER_nondet_int()
        VAL             [__VERIFIER_nondet_int()=0, arg={0:0}, arg={0:0}, data=0, data = __VERIFIER_nondet_int()=51, data_mutex={3:0}, threads_alive=0, threads_alive_cond={2:0}, threads_alive_mutex={1:0}]
[L708]               0  return data;
        VAL             [__VERIFIER_nondet_int()=0, arg={0:0}, arg={0:0}, data=0, data = __VERIFIER_nondet_int()=51, data_mutex={3:0}, i=1, threads_alive=0, threads_alive_cond={2:0}, threads_alive_mutex={1:0}, threads_total=1]

Now there is a data race on ~data~0 between 
	C: data = __VERIFIER_nondet_int() [689]
and
	C: return data; [708]

  - UnprovableResult [Line: 698]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 705]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 698]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 702]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 701]: Unable to prove that petrification did provide enough thread instances (tool internal message, not intended for end users)
    Unable to prove that petrification did provide enough thread instances (tool internal message, not intended for end users)
 Reason: Not analyzed. 
  - UnprovableResult [Line: 685]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 685]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 689]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - StatisticsResult: Ultimate Automizer benchmark data with 1 thread instances
    CFG has 3 procedures, 162 locations, 12 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 6.5s, OverallIterations: 5, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 4.6s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 164 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 77 mSDsluCounter, 26 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 26 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 289 IncrementalHoareTripleChecker+Invalid, 315 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 26 mSolverCounterUnsat, 26 mSDtfsCounter, 289 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 8 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=291occurred in iteration=4, InterpolantAutomatonStates: 12, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 0.4s InterpolantComputationTime, 57 NumberOfCodeBlocks, 57 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 33 ConstructedInterpolants, 0 QuantifiedInterpolants, 41 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 4 InterpolantComputations, 4 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
  - StatisticsResult: Ultimate Automizer benchmark data with 2 thread instances
    CFG has 4 procedures, 191 locations, 15 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 14.1s, OverallIterations: 8, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 9.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 3.9s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 371 SdHoareTripleChecker+Valid, 1.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 201 mSDsluCounter, 34 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 58 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 743 IncrementalHoareTripleChecker+Invalid, 801 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 58 mSolverCounterUnsat, 34 mSDtfsCounter, 743 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 15 GetRequests, 8 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=598occurred in iteration=7, InterpolantAutomatonStates: 21, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.3s InterpolantComputationTime, 138 NumberOfCodeBlocks, 138 NumberOfCodeBlocksAsserted, 8 NumberOfCheckSat, 101 ConstructedInterpolants, 0 QuantifiedInterpolants, 125 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 7 InterpolantComputations, 7 PerfectInterpolantSequences, 10/10 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2023-10-27 12:50:42,800 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...
--- End real Ultimate output ---

Execution finished normally
Writing output log to file Ultimate.log
Writing human readable error path to file UltimateCounterExample.errorpath
Result:
FALSE
