./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-array-dynamic-race.i --full-output --architecture 32bit


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


Checking for data races
Using default analysis
Version 0e0057cc
Calling Ultimate with: /usr/lib/jvm/java-11-openjdk-amd64/bin/java -Dosgi.configuration.area=/mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data -tc /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/config/AutomizerReach.xml -i /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-array-dynamic-race.i -s /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf --cacsl2boogietranslator.entry.function main --witnessprinter.witness.directory /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux --witnessprinter.witness.filename witness --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 42baa13f3c833f066425b90d7117bc629a4606afd0b2e1bcf57fcc9bd3837ebb
--- Real Ultimate output ---
This is Ultimate 0.2.4-dev-0e0057c
[2024-02-28 21:17:22,681 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2024-02-28 21:17:22,718 INFO  L114        SettingsManager]: Loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2024-02-28 21:17:22,722 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2024-02-28 21:17:22,722 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2024-02-28 21:17:22,738 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2024-02-28 21:17:22,739 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2024-02-28 21:17:22,739 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2024-02-28 21:17:22,739 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2024-02-28 21:17:22,740 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2024-02-28 21:17:22,740 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2024-02-28 21:17:22,740 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2024-02-28 21:17:22,741 INFO  L153        SettingsManager]:  * Use SBE=true
[2024-02-28 21:17:22,741 INFO  L151        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2024-02-28 21:17:22,741 INFO  L153        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2024-02-28 21:17:22,741 INFO  L153        SettingsManager]:  * sizeof long=4
[2024-02-28 21:17:22,742 INFO  L153        SettingsManager]:  * Overapproximate operations on floating types=true
[2024-02-28 21:17:22,742 INFO  L153        SettingsManager]:  * sizeof POINTER=4
[2024-02-28 21:17:22,742 INFO  L153        SettingsManager]:  * Check division by zero=IGNORE
[2024-02-28 21:17:22,742 INFO  L153        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2024-02-28 21:17:22,743 INFO  L153        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2024-02-28 21:17:22,743 INFO  L153        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2024-02-28 21:17:22,744 INFO  L153        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2024-02-28 21:17:22,744 INFO  L153        SettingsManager]:  * Check unreachability of reach_error function=false
[2024-02-28 21:17:22,744 INFO  L153        SettingsManager]:  * sizeof long double=12
[2024-02-28 21:17:22,744 INFO  L153        SettingsManager]:  * Check if freed pointer was valid=false
[2024-02-28 21:17:22,744 INFO  L153        SettingsManager]:  * Use constant arrays=true
[2024-02-28 21:17:22,745 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2024-02-28 21:17:22,745 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2024-02-28 21:17:22,745 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2024-02-28 21:17:22,745 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000
[2024-02-28 21:17:22,745 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2024-02-28 21:17:22,746 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2024-02-28 21:17:22,746 INFO  L153        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopHeads
[2024-02-28 21:17:22,746 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2024-02-28 21:17:22,746 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2024-02-28 21:17:22,746 INFO  L153        SettingsManager]:  * Apply one-shot large block encoding in concurrent analysis=false
[2024-02-28 21:17:22,747 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2024-02-28 21:17:22,747 INFO  L153        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2024-02-28 21:17:22,747 INFO  L153        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2024-02-28 21:17:22,747 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2024-02-28 21:17:22,748 INFO  L153        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-pldi24/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-pldi24/UAutomizer-linux
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness filename -> witness
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 -> 42baa13f3c833f066425b90d7117bc629a4606afd0b2e1bcf57fcc9bd3837ebb
[2024-02-28 21:17:23,036 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2024-02-28 21:17:23,053 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2024-02-28 21:17:23,055 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2024-02-28 21:17:23,056 INFO  L270        PluginConnector]: Initializing CDTParser...
[2024-02-28 21:17:23,056 INFO  L274        PluginConnector]: CDTParser initialized
[2024-02-28 21:17:23,057 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-array-dynamic-race.i
[2024-02-28 21:17:24,715 INFO  L533              CDTParser]: Created temporary CDT project at NULL
[2024-02-28 21:17:24,892 INFO  L384              CDTParser]: Found 1 translation units.
[2024-02-28 21:17:24,892 INFO  L180              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-array-dynamic-race.i
[2024-02-28 21:17:24,905 INFO  L427              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data/968f9f5b4/ff61f6860540408caaa0cd6be6efaf50/FLAG9ac2c6d70
[2024-02-28 21:17:24,915 INFO  L435              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data/968f9f5b4/ff61f6860540408caaa0cd6be6efaf50
[2024-02-28 21:17:24,917 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2024-02-28 21:17:24,918 INFO  L133        ToolchainWalker]: Walking toolchain with 6 elements.
[2024-02-28 21:17:24,919 INFO  L112        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2024-02-28 21:17:24,919 INFO  L270        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2024-02-28 21:17:24,923 INFO  L274        PluginConnector]: CACSL2BoogieTranslator initialized
[2024-02-28 21:17:24,924 INFO  L184        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 28.02 09:17:24" (1/1) ...
[2024-02-28 21:17:24,925 INFO  L204        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@2c4f85c2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:24, skipping insertion in model container
[2024-02-28 21:17:24,925 INFO  L184        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 28.02 09:17:24" (1/1) ...
[2024-02-28 21:17:24,963 INFO  L177         MainTranslator]: Built tables and reachable declarations
[2024-02-28 21:17:25,261 INFO  L209          PostProcessor]: Analyzing one entry point: main
[2024-02-28 21:17:25,271 INFO  L202         MainTranslator]: Completed pre-run
[2024-02-28 21:17:25,299 INFO  L209          PostProcessor]: Analyzing one entry point: main
[2024-02-28 21:17:25,336 INFO  L206         MainTranslator]: Completed translation
[2024-02-28 21:17:25,337 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25 WrapperNode
[2024-02-28 21:17:25,337 INFO  L131        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2024-02-28 21:17:25,338 INFO  L112        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2024-02-28 21:17:25,338 INFO  L270        PluginConnector]: Initializing Boogie Procedure Inliner...
[2024-02-28 21:17:25,338 INFO  L274        PluginConnector]: Boogie Procedure Inliner initialized
[2024-02-28 21:17:25,343 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,356 INFO  L184        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,374 INFO  L138                Inliner]: procedures = 269, calls = 23, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 86
[2024-02-28 21:17:25,374 INFO  L131        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2024-02-28 21:17:25,375 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2024-02-28 21:17:25,375 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2024-02-28 21:17:25,375 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2024-02-28 21:17:25,382 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,382 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,386 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,386 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,392 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,394 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,396 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,397 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,400 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2024-02-28 21:17:25,400 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2024-02-28 21:17:25,400 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2024-02-28 21:17:25,401 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2024-02-28 21:17:25,401 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (1/1) ...
[2024-02-28 21:17:25,405 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000
[2024-02-28 21:17:25,414 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-02-28 21:17:25,476 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000 (exit command is (exit), workingDir is null)
[2024-02-28 21:17:25,478 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000 (1)] Waiting until timeout for monitored process
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexUnlock
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2024-02-28 21:17:25,497 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexLock
[2024-02-28 21:17:25,498 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2024-02-28 21:17:25,498 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2024-02-28 21:17:25,498 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2024-02-28 21:17:25,498 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2024-02-28 21:17:25,498 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2024-02-28 21:17:25,498 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2024-02-28 21:17:25,498 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2024-02-28 21:17:25,499 WARN  L213             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to OneNontrivialStatement
[2024-02-28 21:17:25,652 INFO  L241             CfgBuilder]: Building ICFG
[2024-02-28 21:17:25,654 INFO  L267             CfgBuilder]: Building CFG for each procedure with an implementation
[2024-02-28 21:17:25,831 INFO  L282             CfgBuilder]: Performing block encoding
[2024-02-28 21:17:25,859 INFO  L304             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2024-02-28 21:17:25,859 INFO  L309             CfgBuilder]: Removed 2 assume(true) statements.
[2024-02-28 21:17:25,861 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.02 09:17:25 BoogieIcfgContainer
[2024-02-28 21:17:25,861 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2024-02-28 21:17:25,864 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2024-02-28 21:17:25,864 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2024-02-28 21:17:25,867 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2024-02-28 21:17:25,868 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 28.02 09:17:24" (1/3) ...
[2024-02-28 21:17:25,868 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@718785d3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.02 09:17:25, skipping insertion in model container
[2024-02-28 21:17:25,868 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 09:17:25" (2/3) ...
[2024-02-28 21:17:25,869 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@718785d3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.02 09:17:25, skipping insertion in model container
[2024-02-28 21:17:25,869 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.02 09:17:25" (3/3) ...
[2024-02-28 21:17:25,870 INFO  L112   eAbstractionObserver]: Analyzing ICFG thread-join-array-dynamic-race.i
[2024-02-28 21:17:25,883 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2024-02-28 21:17:26,001 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2024-02-28 21:17:26,002 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 6 error locations.
[2024-02-28 21:17:26,002 INFO  L514   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2024-02-28 21:17:26,047 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2024-02-28 21:17:26,125 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 109 places, 110 transitions, 227 flow
[2024-02-28 21:17:26,230 INFO  L124   PetriNetUnfolderBase]: 6/161 cut-off events.
[2024-02-28 21:17:26,231 INFO  L125   PetriNetUnfolderBase]: For 1/1 co-relation queries the response was YES.
[2024-02-28 21:17:26,235 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 166 conditions, 161 events. 6/161 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 327 event pairs, 0 based on Foata normal form. 0/141 useless extension candidates. Maximal degree in co-relation 80. Up to 4 conditions per place. 
[2024-02-28 21:17:26,235 INFO  L82        GeneralOperation]: Start removeDead. Operand has 109 places, 110 transitions, 227 flow
[2024-02-28 21:17:26,239 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 109 places, 110 transitions, 227 flow
[2024-02-28 21:17:26,247 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-02-28 21:17:26,252 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=LoopHeads, 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;@14e9d079, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2024-02-28 21:17:26,252 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 8 error locations.
[2024-02-28 21:17:26,263 INFO  L185   PetriNetUnfolderBase]: Found word, exiting Unfolder.
[2024-02-28 21:17:26,264 INFO  L124   PetriNetUnfolderBase]: 3/52 cut-off events.
[2024-02-28 21:17:26,264 INFO  L125   PetriNetUnfolderBase]: For 0/0 co-relation queries the response was YES.
[2024-02-28 21:17:26,264 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:26,264 INFO  L208   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, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:26,265 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 21:17:26,269 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:26,269 INFO  L85        PathProgramCache]: Analyzing trace with hash -1522027751, now seen corresponding path program 1 times
[2024-02-28 21:17:26,275 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:26,276 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2137557043]
[2024-02-28 21:17:26,276 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:26,276 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:26,424 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:26,890 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:26,891 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:26,891 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2137557043]
[2024-02-28 21:17:26,892 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2137557043] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:26,892 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:26,892 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-02-28 21:17:26,893 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1666839195]
[2024-02-28 21:17:26,894 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:26,899 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-02-28 21:17:26,903 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:26,921 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-02-28 21:17:26,922 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-02-28 21:17:27,150 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 81 out of 110
[2024-02-28 21:17:27,153 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 109 places, 110 transitions, 227 flow. Second operand  has 6 states, 6 states have (on average 82.16666666666667) internal successors, (493), 6 states have internal predecessors, (493), 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)
[2024-02-28 21:17:27,154 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:27,154 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 81 of 110
[2024-02-28 21:17:27,155 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:27,269 INFO  L124   PetriNetUnfolderBase]: 36/306 cut-off events.
[2024-02-28 21:17:27,269 INFO  L125   PetriNetUnfolderBase]: For 4/4 co-relation queries the response was YES.
[2024-02-28 21:17:27,270 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 428 conditions, 306 events. 36/306 cut-off events. For 4/4 co-relation queries the response was YES. Maximal size of possible extension queue 17. Compared 1232 event pairs, 30 based on Foata normal form. 8/281 useless extension candidates. Maximal degree in co-relation 296. Up to 93 conditions per place. 
[2024-02-28 21:17:27,272 INFO  L140   encePairwiseOnDemand]: 91/110 looper letters, 23 selfloop transitions, 13 changer transitions 2/118 dead transitions.
[2024-02-28 21:17:27,272 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 111 places, 118 transitions, 317 flow
[2024-02-28 21:17:27,276 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-02-28 21:17:27,278 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-02-28 21:17:27,286 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 531 transitions.
[2024-02-28 21:17:27,290 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8045454545454546
[2024-02-28 21:17:27,290 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 531 transitions.
[2024-02-28 21:17:27,291 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 531 transitions.
[2024-02-28 21:17:27,294 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:27,296 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 531 transitions.
[2024-02-28 21:17:27,300 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 88.5) internal successors, (531), 6 states have internal predecessors, (531), 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)
[2024-02-28 21:17:27,305 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 110.0) internal successors, (770), 7 states have internal predecessors, (770), 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)
[2024-02-28 21:17:27,305 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 110.0) internal successors, (770), 7 states have internal predecessors, (770), 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)
[2024-02-28 21:17:27,307 INFO  L175             Difference]: Start difference. First operand has 109 places, 110 transitions, 227 flow. Second operand 6 states and 531 transitions.
[2024-02-28 21:17:27,307 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 111 places, 118 transitions, 317 flow
[2024-02-28 21:17:27,310 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 111 places, 118 transitions, 317 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 21:17:27,313 INFO  L231             Difference]: Finished difference. Result has 115 places, 115 transitions, 309 flow
[2024-02-28 21:17:27,314 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=110, PETRI_DIFFERENCE_MINUEND_FLOW=215, PETRI_DIFFERENCE_MINUEND_PLACES=106, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=104, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=91, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=309, PETRI_PLACES=115, PETRI_TRANSITIONS=115}
[2024-02-28 21:17:27,317 INFO  L281   CegarLoopForPetriNet]: 109 programPoint places, 6 predicate places.
[2024-02-28 21:17:27,317 INFO  L495      AbstractCegarLoop]: Abstraction has has 115 places, 115 transitions, 309 flow
[2024-02-28 21:17:27,318 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 82.16666666666667) internal successors, (493), 6 states have internal predecessors, (493), 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)
[2024-02-28 21:17:27,318 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:27,318 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:27,318 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2024-02-28 21:17:27,318 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 21:17:27,319 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:27,319 INFO  L85        PathProgramCache]: Analyzing trace with hash -722223590, now seen corresponding path program 1 times
[2024-02-28 21:17:27,319 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:27,319 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [702362161]
[2024-02-28 21:17:27,319 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:27,320 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:27,333 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:27,352 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:27,353 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:27,353 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [702362161]
[2024-02-28 21:17:27,353 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [702362161] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:27,353 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:27,353 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 21:17:27,353 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2106450263]
[2024-02-28 21:17:27,353 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:27,354 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 21:17:27,355 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:27,355 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 21:17:27,355 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 21:17:27,362 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 99 out of 110
[2024-02-28 21:17:27,362 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 115 places, 115 transitions, 309 flow. Second operand  has 3 states, 3 states have (on average 99.66666666666667) internal successors, (299), 3 states have internal predecessors, (299), 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)
[2024-02-28 21:17:27,362 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:27,363 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 99 of 110
[2024-02-28 21:17:27,363 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:27,393 INFO  L124   PetriNetUnfolderBase]: 9/211 cut-off events.
[2024-02-28 21:17:27,393 INFO  L125   PetriNetUnfolderBase]: For 15/18 co-relation queries the response was YES.
[2024-02-28 21:17:27,394 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 298 conditions, 211 events. 9/211 cut-off events. For 15/18 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 528 event pairs, 1 based on Foata normal form. 0/195 useless extension candidates. Maximal degree in co-relation 174. Up to 16 conditions per place. 
[2024-02-28 21:17:27,395 INFO  L140   encePairwiseOnDemand]: 106/110 looper letters, 8 selfloop transitions, 3 changer transitions 5/119 dead transitions.
[2024-02-28 21:17:27,395 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 116 places, 119 transitions, 341 flow
[2024-02-28 21:17:27,395 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 21:17:27,395 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 21:17:27,396 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 310 transitions.
[2024-02-28 21:17:27,396 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.9393939393939394
[2024-02-28 21:17:27,396 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 310 transitions.
[2024-02-28 21:17:27,396 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 310 transitions.
[2024-02-28 21:17:27,397 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:27,397 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 310 transitions.
[2024-02-28 21:17:27,397 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 103.33333333333333) internal successors, (310), 3 states have internal predecessors, (310), 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)
[2024-02-28 21:17:27,398 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 110.0) internal successors, (440), 4 states have internal predecessors, (440), 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)
[2024-02-28 21:17:27,399 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 110.0) internal successors, (440), 4 states have internal predecessors, (440), 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)
[2024-02-28 21:17:27,399 INFO  L175             Difference]: Start difference. First operand has 115 places, 115 transitions, 309 flow. Second operand 3 states and 310 transitions.
[2024-02-28 21:17:27,399 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 116 places, 119 transitions, 341 flow
[2024-02-28 21:17:27,400 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 115 places, 119 transitions, 337 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-02-28 21:17:27,402 INFO  L231             Difference]: Finished difference. Result has 117 places, 113 transitions, 305 flow
[2024-02-28 21:17:27,402 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=110, PETRI_DIFFERENCE_MINUEND_FLOW=305, PETRI_DIFFERENCE_MINUEND_PLACES=113, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=115, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=112, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=305, PETRI_PLACES=117, PETRI_TRANSITIONS=113}
[2024-02-28 21:17:27,403 INFO  L281   CegarLoopForPetriNet]: 109 programPoint places, 8 predicate places.
[2024-02-28 21:17:27,403 INFO  L495      AbstractCegarLoop]: Abstraction has has 117 places, 113 transitions, 305 flow
[2024-02-28 21:17:27,403 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 99.66666666666667) internal successors, (299), 3 states have internal predecessors, (299), 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)
[2024-02-28 21:17:27,403 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:27,403 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:27,404 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2024-02-28 21:17:27,404 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 21:17:27,404 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:27,404 INFO  L85        PathProgramCache]: Analyzing trace with hash -2017590564, now seen corresponding path program 1 times
[2024-02-28 21:17:27,405 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:27,405 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1658193794]
[2024-02-28 21:17:27,405 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:27,405 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:27,420 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:27,486 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:27,486 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:27,486 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1658193794]
[2024-02-28 21:17:27,487 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1658193794] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:27,487 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:27,487 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-02-28 21:17:27,487 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [806969328]
[2024-02-28 21:17:27,487 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:27,487 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2024-02-28 21:17:27,488 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:27,488 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2024-02-28 21:17:27,488 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=8, Invalid=12, Unknown=0, NotChecked=0, Total=20
[2024-02-28 21:17:27,540 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 92 out of 110
[2024-02-28 21:17:27,541 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 117 places, 113 transitions, 305 flow. Second operand  has 5 states, 5 states have (on average 93.4) internal successors, (467), 5 states have internal predecessors, (467), 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)
[2024-02-28 21:17:27,541 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:27,541 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 92 of 110
[2024-02-28 21:17:27,541 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:27,595 INFO  L124   PetriNetUnfolderBase]: 16/291 cut-off events.
[2024-02-28 21:17:27,596 INFO  L125   PetriNetUnfolderBase]: For 11/11 co-relation queries the response was YES.
[2024-02-28 21:17:27,596 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 437 conditions, 291 events. 16/291 cut-off events. For 11/11 co-relation queries the response was YES. Maximal size of possible extension queue 13. Compared 1031 event pairs, 1 based on Foata normal form. 1/279 useless extension candidates. Maximal degree in co-relation 325. Up to 48 conditions per place. 
[2024-02-28 21:17:27,597 INFO  L140   encePairwiseOnDemand]: 103/110 looper letters, 15 selfloop transitions, 2 changer transitions 4/115 dead transitions.
[2024-02-28 21:17:27,597 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 122 places, 115 transitions, 337 flow
[2024-02-28 21:17:27,599 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-02-28 21:17:27,599 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-02-28 21:17:27,600 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 574 transitions.
[2024-02-28 21:17:27,601 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8696969696969697
[2024-02-28 21:17:27,601 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 574 transitions.
[2024-02-28 21:17:27,601 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 574 transitions.
[2024-02-28 21:17:27,601 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:27,601 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 574 transitions.
[2024-02-28 21:17:27,602 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 95.66666666666667) internal successors, (574), 6 states have internal predecessors, (574), 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)
[2024-02-28 21:17:27,604 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 110.0) internal successors, (770), 7 states have internal predecessors, (770), 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)
[2024-02-28 21:17:27,605 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 110.0) internal successors, (770), 7 states have internal predecessors, (770), 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)
[2024-02-28 21:17:27,605 INFO  L175             Difference]: Start difference. First operand has 117 places, 113 transitions, 305 flow. Second operand 6 states and 574 transitions.
[2024-02-28 21:17:27,605 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 122 places, 115 transitions, 337 flow
[2024-02-28 21:17:27,608 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 120 places, 115 transitions, 317 flow, removed 7 selfloop flow, removed 2 redundant places.
[2024-02-28 21:17:27,611 INFO  L231             Difference]: Finished difference. Result has 124 places, 109 transitions, 279 flow
[2024-02-28 21:17:27,611 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=110, PETRI_DIFFERENCE_MINUEND_FLOW=263, PETRI_DIFFERENCE_MINUEND_PLACES=115, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=109, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=107, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=279, PETRI_PLACES=124, PETRI_TRANSITIONS=109}
[2024-02-28 21:17:27,612 INFO  L281   CegarLoopForPetriNet]: 109 programPoint places, 15 predicate places.
[2024-02-28 21:17:27,612 INFO  L495      AbstractCegarLoop]: Abstraction has has 124 places, 109 transitions, 279 flow
[2024-02-28 21:17:27,613 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 5 states have (on average 93.4) internal successors, (467), 5 states have internal predecessors, (467), 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)
[2024-02-28 21:17:27,613 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:27,613 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:27,613 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2024-02-28 21:17:27,614 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 21:17:27,614 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:27,614 INFO  L85        PathProgramCache]: Analyzing trace with hash 1145773921, now seen corresponding path program 1 times
[2024-02-28 21:17:27,615 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:27,615 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1638120474]
[2024-02-28 21:17:27,615 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:27,615 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:27,628 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:27,647 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:27,647 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:27,647 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1638120474]
[2024-02-28 21:17:27,647 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1638120474] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:27,647 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:27,648 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 21:17:27,648 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1708449165]
[2024-02-28 21:17:27,648 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:27,648 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 21:17:27,648 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:27,649 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 21:17:27,649 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 21:17:27,658 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 97 out of 110
[2024-02-28 21:17:27,659 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 124 places, 109 transitions, 279 flow. Second operand  has 3 states, 3 states have (on average 98.66666666666667) internal successors, (296), 3 states have internal predecessors, (296), 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)
[2024-02-28 21:17:27,659 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:27,659 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 97 of 110
[2024-02-28 21:17:27,659 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:27,684 INFO  L124   PetriNetUnfolderBase]: 5/209 cut-off events.
[2024-02-28 21:17:27,684 INFO  L125   PetriNetUnfolderBase]: For 20/33 co-relation queries the response was YES.
[2024-02-28 21:17:27,684 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 303 conditions, 209 events. 5/209 cut-off events. For 20/33 co-relation queries the response was YES. Maximal size of possible extension queue 11. Compared 553 event pairs, 3 based on Foata normal form. 1/200 useless extension candidates. Maximal degree in co-relation 243. Up to 25 conditions per place. 
[2024-02-28 21:17:27,685 INFO  L140   encePairwiseOnDemand]: 105/110 looper letters, 8 selfloop transitions, 4 changer transitions 3/112 dead transitions.
[2024-02-28 21:17:27,685 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 123 places, 112 transitions, 315 flow
[2024-02-28 21:17:27,685 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 21:17:27,685 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 21:17:27,686 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 305 transitions.
[2024-02-28 21:17:27,686 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.9242424242424242
[2024-02-28 21:17:27,686 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 305 transitions.
[2024-02-28 21:17:27,686 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 305 transitions.
[2024-02-28 21:17:27,686 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:27,687 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 305 transitions.
[2024-02-28 21:17:27,687 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 101.66666666666667) internal successors, (305), 3 states have internal predecessors, (305), 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)
[2024-02-28 21:17:27,688 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 110.0) internal successors, (440), 4 states have internal predecessors, (440), 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)
[2024-02-28 21:17:27,688 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 110.0) internal successors, (440), 4 states have internal predecessors, (440), 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)
[2024-02-28 21:17:27,688 INFO  L175             Difference]: Start difference. First operand has 124 places, 109 transitions, 279 flow. Second operand 3 states and 305 transitions.
[2024-02-28 21:17:27,688 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 123 places, 112 transitions, 315 flow
[2024-02-28 21:17:27,690 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 118 places, 112 transitions, 301 flow, removed 5 selfloop flow, removed 5 redundant places.
[2024-02-28 21:17:27,691 INFO  L231             Difference]: Finished difference. Result has 120 places, 109 transitions, 287 flow
[2024-02-28 21:17:27,691 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=110, PETRI_DIFFERENCE_MINUEND_FLOW=265, PETRI_DIFFERENCE_MINUEND_PLACES=116, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=109, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=3, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=105, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=287, PETRI_PLACES=120, PETRI_TRANSITIONS=109}
[2024-02-28 21:17:27,692 INFO  L281   CegarLoopForPetriNet]: 109 programPoint places, 11 predicate places.
[2024-02-28 21:17:27,692 INFO  L495      AbstractCegarLoop]: Abstraction has has 120 places, 109 transitions, 287 flow
[2024-02-28 21:17:27,692 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 98.66666666666667) internal successors, (296), 3 states have internal predecessors, (296), 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)
[2024-02-28 21:17:27,692 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:27,692 INFO  L208   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1]
[2024-02-28 21:17:27,693 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2024-02-28 21:17:27,693 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 21:17:27,693 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:27,693 INFO  L85        PathProgramCache]: Analyzing trace with hash 998697632, now seen corresponding path program 1 times
[2024-02-28 21:17:27,693 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:27,693 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [353218235]
[2024-02-28 21:17:27,694 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:27,694 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:27,714 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 21:17:27,715 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-02-28 21:17:27,726 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 21:17:27,746 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-02-28 21:17:27,746 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-02-28 21:17:27,747 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (7 of 8 remaining)
[2024-02-28 21:17:27,748 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (6 of 8 remaining)
[2024-02-28 21:17:27,748 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (5 of 8 remaining)
[2024-02-28 21:17:27,748 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (4 of 8 remaining)
[2024-02-28 21:17:27,749 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (3 of 8 remaining)
[2024-02-28 21:17:27,749 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (2 of 8 remaining)
[2024-02-28 21:17:27,749 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 8 remaining)
[2024-02-28 21:17:27,749 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 8 remaining)
[2024-02-28 21:17:27,749 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2024-02-28 21:17:27,749 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2024-02-28 21:17:27,751 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-02-28 21:17:27,752 INFO  L514   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2024-02-28 21:17:27,768 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2024-02-28 21:17:27,770 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 128 places, 128 transitions, 272 flow
[2024-02-28 21:17:27,791 INFO  L124   PetriNetUnfolderBase]: 11/284 cut-off events.
[2024-02-28 21:17:27,792 INFO  L125   PetriNetUnfolderBase]: For 6/6 co-relation queries the response was YES.
[2024-02-28 21:17:27,792 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 296 conditions, 284 events. 11/284 cut-off events. For 6/6 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 697 event pairs, 0 based on Foata normal form. 0/248 useless extension candidates. Maximal degree in co-relation 163. Up to 8 conditions per place. 
[2024-02-28 21:17:27,792 INFO  L82        GeneralOperation]: Start removeDead. Operand has 128 places, 128 transitions, 272 flow
[2024-02-28 21:17:27,794 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 128 places, 128 transitions, 272 flow
[2024-02-28 21:17:27,795 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-02-28 21:17:27,795 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=LoopHeads, 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;@14e9d079, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2024-02-28 21:17:27,796 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 9 error locations.
[2024-02-28 21:17:27,799 INFO  L185   PetriNetUnfolderBase]: Found word, exiting Unfolder.
[2024-02-28 21:17:27,799 INFO  L124   PetriNetUnfolderBase]: 3/52 cut-off events.
[2024-02-28 21:17:27,799 INFO  L125   PetriNetUnfolderBase]: For 0/0 co-relation queries the response was YES.
[2024-02-28 21:17:27,799 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:27,799 INFO  L208   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, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:27,799 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:27,799 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:27,799 INFO  L85        PathProgramCache]: Analyzing trace with hash -115027175, now seen corresponding path program 1 times
[2024-02-28 21:17:27,800 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:27,800 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [736371514]
[2024-02-28 21:17:27,800 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:27,800 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:27,811 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:27,981 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:27,982 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:27,982 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [736371514]
[2024-02-28 21:17:27,982 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [736371514] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:27,982 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:27,982 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-02-28 21:17:27,982 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1276061297]
[2024-02-28 21:17:27,982 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:27,983 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-02-28 21:17:27,983 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:27,983 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-02-28 21:17:27,983 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-02-28 21:17:28,145 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 95 out of 128
[2024-02-28 21:17:28,146 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 128 places, 128 transitions, 272 flow. Second operand  has 6 states, 6 states have (on average 96.16666666666667) internal successors, (577), 6 states have internal predecessors, (577), 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)
[2024-02-28 21:17:28,146 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:28,146 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 95 of 128
[2024-02-28 21:17:28,146 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:28,346 INFO  L124   PetriNetUnfolderBase]: 280/1695 cut-off events.
[2024-02-28 21:17:28,346 INFO  L125   PetriNetUnfolderBase]: For 37/37 co-relation queries the response was YES.
[2024-02-28 21:17:28,350 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 2281 conditions, 1695 events. 280/1695 cut-off events. For 37/37 co-relation queries the response was YES. Maximal size of possible extension queue 84. Compared 13380 event pairs, 240 based on Foata normal form. 24/1588 useless extension candidates. Maximal degree in co-relation 731. Up to 488 conditions per place. 
[2024-02-28 21:17:28,354 INFO  L140   encePairwiseOnDemand]: 109/128 looper letters, 30 selfloop transitions, 13 changer transitions 1/138 dead transitions.
[2024-02-28 21:17:28,354 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 130 places, 138 transitions, 378 flow
[2024-02-28 21:17:28,355 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-02-28 21:17:28,355 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-02-28 21:17:28,356 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 621 transitions.
[2024-02-28 21:17:28,356 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.80859375
[2024-02-28 21:17:28,357 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 621 transitions.
[2024-02-28 21:17:28,357 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 621 transitions.
[2024-02-28 21:17:28,357 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:28,357 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 621 transitions.
[2024-02-28 21:17:28,358 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 103.5) internal successors, (621), 6 states have internal predecessors, (621), 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)
[2024-02-28 21:17:28,359 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 128.0) internal successors, (896), 7 states have internal predecessors, (896), 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)
[2024-02-28 21:17:28,360 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 128.0) internal successors, (896), 7 states have internal predecessors, (896), 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)
[2024-02-28 21:17:28,360 INFO  L175             Difference]: Start difference. First operand has 128 places, 128 transitions, 272 flow. Second operand 6 states and 621 transitions.
[2024-02-28 21:17:28,360 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 130 places, 138 transitions, 378 flow
[2024-02-28 21:17:28,361 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 130 places, 138 transitions, 378 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 21:17:28,362 INFO  L231             Difference]: Finished difference. Result has 134 places, 133 transitions, 354 flow
[2024-02-28 21:17:28,362 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=128, PETRI_DIFFERENCE_MINUEND_FLOW=260, PETRI_DIFFERENCE_MINUEND_PLACES=125, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=122, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=109, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=354, PETRI_PLACES=134, PETRI_TRANSITIONS=133}
[2024-02-28 21:17:28,363 INFO  L281   CegarLoopForPetriNet]: 128 programPoint places, 6 predicate places.
[2024-02-28 21:17:28,363 INFO  L495      AbstractCegarLoop]: Abstraction has has 134 places, 133 transitions, 354 flow
[2024-02-28 21:17:28,363 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 96.16666666666667) internal successors, (577), 6 states have internal predecessors, (577), 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)
[2024-02-28 21:17:28,363 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:28,363 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:28,363 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2024-02-28 21:17:28,364 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:28,364 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:28,364 INFO  L85        PathProgramCache]: Analyzing trace with hash -1205006822, now seen corresponding path program 1 times
[2024-02-28 21:17:28,364 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:28,364 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [576762175]
[2024-02-28 21:17:28,364 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:28,364 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:28,373 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:28,388 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:28,388 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:28,388 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [576762175]
[2024-02-28 21:17:28,388 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [576762175] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:28,388 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:28,388 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 21:17:28,389 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [94876046]
[2024-02-28 21:17:28,389 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:28,389 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 21:17:28,389 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:28,389 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 21:17:28,390 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 21:17:28,401 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 112 out of 128
[2024-02-28 21:17:28,401 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 134 places, 133 transitions, 354 flow. Second operand  has 3 states, 3 states have (on average 112.66666666666667) internal successors, (338), 3 states have internal predecessors, (338), 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)
[2024-02-28 21:17:28,401 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:28,401 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 112 of 128
[2024-02-28 21:17:28,401 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:28,494 INFO  L124   PetriNetUnfolderBase]: 120/888 cut-off events.
[2024-02-28 21:17:28,494 INFO  L125   PetriNetUnfolderBase]: For 88/131 co-relation queries the response was YES.
[2024-02-28 21:17:28,497 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1277 conditions, 888 events. 120/888 cut-off events. For 88/131 co-relation queries the response was YES. Maximal size of possible extension queue 42. Compared 5267 event pairs, 50 based on Foata normal form. 0/798 useless extension candidates. Maximal degree in co-relation 1052. Up to 139 conditions per place. 
[2024-02-28 21:17:28,499 INFO  L140   encePairwiseOnDemand]: 123/128 looper letters, 16 selfloop transitions, 4 changer transitions 4/140 dead transitions.
[2024-02-28 21:17:28,499 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 135 places, 140 transitions, 408 flow
[2024-02-28 21:17:28,500 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 21:17:28,500 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 21:17:28,501 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 357 transitions.
[2024-02-28 21:17:28,501 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.9296875
[2024-02-28 21:17:28,501 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 357 transitions.
[2024-02-28 21:17:28,501 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 357 transitions.
[2024-02-28 21:17:28,501 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:28,501 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 357 transitions.
[2024-02-28 21:17:28,502 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 119.0) internal successors, (357), 3 states have internal predecessors, (357), 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)
[2024-02-28 21:17:28,503 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 128.0) internal successors, (512), 4 states have internal predecessors, (512), 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)
[2024-02-28 21:17:28,503 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 128.0) internal successors, (512), 4 states have internal predecessors, (512), 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)
[2024-02-28 21:17:28,503 INFO  L175             Difference]: Start difference. First operand has 134 places, 133 transitions, 354 flow. Second operand 3 states and 357 transitions.
[2024-02-28 21:17:28,503 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 135 places, 140 transitions, 408 flow
[2024-02-28 21:17:28,505 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 134 places, 140 transitions, 404 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-02-28 21:17:28,506 INFO  L231             Difference]: Finished difference. Result has 136 places, 132 transitions, 358 flow
[2024-02-28 21:17:28,506 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=128, PETRI_DIFFERENCE_MINUEND_FLOW=350, PETRI_DIFFERENCE_MINUEND_PLACES=132, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=133, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=129, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=358, PETRI_PLACES=136, PETRI_TRANSITIONS=132}
[2024-02-28 21:17:28,507 INFO  L281   CegarLoopForPetriNet]: 128 programPoint places, 8 predicate places.
[2024-02-28 21:17:28,507 INFO  L495      AbstractCegarLoop]: Abstraction has has 136 places, 132 transitions, 358 flow
[2024-02-28 21:17:28,507 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 112.66666666666667) internal successors, (338), 3 states have internal predecessors, (338), 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)
[2024-02-28 21:17:28,507 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:28,507 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:28,508 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2024-02-28 21:17:28,508 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:28,508 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:28,508 INFO  L85        PathProgramCache]: Analyzing trace with hash 195998556, now seen corresponding path program 1 times
[2024-02-28 21:17:28,508 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:28,508 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1218615197]
[2024-02-28 21:17:28,508 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:28,509 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:28,520 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:28,572 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:28,572 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:28,573 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1218615197]
[2024-02-28 21:17:28,573 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1218615197] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:28,573 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:28,573 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-02-28 21:17:28,573 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1274462605]
[2024-02-28 21:17:28,573 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:28,573 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2024-02-28 21:17:28,574 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:28,574 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2024-02-28 21:17:28,574 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=8, Invalid=12, Unknown=0, NotChecked=0, Total=20
[2024-02-28 21:17:28,653 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 106 out of 128
[2024-02-28 21:17:28,654 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 136 places, 132 transitions, 358 flow. Second operand  has 5 states, 5 states have (on average 107.4) internal successors, (537), 5 states have internal predecessors, (537), 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)
[2024-02-28 21:17:28,654 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:28,654 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 106 of 128
[2024-02-28 21:17:28,654 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:28,805 INFO  L124   PetriNetUnfolderBase]: 187/1317 cut-off events.
[2024-02-28 21:17:28,806 INFO  L125   PetriNetUnfolderBase]: For 68/69 co-relation queries the response was YES.
[2024-02-28 21:17:28,809 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1916 conditions, 1317 events. 187/1317 cut-off events. For 68/69 co-relation queries the response was YES. Maximal size of possible extension queue 50. Compared 9551 event pairs, 131 based on Foata normal form. 1/1224 useless extension candidates. Maximal degree in co-relation 1287. Up to 313 conditions per place. 
[2024-02-28 21:17:28,812 INFO  L140   encePairwiseOnDemand]: 121/128 looper letters, 20 selfloop transitions, 2 changer transitions 4/135 dead transitions.
[2024-02-28 21:17:28,812 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 141 places, 135 transitions, 402 flow
[2024-02-28 21:17:28,813 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-02-28 21:17:28,813 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-02-28 21:17:28,814 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 663 transitions.
[2024-02-28 21:17:28,814 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.86328125
[2024-02-28 21:17:28,814 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 663 transitions.
[2024-02-28 21:17:28,814 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 663 transitions.
[2024-02-28 21:17:28,815 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:28,815 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 663 transitions.
[2024-02-28 21:17:28,816 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 110.5) internal successors, (663), 6 states have internal predecessors, (663), 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)
[2024-02-28 21:17:28,817 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 128.0) internal successors, (896), 7 states have internal predecessors, (896), 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)
[2024-02-28 21:17:28,817 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 128.0) internal successors, (896), 7 states have internal predecessors, (896), 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)
[2024-02-28 21:17:28,818 INFO  L175             Difference]: Start difference. First operand has 136 places, 132 transitions, 358 flow. Second operand 6 states and 663 transitions.
[2024-02-28 21:17:28,818 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 141 places, 135 transitions, 402 flow
[2024-02-28 21:17:28,819 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 139 places, 135 transitions, 380 flow, removed 7 selfloop flow, removed 2 redundant places.
[2024-02-28 21:17:28,821 INFO  L231             Difference]: Finished difference. Result has 143 places, 129 transitions, 334 flow
[2024-02-28 21:17:28,821 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=128, PETRI_DIFFERENCE_MINUEND_FLOW=314, PETRI_DIFFERENCE_MINUEND_PLACES=134, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=128, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=126, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=334, PETRI_PLACES=143, PETRI_TRANSITIONS=129}
[2024-02-28 21:17:28,821 INFO  L281   CegarLoopForPetriNet]: 128 programPoint places, 15 predicate places.
[2024-02-28 21:17:28,821 INFO  L495      AbstractCegarLoop]: Abstraction has has 143 places, 129 transitions, 334 flow
[2024-02-28 21:17:28,822 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 5 states have (on average 107.4) internal successors, (537), 5 states have internal predecessors, (537), 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)
[2024-02-28 21:17:28,822 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:28,822 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:28,822 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2024-02-28 21:17:28,822 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:28,822 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:28,822 INFO  L85        PathProgramCache]: Analyzing trace with hash 1279443409, now seen corresponding path program 1 times
[2024-02-28 21:17:28,823 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:28,823 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [43348007]
[2024-02-28 21:17:28,823 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:28,823 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:28,847 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:28,867 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:28,867 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:28,867 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [43348007]
[2024-02-28 21:17:28,867 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [43348007] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:28,867 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:28,867 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 21:17:28,868 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1811107967]
[2024-02-28 21:17:28,868 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:28,868 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 21:17:28,868 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:28,868 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 21:17:28,869 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 21:17:28,881 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 110 out of 128
[2024-02-28 21:17:28,881 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 143 places, 129 transitions, 334 flow. Second operand  has 3 states, 3 states have (on average 111.66666666666667) internal successors, (335), 3 states have internal predecessors, (335), 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)
[2024-02-28 21:17:28,881 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:28,881 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 110 of 128
[2024-02-28 21:17:28,881 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:29,016 INFO  L124   PetriNetUnfolderBase]: 172/1228 cut-off events.
[2024-02-28 21:17:29,016 INFO  L125   PetriNetUnfolderBase]: For 203/444 co-relation queries the response was YES.
[2024-02-28 21:17:29,018 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1870 conditions, 1228 events. 172/1228 cut-off events. For 203/444 co-relation queries the response was YES. Maximal size of possible extension queue 67. Compared 8865 event pairs, 77 based on Foata normal form. 3/1083 useless extension candidates. Maximal degree in co-relation 1800. Up to 270 conditions per place. 
[2024-02-28 21:17:29,022 INFO  L140   encePairwiseOnDemand]: 122/128 looper letters, 19 selfloop transitions, 7 changer transitions 0/138 dead transitions.
[2024-02-28 21:17:29,022 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 142 places, 138 transitions, 418 flow
[2024-02-28 21:17:29,022 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 21:17:29,022 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 21:17:29,023 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 354 transitions.
[2024-02-28 21:17:29,023 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.921875
[2024-02-28 21:17:29,023 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 354 transitions.
[2024-02-28 21:17:29,023 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 354 transitions.
[2024-02-28 21:17:29,024 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:29,024 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 354 transitions.
[2024-02-28 21:17:29,024 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 118.0) internal successors, (354), 3 states have internal predecessors, (354), 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)
[2024-02-28 21:17:29,025 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 128.0) internal successors, (512), 4 states have internal predecessors, (512), 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)
[2024-02-28 21:17:29,025 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 128.0) internal successors, (512), 4 states have internal predecessors, (512), 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)
[2024-02-28 21:17:29,025 INFO  L175             Difference]: Start difference. First operand has 143 places, 129 transitions, 334 flow. Second operand 3 states and 354 transitions.
[2024-02-28 21:17:29,026 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 142 places, 138 transitions, 418 flow
[2024-02-28 21:17:29,027 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 138 places, 138 transitions, 406 flow, removed 5 selfloop flow, removed 4 redundant places.
[2024-02-28 21:17:29,029 INFO  L231             Difference]: Finished difference. Result has 140 places, 134 transitions, 378 flow
[2024-02-28 21:17:29,029 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=128, PETRI_DIFFERENCE_MINUEND_FLOW=322, PETRI_DIFFERENCE_MINUEND_PLACES=136, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=129, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=122, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=378, PETRI_PLACES=140, PETRI_TRANSITIONS=134}
[2024-02-28 21:17:29,029 INFO  L281   CegarLoopForPetriNet]: 128 programPoint places, 12 predicate places.
[2024-02-28 21:17:29,029 INFO  L495      AbstractCegarLoop]: Abstraction has has 140 places, 134 transitions, 378 flow
[2024-02-28 21:17:29,030 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 111.66666666666667) internal successors, (335), 3 states have internal predecessors, (335), 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)
[2024-02-28 21:17:29,030 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:29,030 INFO  L208   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, 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]
[2024-02-28 21:17:29,030 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2024-02-28 21:17:29,030 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:29,031 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:29,031 INFO  L85        PathProgramCache]: Analyzing trace with hash 829025416, now seen corresponding path program 1 times
[2024-02-28 21:17:29,031 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:29,031 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1927849243]
[2024-02-28 21:17:29,031 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:29,031 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:29,046 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:29,150 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:29,150 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:29,150 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1927849243]
[2024-02-28 21:17:29,151 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1927849243] provided 0 perfect and 1 imperfect interpolant sequences
[2024-02-28 21:17:29,151 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [634846262]
[2024-02-28 21:17:29,151 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:29,151 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-02-28 21:17:29,151 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-02-28 21:17:29,153 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-02-28 21:17:29,159 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2024-02-28 21:17:29,273 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:29,275 INFO  L262         TraceCheckSpWp]: Trace formula consists of 183 conjuncts, 6 conjunts are in the unsatisfiable core
[2024-02-28 21:17:29,277 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-02-28 21:17:29,352 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:29,352 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-02-28 21:17:29,408 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 21:17:29,408 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [634846262] provided 0 perfect and 2 imperfect interpolant sequences
[2024-02-28 21:17:29,408 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-02-28 21:17:29,408 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 11
[2024-02-28 21:17:29,409 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [36131822]
[2024-02-28 21:17:29,409 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-02-28 21:17:29,410 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2024-02-28 21:17:29,411 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:29,411 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2024-02-28 21:17:29,412 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=82, Unknown=0, NotChecked=0, Total=110
[2024-02-28 21:17:29,522 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 102 out of 128
[2024-02-28 21:17:29,523 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 140 places, 134 transitions, 378 flow. Second operand  has 11 states, 11 states have (on average 103.9090909090909) internal successors, (1143), 11 states have internal predecessors, (1143), 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)
[2024-02-28 21:17:29,524 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:29,524 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 102 of 128
[2024-02-28 21:17:29,524 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:29,798 INFO  L124   PetriNetUnfolderBase]: 338/2051 cut-off events.
[2024-02-28 21:17:29,798 INFO  L125   PetriNetUnfolderBase]: For 255/344 co-relation queries the response was YES.
[2024-02-28 21:17:29,802 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 3230 conditions, 2051 events. 338/2051 cut-off events. For 255/344 co-relation queries the response was YES. Maximal size of possible extension queue 81. Compared 16745 event pairs, 48 based on Foata normal form. 0/1866 useless extension candidates. Maximal degree in co-relation 1673. Up to 430 conditions per place. 
[2024-02-28 21:17:29,807 INFO  L140   encePairwiseOnDemand]: 117/128 looper letters, 40 selfloop transitions, 12 changer transitions 2/164 dead transitions.
[2024-02-28 21:17:29,807 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 149 places, 164 transitions, 548 flow
[2024-02-28 21:17:29,807 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2024-02-28 21:17:29,808 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 10 states.
[2024-02-28 21:17:29,809 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 10 states to 10 states and 1075 transitions.
[2024-02-28 21:17:29,810 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.83984375
[2024-02-28 21:17:29,810 INFO  L72            ComplementDD]: Start complementDD. Operand 10 states and 1075 transitions.
[2024-02-28 21:17:29,810 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 10 states and 1075 transitions.
[2024-02-28 21:17:29,810 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:29,810 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 10 states and 1075 transitions.
[2024-02-28 21:17:29,812 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 11 states, 10 states have (on average 107.5) internal successors, (1075), 10 states have internal predecessors, (1075), 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)
[2024-02-28 21:17:29,814 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 11 states, 11 states have (on average 128.0) internal successors, (1408), 11 states have internal predecessors, (1408), 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)
[2024-02-28 21:17:29,814 INFO  L81            ComplementDD]: Finished complementDD. Result  has 11 states, 11 states have (on average 128.0) internal successors, (1408), 11 states have internal predecessors, (1408), 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)
[2024-02-28 21:17:29,814 INFO  L175             Difference]: Start difference. First operand has 140 places, 134 transitions, 378 flow. Second operand 10 states and 1075 transitions.
[2024-02-28 21:17:29,814 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 149 places, 164 transitions, 548 flow
[2024-02-28 21:17:29,816 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 147 places, 164 transitions, 534 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-02-28 21:17:29,818 INFO  L231             Difference]: Finished difference. Result has 154 places, 142 transitions, 442 flow
[2024-02-28 21:17:29,818 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=128, PETRI_DIFFERENCE_MINUEND_FLOW=364, PETRI_DIFFERENCE_MINUEND_PLACES=138, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=134, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=123, PETRI_DIFFERENCE_SUBTRAHEND_STATES=10, PETRI_FLOW=442, PETRI_PLACES=154, PETRI_TRANSITIONS=142}
[2024-02-28 21:17:29,819 INFO  L281   CegarLoopForPetriNet]: 128 programPoint places, 26 predicate places.
[2024-02-28 21:17:29,819 INFO  L495      AbstractCegarLoop]: Abstraction has has 154 places, 142 transitions, 442 flow
[2024-02-28 21:17:29,819 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 11 states have (on average 103.9090909090909) internal successors, (1143), 11 states have internal predecessors, (1143), 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)
[2024-02-28 21:17:29,819 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:29,819 INFO  L208   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:29,864 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2024-02-28 21:17:30,021 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,2 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-02-28 21:17:30,022 INFO  L420      AbstractCegarLoop]: === Iteration 6 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:30,022 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:30,023 INFO  L85        PathProgramCache]: Analyzing trace with hash 1667427884, now seen corresponding path program 1 times
[2024-02-28 21:17:30,023 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:30,023 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [523293501]
[2024-02-28 21:17:30,023 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:30,024 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:30,052 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 21:17:30,075 INFO  L134       CoverageAnalysis]: Checked inductivity of 11 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2024-02-28 21:17:30,075 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 21:17:30,075 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [523293501]
[2024-02-28 21:17:30,075 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [523293501] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 21:17:30,075 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 21:17:30,075 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 21:17:30,075 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1415355435]
[2024-02-28 21:17:30,075 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 21:17:30,076 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 21:17:30,076 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 21:17:30,076 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 21:17:30,076 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 21:17:30,086 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 110 out of 128
[2024-02-28 21:17:30,086 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 154 places, 142 transitions, 442 flow. Second operand  has 3 states, 3 states have (on average 112.0) internal successors, (336), 3 states have internal predecessors, (336), 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)
[2024-02-28 21:17:30,086 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 21:17:30,086 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 110 of 128
[2024-02-28 21:17:30,086 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 21:17:30,257 INFO  L124   PetriNetUnfolderBase]: 238/1745 cut-off events.
[2024-02-28 21:17:30,257 INFO  L125   PetriNetUnfolderBase]: For 583/1649 co-relation queries the response was YES.
[2024-02-28 21:17:30,260 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 3003 conditions, 1745 events. 238/1745 cut-off events. For 583/1649 co-relation queries the response was YES. Maximal size of possible extension queue 98. Compared 14102 event pairs, 98 based on Foata normal form. 3/1600 useless extension candidates. Maximal degree in co-relation 2752. Up to 357 conditions per place. 
[2024-02-28 21:17:30,264 INFO  L140   encePairwiseOnDemand]: 122/128 looper letters, 19 selfloop transitions, 10 changer transitions 0/151 dead transitions.
[2024-02-28 21:17:30,264 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 156 places, 151 transitions, 537 flow
[2024-02-28 21:17:30,264 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 21:17:30,265 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 21:17:30,265 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 353 transitions.
[2024-02-28 21:17:30,265 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.9192708333333334
[2024-02-28 21:17:30,265 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 353 transitions.
[2024-02-28 21:17:30,265 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 353 transitions.
[2024-02-28 21:17:30,266 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 21:17:30,266 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 353 transitions.
[2024-02-28 21:17:30,267 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 117.66666666666667) internal successors, (353), 3 states have internal predecessors, (353), 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)
[2024-02-28 21:17:30,268 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 128.0) internal successors, (512), 4 states have internal predecessors, (512), 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)
[2024-02-28 21:17:30,268 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 128.0) internal successors, (512), 4 states have internal predecessors, (512), 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)
[2024-02-28 21:17:30,268 INFO  L175             Difference]: Start difference. First operand has 154 places, 142 transitions, 442 flow. Second operand 3 states and 353 transitions.
[2024-02-28 21:17:30,268 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 156 places, 151 transitions, 537 flow
[2024-02-28 21:17:30,270 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 155 places, 151 transitions, 531 flow, removed 2 selfloop flow, removed 1 redundant places.
[2024-02-28 21:17:30,272 INFO  L231             Difference]: Finished difference. Result has 157 places, 148 transitions, 518 flow
[2024-02-28 21:17:30,272 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=128, PETRI_DIFFERENCE_MINUEND_FLOW=436, PETRI_DIFFERENCE_MINUEND_PLACES=153, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=142, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=132, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=518, PETRI_PLACES=157, PETRI_TRANSITIONS=148}
[2024-02-28 21:17:30,272 INFO  L281   CegarLoopForPetriNet]: 128 programPoint places, 29 predicate places.
[2024-02-28 21:17:30,273 INFO  L495      AbstractCegarLoop]: Abstraction has has 157 places, 148 transitions, 518 flow
[2024-02-28 21:17:30,273 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 112.0) internal successors, (336), 3 states have internal predecessors, (336), 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)
[2024-02-28 21:17:30,273 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-02-28 21:17:30,273 INFO  L208   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, 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, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:30,273 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2024-02-28 21:17:30,273 INFO  L420      AbstractCegarLoop]: === Iteration 7 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 21:17:30,273 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 21:17:30,273 INFO  L85        PathProgramCache]: Analyzing trace with hash 1806570026, now seen corresponding path program 1 times
[2024-02-28 21:17:30,273 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 21:17:30,273 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [277059024]
[2024-02-28 21:17:30,274 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 21:17:30,274 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 21:17:30,294 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 21:17:30,294 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-02-28 21:17:30,302 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 21:17:30,309 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-02-28 21:17:30,309 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-02-28 21:17:30,309 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location threadErr0ASSERT_VIOLATIONDATA_RACE (8 of 9 remaining)
[2024-02-28 21:17:30,309 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (7 of 9 remaining)
[2024-02-28 21:17:30,309 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (6 of 9 remaining)
[2024-02-28 21:17:30,309 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (5 of 9 remaining)
[2024-02-28 21:17:30,309 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (4 of 9 remaining)
[2024-02-28 21:17:30,309 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (3 of 9 remaining)
[2024-02-28 21:17:30,310 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (2 of 9 remaining)
[2024-02-28 21:17:30,310 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 9 remaining)
[2024-02-28 21:17:30,310 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 9 remaining)
[2024-02-28 21:17:30,310 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2024-02-28 21:17:30,310 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1]
[2024-02-28 21:17:30,313 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 2 thread instances
[2024-02-28 21:17:30,314 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2024-02-28 21:17:30,338 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet7 could not be translated
[2024-02-28 21:17:30,339 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~malloc8
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,340 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,341 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem16
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem16
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,342 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,343 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,343 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,350 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.02 09:17:30 BasicIcfg
[2024-02-28 21:17:30,350 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2024-02-28 21:17:30,350 INFO  L112        PluginConnector]: ------------------------Witness Printer----------------------------
[2024-02-28 21:17:30,351 INFO  L270        PluginConnector]: Initializing Witness Printer...
[2024-02-28 21:17:30,351 INFO  L274        PluginConnector]: Witness Printer initialized
[2024-02-28 21:17:30,351 INFO  L184        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.02 09:17:25" (3/4) ...
[2024-02-28 21:17:30,352 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2024-02-28 21:17:30,353 INFO  L131        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2024-02-28 21:17:30,354 INFO  L158              Benchmark]: Toolchain (without parser) took 5435.29ms. Allocated memory was 153.1MB in the beginning and 224.4MB in the end (delta: 71.3MB). Free memory was 108.6MB in the beginning and 112.1MB in the end (delta: -3.5MB). Peak memory consumption was 70.9MB. Max. memory is 16.1GB.
[2024-02-28 21:17:30,354 INFO  L158              Benchmark]: CDTParser took 0.12ms. Allocated memory is still 153.1MB. Free memory is still 123.9MB. There was no memory consumed. Max. memory is 16.1GB.
[2024-02-28 21:17:30,354 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 417.95ms. Allocated memory is still 153.1MB. Free memory was 108.6MB in the beginning and 79.7MB in the end (delta: 28.8MB). Peak memory consumption was 29.4MB. Max. memory is 16.1GB.
[2024-02-28 21:17:30,354 INFO  L158              Benchmark]: Boogie Procedure Inliner took 36.85ms. Allocated memory is still 153.1MB. Free memory was 79.7MB in the beginning and 77.2MB in the end (delta: 2.6MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-02-28 21:17:30,354 INFO  L158              Benchmark]: Boogie Preprocessor took 24.70ms. Allocated memory is still 153.1MB. Free memory was 77.2MB in the beginning and 75.1MB in the end (delta: 2.1MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-02-28 21:17:30,355 INFO  L158              Benchmark]: RCFGBuilder took 460.61ms. Allocated memory was 153.1MB in the beginning and 186.6MB in the end (delta: 33.6MB). Free memory was 75.1MB in the beginning and 155.9MB in the end (delta: -80.8MB). Peak memory consumption was 27.1MB. Max. memory is 16.1GB.
[2024-02-28 21:17:30,355 INFO  L158              Benchmark]: TraceAbstraction took 4486.27ms. Allocated memory was 186.6MB in the beginning and 224.4MB in the end (delta: 37.7MB). Free memory was 154.9MB in the beginning and 112.1MB in the end (delta: 42.8MB). Peak memory consumption was 81.5MB. Max. memory is 16.1GB.
[2024-02-28 21:17:30,355 INFO  L158              Benchmark]: Witness Printer took 2.75ms. Allocated memory is still 224.4MB. Free memory is still 112.1MB. There was no memory consumed. Max. memory is 16.1GB.
[2024-02-28 21:17:30,356 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.12ms. Allocated memory is still 153.1MB. Free memory is still 123.9MB. There was no memory consumed. Max. memory is 16.1GB.
 * CACSL2BoogieTranslator took 417.95ms. Allocated memory is still 153.1MB. Free memory was 108.6MB in the beginning and 79.7MB in the end (delta: 28.8MB). Peak memory consumption was 29.4MB. Max. memory is 16.1GB.
 * Boogie Procedure Inliner took 36.85ms. Allocated memory is still 153.1MB. Free memory was 79.7MB in the beginning and 77.2MB in the end (delta: 2.6MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * Boogie Preprocessor took 24.70ms. Allocated memory is still 153.1MB. Free memory was 77.2MB in the beginning and 75.1MB in the end (delta: 2.1MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * RCFGBuilder took 460.61ms. Allocated memory was 153.1MB in the beginning and 186.6MB in the end (delta: 33.6MB). Free memory was 75.1MB in the beginning and 155.9MB in the end (delta: -80.8MB). Peak memory consumption was 27.1MB. Max. memory is 16.1GB.
 * TraceAbstraction took 4486.27ms. Allocated memory was 186.6MB in the beginning and 224.4MB in the end (delta: 37.7MB). Free memory was 154.9MB in the beginning and 112.1MB in the end (delta: 42.8MB). Peak memory consumption was 81.5MB. Max. memory is 16.1GB.
 * Witness Printer took 2.75ms. Allocated memory is still 224.4MB. Free memory is still 112.1MB. There was no memory consumed. Max. memory is 16.1GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator:
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet7 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: unknown boogie variable #t~malloc8
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: unknown boogie variable #t~mem11
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: unknown boogie variable #t~mem11
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: unknown boogie variable #t~mem11
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: unknown boogie variable #t~mem16
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: unknown boogie variable #t~mem16
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
  - GenericResult: Unfinished Backtranslation
    Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
  - GenericResult: Unfinished Backtranslation
    The program execution was not completely translated back.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - DataRaceFoundResult [Line: 1017]: Data race detected
[2024-02-28 21:17:30,371 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet7 could not be translated
[2024-02-28 21:17:30,371 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~malloc8
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,372 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem16
[2024-02-28 21:17:30,373 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem16
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,374 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,384 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet7 could not be translated
[2024-02-28 21:17:30,384 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~malloc8
[2024-02-28 21:17:30,384 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem11
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~pre10 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,385 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: Expected StepInfo for loop construct to contain Condition, but it did not
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem16
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,386 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: unknown boogie variable #t~mem16
[2024-02-28 21:17:30,387 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,387 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,387 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,387 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
[2024-02-28 21:17:30,387 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet5 could not be translated
[2024-02-28 21:17:30,387 WARN  L1572  BoogieBacktranslator]: Unfinished Backtranslation: IdentifierExpression #t~nondet4 could not be translated
    Data race detected
The following path leads to a data race: 
[L1013]               0  int data = 0;
         VAL             [data=0]
[L1014]               0  pthread_mutex_t data_mutex = { { 0, 0, 0, PTHREAD_MUTEX_TIMED_NP, 0, { { 0, 0 } } } };
         VAL             [data=0, data_mutex={1:0}]
[L1022]               0  int threads_total = __VERIFIER_nondet_int();
         VAL             [data=0, data_mutex={1:0}, threads_total=1]
[L1023]  CALL         0  assume_abort_if_not(threads_total >= 0)
[L1010]  COND FALSE   0  !(!cond)
         VAL             [\old(cond)=1, cond=1, data=0, data_mutex={1:0}]
[L1023]  RET          0  assume_abort_if_not(threads_total >= 0)
[L1024]               0  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
         VAL             [data=0, data_mutex={1:0}, threads_total=1, tids={5:0}]
[L1024]               0  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
         VAL             [data=0, data_mutex={1:0}, threads_total=1, tids={5:0}]
[L1025]               0  int i = 0;
         VAL             [data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1025]  COND TRUE    0  i < threads_total
         VAL             [data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1026]  EXPR         0  \read(*tids)
         VAL             [data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1026]  EXPR         0  tids[i]
         VAL             [data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1026]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [arg={0:0}, data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1017]               1  data = __VERIFIER_nondet_int()
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}]
[L1025]               0  i++
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, i=1, threads_total=1, tids={5:0}]
[L1025]  COND FALSE   0  !(i < threads_total)
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, i=1, threads_total=1, tids={5:0}]
[L1028]               0  int i = 0;
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1028]  COND FALSE   0  !(i < threads_total - 1)
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, i=0, threads_total=1, tids={5:0}]
[L1031]  EXPR         0  \read(*tids)
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, threads_total=1, tids={5:0}]
[L1031]               0  free(tids)
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, threads_total=1, tids={5:0}]
[L1032]               0  return data;
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, threads_total=1, tids={5:0}]
[L1017]               1  data = __VERIFIER_nondet_int()
         VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}]

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

  - UnprovableResult [Line: 1026]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1029]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1031]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1032]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1029]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1026]: Unable to prove that petrification did provide enough thread instances (tool internal message)
    Unable to prove that petrification did provide enough thread instances (tool internal message)
 Reason: Not analyzed. 
  - StatisticsResult: Ultimate Automizer benchmark data with 1 thread instances
    CFG has 3 procedures, 124 locations, 8 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: 1.6s, OverallIterations: 5, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.1s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 202 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 118 mSDsluCounter, 73 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 32 mSDsCounter, 60 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 296 IncrementalHoareTripleChecker+Invalid, 356 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 60 mSolverCounterUnsat, 41 mSDtfsCounter, 296 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 16 GetRequests, 6 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=309occurred in iteration=1, InterpolantAutomatonStates: 18, 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.6s InterpolantComputationTime, 223 NumberOfCodeBlocks, 223 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 164 ConstructedInterpolants, 0 QuantifiedInterpolants, 261 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, 141 locations, 9 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: 2.5s, OverallIterations: 7, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 404 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 263 mSDsluCounter, 312 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 275 mSDsCounter, 60 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 751 IncrementalHoareTripleChecker+Invalid, 811 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 60 mSolverCounterUnsat, 37 mSDtfsCounter, 751 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 146 GetRequests, 119 SyntacticMatches, 4 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 44 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=518occurred in iteration=6, InterpolantAutomatonStates: 31, 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.5s InterpolantComputationTime, 419 NumberOfCodeBlocks, 419 NumberOfCodeBlocksAsserted, 8 NumberOfCheckSat, 404 ConstructedInterpolants, 0 QuantifiedInterpolants, 639 SizeOfPredicates, 6 NumberOfNonLiveVariables, 183 ConjunctsInSsa, 6 ConjunctsInUnsatCore, 8 InterpolantComputations, 5 PerfectInterpolantSequences, 11/14 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!
[2024-02-28 21:17:30,398 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000 (1)] Ended with 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
