./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-local-value-cond.i --full-output --architecture 32bit


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


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

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 32bit --witnessprinter.graph.data.programhash 6b5b373c4b779bf276b10c2aeaff89ba0593b5a6b53d6da47c6c731e506875de
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2023-11-01 18:39:52,202 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2023-11-01 18:39:52,203 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2023-11-01 18:39:52,225 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2023-11-01 18:39:52,226 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2023-11-01 18:39:52,227 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2023-11-01 18:39:52,227 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2023-11-01 18:39:52,228 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2023-11-01 18:39:52,230 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2023-11-01 18:39:52,230 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2023-11-01 18:39:52,231 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2023-11-01 18:39:52,232 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2023-11-01 18:39:52,232 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2023-11-01 18:39:52,233 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2023-11-01 18:39:52,234 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2023-11-01 18:39:52,235 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2023-11-01 18:39:52,235 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2023-11-01 18:39:52,236 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2023-11-01 18:39:52,237 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2023-11-01 18:39:52,238 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2023-11-01 18:39:52,239 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2023-11-01 18:39:52,240 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2023-11-01 18:39:52,241 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2023-11-01 18:39:52,242 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2023-11-01 18:39:52,244 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2023-11-01 18:39:52,245 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2023-11-01 18:39:52,245 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2023-11-01 18:39:52,245 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2023-11-01 18:39:52,246 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2023-11-01 18:39:52,247 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2023-11-01 18:39:52,247 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2023-11-01 18:39:52,247 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2023-11-01 18:39:52,248 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2023-11-01 18:39:52,248 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2023-11-01 18:39:52,249 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2023-11-01 18:39:52,249 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2023-11-01 18:39:52,250 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2023-11-01 18:39:52,250 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2023-11-01 18:39:52,250 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2023-11-01 18:39:52,251 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2023-11-01 18:39:52,251 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2023-11-01 18:39:52,252 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2023-11-01 18:39:52,267 INFO  L113        SettingsManager]: Loading preferences was successful
[2023-11-01 18:39:52,267 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2023-11-01 18:39:52,267 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2023-11-01 18:39:52,267 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2023-11-01 18:39:52,268 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2023-11-01 18:39:52,268 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2023-11-01 18:39:52,268 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * Use SBE=true
[2023-11-01 18:39:52,269 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * sizeof long=4
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2023-11-01 18:39:52,269 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * sizeof long double=12
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2023-11-01 18:39:52,270 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2023-11-01 18:39:52,270 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-11-01 18:39:52,271 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2023-11-01 18:39:52,271 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2023-11-01 18:39:52,272 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2023-11-01 18:39:52,272 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2023-11-01 18:39:52,272 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2023-11-01 18:39:52,272 INFO  L138        SettingsManager]:  * Looper check in Petri net analysis=SEMANTIC
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1 (file:/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/com.sun.xml.bind_2.2.0.v201505121915.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int)
WARNING: Please consider reporting this to the maintainers of com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
Applying setting for plugin de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: Entry function -> main
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness directory -> /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness filename -> witness.graphml
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Write witness besides input file -> false
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data specification -> CHECK( init(main()), LTL(G ! data-race) )


Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data producer -> Automizer
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data architecture -> 32bit
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data programhash -> 6b5b373c4b779bf276b10c2aeaff89ba0593b5a6b53d6da47c6c731e506875de
[2023-11-01 18:39:52,484 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2023-11-01 18:39:52,507 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2023-11-01 18:39:52,510 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2023-11-01 18:39:52,511 INFO  L271        PluginConnector]: Initializing CDTParser...
[2023-11-01 18:39:52,512 INFO  L275        PluginConnector]: CDTParser initialized
[2023-11-01 18:39:52,512 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value-cond.i
[2023-11-01 18:39:53,565 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2023-11-01 18:39:53,813 INFO  L351              CDTParser]: Found 1 translation units.
[2023-11-01 18:39:53,814 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value-cond.i
[2023-11-01 18:39:53,824 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/f9fb41644/eb04ffa0182c42a3a1c11b8255b30048/FLAG495a87e38
[2023-11-01 18:39:54,124 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/f9fb41644/eb04ffa0182c42a3a1c11b8255b30048
[2023-11-01 18:39:54,126 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2023-11-01 18:39:54,127 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2023-11-01 18:39:54,128 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2023-11-01 18:39:54,128 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2023-11-01 18:39:54,132 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2023-11-01 18:39:54,132 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,133 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@6ae1fa84 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54, skipping insertion in model container
[2023-11-01 18:39:54,133 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,138 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2023-11-01 18:39:54,178 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2023-11-01 18:39:54,302 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2023-11-01 18:39:54,431 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-11-01 18:39:54,439 INFO  L203         MainTranslator]: Completed pre-run
[2023-11-01 18:39:54,451 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2023-11-01 18:39:54,476 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-11-01 18:39:54,514 INFO  L208         MainTranslator]: Completed translation
[2023-11-01 18:39:54,515 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54 WrapperNode
[2023-11-01 18:39:54,515 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2023-11-01 18:39:54,516 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2023-11-01 18:39:54,516 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2023-11-01 18:39:54,516 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2023-11-01 18:39:54,521 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,535 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,555 INFO  L138                Inliner]: procedures = 269, calls = 23, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 83
[2023-11-01 18:39:54,556 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2023-11-01 18:39:54,556 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2023-11-01 18:39:54,556 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2023-11-01 18:39:54,556 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2023-11-01 18:39:54,564 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,564 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,572 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,572 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,580 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,583 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,585 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,586 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,588 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2023-11-01 18:39:54,589 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2023-11-01 18:39:54,589 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2023-11-01 18:39:54,590 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2023-11-01 18:39:54,591 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (1/1) ...
[2023-11-01 18:39:54,597 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-11-01 18:39:54,607 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-11-01 18:39:54,622 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2023-11-01 18:39:54,625 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2023-11-01 18:39:54,646 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexLock
[2023-11-01 18:39:54,647 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2023-11-01 18:39:54,647 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2023-11-01 18:39:54,647 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2023-11-01 18:39:54,647 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2023-11-01 18:39:54,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2023-11-01 18:39:54,647 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2023-11-01 18:39:54,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2023-11-01 18:39:54,648 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2023-11-01 18:39:54,770 INFO  L235             CfgBuilder]: Building ICFG
[2023-11-01 18:39:54,771 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2023-11-01 18:39:55,009 INFO  L276             CfgBuilder]: Performing block encoding
[2023-11-01 18:39:55,015 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2023-11-01 18:39:55,016 INFO  L300             CfgBuilder]: Removed 2 assume(true) statements.
[2023-11-01 18:39:55,017 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 01.11 06:39:55 BoogieIcfgContainer
[2023-11-01 18:39:55,017 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2023-11-01 18:39:55,019 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2023-11-01 18:39:55,019 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2023-11-01 18:39:55,022 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2023-11-01 18:39:55,022 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 01.11 06:39:54" (1/3) ...
[2023-11-01 18:39:55,022 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@737cb6ee and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 01.11 06:39:55, skipping insertion in model container
[2023-11-01 18:39:55,022 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 01.11 06:39:54" (2/3) ...
[2023-11-01 18:39:55,023 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@737cb6ee and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 01.11 06:39:55, skipping insertion in model container
[2023-11-01 18:39:55,023 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 01.11 06:39:55" (3/3) ...
[2023-11-01 18:39:55,024 INFO  L112   eAbstractionObserver]: Analyzing ICFG thread-local-value-cond.i
[2023-11-01 18:39:55,030 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2023-11-01 18:39:55,037 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2023-11-01 18:39:55,037 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 9 error locations.
[2023-11-01 18:39:55,037 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2023-11-01 18:39:55,080 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2023-11-01 18:39:55,108 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 123 places, 126 transitions, 260 flow
[2023-11-01 18:39:55,161 INFO  L130       PetriNetUnfolder]: 8/172 cut-off events.
[2023-11-01 18:39:55,161 INFO  L131       PetriNetUnfolder]: For 1/2 co-relation queries the response was YES.
[2023-11-01 18:39:55,166 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 178 conditions, 172 events. 8/172 cut-off events. For 1/2 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 364 event pairs, 0 based on Foata normal form. 0/148 useless extension candidates. Maximal degree in co-relation 85. Up to 4 conditions per place. 
[2023-11-01 18:39:55,166 INFO  L82        GeneralOperation]: Start removeDead. Operand has 123 places, 126 transitions, 260 flow
[2023-11-01 18:39:55,170 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 123 places, 126 transitions, 260 flow
[2023-11-01 18:39:55,173 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-11-01 18:39:55,181 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 123 places, 126 transitions, 260 flow
[2023-11-01 18:39:55,183 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 123 places, 126 transitions, 260 flow
[2023-11-01 18:39:55,183 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 123 places, 126 transitions, 260 flow
[2023-11-01 18:39:55,228 INFO  L130       PetriNetUnfolder]: 8/172 cut-off events.
[2023-11-01 18:39:55,229 INFO  L131       PetriNetUnfolder]: For 1/2 co-relation queries the response was YES.
[2023-11-01 18:39:55,230 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 178 conditions, 172 events. 8/172 cut-off events. For 1/2 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 364 event pairs, 0 based on Foata normal form. 0/148 useless extension candidates. Maximal degree in co-relation 85. Up to 4 conditions per place. 
[2023-11-01 18:39:55,231 INFO  L119        LiptonReduction]: Number of co-enabled transitions 3498
[2023-11-01 18:40:00,009 INFO  L134        LiptonReduction]: Checked pairs total: 3353
[2023-11-01 18:40:00,009 INFO  L136        LiptonReduction]: Total number of compositions: 149
[2023-11-01 18:40:00,021 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-11-01 18:40:00,027 INFO  L357      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mHoare=true, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=LoopsAndPotentialCycles, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@302f80c3, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-11-01 18:40:00,027 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 15 error locations.
[2023-11-01 18:40:00,029 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2023-11-01 18:40:00,029 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-11-01 18:40:00,029 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:00,030 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2023-11-01 18:40:00,030 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-11-01 18:40:00,034 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:00,034 INFO  L85        PathProgramCache]: Analyzing trace with hash 15665, now seen corresponding path program 1 times
[2023-11-01 18:40:00,040 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:00,041 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1565817862]
[2023-11-01 18:40:00,041 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:00,041 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:00,119 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:00,165 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:00,165 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:00,166 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1565817862]
[2023-11-01 18:40:00,166 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1565817862] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:00,166 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:00,166 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2023-11-01 18:40:00,168 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1461581889]
[2023-11-01 18:40:00,168 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:00,174 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2023-11-01 18:40:00,174 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:00,189 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2023-11-01 18:40:00,190 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2023-11-01 18:40:00,192 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 121 out of 275
[2023-11-01 18:40:00,193 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 22 places, 20 transitions, 48 flow. Second operand  has 2 states, 2 states have (on average 122.0) internal successors, (244), 2 states have internal predecessors, (244), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:00,193 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:00,193 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 121 of 275
[2023-11-01 18:40:00,194 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:00,239 INFO  L130       PetriNetUnfolder]: 6/26 cut-off events.
[2023-11-01 18:40:00,239 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2023-11-01 18:40:00,240 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 58 conditions, 26 events. 6/26 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 55 event pairs, 5 based on Foata normal form. 0/20 useless extension candidates. Maximal degree in co-relation 32. Up to 25 conditions per place. 
[2023-11-01 18:40:00,240 INFO  L137   encePairwiseOnDemand]: 266/275 looper letters, 5 selfloop transitions, 0 changer transitions 5/11 dead transitions.
[2023-11-01 18:40:00,240 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 14 places, 11 transitions, 50 flow
[2023-11-01 18:40:00,242 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2023-11-01 18:40:00,243 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2023-11-01 18:40:00,250 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 261 transitions.
[2023-11-01 18:40:00,251 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.47454545454545455
[2023-11-01 18:40:00,252 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 261 transitions.
[2023-11-01 18:40:00,252 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 261 transitions.
[2023-11-01 18:40:00,253 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:00,255 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 261 transitions.
[2023-11-01 18:40:00,257 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 130.5) internal successors, (261), 2 states have internal predecessors, (261), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:00,261 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 275.0) internal successors, (825), 3 states have internal predecessors, (825), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:00,262 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 275.0) internal successors, (825), 3 states have internal predecessors, (825), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:00,263 INFO  L175             Difference]: Start difference. First operand has 22 places, 20 transitions, 48 flow. Second operand 2 states and 261 transitions.
[2023-11-01 18:40:00,264 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 14 places, 11 transitions, 50 flow
[2023-11-01 18:40:00,265 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 14 places, 11 transitions, 50 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-11-01 18:40:00,266 INFO  L231             Difference]: Finished difference. Result has 14 places, 6 transitions, 17 flow
[2023-11-01 18:40:00,267 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=275, PETRI_DIFFERENCE_MINUEND_FLOW=30, PETRI_DIFFERENCE_MINUEND_PLACES=13, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=11, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=11, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=17, PETRI_PLACES=14, PETRI_TRANSITIONS=6}
[2023-11-01 18:40:00,270 INFO  L288   CegarLoopForPetriNet]: 22 programPoint places, -8 predicate places.
[2023-11-01 18:40:00,271 INFO  L495      AbstractCegarLoop]: Abstraction has has 14 places, 6 transitions, 17 flow
[2023-11-01 18:40:00,271 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 122.0) internal successors, (244), 2 states have internal predecessors, (244), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:00,271 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:00,271 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1]
[2023-11-01 18:40:00,272 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2023-11-01 18:40:00,272 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2023-11-01 18:40:00,272 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:00,272 INFO  L85        PathProgramCache]: Analyzing trace with hash 1590976134, now seen corresponding path program 1 times
[2023-11-01 18:40:00,272 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:00,273 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [708129995]
[2023-11-01 18:40:00,273 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:00,273 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:00,314 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-11-01 18:40:00,314 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-11-01 18:40:00,335 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-11-01 18:40:00,352 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-11-01 18:40:00,352 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-11-01 18:40:00,353 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (14 of 15 remaining)
[2023-11-01 18:40:00,354 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (13 of 15 remaining)
[2023-11-01 18:40:00,355 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (12 of 15 remaining)
[2023-11-01 18:40:00,355 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (11 of 15 remaining)
[2023-11-01 18:40:00,355 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (10 of 15 remaining)
[2023-11-01 18:40:00,355 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (9 of 15 remaining)
[2023-11-01 18:40:00,355 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (8 of 15 remaining)
[2023-11-01 18:40:00,356 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (7 of 15 remaining)
[2023-11-01 18:40:00,356 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (6 of 15 remaining)
[2023-11-01 18:40:00,356 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (5 of 15 remaining)
[2023-11-01 18:40:00,356 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (4 of 15 remaining)
[2023-11-01 18:40:00,356 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (3 of 15 remaining)
[2023-11-01 18:40:00,356 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (2 of 15 remaining)
[2023-11-01 18:40:00,357 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (1 of 15 remaining)
[2023-11-01 18:40:00,357 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (0 of 15 remaining)
[2023-11-01 18:40:00,357 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2023-11-01 18:40:00,357 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1]
[2023-11-01 18:40:00,359 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-11-01 18:40:00,359 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2023-11-01 18:40:00,375 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2023-11-01 18:40:00,378 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 157 places, 161 transitions, 340 flow
[2023-11-01 18:40:00,417 INFO  L130       PetriNetUnfolder]: 15/303 cut-off events.
[2023-11-01 18:40:00,417 INFO  L131       PetriNetUnfolder]: For 6/8 co-relation queries the response was YES.
[2023-11-01 18:40:00,419 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 317 conditions, 303 events. 15/303 cut-off events. For 6/8 co-relation queries the response was YES. Maximal size of possible extension queue 9. Compared 779 event pairs, 0 based on Foata normal form. 0/259 useless extension candidates. Maximal degree in co-relation 174. Up to 8 conditions per place. 
[2023-11-01 18:40:00,419 INFO  L82        GeneralOperation]: Start removeDead. Operand has 157 places, 161 transitions, 340 flow
[2023-11-01 18:40:00,420 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 157 places, 161 transitions, 340 flow
[2023-11-01 18:40:00,421 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-11-01 18:40:00,421 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 157 places, 161 transitions, 340 flow
[2023-11-01 18:40:00,421 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 157 places, 161 transitions, 340 flow
[2023-11-01 18:40:00,421 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 157 places, 161 transitions, 340 flow
[2023-11-01 18:40:00,459 INFO  L130       PetriNetUnfolder]: 15/303 cut-off events.
[2023-11-01 18:40:00,459 INFO  L131       PetriNetUnfolder]: For 6/8 co-relation queries the response was YES.
[2023-11-01 18:40:00,461 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 317 conditions, 303 events. 15/303 cut-off events. For 6/8 co-relation queries the response was YES. Maximal size of possible extension queue 9. Compared 779 event pairs, 0 based on Foata normal form. 0/259 useless extension candidates. Maximal degree in co-relation 174. Up to 8 conditions per place. 
[2023-11-01 18:40:00,466 INFO  L119        LiptonReduction]: Number of co-enabled transitions 10032
[2023-11-01 18:40:05,007 INFO  L134        LiptonReduction]: Checked pairs total: 40957
[2023-11-01 18:40:05,007 INFO  L136        LiptonReduction]: Total number of compositions: 117
[2023-11-01 18:40:05,009 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-11-01 18:40:05,010 INFO  L357      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mHoare=true, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=LoopsAndPotentialCycles, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@302f80c3, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-11-01 18:40:05,010 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 20 error locations.
[2023-11-01 18:40:05,011 INFO  L130       PetriNetUnfolder]: 0/2 cut-off events.
[2023-11-01 18:40:05,011 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-11-01 18:40:05,011 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:05,011 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2023-11-01 18:40:05,011 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 17 more)] ===
[2023-11-01 18:40:05,012 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:05,012 INFO  L85        PathProgramCache]: Analyzing trace with hash 25883, now seen corresponding path program 1 times
[2023-11-01 18:40:05,012 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:05,012 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [141519197]
[2023-11-01 18:40:05,012 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:05,012 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:05,022 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:05,032 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:05,033 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:05,033 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [141519197]
[2023-11-01 18:40:05,033 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [141519197] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:05,033 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:05,033 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2023-11-01 18:40:05,033 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1415814439]
[2023-11-01 18:40:05,033 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:05,034 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2023-11-01 18:40:05,034 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:05,034 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2023-11-01 18:40:05,034 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2023-11-01 18:40:05,035 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 154 out of 278
[2023-11-01 18:40:05,035 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 65 places, 66 transitions, 150 flow. Second operand  has 2 states, 2 states have (on average 155.0) internal successors, (310), 2 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)
[2023-11-01 18:40:05,035 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:05,035 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 154 of 278
[2023-11-01 18:40:05,036 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:05,233 INFO  L130       PetriNetUnfolder]: 930/2293 cut-off events.
[2023-11-01 18:40:05,233 INFO  L131       PetriNetUnfolder]: For 48/48 co-relation queries the response was YES.
[2023-11-01 18:40:05,236 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 3769 conditions, 2293 events. 930/2293 cut-off events. For 48/48 co-relation queries the response was YES. Maximal size of possible extension queue 104. Compared 16373 event pairs, 700 based on Foata normal form. 0/1837 useless extension candidates. Maximal degree in co-relation 1386. Up to 1419 conditions per place. 
[2023-11-01 18:40:05,244 INFO  L137   encePairwiseOnDemand]: 274/278 looper letters, 28 selfloop transitions, 0 changer transitions 0/62 dead transitions.
[2023-11-01 18:40:05,245 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 62 places, 62 transitions, 198 flow
[2023-11-01 18:40:05,245 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2023-11-01 18:40:05,246 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2023-11-01 18:40:05,247 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 340 transitions.
[2023-11-01 18:40:05,248 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6115107913669064
[2023-11-01 18:40:05,248 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 340 transitions.
[2023-11-01 18:40:05,248 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 340 transitions.
[2023-11-01 18:40:05,248 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:05,248 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 340 transitions.
[2023-11-01 18:40:05,250 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 170.0) internal successors, (340), 2 states have internal predecessors, (340), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,251 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 278.0) internal successors, (834), 3 states have internal predecessors, (834), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,252 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 278.0) internal successors, (834), 3 states have internal predecessors, (834), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,252 INFO  L175             Difference]: Start difference. First operand has 65 places, 66 transitions, 150 flow. Second operand 2 states and 340 transitions.
[2023-11-01 18:40:05,252 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 62 places, 62 transitions, 198 flow
[2023-11-01 18:40:05,253 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 62 places, 62 transitions, 198 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-11-01 18:40:05,254 INFO  L231             Difference]: Finished difference. Result has 62 places, 62 transitions, 142 flow
[2023-11-01 18:40:05,254 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, PETRI_DIFFERENCE_MINUEND_FLOW=142, PETRI_DIFFERENCE_MINUEND_PLACES=61, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=62, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=62, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=142, PETRI_PLACES=62, PETRI_TRANSITIONS=62}
[2023-11-01 18:40:05,254 INFO  L288   CegarLoopForPetriNet]: 65 programPoint places, -3 predicate places.
[2023-11-01 18:40:05,254 INFO  L495      AbstractCegarLoop]: Abstraction has has 62 places, 62 transitions, 142 flow
[2023-11-01 18:40:05,255 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 155.0) internal successors, (310), 2 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)
[2023-11-01 18:40:05,255 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:05,255 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:05,255 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2023-11-01 18:40:05,255 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 17 more)] ===
[2023-11-01 18:40:05,256 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:05,256 INFO  L85        PathProgramCache]: Analyzing trace with hash -1846904749, now seen corresponding path program 1 times
[2023-11-01 18:40:05,256 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:05,256 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1579492197]
[2023-11-01 18:40:05,256 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:05,256 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:05,270 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:05,299 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:05,299 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:05,300 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1579492197]
[2023-11-01 18:40:05,300 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1579492197] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:05,300 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:05,300 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-11-01 18:40:05,300 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [800817988]
[2023-11-01 18:40:05,300 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:05,300 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:05,300 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:05,301 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:05,301 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:05,329 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 144 out of 278
[2023-11-01 18:40:05,330 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 62 places, 62 transitions, 142 flow. Second operand  has 3 states, 3 states have (on average 146.0) internal successors, (438), 3 states have internal predecessors, (438), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,330 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:05,330 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 144 of 278
[2023-11-01 18:40:05,330 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:05,625 INFO  L130       PetriNetUnfolder]: 1444/3265 cut-off events.
[2023-11-01 18:40:05,625 INFO  L131       PetriNetUnfolder]: For 60/60 co-relation queries the response was YES.
[2023-11-01 18:40:05,628 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 5539 conditions, 3265 events. 1444/3265 cut-off events. For 60/60 co-relation queries the response was YES. Maximal size of possible extension queue 130. Compared 23374 event pairs, 989 based on Foata normal form. 0/2544 useless extension candidates. Maximal degree in co-relation 5534. Up to 2044 conditions per place. 
[2023-11-01 18:40:05,639 INFO  L137   encePairwiseOnDemand]: 272/278 looper letters, 46 selfloop transitions, 5 changer transitions 0/81 dead transitions.
[2023-11-01 18:40:05,639 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 64 places, 81 transitions, 290 flow
[2023-11-01 18:40:05,640 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:05,640 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:05,641 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 484 transitions.
[2023-11-01 18:40:05,642 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.580335731414868
[2023-11-01 18:40:05,642 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 484 transitions.
[2023-11-01 18:40:05,642 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 484 transitions.
[2023-11-01 18:40:05,643 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:05,643 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 484 transitions.
[2023-11-01 18:40:05,644 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 161.33333333333334) internal successors, (484), 3 states have internal predecessors, (484), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,646 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,647 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,647 INFO  L175             Difference]: Start difference. First operand has 62 places, 62 transitions, 142 flow. Second operand 3 states and 484 transitions.
[2023-11-01 18:40:05,647 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 64 places, 81 transitions, 290 flow
[2023-11-01 18:40:05,648 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 64 places, 81 transitions, 290 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-11-01 18:40:05,649 INFO  L231             Difference]: Finished difference. Result has 65 places, 66 transitions, 175 flow
[2023-11-01 18:40:05,649 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, PETRI_DIFFERENCE_MINUEND_FLOW=142, PETRI_DIFFERENCE_MINUEND_PLACES=62, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=62, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=57, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=175, PETRI_PLACES=65, PETRI_TRANSITIONS=66}
[2023-11-01 18:40:05,650 INFO  L288   CegarLoopForPetriNet]: 65 programPoint places, 0 predicate places.
[2023-11-01 18:40:05,650 INFO  L495      AbstractCegarLoop]: Abstraction has has 65 places, 66 transitions, 175 flow
[2023-11-01 18:40:05,650 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 146.0) internal successors, (438), 3 states have internal predecessors, (438), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,650 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:05,650 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:05,650 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2023-11-01 18:40:05,651 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 17 more)] ===
[2023-11-01 18:40:05,651 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:05,651 INFO  L85        PathProgramCache]: Analyzing trace with hash -1053843740, now seen corresponding path program 1 times
[2023-11-01 18:40:05,651 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:05,651 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [474497143]
[2023-11-01 18:40:05,651 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:05,652 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:05,663 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:05,685 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:05,685 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:05,685 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [474497143]
[2023-11-01 18:40:05,685 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [474497143] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:05,686 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:05,686 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-11-01 18:40:05,686 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1040044132]
[2023-11-01 18:40:05,686 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:05,686 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:05,686 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:05,687 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:05,687 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:05,706 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 140 out of 278
[2023-11-01 18:40:05,707 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 65 places, 66 transitions, 175 flow. Second operand  has 3 states, 3 states have (on average 142.66666666666666) internal successors, (428), 3 states have internal predecessors, (428), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:05,707 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:05,707 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 140 of 278
[2023-11-01 18:40:05,707 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:06,108 INFO  L130       PetriNetUnfolder]: 2488/5236 cut-off events.
[2023-11-01 18:40:06,108 INFO  L131       PetriNetUnfolder]: For 516/556 co-relation queries the response was YES.
[2023-11-01 18:40:06,114 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 9980 conditions, 5236 events. 2488/5236 cut-off events. For 516/556 co-relation queries the response was YES. Maximal size of possible extension queue 185. Compared 38412 event pairs, 724 based on Foata normal form. 0/4398 useless extension candidates. Maximal degree in co-relation 9973. Up to 2984 conditions per place. 
[2023-11-01 18:40:06,131 INFO  L137   encePairwiseOnDemand]: 264/278 looper letters, 66 selfloop transitions, 12 changer transitions 0/101 dead transitions.
[2023-11-01 18:40:06,131 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 67 places, 101 transitions, 429 flow
[2023-11-01 18:40:06,132 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:06,132 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:06,133 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 496 transitions.
[2023-11-01 18:40:06,133 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5947242206235012
[2023-11-01 18:40:06,134 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 496 transitions.
[2023-11-01 18:40:06,134 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 496 transitions.
[2023-11-01 18:40:06,134 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:06,134 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 496 transitions.
[2023-11-01 18:40:06,135 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 165.33333333333334) internal successors, (496), 3 states have internal predecessors, (496), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,137 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,138 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,138 INFO  L175             Difference]: Start difference. First operand has 65 places, 66 transitions, 175 flow. Second operand 3 states and 496 transitions.
[2023-11-01 18:40:06,138 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 67 places, 101 transitions, 429 flow
[2023-11-01 18:40:06,143 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 66 places, 101 transitions, 421 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-11-01 18:40:06,144 INFO  L231             Difference]: Finished difference. Result has 68 places, 77 transitions, 280 flow
[2023-11-01 18:40:06,144 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, PETRI_DIFFERENCE_MINUEND_FLOW=170, PETRI_DIFFERENCE_MINUEND_PLACES=64, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=66, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=54, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=280, PETRI_PLACES=68, PETRI_TRANSITIONS=77}
[2023-11-01 18:40:06,145 INFO  L288   CegarLoopForPetriNet]: 65 programPoint places, 3 predicate places.
[2023-11-01 18:40:06,145 INFO  L495      AbstractCegarLoop]: Abstraction has has 68 places, 77 transitions, 280 flow
[2023-11-01 18:40:06,145 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 142.66666666666666) internal successors, (428), 3 states have internal predecessors, (428), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,145 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:06,146 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:06,146 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2023-11-01 18:40:06,146 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 17 more)] ===
[2023-11-01 18:40:06,146 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:06,146 INFO  L85        PathProgramCache]: Analyzing trace with hash 1117300612, now seen corresponding path program 1 times
[2023-11-01 18:40:06,147 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:06,147 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [729869917]
[2023-11-01 18:40:06,147 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:06,147 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:06,160 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:06,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2023-11-01 18:40:06,189 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:06,189 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [729869917]
[2023-11-01 18:40:06,190 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [729869917] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:06,190 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:06,190 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-11-01 18:40:06,190 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [137836116]
[2023-11-01 18:40:06,190 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:06,191 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:06,191 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:06,191 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:06,191 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:06,219 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 144 out of 278
[2023-11-01 18:40:06,220 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 68 places, 77 transitions, 280 flow. Second operand  has 3 states, 3 states have (on average 146.66666666666666) internal successors, (440), 3 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)
[2023-11-01 18:40:06,220 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:06,220 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 144 of 278
[2023-11-01 18:40:06,220 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:06,556 INFO  L130       PetriNetUnfolder]: 2202/5012 cut-off events.
[2023-11-01 18:40:06,557 INFO  L131       PetriNetUnfolder]: For 1694/1776 co-relation queries the response was YES.
[2023-11-01 18:40:06,563 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 10394 conditions, 5012 events. 2202/5012 cut-off events. For 1694/1776 co-relation queries the response was YES. Maximal size of possible extension queue 196. Compared 39136 event pairs, 1240 based on Foata normal form. 30/4164 useless extension candidates. Maximal degree in co-relation 10386. Up to 3095 conditions per place. 
[2023-11-01 18:40:06,579 INFO  L137   encePairwiseOnDemand]: 272/278 looper letters, 54 selfloop transitions, 8 changer transitions 0/96 dead transitions.
[2023-11-01 18:40:06,579 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 70 places, 96 transitions, 461 flow
[2023-11-01 18:40:06,580 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:06,580 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:06,581 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 483 transitions.
[2023-11-01 18:40:06,582 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.579136690647482
[2023-11-01 18:40:06,582 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 483 transitions.
[2023-11-01 18:40:06,582 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 483 transitions.
[2023-11-01 18:40:06,582 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:06,582 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 483 transitions.
[2023-11-01 18:40:06,583 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 161.0) internal successors, (483), 3 states have internal predecessors, (483), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,585 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,585 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:06,585 INFO  L175             Difference]: Start difference. First operand has 68 places, 77 transitions, 280 flow. Second operand 3 states and 483 transitions.
[2023-11-01 18:40:06,585 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 70 places, 96 transitions, 461 flow
[2023-11-01 18:40:06,590 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 68 places, 96 transitions, 433 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-11-01 18:40:06,591 INFO  L231             Difference]: Finished difference. Result has 69 places, 82 transitions, 312 flow
[2023-11-01 18:40:06,591 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, PETRI_DIFFERENCE_MINUEND_FLOW=256, PETRI_DIFFERENCE_MINUEND_PLACES=66, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=77, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=3, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=69, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=312, PETRI_PLACES=69, PETRI_TRANSITIONS=82}
[2023-11-01 18:40:06,592 INFO  L288   CegarLoopForPetriNet]: 65 programPoint places, 4 predicate places.
[2023-11-01 18:40:06,592 INFO  L495      AbstractCegarLoop]: Abstraction has has 69 places, 82 transitions, 312 flow
[2023-11-01 18:40:06,592 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 146.66666666666666) internal successors, (440), 3 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)
[2023-11-01 18:40:06,592 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:06,592 INFO  L209   CegarLoopForPetriNet]: trace histogram [3, 2, 2, 1, 1, 1, 1]
[2023-11-01 18:40:06,592 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2023-11-01 18:40:06,593 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 17 more)] ===
[2023-11-01 18:40:06,593 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:06,593 INFO  L85        PathProgramCache]: Analyzing trace with hash 273310607, now seen corresponding path program 1 times
[2023-11-01 18:40:06,593 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:06,593 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [167138193]
[2023-11-01 18:40:06,593 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:06,594 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:06,619 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-11-01 18:40:06,619 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-11-01 18:40:06,630 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-11-01 18:40:06,636 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-11-01 18:40:06,636 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-11-01 18:40:06,636 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (19 of 20 remaining)
[2023-11-01 18:40:06,636 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (18 of 20 remaining)
[2023-11-01 18:40:06,636 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (17 of 20 remaining)
[2023-11-01 18:40:06,636 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (16 of 20 remaining)
[2023-11-01 18:40:06,636 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (15 of 20 remaining)
[2023-11-01 18:40:06,637 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (14 of 20 remaining)
[2023-11-01 18:40:06,637 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (13 of 20 remaining)
[2023-11-01 18:40:06,637 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (12 of 20 remaining)
[2023-11-01 18:40:06,637 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (11 of 20 remaining)
[2023-11-01 18:40:06,644 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (10 of 20 remaining)
[2023-11-01 18:40:06,645 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (9 of 20 remaining)
[2023-11-01 18:40:06,645 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (8 of 20 remaining)
[2023-11-01 18:40:06,645 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (7 of 20 remaining)
[2023-11-01 18:40:06,645 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (6 of 20 remaining)
[2023-11-01 18:40:06,645 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (5 of 20 remaining)
[2023-11-01 18:40:06,645 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (4 of 20 remaining)
[2023-11-01 18:40:06,646 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (3 of 20 remaining)
[2023-11-01 18:40:06,646 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (2 of 20 remaining)
[2023-11-01 18:40:06,646 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (1 of 20 remaining)
[2023-11-01 18:40:06,646 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (0 of 20 remaining)
[2023-11-01 18:40:06,646 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2023-11-01 18:40:06,646 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2023-11-01 18:40:06,647 WARN  L233   ceAbstractionStarter]: 2 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-11-01 18:40:06,647 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 3 thread instances.
[2023-11-01 18:40:06,662 INFO  L144    ThreadInstanceAdder]: Constructed 3 joinOtherThreadTransitions.
[2023-11-01 18:40:06,664 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 191 places, 196 transitions, 422 flow
[2023-11-01 18:40:06,705 INFO  L130       PetriNetUnfolder]: 27/513 cut-off events.
[2023-11-01 18:40:06,705 INFO  L131       PetriNetUnfolder]: For 19/22 co-relation queries the response was YES.
[2023-11-01 18:40:06,707 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 541 conditions, 513 events. 27/513 cut-off events. For 19/22 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 1646 event pairs, 1 based on Foata normal form. 0/439 useless extension candidates. Maximal degree in co-relation 311. Up to 16 conditions per place. 
[2023-11-01 18:40:06,707 INFO  L82        GeneralOperation]: Start removeDead. Operand has 191 places, 196 transitions, 422 flow
[2023-11-01 18:40:06,709 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 191 places, 196 transitions, 422 flow
[2023-11-01 18:40:06,709 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-11-01 18:40:06,709 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 191 places, 196 transitions, 422 flow
[2023-11-01 18:40:06,710 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 191 places, 196 transitions, 422 flow
[2023-11-01 18:40:06,710 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 191 places, 196 transitions, 422 flow
[2023-11-01 18:40:06,746 INFO  L130       PetriNetUnfolder]: 27/513 cut-off events.
[2023-11-01 18:40:06,746 INFO  L131       PetriNetUnfolder]: For 19/22 co-relation queries the response was YES.
[2023-11-01 18:40:06,747 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 541 conditions, 513 events. 27/513 cut-off events. For 19/22 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 1646 event pairs, 1 based on Foata normal form. 0/439 useless extension candidates. Maximal degree in co-relation 311. Up to 16 conditions per place. 
[2023-11-01 18:40:06,760 INFO  L119        LiptonReduction]: Number of co-enabled transitions 18612
[2023-11-01 18:40:10,873 INFO  L134        LiptonReduction]: Checked pairs total: 81653
[2023-11-01 18:40:10,873 INFO  L136        LiptonReduction]: Total number of compositions: 124
[2023-11-01 18:40:10,875 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-11-01 18:40:10,876 INFO  L357      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mHoare=true, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=LoopsAndPotentialCycles, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@302f80c3, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-11-01 18:40:10,877 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 25 error locations.
[2023-11-01 18:40:10,878 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2023-11-01 18:40:10,878 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-11-01 18:40:10,878 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:10,879 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2023-11-01 18:40:10,879 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 22 more)] ===
[2023-11-01 18:40:10,879 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:10,879 INFO  L85        PathProgramCache]: Analyzing trace with hash 37242, now seen corresponding path program 1 times
[2023-11-01 18:40:10,880 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:10,880 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [354131420]
[2023-11-01 18:40:10,880 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:10,880 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:10,886 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:10,891 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:10,892 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:10,892 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [354131420]
[2023-11-01 18:40:10,892 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [354131420] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:10,892 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:10,892 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2023-11-01 18:40:10,892 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1839889247]
[2023-11-01 18:40:10,892 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:10,892 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2023-11-01 18:40:10,892 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:10,893 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2023-11-01 18:40:10,893 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2023-11-01 18:40:10,893 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 187 out of 320
[2023-11-01 18:40:10,894 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 92 places, 94 transitions, 218 flow. Second operand  has 2 states, 2 states have (on average 188.0) internal successors, (376), 2 states have internal predecessors, (376), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:10,894 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:10,894 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 187 of 320
[2023-11-01 18:40:10,894 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:12,245 INFO  L130       PetriNetUnfolder]: 12916/23507 cut-off events.
[2023-11-01 18:40:12,246 INFO  L131       PetriNetUnfolder]: For 842/842 co-relation queries the response was YES.
[2023-11-01 18:40:12,272 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 41422 conditions, 23507 events. 12916/23507 cut-off events. For 842/842 co-relation queries the response was YES. Maximal size of possible extension queue 834. Compared 206204 event pairs, 9875 based on Foata normal form. 0/19435 useless extension candidates. Maximal degree in co-relation 7761. Up to 17305 conditions per place. 
[2023-11-01 18:40:12,344 INFO  L137   encePairwiseOnDemand]: 316/320 looper letters, 38 selfloop transitions, 0 changer transitions 0/90 dead transitions.
[2023-11-01 18:40:12,344 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 89 places, 90 transitions, 286 flow
[2023-11-01 18:40:12,345 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2023-11-01 18:40:12,345 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2023-11-01 18:40:12,346 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 416 transitions.
[2023-11-01 18:40:12,346 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.65
[2023-11-01 18:40:12,346 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 416 transitions.
[2023-11-01 18:40:12,346 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 416 transitions.
[2023-11-01 18:40:12,346 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:12,347 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 416 transitions.
[2023-11-01 18:40:12,347 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 208.0) internal successors, (416), 2 states have internal predecessors, (416), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:12,348 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 320.0) internal successors, (960), 3 states have internal predecessors, (960), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:12,349 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 320.0) internal successors, (960), 3 states have internal predecessors, (960), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:12,349 INFO  L175             Difference]: Start difference. First operand has 92 places, 94 transitions, 218 flow. Second operand 2 states and 416 transitions.
[2023-11-01 18:40:12,349 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 89 places, 90 transitions, 286 flow
[2023-11-01 18:40:12,350 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 89 places, 90 transitions, 286 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-11-01 18:40:12,351 INFO  L231             Difference]: Finished difference. Result has 89 places, 90 transitions, 210 flow
[2023-11-01 18:40:12,351 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=320, PETRI_DIFFERENCE_MINUEND_FLOW=210, PETRI_DIFFERENCE_MINUEND_PLACES=88, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=90, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=90, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=210, PETRI_PLACES=89, PETRI_TRANSITIONS=90}
[2023-11-01 18:40:12,352 INFO  L288   CegarLoopForPetriNet]: 92 programPoint places, -3 predicate places.
[2023-11-01 18:40:12,352 INFO  L495      AbstractCegarLoop]: Abstraction has has 89 places, 90 transitions, 210 flow
[2023-11-01 18:40:12,352 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 188.0) internal successors, (376), 2 states have internal predecessors, (376), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:12,352 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:12,352 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:12,352 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2023-11-01 18:40:12,353 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 22 more)] ===
[2023-11-01 18:40:12,353 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:12,353 INFO  L85        PathProgramCache]: Analyzing trace with hash 65970927, now seen corresponding path program 1 times
[2023-11-01 18:40:12,353 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:12,353 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2001973296]
[2023-11-01 18:40:12,353 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:12,353 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:12,361 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:12,376 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:12,376 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:12,376 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2001973296]
[2023-11-01 18:40:12,376 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2001973296] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:12,376 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:12,376 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-11-01 18:40:12,376 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1223181611]
[2023-11-01 18:40:12,377 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:12,377 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:12,377 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:12,377 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:12,377 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:12,411 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 174 out of 320
[2023-11-01 18:40:12,412 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 89 places, 90 transitions, 210 flow. Second operand  has 3 states, 3 states have (on average 176.0) internal successors, (528), 3 states have internal predecessors, (528), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:12,412 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:12,412 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 174 of 320
[2023-11-01 18:40:12,412 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:14,839 INFO  L130       PetriNetUnfolder]: 22362/39065 cut-off events.
[2023-11-01 18:40:14,839 INFO  L131       PetriNetUnfolder]: For 1415/1415 co-relation queries the response was YES.
[2023-11-01 18:40:14,889 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 70043 conditions, 39065 events. 22362/39065 cut-off events. For 1415/1415 co-relation queries the response was YES. Maximal size of possible extension queue 1293. Compared 346238 event pairs, 13805 based on Foata normal form. 0/31721 useless extension candidates. Maximal degree in co-relation 70037. Up to 25651 conditions per place. 
[2023-11-01 18:40:15,032 INFO  L137   encePairwiseOnDemand]: 310/320 looper letters, 63 selfloop transitions, 9 changer transitions 0/120 dead transitions.
[2023-11-01 18:40:15,032 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 91 places, 120 transitions, 432 flow
[2023-11-01 18:40:15,033 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:15,033 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:15,034 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 595 transitions.
[2023-11-01 18:40:15,034 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6197916666666666
[2023-11-01 18:40:15,034 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 595 transitions.
[2023-11-01 18:40:15,034 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 595 transitions.
[2023-11-01 18:40:15,035 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:15,035 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 595 transitions.
[2023-11-01 18:40:15,036 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 198.33333333333334) internal successors, (595), 3 states have internal predecessors, (595), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:15,038 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:15,038 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:15,039 INFO  L175             Difference]: Start difference. First operand has 89 places, 90 transitions, 210 flow. Second operand 3 states and 595 transitions.
[2023-11-01 18:40:15,039 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 91 places, 120 transitions, 432 flow
[2023-11-01 18:40:15,041 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 91 places, 120 transitions, 432 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-11-01 18:40:15,042 INFO  L231             Difference]: Finished difference. Result has 93 places, 98 transitions, 280 flow
[2023-11-01 18:40:15,042 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=320, PETRI_DIFFERENCE_MINUEND_FLOW=210, PETRI_DIFFERENCE_MINUEND_PLACES=89, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=90, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=81, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=280, PETRI_PLACES=93, PETRI_TRANSITIONS=98}
[2023-11-01 18:40:15,043 INFO  L288   CegarLoopForPetriNet]: 92 programPoint places, 1 predicate places.
[2023-11-01 18:40:15,043 INFO  L495      AbstractCegarLoop]: Abstraction has has 93 places, 98 transitions, 280 flow
[2023-11-01 18:40:15,043 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 176.0) internal successors, (528), 3 states have internal predecessors, (528), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:15,043 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:15,044 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:15,044 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2023-11-01 18:40:15,044 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 22 more)] ===
[2023-11-01 18:40:15,044 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:15,045 INFO  L85        PathProgramCache]: Analyzing trace with hash -1026413917, now seen corresponding path program 1 times
[2023-11-01 18:40:15,045 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:15,045 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1849706191]
[2023-11-01 18:40:15,045 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:15,045 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:15,056 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:15,076 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:15,077 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:15,077 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1849706191]
[2023-11-01 18:40:15,077 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1849706191] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:15,078 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:15,078 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-11-01 18:40:15,078 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [742422197]
[2023-11-01 18:40:15,078 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:15,079 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:15,079 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:15,080 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:15,080 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:15,115 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 166 out of 320
[2023-11-01 18:40:15,115 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 93 places, 98 transitions, 280 flow. Second operand  has 3 states, 3 states have (on average 168.33333333333334) internal successors, (505), 3 states have internal predecessors, (505), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:15,115 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:15,115 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 166 of 320
[2023-11-01 18:40:15,115 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:20,476 INFO  L130       PetriNetUnfolder]: 52563/94729 cut-off events.
[2023-11-01 18:40:20,476 INFO  L131       PetriNetUnfolder]: For 22878/25470 co-relation queries the response was YES.
[2023-11-01 18:40:20,660 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 192438 conditions, 94729 events. 52563/94729 cut-off events. For 22878/25470 co-relation queries the response was YES. Maximal size of possible extension queue 2719. Compared 937079 event pairs, 15808 based on Foata normal form. 678/80451 useless extension candidates. Maximal degree in co-relation 192430. Up to 60282 conditions per place. 
[2023-11-01 18:40:20,985 INFO  L137   encePairwiseOnDemand]: 299/320 looper letters, 88 selfloop transitions, 22 changer transitions 0/149 dead transitions.
[2023-11-01 18:40:20,985 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 95 places, 149 transitions, 669 flow
[2023-11-01 18:40:20,986 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:20,986 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:20,987 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 600 transitions.
[2023-11-01 18:40:20,988 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.625
[2023-11-01 18:40:20,988 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 600 transitions.
[2023-11-01 18:40:20,988 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 600 transitions.
[2023-11-01 18:40:20,988 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:20,989 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 600 transitions.
[2023-11-01 18:40:20,990 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 200.0) internal successors, (600), 3 states have internal predecessors, (600), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:20,991 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:20,991 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:20,991 INFO  L175             Difference]: Start difference. First operand has 93 places, 98 transitions, 280 flow. Second operand 3 states and 600 transitions.
[2023-11-01 18:40:20,992 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 95 places, 149 transitions, 669 flow
[2023-11-01 18:40:21,251 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 93 places, 149 transitions, 635 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-11-01 18:40:21,252 INFO  L231             Difference]: Finished difference. Result has 95 places, 120 transitions, 480 flow
[2023-11-01 18:40:21,253 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=320, PETRI_DIFFERENCE_MINUEND_FLOW=262, PETRI_DIFFERENCE_MINUEND_PLACES=91, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=98, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=76, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=480, PETRI_PLACES=95, PETRI_TRANSITIONS=120}
[2023-11-01 18:40:21,253 INFO  L288   CegarLoopForPetriNet]: 92 programPoint places, 3 predicate places.
[2023-11-01 18:40:21,253 INFO  L495      AbstractCegarLoop]: Abstraction has has 95 places, 120 transitions, 480 flow
[2023-11-01 18:40:21,254 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 168.33333333333334) internal successors, (505), 3 states have internal predecessors, (505), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:21,254 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:21,254 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:21,254 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2023-11-01 18:40:21,254 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 22 more)] ===
[2023-11-01 18:40:21,254 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:21,254 INFO  L85        PathProgramCache]: Analyzing trace with hash -954527406, now seen corresponding path program 1 times
[2023-11-01 18:40:21,255 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:21,255 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1657734668]
[2023-11-01 18:40:21,255 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:21,255 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:21,264 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:21,281 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2023-11-01 18:40:21,282 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:21,282 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1657734668]
[2023-11-01 18:40:21,282 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1657734668] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:21,282 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:21,282 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-11-01 18:40:21,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1702859938]
[2023-11-01 18:40:21,282 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:21,282 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:21,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:21,283 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:21,283 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:21,315 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 174 out of 320
[2023-11-01 18:40:21,316 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 95 places, 120 transitions, 480 flow. Second operand  has 3 states, 3 states have (on average 176.66666666666666) internal successors, (530), 3 states have internal predecessors, (530), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:21,316 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:21,316 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 174 of 320
[2023-11-01 18:40:21,316 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:25,681 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1011] L1021-2-->L1021-4: Formula: (= v_~shared~0_68 (+ |v_threadThread1of3ForFork0_#t~post5_9| 1))  InVars {threadThread1of3ForFork0_#t~post5=|v_threadThread1of3ForFork0_#t~post5_9|}  OutVars{threadThread1of3ForFork0_#t~post5=|v_threadThread1of3ForFork0_#t~post5_9|, ~shared~0=v_~shared~0_68, threadThread1of3ForFork0_#t~nondet6=|v_threadThread1of3ForFork0_#t~nondet6_13|}  AuxVars[]  AssignedVars[~shared~0, threadThread1of3ForFork0_#t~nondet6][79], [211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), Black: 203#true, 205#(= |#race~data~0| 0), 194#true, 14#L1021-4true, Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 46#L1017-4true, threadThread1of3ForFork0InUse, 184#L1034-5true, threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:25,681 INFO  L383   tUnfolder$Statistics]: this new event has 46 ancestors and is cut-off event
[2023-11-01 18:40:25,681 INFO  L386   tUnfolder$Statistics]:   existing Event has 23 ancestors and is cut-off event
[2023-11-01 18:40:25,681 INFO  L386   tUnfolder$Statistics]:   existing Event has 23 ancestors and is cut-off event
[2023-11-01 18:40:25,681 INFO  L386   tUnfolder$Statistics]:   existing Event has 24 ancestors and is cut-off event
[2023-11-01 18:40:25,950 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1011] L1021-2-->L1021-4: Formula: (= v_~shared~0_68 (+ |v_threadThread1of3ForFork0_#t~post5_9| 1))  InVars {threadThread1of3ForFork0_#t~post5=|v_threadThread1of3ForFork0_#t~post5_9|}  OutVars{threadThread1of3ForFork0_#t~post5=|v_threadThread1of3ForFork0_#t~post5_9|, ~shared~0=v_~shared~0_68, threadThread1of3ForFork0_#t~nondet6=|v_threadThread1of3ForFork0_#t~nondet6_13|}  AuxVars[]  AssignedVars[~shared~0, threadThread1of3ForFork0_#t~nondet6][79], [Black: 203#true, 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), 205#(= |#race~data~0| 0), 194#true, 2#ULTIMATE.startEXITtrue, 14#L1021-4true, Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 46#L1017-4true, threadThread1of3ForFork0InUse, threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:25,950 INFO  L383   tUnfolder$Statistics]: this new event has 47 ancestors and is cut-off event
[2023-11-01 18:40:25,950 INFO  L386   tUnfolder$Statistics]:   existing Event has 24 ancestors and is cut-off event
[2023-11-01 18:40:25,950 INFO  L386   tUnfolder$Statistics]:   existing Event has 25 ancestors and is cut-off event
[2023-11-01 18:40:25,950 INFO  L386   tUnfolder$Statistics]:   existing Event has 24 ancestors and is cut-off event
[2023-11-01 18:40:25,951 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1011] L1021-2-->L1021-4: Formula: (= v_~shared~0_68 (+ |v_threadThread1of3ForFork0_#t~post5_9| 1))  InVars {threadThread1of3ForFork0_#t~post5=|v_threadThread1of3ForFork0_#t~post5_9|}  OutVars{threadThread1of3ForFork0_#t~post5=|v_threadThread1of3ForFork0_#t~post5_9|, ~shared~0=v_~shared~0_68, threadThread1of3ForFork0_#t~nondet6=|v_threadThread1of3ForFork0_#t~nondet6_13|}  AuxVars[]  AssignedVars[~shared~0, threadThread1of3ForFork0_#t~nondet6][79], [211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), Black: 203#true, 205#(= |#race~data~0| 0), 194#true, 14#L1021-4true, Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 31#L1035-12true, 46#L1017-4true, threadThread1of3ForFork0InUse, threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:25,951 INFO  L383   tUnfolder$Statistics]: this new event has 47 ancestors and is cut-off event
[2023-11-01 18:40:25,951 INFO  L386   tUnfolder$Statistics]:   existing Event has 24 ancestors and is cut-off event
[2023-11-01 18:40:25,951 INFO  L386   tUnfolder$Statistics]:   existing Event has 24 ancestors and is cut-off event
[2023-11-01 18:40:25,951 INFO  L386   tUnfolder$Statistics]:   existing Event has 25 ancestors and is cut-off event
[2023-11-01 18:40:27,716 INFO  L130       PetriNetUnfolder]: 56550/105928 cut-off events.
[2023-11-01 18:40:27,716 INFO  L131       PetriNetUnfolder]: For 79071/83923 co-relation queries the response was YES.
[2023-11-01 18:40:27,969 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 245693 conditions, 105928 events. 56550/105928 cut-off events. For 79071/83923 co-relation queries the response was YES. Maximal size of possible extension queue 3163. Compared 1115404 event pairs, 25707 based on Foata normal form. 1108/88970 useless extension candidates. Maximal degree in co-relation 245684. Up to 61883 conditions per place. 
[2023-11-01 18:40:28,377 INFO  L137   encePairwiseOnDemand]: 310/320 looper letters, 81 selfloop transitions, 27 changer transitions 0/163 dead transitions.
[2023-11-01 18:40:28,377 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 97 places, 163 transitions, 895 flow
[2023-11-01 18:40:28,378 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:28,378 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:28,379 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 594 transitions.
[2023-11-01 18:40:28,379 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.61875
[2023-11-01 18:40:28,379 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 594 transitions.
[2023-11-01 18:40:28,379 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 594 transitions.
[2023-11-01 18:40:28,380 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:28,380 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 594 transitions.
[2023-11-01 18:40:28,381 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 198.0) internal successors, (594), 3 states have internal predecessors, (594), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:28,382 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:28,382 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:28,382 INFO  L175             Difference]: Start difference. First operand has 95 places, 120 transitions, 480 flow. Second operand 3 states and 594 transitions.
[2023-11-01 18:40:28,382 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 97 places, 163 transitions, 895 flow
[2023-11-01 18:40:28,467 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 95 places, 163 transitions, 831 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-11-01 18:40:28,470 INFO  L231             Difference]: Finished difference. Result has 97 places, 142 transitions, 714 flow
[2023-11-01 18:40:28,470 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=320, PETRI_DIFFERENCE_MINUEND_FLOW=436, PETRI_DIFFERENCE_MINUEND_PLACES=93, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=120, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=5, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=93, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=714, PETRI_PLACES=97, PETRI_TRANSITIONS=142}
[2023-11-01 18:40:28,470 INFO  L288   CegarLoopForPetriNet]: 92 programPoint places, 5 predicate places.
[2023-11-01 18:40:28,471 INFO  L495      AbstractCegarLoop]: Abstraction has has 97 places, 142 transitions, 714 flow
[2023-11-01 18:40:28,471 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 176.66666666666666) internal successors, (530), 3 states have internal predecessors, (530), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:28,471 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:28,471 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:28,471 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2023-11-01 18:40:28,471 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting threadErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 22 more)] ===
[2023-11-01 18:40:28,472 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:28,472 INFO  L85        PathProgramCache]: Analyzing trace with hash -2023816140, now seen corresponding path program 1 times
[2023-11-01 18:40:28,472 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:28,472 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1490534779]
[2023-11-01 18:40:28,472 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:28,472 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:28,481 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-11-01 18:40:28,498 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-11-01 18:40:28,498 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-11-01 18:40:28,499 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1490534779]
[2023-11-01 18:40:28,499 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1490534779] provided 1 perfect and 0 imperfect interpolant sequences
[2023-11-01 18:40:28,499 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-11-01 18:40:28,499 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [3] imperfect sequences [] total 3
[2023-11-01 18:40:28,499 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1495864414]
[2023-11-01 18:40:28,499 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-11-01 18:40:28,500 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-11-01 18:40:28,500 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-11-01 18:40:28,500 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-11-01 18:40:28,500 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-11-01 18:40:28,520 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 171 out of 320
[2023-11-01 18:40:28,520 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 97 places, 142 transitions, 714 flow. Second operand  has 3 states, 3 states have (on average 173.0) internal successors, (519), 3 states have internal predecessors, (519), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:28,521 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-11-01 18:40:28,521 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 171 of 320
[2023-11-01 18:40:28,521 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-11-01 18:40:32,552 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1036] L1017-4-->L1018-1: Formula: (= |v_#race~data~0_102| 0)  InVars {}  OutVars{threadThread2of3ForFork0_#t~nondet3=|v_threadThread2of3ForFork0_#t~nondet3_15|, #race~data~0=|v_#race~data~0_102|}  AuxVars[]  AssignedVars[threadThread2of3ForFork0_#t~nondet3, #race~data~0][46], [Black: 203#true, 17#L1018-1true, 194#true, Black: 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 91#L1017-4true, 184#L1034-5true, threadThread1of3ForFork0InUse, 209#true, 217#(= ~data~0 1), threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:32,552 INFO  L383   tUnfolder$Statistics]: this new event has 42 ancestors and is cut-off event
[2023-11-01 18:40:32,552 INFO  L386   tUnfolder$Statistics]:   existing Event has 17 ancestors and is cut-off event
[2023-11-01 18:40:32,552 INFO  L386   tUnfolder$Statistics]:   existing Event has 42 ancestors and is cut-off event
[2023-11-01 18:40:32,552 INFO  L386   tUnfolder$Statistics]:   existing Event has 17 ancestors and is cut-off event
[2023-11-01 18:40:32,553 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1056] L1017-4-->L1018-1: Formula: (= |v_#race~data~0_104| 0)  InVars {}  OutVars{threadThread1of3ForFork0_#t~nondet3=|v_threadThread1of3ForFork0_#t~nondet3_15|, #race~data~0=|v_#race~data~0_104|}  AuxVars[]  AssignedVars[threadThread1of3ForFork0_#t~nondet3, #race~data~0][45], [Black: 203#true, 194#true, Black: 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 46#L1017-4true, 184#L1034-5true, threadThread1of3ForFork0InUse, 127#L1018-1true, 209#true, 217#(= ~data~0 1), threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:32,553 INFO  L383   tUnfolder$Statistics]: this new event has 42 ancestors and is cut-off event
[2023-11-01 18:40:32,553 INFO  L386   tUnfolder$Statistics]:   existing Event has 17 ancestors and is cut-off event
[2023-11-01 18:40:32,553 INFO  L386   tUnfolder$Statistics]:   existing Event has 17 ancestors and is cut-off event
[2023-11-01 18:40:32,553 INFO  L386   tUnfolder$Statistics]:   existing Event has 42 ancestors and is cut-off event
[2023-11-01 18:40:32,780 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1036] L1017-4-->L1018-1: Formula: (= |v_#race~data~0_102| 0)  InVars {}  OutVars{threadThread2of3ForFork0_#t~nondet3=|v_threadThread2of3ForFork0_#t~nondet3_15|, #race~data~0=|v_#race~data~0_102|}  AuxVars[]  AssignedVars[threadThread2of3ForFork0_#t~nondet3, #race~data~0][46], [Black: 203#true, 17#L1018-1true, 194#true, 2#ULTIMATE.startEXITtrue, Black: 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 91#L1017-4true, threadThread1of3ForFork0InUse, 209#true, threadThread2of3ForFork0InUse, 217#(= ~data~0 1), threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:32,781 INFO  L383   tUnfolder$Statistics]: this new event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,781 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,781 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,781 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,781 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1056] L1017-4-->L1018-1: Formula: (= |v_#race~data~0_104| 0)  InVars {}  OutVars{threadThread1of3ForFork0_#t~nondet3=|v_threadThread1of3ForFork0_#t~nondet3_15|, #race~data~0=|v_#race~data~0_104|}  AuxVars[]  AssignedVars[threadThread1of3ForFork0_#t~nondet3, #race~data~0][45], [Black: 203#true, 194#true, Black: 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), 2#ULTIMATE.startEXITtrue, Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 46#L1017-4true, 127#L1018-1true, threadThread1of3ForFork0InUse, 217#(= ~data~0 1), 209#true, threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:32,781 INFO  L383   tUnfolder$Statistics]: this new event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,781 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,782 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,782 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,783 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1036] L1017-4-->L1018-1: Formula: (= |v_#race~data~0_102| 0)  InVars {}  OutVars{threadThread2of3ForFork0_#t~nondet3=|v_threadThread2of3ForFork0_#t~nondet3_15|, #race~data~0=|v_#race~data~0_102|}  AuxVars[]  AssignedVars[threadThread2of3ForFork0_#t~nondet3, #race~data~0][46], [Black: 203#true, 17#L1018-1true, 194#true, Black: 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), 31#L1035-12true, Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 91#L1017-4true, threadThread1of3ForFork0InUse, 209#true, 217#(= ~data~0 1), threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:32,783 INFO  L383   tUnfolder$Statistics]: this new event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,783 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,783 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,783 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,784 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([1056] L1017-4-->L1018-1: Formula: (= |v_#race~data~0_104| 0)  InVars {}  OutVars{threadThread1of3ForFork0_#t~nondet3=|v_threadThread1of3ForFork0_#t~nondet3_15|, #race~data~0=|v_#race~data~0_104|}  AuxVars[]  AssignedVars[threadThread1of3ForFork0_#t~nondet3, #race~data~0][45], [Black: 203#true, 194#true, Black: 211#(= |threadThread2of3ForFork0_#t~nondet3| |#race~data~0|), 31#L1035-12true, Black: 199#(= |#race~data~0| |threadThread1of3ForFork0_#t~nondet3|), 46#L1017-4true, 127#L1018-1true, threadThread1of3ForFork0InUse, 209#true, 217#(= ~data~0 1), threadThread2of3ForFork0InUse, threadThread3of3ForFork0NotInUse])
[2023-11-01 18:40:32,784 INFO  L383   tUnfolder$Statistics]: this new event has 43 ancestors and is cut-off event
[2023-11-01 18:40:32,784 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,784 INFO  L386   tUnfolder$Statistics]:   existing Event has 18 ancestors and is cut-off event
[2023-11-01 18:40:32,784 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2023-11-01 18:40:35,988 INFO  L130       PetriNetUnfolder]: 63887/112838 cut-off events.
[2023-11-01 18:40:35,988 INFO  L131       PetriNetUnfolder]: For 176458/201381 co-relation queries the response was YES.
[2023-11-01 18:40:36,284 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 306730 conditions, 112838 events. 63887/112838 cut-off events. For 176458/201381 co-relation queries the response was YES. Maximal size of possible extension queue 2852. Compared 1111971 event pairs, 23151 based on Foata normal form. 6863/101988 useless extension candidates. Maximal degree in co-relation 306720. Up to 86185 conditions per place. 
[2023-11-01 18:40:36,729 INFO  L137   encePairwiseOnDemand]: 311/320 looper letters, 86 selfloop transitions, 3 changer transitions 0/144 dead transitions.
[2023-11-01 18:40:36,730 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 97 places, 144 transitions, 908 flow
[2023-11-01 18:40:36,730 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-11-01 18:40:36,730 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-11-01 18:40:36,731 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 570 transitions.
[2023-11-01 18:40:36,731 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.59375
[2023-11-01 18:40:36,732 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 570 transitions.
[2023-11-01 18:40:36,732 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 570 transitions.
[2023-11-01 18:40:36,732 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-11-01 18:40:36,732 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 570 transitions.
[2023-11-01 18:40:36,733 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 190.0) internal successors, (570), 3 states have internal predecessors, (570), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:36,734 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:36,734 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 320.0) internal successors, (1280), 4 states have internal predecessors, (1280), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:36,734 INFO  L175             Difference]: Start difference. First operand has 97 places, 142 transitions, 714 flow. Second operand 3 states and 570 transitions.
[2023-11-01 18:40:36,734 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 97 places, 144 transitions, 908 flow
[2023-11-01 18:40:36,859 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 95 places, 144 transitions, 854 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-11-01 18:40:36,860 INFO  L231             Difference]: Finished difference. Result has 96 places, 137 transitions, 665 flow
[2023-11-01 18:40:36,861 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=320, PETRI_DIFFERENCE_MINUEND_FLOW=644, PETRI_DIFFERENCE_MINUEND_PLACES=93, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=134, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=131, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=665, PETRI_PLACES=96, PETRI_TRANSITIONS=137}
[2023-11-01 18:40:36,861 INFO  L288   CegarLoopForPetriNet]: 92 programPoint places, 4 predicate places.
[2023-11-01 18:40:36,861 INFO  L495      AbstractCegarLoop]: Abstraction has has 96 places, 137 transitions, 665 flow
[2023-11-01 18:40:36,862 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 173.0) internal successors, (519), 3 states have internal predecessors, (519), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-11-01 18:40:36,862 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-11-01 18:40:36,862 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:36,862 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2023-11-01 18:40:36,862 INFO  L420      AbstractCegarLoop]: === Iteration 6 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 22 more)] ===
[2023-11-01 18:40:36,862 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-11-01 18:40:36,862 INFO  L85        PathProgramCache]: Analyzing trace with hash 1831620773, now seen corresponding path program 1 times
[2023-11-01 18:40:36,862 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-11-01 18:40:36,863 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1623713857]
[2023-11-01 18:40:36,863 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-11-01 18:40:36,863 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-11-01 18:40:36,878 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-11-01 18:40:36,878 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-11-01 18:40:36,886 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-11-01 18:40:36,890 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-11-01 18:40:36,890 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-11-01 18:40:36,890 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location threadErr0ASSERT_VIOLATIONDATA_RACE (24 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (23 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (22 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (21 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (20 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (19 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (18 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (17 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (16 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (15 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (14 of 25 remaining)
[2023-11-01 18:40:36,891 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (13 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (12 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (11 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (10 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (9 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (8 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (7 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (6 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (5 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (4 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (3 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (2 of 25 remaining)
[2023-11-01 18:40:36,892 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (1 of 25 remaining)
[2023-11-01 18:40:36,893 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr4ASSERT_VIOLATIONDATA_RACE (0 of 25 remaining)
[2023-11-01 18:40:36,893 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2023-11-01 18:40:36,893 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1]
[2023-11-01 18:40:36,897 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 3 thread instances
[2023-11-01 18:40:36,897 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2023-11-01 18:40:36,920 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 01.11 06:40:36 BasicIcfg
[2023-11-01 18:40:36,921 INFO  L132        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2023-11-01 18:40:36,921 INFO  L113        PluginConnector]: ------------------------Witness Printer----------------------------
[2023-11-01 18:40:36,921 INFO  L271        PluginConnector]: Initializing Witness Printer...
[2023-11-01 18:40:36,921 INFO  L275        PluginConnector]: Witness Printer initialized
[2023-11-01 18:40:36,922 INFO  L185        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 01.11 06:39:55" (3/4) ...
[2023-11-01 18:40:36,924 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2023-11-01 18:40:36,924 INFO  L132        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2023-11-01 18:40:36,924 INFO  L158              Benchmark]: Toolchain (without parser) took 42796.79ms. Allocated memory was 188.7MB in the beginning and 5.0GB in the end (delta: 4.8GB). Free memory was 151.8MB in the beginning and 1.6GB in the end (delta: -1.5GB). Peak memory consumption was 3.3GB. Max. memory is 16.1GB.
[2023-11-01 18:40:36,924 INFO  L158              Benchmark]: CDTParser took 0.11ms. Allocated memory is still 188.7MB. Free memory was 159.3MB in the beginning and 159.2MB in the end (delta: 156.2kB). There was no memory consumed. Max. memory is 16.1GB.
[2023-11-01 18:40:36,924 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 386.92ms. Allocated memory is still 188.7MB. Free memory was 151.2MB in the beginning and 123.3MB in the end (delta: 27.9MB). Peak memory consumption was 27.3MB. Max. memory is 16.1GB.
[2023-11-01 18:40:36,925 INFO  L158              Benchmark]: Boogie Procedure Inliner took 40.09ms. Allocated memory is still 188.7MB. Free memory was 123.3MB in the beginning and 120.6MB in the end (delta: 2.7MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2023-11-01 18:40:36,925 INFO  L158              Benchmark]: Boogie Preprocessor took 32.36ms. Allocated memory is still 188.7MB. Free memory was 120.6MB in the beginning and 119.1MB in the end (delta: 1.4MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2023-11-01 18:40:36,925 INFO  L158              Benchmark]: RCFGBuilder took 428.30ms. Allocated memory is still 188.7MB. Free memory was 118.5MB in the beginning and 101.7MB in the end (delta: 16.8MB). Peak memory consumption was 16.8MB. Max. memory is 16.1GB.
[2023-11-01 18:40:36,926 INFO  L158              Benchmark]: TraceAbstraction took 41901.31ms. Allocated memory was 188.7MB in the beginning and 5.0GB in the end (delta: 4.8GB). Free memory was 100.8MB in the beginning and 1.6GB in the end (delta: -1.5GB). Peak memory consumption was 3.2GB. Max. memory is 16.1GB.
[2023-11-01 18:40:36,926 INFO  L158              Benchmark]: Witness Printer took 2.71ms. Allocated memory is still 5.0GB. Free memory is still 1.6GB. There was no memory consumed. Max. memory is 16.1GB.
[2023-11-01 18:40:36,927 INFO  L339   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.11ms. Allocated memory is still 188.7MB. Free memory was 159.3MB in the beginning and 159.2MB in the end (delta: 156.2kB). There was no memory consumed. Max. memory is 16.1GB.
 * CACSL2BoogieTranslator took 386.92ms. Allocated memory is still 188.7MB. Free memory was 151.2MB in the beginning and 123.3MB in the end (delta: 27.9MB). Peak memory consumption was 27.3MB. Max. memory is 16.1GB.
 * Boogie Procedure Inliner took 40.09ms. Allocated memory is still 188.7MB. Free memory was 123.3MB in the beginning and 120.6MB in the end (delta: 2.7MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * Boogie Preprocessor took 32.36ms. Allocated memory is still 188.7MB. Free memory was 120.6MB in the beginning and 119.1MB in the end (delta: 1.4MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * RCFGBuilder took 428.30ms. Allocated memory is still 188.7MB. Free memory was 118.5MB in the beginning and 101.7MB in the end (delta: 16.8MB). Peak memory consumption was 16.8MB. Max. memory is 16.1GB.
 * TraceAbstraction took 41901.31ms. Allocated memory was 188.7MB in the beginning and 5.0GB in the end (delta: 4.8GB). Free memory was 100.8MB in the beginning and 1.6GB in the end (delta: -1.5GB). Peak memory consumption was 3.2GB. Max. memory is 16.1GB.
 * Witness Printer took 2.71ms. Allocated memory is still 5.0GB. Free memory is still 1.6GB. There was no memory consumed. Max. memory is 16.1GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 4.8s, 123 PlacesBefore, 22 PlacesAfterwards, 126 TransitionsBefore, 20 TransitionsAfterwards, 3498 CoEnabledTransitionPairs, 7 FixpointIterations, 35 TrivialSequentialCompositions, 95 ConcurrentSequentialCompositions, 5 TrivialYvCompositions, 9 ConcurrentYvCompositions, 5 ChoiceCompositions, 149 TotalNumberOfCompositions, 3353 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 3353, independent: 3353, independent conditional: 0, independent unconditional: 3353, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 1929, independent: 1929, independent conditional: 0, independent unconditional: 1929, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 3353, independent: 1424, independent conditional: 0, independent unconditional: 1424, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 1929, unknown conditional: 0, unknown unconditional: 1929] , Statistics on independence cache: Total cache size (in pairs): 20, Positive cache size: 20, Positive conditional cache size: 0, Positive unconditional cache size: 20, Negative cache size: 0, Negative conditional cache size: 0, Negative unconditional cache size: 0, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 4.6s, 157 PlacesBefore, 65 PlacesAfterwards, 161 TransitionsBefore, 66 TransitionsAfterwards, 10032 CoEnabledTransitionPairs, 7 FixpointIterations, 32 TrivialSequentialCompositions, 67 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 12 ConcurrentYvCompositions, 3 ChoiceCompositions, 117 TotalNumberOfCompositions, 40957 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 18893, independent: 18214, independent conditional: 0, independent unconditional: 18214, dependent: 679, dependent conditional: 0, dependent unconditional: 679, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 5175, independent: 5097, independent conditional: 0, independent unconditional: 5097, dependent: 78, dependent conditional: 0, dependent unconditional: 78, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 18893, independent: 13117, independent conditional: 0, independent unconditional: 13117, dependent: 601, dependent conditional: 0, dependent unconditional: 601, unknown: 5175, unknown conditional: 0, unknown unconditional: 5175] , Statistics on independence cache: Total cache size (in pairs): 834, Positive cache size: 793, Positive conditional cache size: 0, Positive unconditional cache size: 793, Negative cache size: 41, Negative conditional cache size: 0, Negative unconditional cache size: 41, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 4.2s, 191 PlacesBefore, 92 PlacesAfterwards, 196 TransitionsBefore, 94 TransitionsAfterwards, 18612 CoEnabledTransitionPairs, 6 FixpointIterations, 32 TrivialSequentialCompositions, 68 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 18 ConcurrentYvCompositions, 3 ChoiceCompositions, 124 TotalNumberOfCompositions, 81653 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 25285, independent: 24418, independent conditional: 0, independent unconditional: 24418, dependent: 867, dependent conditional: 0, dependent unconditional: 867, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 8620, independent: 8494, independent conditional: 0, independent unconditional: 8494, dependent: 126, dependent conditional: 0, dependent unconditional: 126, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 25285, independent: 15924, independent conditional: 0, independent unconditional: 15924, dependent: 741, dependent conditional: 0, dependent unconditional: 741, unknown: 8620, unknown conditional: 0, unknown unconditional: 8620] , Statistics on independence cache: Total cache size (in pairs): 1223, Positive cache size: 1149, Positive conditional cache size: 0, Positive unconditional cache size: 1149, Negative cache size: 74, Negative conditional cache size: 0, Negative unconditional cache size: 74, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - DataRaceFoundResult [Line: 1017]: Data race detected
    Data race detected
The following path leads to a data race: 
[L1013]               0  int data = 0;
[L1014]               0  int shared = 0;
[L1015]               0  pthread_mutex_t shared_mutex = { { 0, 0, 0, PTHREAD_MUTEX_TIMED_NP, 0, { { 0, 0 } } } };
[L1028]               0  int threads_total = __VERIFIER_nondet_int();
[L1029]  CALL         0  assume_abort_if_not(threads_total >= 0)
[L1010]  COND FALSE   0  !(!cond)
[L1029]  RET          0  assume_abort_if_not(threads_total >= 0)
[L1030]               0  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
[L1030]               0  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
[L1031]               0  int i = 0;
         VAL             [data=0, i=0, shared=0, shared_mutex={1:0}, threads_total=5, tids={5:0}]
[L1031]  COND TRUE    0  i < threads_total
[L1032]  EXPR         0  \read(*tids)
[L1032]  EXPR         0  tids[i]
[L1032]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [\read(*tids)={-2:0}, arg={0:0}, data=0, i=0, pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))=-1, shared=0, shared_mutex={1:0}, threads_total=5, tids={5:0}]
[L1031]               0  i++
         VAL             [arg={0:0}, data=0, i=1, shared=0, shared_mutex={1:0}, threads_total=5, tids={5:0}]
[L1031]  COND TRUE    0  i < threads_total
[L1032]  EXPR         0  \read(*tids)
[L1032]  EXPR         0  tids[i]
[L1032]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [\read(*tids)={-2:0}, arg={0:0}, data=0, i=1, pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))=0, shared=0, shared_mutex={1:0}, threads_total=5, tids={5:0}]
[L1017]               1  data = 1
         VAL             [arg={0:0}, arg={0:0}, data=1, data = 1=25, shared=0, shared_mutex={1:0}]
[L1017]               2  data = 1
         VAL             [arg={0:0}, arg={0:0}, data=1, data = 1=26, shared=0, shared_mutex={1:0}]

Now there is a data race, but we were unable to determine exactly which statements and variables are involved. There could be a race between one of the statements
	* C: tids[i] [1032]
	* C: tids[i] [1032]
	* C: tids[i] [1032]
	* C: tids[i] [1032]
and
	C: data = 1 [1017]

  - 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: 1035]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1037]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1035]: 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 petrification did provide enough thread instances (tool internal message, not intended for end users)
    Unable to prove that petrification did provide enough thread instances (tool internal message, not intended for end users)
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1018]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1021]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1021]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1022]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - StatisticsResult: Ultimate Automizer benchmark data with 1 thread instances
    CFG has 3 procedures, 153 locations, 15 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 5.3s, OverallIterations: 2, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 4.9s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 0 SdHoareTripleChecker+Valid, 0.0s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 0 mSDsluCounter, 0 SdHoareTripleChecker+Invalid, 0.0s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 10 IncrementalHoareTripleChecker+Invalid, 10 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 0 mSDtfsCounter, 10 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 1 GetRequests, 1 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=48occurred in iteration=0, InterpolantAutomatonStates: 2, 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.0s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 8 NumberOfCodeBlocks, 8 NumberOfCodeBlocksAsserted, 2 NumberOfCheckSat, 1 ConstructedInterpolants, 0 QuantifiedInterpolants, 1 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 1 InterpolantComputations, 1 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, 185 locations, 20 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 6.3s, OverallIterations: 5, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.4s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 4.6s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 176 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 88 mSDsluCounter, 10 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 26 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 320 IncrementalHoareTripleChecker+Invalid, 346 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 26 mSolverCounterUnsat, 10 mSDtfsCounter, 320 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=312occurred in iteration=4, InterpolantAutomatonStates: 11, 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.0s SatisfiabilityAnalysisTime, 0.1s InterpolantComputationTime, 37 NumberOfCodeBlocks, 37 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 22 ConstructedInterpolants, 0 QuantifiedInterpolants, 28 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 4 InterpolantComputations, 4 PerfectInterpolantSequences, 2/2 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 3 thread instances
    CFG has 5 procedures, 217 locations, 25 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: 30.2s, OverallIterations: 6, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 25.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 4.2s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 280 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 161 mSDsluCounter, 30 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 60 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 523 IncrementalHoareTripleChecker+Invalid, 583 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 60 mSolverCounterUnsat, 30 mSDtfsCounter, 523 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 10 GetRequests, 6 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=714occurred in iteration=4, InterpolantAutomatonStates: 14, 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.0s SatisfiabilityAnalysisTime, 0.1s InterpolantComputationTime, 49 NumberOfCodeBlocks, 49 NumberOfCodeBlocksAsserted, 6 NumberOfCheckSat, 32 ConstructedInterpolants, 0 QuantifiedInterpolants, 48 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 5 InterpolantComputations, 5 PerfectInterpolantSequences, 2/2 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2023-11-01 18:40:36,964 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...
--- End real Ultimate output ---

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