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


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


Checking for data races
Using default analysis
Version 2329fc70
Calling Ultimate with: /usr/lib/jvm/java-11-openjdk-amd64/bin/java -Dosgi.configuration.area=/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data -tc /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/AutomizerReach.xml -i /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race.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 55806f013f90e7fc2dfd81c7759c593947a98a3fbf4b7b5de0859bd2c1ce6228
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2024-03-11 23:19:21,210 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2024-03-11 23:19:21,211 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2024-03-11 23:19:21,235 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2024-03-11 23:19:21,235 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2024-03-11 23:19:21,236 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2024-03-11 23:19:21,237 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2024-03-11 23:19:21,238 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2024-03-11 23:19:21,239 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2024-03-11 23:19:21,240 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2024-03-11 23:19:21,240 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2024-03-11 23:19:21,241 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2024-03-11 23:19:21,241 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2024-03-11 23:19:21,242 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2024-03-11 23:19:21,243 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2024-03-11 23:19:21,244 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2024-03-11 23:19:21,244 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2024-03-11 23:19:21,245 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2024-03-11 23:19:21,246 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2024-03-11 23:19:21,247 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2024-03-11 23:19:21,248 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2024-03-11 23:19:21,249 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2024-03-11 23:19:21,250 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2024-03-11 23:19:21,250 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2024-03-11 23:19:21,253 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2024-03-11 23:19:21,253 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2024-03-11 23:19:21,253 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2024-03-11 23:19:21,254 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2024-03-11 23:19:21,254 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2024-03-11 23:19:21,254 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2024-03-11 23:19:21,255 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2024-03-11 23:19:21,255 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2024-03-11 23:19:21,256 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2024-03-11 23:19:21,256 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2024-03-11 23:19:21,257 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2024-03-11 23:19:21,257 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2024-03-11 23:19:21,257 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2024-03-11 23:19:21,258 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2024-03-11 23:19:21,258 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2024-03-11 23:19:21,258 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2024-03-11 23:19:21,259 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2024-03-11 23:19:21,260 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2024-03-11 23:19:21,274 INFO  L113        SettingsManager]: Loading preferences was successful
[2024-03-11 23:19:21,274 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2024-03-11 23:19:21,275 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2024-03-11 23:19:21,275 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2024-03-11 23:19:21,275 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2024-03-11 23:19:21,275 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2024-03-11 23:19:21,276 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2024-03-11 23:19:21,276 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2024-03-11 23:19:21,276 INFO  L138        SettingsManager]:  * Use SBE=true
[2024-03-11 23:19:21,276 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2024-03-11 23:19:21,276 INFO  L138        SettingsManager]:  * sizeof long=4
[2024-03-11 23:19:21,276 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * sizeof long double=12
[2024-03-11 23:19:21,277 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2024-03-11 23:19:21,278 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2024-03-11 23:19:21,278 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2024-03-11 23:19:21,278 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2024-03-11 23:19:21,278 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2024-03-11 23:19:21,278 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2024-03-11 23:19:21,278 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2024-03-11 23:19:21,278 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2024-03-11 23:19:21,278 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2024-03-11 23:19:21,279 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2024-03-11 23:19:21,280 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 -> 55806f013f90e7fc2dfd81c7759c593947a98a3fbf4b7b5de0859bd2c1ce6228
[2024-03-11 23:19:21,448 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2024-03-11 23:19:21,475 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2024-03-11 23:19:21,477 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2024-03-11 23:19:21,478 INFO  L271        PluginConnector]: Initializing CDTParser...
[2024-03-11 23:19:21,479 INFO  L275        PluginConnector]: CDTParser initialized
[2024-03-11 23:19:21,480 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race.i
[2024-03-11 23:19:22,475 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2024-03-11 23:19:22,724 INFO  L351              CDTParser]: Found 1 translation units.
[2024-03-11 23:19:22,724 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race.i
[2024-03-11 23:19:22,732 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/11dab86da/8b071f8fdd384f4cafcd44d97ec6d849/FLAG40753d39b
[2024-03-11 23:19:22,742 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/11dab86da/8b071f8fdd384f4cafcd44d97ec6d849
[2024-03-11 23:19:22,744 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2024-03-11 23:19:22,745 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2024-03-11 23:19:22,746 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2024-03-11 23:19:22,746 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2024-03-11 23:19:22,749 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2024-03-11 23:19:22,749 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 11.03 11:19:22" (1/1) ...
[2024-03-11 23:19:22,750 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@47ec560b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:22, skipping insertion in model container
[2024-03-11 23:19:22,750 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 11.03 11:19:22" (1/1) ...
[2024-03-11 23:19:22,755 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2024-03-11 23:19:22,785 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2024-03-11 23:19:22,982 WARN  L623        FunctionHandler]: Unknown extern function pthread_detach
[2024-03-11 23:19:22,984 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2024-03-11 23:19:22,993 INFO  L203         MainTranslator]: Completed pre-run
[2024-03-11 23:19:23,018 WARN  L623        FunctionHandler]: Unknown extern function pthread_detach
[2024-03-11 23:19:23,020 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2024-03-11 23:19:23,043 INFO  L208         MainTranslator]: Completed translation
[2024-03-11 23:19:23,044 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23 WrapperNode
[2024-03-11 23:19:23,044 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2024-03-11 23:19:23,045 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2024-03-11 23:19:23,045 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2024-03-11 23:19:23,045 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2024-03-11 23:19:23,050 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,059 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,075 INFO  L138                Inliner]: procedures = 159, calls = 16, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 67
[2024-03-11 23:19:23,076 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2024-03-11 23:19:23,076 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2024-03-11 23:19:23,076 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2024-03-11 23:19:23,076 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2024-03-11 23:19:23,083 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,083 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,086 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,086 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,090 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,092 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,093 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,094 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,097 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2024-03-11 23:19:23,097 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2024-03-11 23:19:23,097 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2024-03-11 23:19:23,098 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2024-03-11 23:19:23,098 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (1/1) ...
[2024-03-11 23:19:23,103 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2024-03-11 23:19:23,110 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2024-03-11 23:19:23,120 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)
[2024-03-11 23:19:23,126 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
[2024-03-11 23:19:23,154 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2024-03-11 23:19:23,154 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2024-03-11 23:19:23,154 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexLock
[2024-03-11 23:19:23,154 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2024-03-11 23:19:23,155 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2024-03-11 23:19:23,155 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2024-03-11 23:19:23,155 INFO  L130     BoogieDeclarations]: Found specification of procedure pthread_detach
[2024-03-11 23:19:23,155 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2024-03-11 23:19:23,155 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2024-03-11 23:19:23,155 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2024-03-11 23:19:23,155 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2024-03-11 23:19:23,155 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2024-03-11 23:19:23,157 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2024-03-11 23:19:23,293 INFO  L235             CfgBuilder]: Building ICFG
[2024-03-11 23:19:23,294 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2024-03-11 23:19:23,450 INFO  L276             CfgBuilder]: Performing block encoding
[2024-03-11 23:19:23,456 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2024-03-11 23:19:23,456 INFO  L300             CfgBuilder]: Removed 2 assume(true) statements.
[2024-03-11 23:19:23,458 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 11.03 11:19:23 BoogieIcfgContainer
[2024-03-11 23:19:23,459 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2024-03-11 23:19:23,460 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2024-03-11 23:19:23,460 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2024-03-11 23:19:23,463 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2024-03-11 23:19:23,463 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 11.03 11:19:22" (1/3) ...
[2024-03-11 23:19:23,463 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1da64ff3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 11.03 11:19:23, skipping insertion in model container
[2024-03-11 23:19:23,464 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:19:23" (2/3) ...
[2024-03-11 23:19:23,464 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1da64ff3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 11.03 11:19:23, skipping insertion in model container
[2024-03-11 23:19:23,464 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 11.03 11:19:23" (3/3) ...
[2024-03-11 23:19:23,465 INFO  L112   eAbstractionObserver]: Analyzing ICFG thread-join-counter-outer-race.i
[2024-03-11 23:19:23,471 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2024-03-11 23:19:23,479 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2024-03-11 23:19:23,479 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 8 error locations.
[2024-03-11 23:19:23,479 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2024-03-11 23:19:23,519 INFO  L144    ThreadInstanceAdder]: Constructed 0 joinOtherThreadTransitions.
[2024-03-11 23:19:23,547 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 104 places, 105 transitions, 215 flow
[2024-03-11 23:19:23,590 INFO  L130       PetriNetUnfolder]: 7/136 cut-off events.
[2024-03-11 23:19:23,590 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:19:23,594 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 141 conditions, 136 events. 7/136 cut-off events. For 0/0 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 164 event pairs, 0 based on Foata normal form. 0/115 useless extension candidates. Maximal degree in co-relation 74. Up to 6 conditions per place. 
[2024-03-11 23:19:23,595 INFO  L82        GeneralOperation]: Start removeDead. Operand has 104 places, 105 transitions, 215 flow
[2024-03-11 23:19:23,598 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 104 places, 105 transitions, 215 flow
[2024-03-11 23:19:23,601 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-03-11 23:19:23,616 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 104 places, 105 transitions, 215 flow
[2024-03-11 23:19:23,618 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 104 places, 105 transitions, 215 flow
[2024-03-11 23:19:23,618 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 104 places, 105 transitions, 215 flow
[2024-03-11 23:19:23,641 INFO  L130       PetriNetUnfolder]: 7/136 cut-off events.
[2024-03-11 23:19:23,641 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:19:23,642 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 141 conditions, 136 events. 7/136 cut-off events. For 0/0 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 164 event pairs, 0 based on Foata normal form. 0/115 useless extension candidates. Maximal degree in co-relation 74. Up to 6 conditions per place. 
[2024-03-11 23:19:23,643 INFO  L119        LiptonReduction]: Number of co-enabled transitions 2500
[2024-03-11 23:19:25,122 INFO  L134        LiptonReduction]: Checked pairs total: 7962
[2024-03-11 23:19:25,122 INFO  L136        LiptonReduction]: Total number of compositions: 78
[2024-03-11 23:19:25,134 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-11 23:19:25,140 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;@57764ce0, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-03-11 23:19:25,140 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 12 error locations.
[2024-03-11 23:19:25,142 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2024-03-11 23:19:25,142 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:19:25,142 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:25,142 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1]
[2024-03-11 23:19:25,143 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2024-03-11 23:19:25,146 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:25,147 INFO  L85        PathProgramCache]: Analyzing trace with hash 360721, now seen corresponding path program 1 times
[2024-03-11 23:19:25,153 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:25,154 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1058235167]
[2024-03-11 23:19:25,154 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:25,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:25,226 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:25,287 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:25,287 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:25,288 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1058235167]
[2024-03-11 23:19:25,288 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1058235167] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:25,288 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:25,289 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:25,290 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [932611321]
[2024-03-11 23:19:25,290 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:25,296 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:25,297 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:25,313 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:25,314 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:25,335 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 90 out of 183
[2024-03-11 23:19:25,337 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 37 places, 36 transitions, 77 flow. Second operand  has 3 states, 3 states have (on average 91.0) internal successors, (273), 3 states have internal predecessors, (273), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,337 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:25,337 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 90 of 183
[2024-03-11 23:19:25,338 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:25,396 INFO  L130       PetriNetUnfolder]: 72/260 cut-off events.
[2024-03-11 23:19:25,397 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:19:25,397 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 439 conditions, 260 events. 72/260 cut-off events. For 0/0 co-relation queries the response was YES. Maximal size of possible extension queue 23. Compared 1241 event pairs, 25 based on Foata normal form. 0/231 useless extension candidates. Maximal degree in co-relation 398. Up to 97 conditions per place. 
[2024-03-11 23:19:25,399 INFO  L137   encePairwiseOnDemand]: 170/183 looper letters, 27 selfloop transitions, 8 changer transitions 0/49 dead transitions.
[2024-03-11 23:19:25,400 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 38 places, 49 transitions, 173 flow
[2024-03-11 23:19:25,401 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:25,403 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:25,409 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 312 transitions.
[2024-03-11 23:19:25,411 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5683060109289617
[2024-03-11 23:19:25,412 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 312 transitions.
[2024-03-11 23:19:25,412 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 312 transitions.
[2024-03-11 23:19:25,413 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:25,415 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 312 transitions.
[2024-03-11 23:19:25,418 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 104.0) internal successors, (312), 3 states have internal predecessors, (312), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,422 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,423 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,425 INFO  L175             Difference]: Start difference. First operand has 37 places, 36 transitions, 77 flow. Second operand 3 states and 312 transitions.
[2024-03-11 23:19:25,426 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 38 places, 49 transitions, 173 flow
[2024-03-11 23:19:25,428 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 38 places, 49 transitions, 173 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:19:25,429 INFO  L231             Difference]: Finished difference. Result has 40 places, 42 transitions, 143 flow
[2024-03-11 23:19:25,431 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=183, PETRI_DIFFERENCE_MINUEND_FLOW=73, PETRI_DIFFERENCE_MINUEND_PLACES=36, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=34, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=26, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=143, PETRI_PLACES=40, PETRI_TRANSITIONS=42}
[2024-03-11 23:19:25,434 INFO  L288   CegarLoopForPetriNet]: 37 programPoint places, 3 predicate places.
[2024-03-11 23:19:25,434 INFO  L495      AbstractCegarLoop]: Abstraction has has 40 places, 42 transitions, 143 flow
[2024-03-11 23:19:25,434 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 91.0) internal successors, (273), 3 states have internal predecessors, (273), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,434 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:25,435 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:25,435 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2024-03-11 23:19:25,435 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2024-03-11 23:19:25,436 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:25,436 INFO  L85        PathProgramCache]: Analyzing trace with hash -1868668675, now seen corresponding path program 1 times
[2024-03-11 23:19:25,436 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:25,437 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1842270463]
[2024-03-11 23:19:25,437 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:25,437 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:25,448 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:25,471 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:25,472 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:25,472 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1842270463]
[2024-03-11 23:19:25,472 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1842270463] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:25,472 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:25,472 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:25,473 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1099592041]
[2024-03-11 23:19:25,473 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:25,474 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:25,474 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:25,475 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:25,475 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:25,500 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 91 out of 183
[2024-03-11 23:19:25,501 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 40 places, 42 transitions, 143 flow. Second operand  has 3 states, 3 states have (on average 92.33333333333333) internal successors, (277), 3 states have internal predecessors, (277), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,501 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:25,501 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 91 of 183
[2024-03-11 23:19:25,501 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:25,542 INFO  L130       PetriNetUnfolder]: 57/229 cut-off events.
[2024-03-11 23:19:25,542 INFO  L131       PetriNetUnfolder]: For 100/102 co-relation queries the response was YES.
[2024-03-11 23:19:25,543 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 489 conditions, 229 events. 57/229 cut-off events. For 100/102 co-relation queries the response was YES. Maximal size of possible extension queue 24. Compared 1086 event pairs, 31 based on Foata normal form. 0/207 useless extension candidates. Maximal degree in co-relation 440. Up to 114 conditions per place. 
[2024-03-11 23:19:25,544 INFO  L137   encePairwiseOnDemand]: 178/183 looper letters, 21 selfloop transitions, 6 changer transitions 0/49 dead transitions.
[2024-03-11 23:19:25,545 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 42 places, 49 transitions, 221 flow
[2024-03-11 23:19:25,545 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:25,545 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:25,547 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 295 transitions.
[2024-03-11 23:19:25,547 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5373406193078324
[2024-03-11 23:19:25,547 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 295 transitions.
[2024-03-11 23:19:25,548 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 295 transitions.
[2024-03-11 23:19:25,548 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:25,548 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 295 transitions.
[2024-03-11 23:19:25,549 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 98.33333333333333) internal successors, (295), 3 states have internal predecessors, (295), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,551 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,551 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,551 INFO  L175             Difference]: Start difference. First operand has 40 places, 42 transitions, 143 flow. Second operand 3 states and 295 transitions.
[2024-03-11 23:19:25,551 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 42 places, 49 transitions, 221 flow
[2024-03-11 23:19:25,553 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 40 places, 49 transitions, 201 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:19:25,554 INFO  L231             Difference]: Finished difference. Result has 41 places, 46 transitions, 169 flow
[2024-03-11 23:19:25,554 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=183, PETRI_DIFFERENCE_MINUEND_FLOW=127, PETRI_DIFFERENCE_MINUEND_PLACES=38, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=42, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=36, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=169, PETRI_PLACES=41, PETRI_TRANSITIONS=46}
[2024-03-11 23:19:25,555 INFO  L288   CegarLoopForPetriNet]: 37 programPoint places, 4 predicate places.
[2024-03-11 23:19:25,555 INFO  L495      AbstractCegarLoop]: Abstraction has has 41 places, 46 transitions, 169 flow
[2024-03-11 23:19:25,555 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 92.33333333333333) internal successors, (277), 3 states have internal predecessors, (277), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,556 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:25,556 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:25,556 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2024-03-11 23:19:25,556 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2024-03-11 23:19:25,557 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:25,557 INFO  L85        PathProgramCache]: Analyzing trace with hash -1597045873, now seen corresponding path program 1 times
[2024-03-11 23:19:25,557 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:25,557 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1856041416]
[2024-03-11 23:19:25,558 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:25,558 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:25,567 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:25,588 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:25,588 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:25,588 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1856041416]
[2024-03-11 23:19:25,589 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1856041416] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:25,589 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:25,589 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:25,589 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [409564225]
[2024-03-11 23:19:25,589 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:25,590 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:25,590 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:25,590 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:25,590 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:25,597 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 97 out of 183
[2024-03-11 23:19:25,598 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 41 places, 46 transitions, 169 flow. Second operand  has 3 states, 3 states have (on average 98.33333333333333) internal successors, (295), 3 states have internal predecessors, (295), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,598 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:25,598 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 97 of 183
[2024-03-11 23:19:25,598 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:25,647 INFO  L130       PetriNetUnfolder]: 81/287 cut-off events.
[2024-03-11 23:19:25,648 INFO  L131       PetriNetUnfolder]: For 143/147 co-relation queries the response was YES.
[2024-03-11 23:19:25,649 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 637 conditions, 287 events. 81/287 cut-off events. For 143/147 co-relation queries the response was YES. Maximal size of possible extension queue 27. Compared 1469 event pairs, 33 based on Foata normal form. 0/263 useless extension candidates. Maximal degree in co-relation 588. Up to 131 conditions per place. 
[2024-03-11 23:19:25,650 INFO  L137   encePairwiseOnDemand]: 179/183 looper letters, 29 selfloop transitions, 3 changer transitions 1/54 dead transitions.
[2024-03-11 23:19:25,650 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 43 places, 54 transitions, 257 flow
[2024-03-11 23:19:25,650 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:25,650 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:25,651 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 317 transitions.
[2024-03-11 23:19:25,652 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5774134790528234
[2024-03-11 23:19:25,652 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 317 transitions.
[2024-03-11 23:19:25,652 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 317 transitions.
[2024-03-11 23:19:25,652 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:25,652 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 317 transitions.
[2024-03-11 23:19:25,653 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 105.66666666666667) internal successors, (317), 3 states have internal predecessors, (317), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,655 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,655 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,655 INFO  L175             Difference]: Start difference. First operand has 41 places, 46 transitions, 169 flow. Second operand 3 states and 317 transitions.
[2024-03-11 23:19:25,656 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 43 places, 54 transitions, 257 flow
[2024-03-11 23:19:25,657 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 42 places, 54 transitions, 251 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-03-11 23:19:25,658 INFO  L231             Difference]: Finished difference. Result has 44 places, 48 transitions, 185 flow
[2024-03-11 23:19:25,658 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=183, PETRI_DIFFERENCE_MINUEND_FLOW=163, PETRI_DIFFERENCE_MINUEND_PLACES=40, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=46, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=43, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=185, PETRI_PLACES=44, PETRI_TRANSITIONS=48}
[2024-03-11 23:19:25,658 INFO  L288   CegarLoopForPetriNet]: 37 programPoint places, 7 predicate places.
[2024-03-11 23:19:25,659 INFO  L495      AbstractCegarLoop]: Abstraction has has 44 places, 48 transitions, 185 flow
[2024-03-11 23:19:25,659 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 98.33333333333333) internal successors, (295), 3 states have internal predecessors, (295), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,659 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:25,659 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:25,659 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2024-03-11 23:19:25,660 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2024-03-11 23:19:25,660 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:25,660 INFO  L85        PathProgramCache]: Analyzing trace with hash 1846542559, now seen corresponding path program 1 times
[2024-03-11 23:19:25,660 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:25,661 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1481495924]
[2024-03-11 23:19:25,661 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:25,661 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:25,674 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:25,699 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:25,699 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:25,700 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1481495924]
[2024-03-11 23:19:25,700 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1481495924] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:25,700 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:25,700 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:25,700 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1495001613]
[2024-03-11 23:19:25,701 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:25,701 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:25,701 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:25,702 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:25,702 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:25,711 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 95 out of 183
[2024-03-11 23:19:25,712 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 44 places, 48 transitions, 185 flow. Second operand  has 3 states, 3 states have (on average 97.66666666666667) internal successors, (293), 3 states have internal predecessors, (293), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,712 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:25,712 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 95 of 183
[2024-03-11 23:19:25,712 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:25,758 INFO  L130       PetriNetUnfolder]: 73/269 cut-off events.
[2024-03-11 23:19:25,758 INFO  L131       PetriNetUnfolder]: For 135/142 co-relation queries the response was YES.
[2024-03-11 23:19:25,759 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 628 conditions, 269 events. 73/269 cut-off events. For 135/142 co-relation queries the response was YES. Maximal size of possible extension queue 28. Compared 1394 event pairs, 32 based on Foata normal form. 0/249 useless extension candidates. Maximal degree in co-relation 577. Up to 130 conditions per place. 
[2024-03-11 23:19:25,760 INFO  L137   encePairwiseOnDemand]: 178/183 looper letters, 27 selfloop transitions, 7 changer transitions 0/57 dead transitions.
[2024-03-11 23:19:25,760 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 46 places, 57 transitions, 285 flow
[2024-03-11 23:19:25,761 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:25,761 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:25,762 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 311 transitions.
[2024-03-11 23:19:25,762 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5664845173041895
[2024-03-11 23:19:25,762 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 311 transitions.
[2024-03-11 23:19:25,762 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 311 transitions.
[2024-03-11 23:19:25,762 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:25,763 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 311 transitions.
[2024-03-11 23:19:25,763 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 103.66666666666667) internal successors, (311), 3 states have internal predecessors, (311), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,765 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,765 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 183.0) internal successors, (732), 4 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,765 INFO  L175             Difference]: Start difference. First operand has 44 places, 48 transitions, 185 flow. Second operand 3 states and 311 transitions.
[2024-03-11 23:19:25,765 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 46 places, 57 transitions, 285 flow
[2024-03-11 23:19:25,767 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 44 places, 57 transitions, 277 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:19:25,768 INFO  L231             Difference]: Finished difference. Result has 46 places, 51 transitions, 225 flow
[2024-03-11 23:19:25,768 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=183, PETRI_DIFFERENCE_MINUEND_FLOW=179, PETRI_DIFFERENCE_MINUEND_PLACES=42, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=48, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=41, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=225, PETRI_PLACES=46, PETRI_TRANSITIONS=51}
[2024-03-11 23:19:25,769 INFO  L288   CegarLoopForPetriNet]: 37 programPoint places, 9 predicate places.
[2024-03-11 23:19:25,769 INFO  L495      AbstractCegarLoop]: Abstraction has has 46 places, 51 transitions, 225 flow
[2024-03-11 23:19:25,769 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 97.66666666666667) internal successors, (293), 3 states have internal predecessors, (293), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:25,769 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:25,769 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 1, 1, 1, 1]
[2024-03-11 23:19:25,770 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2024-03-11 23:19:25,770 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 9 more)] ===
[2024-03-11 23:19:25,770 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:25,770 INFO  L85        PathProgramCache]: Analyzing trace with hash 1058997609, now seen corresponding path program 1 times
[2024-03-11 23:19:25,771 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:25,771 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [960019712]
[2024-03-11 23:19:25,771 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:25,771 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:25,795 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:19:25,795 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-03-11 23:19:25,807 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:19:25,823 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-03-11 23:19:25,824 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-03-11 23:19:25,824 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (11 of 12 remaining)
[2024-03-11 23:19:25,826 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (10 of 12 remaining)
[2024-03-11 23:19:25,826 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (9 of 12 remaining)
[2024-03-11 23:19:25,826 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (8 of 12 remaining)
[2024-03-11 23:19:25,827 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (7 of 12 remaining)
[2024-03-11 23:19:25,827 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (6 of 12 remaining)
[2024-03-11 23:19:25,827 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (5 of 12 remaining)
[2024-03-11 23:19:25,827 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (4 of 12 remaining)
[2024-03-11 23:19:25,827 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (3 of 12 remaining)
[2024-03-11 23:19:25,828 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 12 remaining)
[2024-03-11 23:19:25,828 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (1 of 12 remaining)
[2024-03-11 23:19:25,828 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (0 of 12 remaining)
[2024-03-11 23:19:25,828 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2024-03-11 23:19:25,828 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2024-03-11 23:19:25,830 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-03-11 23:19:25,830 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2024-03-11 23:19:25,847 INFO  L144    ThreadInstanceAdder]: Constructed 0 joinOtherThreadTransitions.
[2024-03-11 23:19:25,849 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 132 places, 131 transitions, 274 flow
[2024-03-11 23:19:25,865 INFO  L130       PetriNetUnfolder]: 10/211 cut-off events.
[2024-03-11 23:19:25,866 INFO  L131       PetriNetUnfolder]: For 2/2 co-relation queries the response was YES.
[2024-03-11 23:19:25,866 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 221 conditions, 211 events. 10/211 cut-off events. For 2/2 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 278 event pairs, 0 based on Foata normal form. 0/178 useless extension candidates. Maximal degree in co-relation 137. Up to 9 conditions per place. 
[2024-03-11 23:19:25,866 INFO  L82        GeneralOperation]: Start removeDead. Operand has 132 places, 131 transitions, 274 flow
[2024-03-11 23:19:25,868 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 132 places, 131 transitions, 274 flow
[2024-03-11 23:19:25,868 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-03-11 23:19:25,868 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 132 places, 131 transitions, 274 flow
[2024-03-11 23:19:25,868 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 132 places, 131 transitions, 274 flow
[2024-03-11 23:19:25,868 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 132 places, 131 transitions, 274 flow
[2024-03-11 23:19:25,882 INFO  L130       PetriNetUnfolder]: 10/211 cut-off events.
[2024-03-11 23:19:25,883 INFO  L131       PetriNetUnfolder]: For 2/2 co-relation queries the response was YES.
[2024-03-11 23:19:25,883 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 221 conditions, 211 events. 10/211 cut-off events. For 2/2 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 278 event pairs, 0 based on Foata normal form. 0/178 useless extension candidates. Maximal degree in co-relation 137. Up to 9 conditions per place. 
[2024-03-11 23:19:25,886 INFO  L119        LiptonReduction]: Number of co-enabled transitions 6300
[2024-03-11 23:19:27,263 INFO  L134        LiptonReduction]: Checked pairs total: 24128
[2024-03-11 23:19:27,263 INFO  L136        LiptonReduction]: Total number of compositions: 87
[2024-03-11 23:19:27,265 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-11 23:19:27,266 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;@57764ce0, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-03-11 23:19:27,266 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 15 error locations.
[2024-03-11 23:19:27,267 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2024-03-11 23:19:27,267 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:19:27,267 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:27,267 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1]
[2024-03-11 23:19:27,267 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:27,268 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:27,268 INFO  L85        PathProgramCache]: Analyzing trace with hash 602978, now seen corresponding path program 1 times
[2024-03-11 23:19:27,268 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:27,268 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [21568714]
[2024-03-11 23:19:27,268 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:27,269 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:27,273 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:27,287 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:27,287 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:27,288 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [21568714]
[2024-03-11 23:19:27,288 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [21568714] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:27,288 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:27,289 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:27,289 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1651712146]
[2024-03-11 23:19:27,289 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:27,290 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:27,290 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:27,290 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:27,291 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:27,308 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 111 out of 218
[2024-03-11 23:19:27,309 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 57 places, 54 transitions, 120 flow. Second operand  has 3 states, 3 states have (on average 112.0) internal successors, (336), 3 states have internal predecessors, (336), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:27,309 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:27,309 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 111 of 218
[2024-03-11 23:19:27,309 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:27,651 INFO  L130       PetriNetUnfolder]: 2566/5288 cut-off events.
[2024-03-11 23:19:27,652 INFO  L131       PetriNetUnfolder]: For 63/63 co-relation queries the response was YES.
[2024-03-11 23:19:27,656 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 9572 conditions, 5288 events. 2566/5288 cut-off events. For 63/63 co-relation queries the response was YES. Maximal size of possible extension queue 226. Compared 40200 event pairs, 1044 based on Foata normal form. 0/4801 useless extension candidates. Maximal degree in co-relation 4153. Up to 2335 conditions per place. 
[2024-03-11 23:19:27,672 INFO  L137   encePairwiseOnDemand]: 201/218 looper letters, 49 selfloop transitions, 11 changer transitions 0/79 dead transitions.
[2024-03-11 23:19:27,673 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 58 places, 79 transitions, 295 flow
[2024-03-11 23:19:27,673 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:27,673 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:27,674 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 401 transitions.
[2024-03-11 23:19:27,674 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6131498470948012
[2024-03-11 23:19:27,674 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 401 transitions.
[2024-03-11 23:19:27,675 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 401 transitions.
[2024-03-11 23:19:27,675 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:27,675 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 401 transitions.
[2024-03-11 23:19:27,676 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 133.66666666666666) internal successors, (401), 3 states have internal predecessors, (401), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:27,678 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:27,678 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:27,678 INFO  L175             Difference]: Start difference. First operand has 57 places, 54 transitions, 120 flow. Second operand 3 states and 401 transitions.
[2024-03-11 23:19:27,678 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 58 places, 79 transitions, 295 flow
[2024-03-11 23:19:27,679 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 58 places, 79 transitions, 293 flow, removed 1 selfloop flow, removed 0 redundant places.
[2024-03-11 23:19:27,680 INFO  L231             Difference]: Finished difference. Result has 60 places, 63 transitions, 210 flow
[2024-03-11 23:19:27,680 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=114, PETRI_DIFFERENCE_MINUEND_PLACES=56, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=52, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=41, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=210, PETRI_PLACES=60, PETRI_TRANSITIONS=63}
[2024-03-11 23:19:27,681 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 3 predicate places.
[2024-03-11 23:19:27,681 INFO  L495      AbstractCegarLoop]: Abstraction has has 60 places, 63 transitions, 210 flow
[2024-03-11 23:19:27,681 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 112.0) internal successors, (336), 3 states have internal predecessors, (336), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:27,682 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:27,682 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:27,682 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2024-03-11 23:19:27,682 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:27,682 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:27,682 INFO  L85        PathProgramCache]: Analyzing trace with hash -1471106384, now seen corresponding path program 1 times
[2024-03-11 23:19:27,683 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:27,683 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [917729067]
[2024-03-11 23:19:27,683 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:27,683 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:27,688 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:27,699 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:27,699 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:27,699 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [917729067]
[2024-03-11 23:19:27,699 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [917729067] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:27,700 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:27,700 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:27,700 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1468412788]
[2024-03-11 23:19:27,700 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:27,700 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:27,700 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:27,701 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:27,701 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:27,722 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 114 out of 218
[2024-03-11 23:19:27,723 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 60 places, 63 transitions, 210 flow. Second operand  has 3 states, 3 states have (on average 115.33333333333333) internal successors, (346), 3 states have internal predecessors, (346), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:27,723 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:27,723 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 114 of 218
[2024-03-11 23:19:27,723 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:27,877 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][12], [112#L685-2true, threadThread1of2ForFork0InUse, 141#true, threadThread2of2ForFork0InUse, 29#L683-2true, 137#(= |#race~threads_alive~0| 0), 31#L697true, Black: 135#true])
[2024-03-11 23:19:27,878 INFO  L383   tUnfolder$Statistics]: this new event has 33 ancestors and is cut-off event
[2024-03-11 23:19:27,878 INFO  L386   tUnfolder$Statistics]:   existing Event has 33 ancestors and is cut-off event
[2024-03-11 23:19:27,878 INFO  L386   tUnfolder$Statistics]:   existing Event has 30 ancestors and is cut-off event
[2024-03-11 23:19:27,878 INFO  L386   tUnfolder$Statistics]:   existing Event has 30 ancestors and is cut-off event
[2024-03-11 23:19:27,878 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][12], [112#L685-2true, threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 141#true, 137#(= |#race~threads_alive~0| 0), 31#L697true, 103#L682-1true, Black: 135#true])
[2024-03-11 23:19:27,878 INFO  L383   tUnfolder$Statistics]: this new event has 32 ancestors and is cut-off event
[2024-03-11 23:19:27,878 INFO  L386   tUnfolder$Statistics]:   existing Event has 29 ancestors and is cut-off event
[2024-03-11 23:19:27,879 INFO  L386   tUnfolder$Statistics]:   existing Event has 32 ancestors and is cut-off event
[2024-03-11 23:19:27,879 INFO  L386   tUnfolder$Statistics]:   existing Event has 29 ancestors and is cut-off event
[2024-03-11 23:19:27,880 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][12], [112#L685-2true, threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 141#true, 32#L683-4true, 137#(= |#race~threads_alive~0| 0), 31#L697true, Black: 135#true])
[2024-03-11 23:19:27,880 INFO  L383   tUnfolder$Statistics]: this new event has 34 ancestors and is cut-off event
[2024-03-11 23:19:27,881 INFO  L386   tUnfolder$Statistics]:   existing Event has 31 ancestors and is cut-off event
[2024-03-11 23:19:27,881 INFO  L386   tUnfolder$Statistics]:   existing Event has 34 ancestors and is cut-off event
[2024-03-11 23:19:27,881 INFO  L386   tUnfolder$Statistics]:   existing Event has 31 ancestors and is cut-off event
[2024-03-11 23:19:27,894 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][12], [112#L685-2true, threadThread1of2ForFork0InUse, 141#true, threadThread2of2ForFork0InUse, 44#L684true, 137#(= |#race~threads_alive~0| 0), 31#L697true, Black: 135#true])
[2024-03-11 23:19:27,895 INFO  L383   tUnfolder$Statistics]: this new event has 35 ancestors and is cut-off event
[2024-03-11 23:19:27,895 INFO  L386   tUnfolder$Statistics]:   existing Event has 32 ancestors and is cut-off event
[2024-03-11 23:19:27,895 INFO  L386   tUnfolder$Statistics]:   existing Event has 35 ancestors and is cut-off event
[2024-03-11 23:19:27,895 INFO  L386   tUnfolder$Statistics]:   existing Event has 32 ancestors and is cut-off event
[2024-03-11 23:19:28,075 INFO  L130       PetriNetUnfolder]: 2100/4555 cut-off events.
[2024-03-11 23:19:28,075 INFO  L131       PetriNetUnfolder]: For 2315/2399 co-relation queries the response was YES.
[2024-03-11 23:19:28,080 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 10309 conditions, 4555 events. 2100/4555 cut-off events. For 2315/2399 co-relation queries the response was YES. Maximal size of possible extension queue 217. Compared 35646 event pairs, 1329 based on Foata normal form. 0/4168 useless extension candidates. Maximal degree in co-relation 3797. Up to 2913 conditions per place. 
[2024-03-11 23:19:28,096 INFO  L137   encePairwiseOnDemand]: 211/218 looper letters, 42 selfloop transitions, 11 changer transitions 0/83 dead transitions.
[2024-03-11 23:19:28,096 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 62 places, 83 transitions, 380 flow
[2024-03-11 23:19:28,097 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:28,097 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:28,098 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 385 transitions.
[2024-03-11 23:19:28,098 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5886850152905199
[2024-03-11 23:19:28,098 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 385 transitions.
[2024-03-11 23:19:28,098 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 385 transitions.
[2024-03-11 23:19:28,099 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:28,099 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 385 transitions.
[2024-03-11 23:19:28,100 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 128.33333333333334) internal successors, (385), 3 states have internal predecessors, (385), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,101 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,102 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,102 INFO  L175             Difference]: Start difference. First operand has 60 places, 63 transitions, 210 flow. Second operand 3 states and 385 transitions.
[2024-03-11 23:19:28,102 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 62 places, 83 transitions, 380 flow
[2024-03-11 23:19:28,106 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 60 places, 83 transitions, 350 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:19:28,107 INFO  L231             Difference]: Finished difference. Result has 61 places, 72 transitions, 275 flow
[2024-03-11 23:19:28,108 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=188, PETRI_DIFFERENCE_MINUEND_PLACES=58, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=63, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=52, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=275, PETRI_PLACES=61, PETRI_TRANSITIONS=72}
[2024-03-11 23:19:28,108 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 4 predicate places.
[2024-03-11 23:19:28,108 INFO  L495      AbstractCegarLoop]: Abstraction has has 61 places, 72 transitions, 275 flow
[2024-03-11 23:19:28,109 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 115.33333333333333) internal successors, (346), 3 states have internal predecessors, (346), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,109 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:28,109 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:28,109 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2024-03-11 23:19:28,109 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:28,110 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:28,110 INFO  L85        PathProgramCache]: Analyzing trace with hash -1256742814, now seen corresponding path program 1 times
[2024-03-11 23:19:28,110 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:28,110 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1281049558]
[2024-03-11 23:19:28,110 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:28,111 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:28,116 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:28,126 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:28,126 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:28,126 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1281049558]
[2024-03-11 23:19:28,126 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1281049558] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:28,127 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:28,127 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:28,127 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [279122222]
[2024-03-11 23:19:28,127 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:28,128 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:28,128 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:28,128 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:28,128 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:28,138 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 121 out of 218
[2024-03-11 23:19:28,138 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 61 places, 72 transitions, 275 flow. Second operand  has 3 states, 3 states have (on average 122.33333333333333) internal successors, (367), 3 states have internal predecessors, (367), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,138 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:28,138 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 121 of 218
[2024-03-11 23:19:28,139 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:28,514 INFO  L130       PetriNetUnfolder]: 2469/5615 cut-off events.
[2024-03-11 23:19:28,515 INFO  L131       PetriNetUnfolder]: For 2596/2883 co-relation queries the response was YES.
[2024-03-11 23:19:28,522 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 12204 conditions, 5615 events. 2469/5615 cut-off events. For 2596/2883 co-relation queries the response was YES. Maximal size of possible extension queue 282. Compared 47754 event pairs, 1292 based on Foata normal form. 3/5093 useless extension candidates. Maximal degree in co-relation 7605. Up to 2656 conditions per place. 
[2024-03-11 23:19:28,540 INFO  L137   encePairwiseOnDemand]: 213/218 looper letters, 43 selfloop transitions, 4 changer transitions 0/88 dead transitions.
[2024-03-11 23:19:28,540 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 63 places, 88 transitions, 409 flow
[2024-03-11 23:19:28,561 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:28,561 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:28,562 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 404 transitions.
[2024-03-11 23:19:28,562 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.617737003058104
[2024-03-11 23:19:28,562 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 404 transitions.
[2024-03-11 23:19:28,562 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 404 transitions.
[2024-03-11 23:19:28,563 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:28,563 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 404 transitions.
[2024-03-11 23:19:28,564 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 134.66666666666666) internal successors, (404), 3 states have internal predecessors, (404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,565 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,565 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,565 INFO  L175             Difference]: Start difference. First operand has 61 places, 72 transitions, 275 flow. Second operand 3 states and 404 transitions.
[2024-03-11 23:19:28,565 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 63 places, 88 transitions, 409 flow
[2024-03-11 23:19:28,573 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 62 places, 88 transitions, 398 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-03-11 23:19:28,574 INFO  L231             Difference]: Finished difference. Result has 64 places, 75 transitions, 294 flow
[2024-03-11 23:19:28,574 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=264, PETRI_DIFFERENCE_MINUEND_PLACES=60, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=72, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=68, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=294, PETRI_PLACES=64, PETRI_TRANSITIONS=75}
[2024-03-11 23:19:28,574 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 7 predicate places.
[2024-03-11 23:19:28,575 INFO  L495      AbstractCegarLoop]: Abstraction has has 64 places, 75 transitions, 294 flow
[2024-03-11 23:19:28,575 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 122.33333333333333) internal successors, (367), 3 states have internal predecessors, (367), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,575 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:28,575 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:28,575 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2024-03-11 23:19:28,576 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:28,576 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:28,576 INFO  L85        PathProgramCache]: Analyzing trace with hash -351598344, now seen corresponding path program 1 times
[2024-03-11 23:19:28,576 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:28,576 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [847651946]
[2024-03-11 23:19:28,576 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:28,577 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:28,584 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:28,597 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:28,597 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:28,598 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [847651946]
[2024-03-11 23:19:28,598 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [847651946] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:28,598 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:28,598 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:28,598 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [675530364]
[2024-03-11 23:19:28,598 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:28,599 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:28,599 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:28,599 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:28,599 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:28,610 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 119 out of 218
[2024-03-11 23:19:28,611 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 64 places, 75 transitions, 294 flow. Second operand  has 3 states, 3 states have (on average 122.0) internal successors, (366), 3 states have internal predecessors, (366), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:28,611 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:28,611 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 119 of 218
[2024-03-11 23:19:28,611 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:29,037 INFO  L130       PetriNetUnfolder]: 2578/5961 cut-off events.
[2024-03-11 23:19:29,037 INFO  L131       PetriNetUnfolder]: For 2985/3329 co-relation queries the response was YES.
[2024-03-11 23:19:29,045 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 13557 conditions, 5961 events. 2578/5961 cut-off events. For 2985/3329 co-relation queries the response was YES. Maximal size of possible extension queue 319. Compared 52815 event pairs, 1452 based on Foata normal form. 2/5367 useless extension candidates. Maximal degree in co-relation 9075. Up to 3044 conditions per place. 
[2024-03-11 23:19:29,059 INFO  L137   encePairwiseOnDemand]: 212/218 looper letters, 48 selfloop transitions, 7 changer transitions 0/98 dead transitions.
[2024-03-11 23:19:29,059 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 66 places, 98 transitions, 497 flow
[2024-03-11 23:19:29,060 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:29,060 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:29,060 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 398 transitions.
[2024-03-11 23:19:29,061 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6085626911314985
[2024-03-11 23:19:29,061 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 398 transitions.
[2024-03-11 23:19:29,061 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 398 transitions.
[2024-03-11 23:19:29,061 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:29,061 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 398 transitions.
[2024-03-11 23:19:29,062 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 132.66666666666666) internal successors, (398), 3 states have internal predecessors, (398), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,063 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,063 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,064 INFO  L175             Difference]: Start difference. First operand has 64 places, 75 transitions, 294 flow. Second operand 3 states and 398 transitions.
[2024-03-11 23:19:29,064 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 66 places, 98 transitions, 497 flow
[2024-03-11 23:19:29,069 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 64 places, 98 transitions, 485 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:19:29,071 INFO  L231             Difference]: Finished difference. Result has 66 places, 80 transitions, 342 flow
[2024-03-11 23:19:29,071 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=286, PETRI_DIFFERENCE_MINUEND_PLACES=62, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=75, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=68, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=342, PETRI_PLACES=66, PETRI_TRANSITIONS=80}
[2024-03-11 23:19:29,071 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 9 predicate places.
[2024-03-11 23:19:29,072 INFO  L495      AbstractCegarLoop]: Abstraction has has 66 places, 80 transitions, 342 flow
[2024-03-11 23:19:29,072 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 122.0) internal successors, (366), 3 states have internal predecessors, (366), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,072 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:29,072 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:29,072 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2024-03-11 23:19:29,072 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:29,073 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:29,073 INFO  L85        PathProgramCache]: Analyzing trace with hash 1777019964, now seen corresponding path program 1 times
[2024-03-11 23:19:29,073 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:29,073 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1940410838]
[2024-03-11 23:19:29,073 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:29,073 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:29,081 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:29,131 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:29,131 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:29,132 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1940410838]
[2024-03-11 23:19:29,132 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1940410838] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-11 23:19:29,132 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [580733978]
[2024-03-11 23:19:29,132 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:29,132 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-11 23:19:29,133 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2024-03-11 23:19:29,135 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-11 23:19:29,136 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2024-03-11 23:19:29,199 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:29,201 INFO  L263         TraceCheckSpWp]: Trace formula consists of 124 conjuncts, 4 conjunts are in the unsatisfiable core
[2024-03-11 23:19:29,203 INFO  L286         TraceCheckSpWp]: Computing forward predicates...
[2024-03-11 23:19:29,271 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 1 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:29,272 INFO  L324         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2024-03-11 23:19:29,272 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleZ3 [580733978] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:29,272 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2024-03-11 23:19:29,272 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2024-03-11 23:19:29,272 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [700827008]
[2024-03-11 23:19:29,272 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:29,273 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2024-03-11 23:19:29,273 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:29,273 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2024-03-11 23:19:29,273 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2024-03-11 23:19:29,286 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 117 out of 218
[2024-03-11 23:19:29,287 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 66 places, 80 transitions, 342 flow. Second operand  has 5 states, 5 states have (on average 119.4) internal successors, (597), 5 states have internal predecessors, (597), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,287 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:29,287 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 117 of 218
[2024-03-11 23:19:29,287 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:29,908 INFO  L130       PetriNetUnfolder]: 3724/7922 cut-off events.
[2024-03-11 23:19:29,908 INFO  L131       PetriNetUnfolder]: For 3774/4383 co-relation queries the response was YES.
[2024-03-11 23:19:29,920 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 19221 conditions, 7922 events. 3724/7922 cut-off events. For 3774/4383 co-relation queries the response was YES. Maximal size of possible extension queue 389. Compared 67676 event pairs, 976 based on Foata normal form. 139/7457 useless extension candidates. Maximal degree in co-relation 9271. Up to 2409 conditions per place. 
[2024-03-11 23:19:29,941 INFO  L137   encePairwiseOnDemand]: 210/218 looper letters, 110 selfloop transitions, 16 changer transitions 3/172 dead transitions.
[2024-03-11 23:19:29,942 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 72 places, 172 transitions, 931 flow
[2024-03-11 23:19:29,942 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2024-03-11 23:19:29,942 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 7 states.
[2024-03-11 23:19:29,944 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 7 states to 7 states and 917 transitions.
[2024-03-11 23:19:29,944 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6009174311926605
[2024-03-11 23:19:29,944 INFO  L72            ComplementDD]: Start complementDD. Operand 7 states and 917 transitions.
[2024-03-11 23:19:29,945 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 7 states and 917 transitions.
[2024-03-11 23:19:29,945 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:29,945 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 7 states and 917 transitions.
[2024-03-11 23:19:29,947 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 8 states, 7 states have (on average 131.0) internal successors, (917), 7 states have internal predecessors, (917), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,949 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 8 states, 8 states have (on average 218.0) internal successors, (1744), 8 states have internal predecessors, (1744), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,949 INFO  L81            ComplementDD]: Finished complementDD. Result  has 8 states, 8 states have (on average 218.0) internal successors, (1744), 8 states have internal predecessors, (1744), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,949 INFO  L175             Difference]: Start difference. First operand has 66 places, 80 transitions, 342 flow. Second operand 7 states and 917 transitions.
[2024-03-11 23:19:29,949 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 72 places, 172 transitions, 931 flow
[2024-03-11 23:19:29,953 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 70 places, 172 transitions, 901 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:19:29,954 INFO  L231             Difference]: Finished difference. Result has 73 places, 95 transitions, 426 flow
[2024-03-11 23:19:29,954 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=322, PETRI_DIFFERENCE_MINUEND_PLACES=64, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=79, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=7, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=71, PETRI_DIFFERENCE_SUBTRAHEND_STATES=7, PETRI_FLOW=426, PETRI_PLACES=73, PETRI_TRANSITIONS=95}
[2024-03-11 23:19:29,955 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 16 predicate places.
[2024-03-11 23:19:29,955 INFO  L495      AbstractCegarLoop]: Abstraction has has 73 places, 95 transitions, 426 flow
[2024-03-11 23:19:29,955 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 5 states have (on average 119.4) internal successors, (597), 5 states have internal predecessors, (597), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:29,956 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:29,956 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:29,964 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2024-03-11 23:19:30,156 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2024-03-11 23:19:30,157 INFO  L420      AbstractCegarLoop]: === Iteration 6 === Targeting threadErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:30,158 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:30,158 INFO  L85        PathProgramCache]: Analyzing trace with hash 1155071363, now seen corresponding path program 1 times
[2024-03-11 23:19:30,158 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:30,159 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1009363404]
[2024-03-11 23:19:30,159 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:30,159 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:30,171 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:30,187 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:19:30,187 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:30,187 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1009363404]
[2024-03-11 23:19:30,187 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1009363404] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:30,187 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:30,187 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:30,188 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2016961652]
[2024-03-11 23:19:30,188 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:30,188 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:30,188 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:30,188 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:30,188 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:30,213 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 115 out of 218
[2024-03-11 23:19:30,214 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 73 places, 95 transitions, 426 flow. Second operand  has 3 states, 3 states have (on average 119.33333333333333) internal successors, (358), 3 states have internal predecessors, (358), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:30,214 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:30,214 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 115 of 218
[2024-03-11 23:19:30,214 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:30,404 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][22], [Black: 220#(and (<= 0 |ULTIMATE.start_main_#t~post7#1|) (<= 0 ~threads_alive~0)), Black: 166#(<= 0 ~threads_alive~0), Black: 176#(<= 0 |ULTIMATE.start_main_#t~post7#1|), threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 162#(<= 1 ~threads_alive~0), Black: 135#true, Black: 143#(= |#race~threads_alive~0| |ULTIMATE.start_main_#t~nondet8#1|), 112#L685-2true, 227#true, Black: 148#(= |#race~data~0| 0), 31#L697true, 103#L682-1true, Black: 154#(= |threadThread1of2ForFork0_#t~nondet2| |#race~data~0|)])
[2024-03-11 23:19:30,404 INFO  L383   tUnfolder$Statistics]: this new event has 32 ancestors and is cut-off event
[2024-03-11 23:19:30,404 INFO  L386   tUnfolder$Statistics]:   existing Event has 29 ancestors and is cut-off event
[2024-03-11 23:19:30,404 INFO  L386   tUnfolder$Statistics]:   existing Event has 29 ancestors and is cut-off event
[2024-03-11 23:19:30,404 INFO  L386   tUnfolder$Statistics]:   existing Event has 32 ancestors and is cut-off event
[2024-03-11 23:19:30,405 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][22], [Black: 220#(and (<= 0 |ULTIMATE.start_main_#t~post7#1|) (<= 0 ~threads_alive~0)), Black: 166#(<= 0 ~threads_alive~0), Black: 176#(<= 0 |ULTIMATE.start_main_#t~post7#1|), threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 162#(<= 1 ~threads_alive~0), 29#L683-2true, Black: 135#true, Black: 143#(= |#race~threads_alive~0| |ULTIMATE.start_main_#t~nondet8#1|), 112#L685-2true, 227#true, Black: 148#(= |#race~data~0| 0), 31#L697true, Black: 154#(= |threadThread1of2ForFork0_#t~nondet2| |#race~data~0|)])
[2024-03-11 23:19:30,405 INFO  L383   tUnfolder$Statistics]: this new event has 33 ancestors and is cut-off event
[2024-03-11 23:19:30,405 INFO  L386   tUnfolder$Statistics]:   existing Event has 30 ancestors and is cut-off event
[2024-03-11 23:19:30,405 INFO  L386   tUnfolder$Statistics]:   existing Event has 33 ancestors and is cut-off event
[2024-03-11 23:19:30,405 INFO  L386   tUnfolder$Statistics]:   existing Event has 30 ancestors and is cut-off event
[2024-03-11 23:19:30,406 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][22], [Black: 220#(and (<= 0 |ULTIMATE.start_main_#t~post7#1|) (<= 0 ~threads_alive~0)), Black: 166#(<= 0 ~threads_alive~0), Black: 176#(<= 0 |ULTIMATE.start_main_#t~post7#1|), threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 162#(<= 1 ~threads_alive~0), 32#L683-4true, Black: 135#true, Black: 143#(= |#race~threads_alive~0| |ULTIMATE.start_main_#t~nondet8#1|), 112#L685-2true, 227#true, Black: 148#(= |#race~data~0| 0), 31#L697true, Black: 154#(= |threadThread1of2ForFork0_#t~nondet2| |#race~data~0|)])
[2024-03-11 23:19:30,407 INFO  L383   tUnfolder$Statistics]: this new event has 34 ancestors and is cut-off event
[2024-03-11 23:19:30,407 INFO  L386   tUnfolder$Statistics]:   existing Event has 31 ancestors and is cut-off event
[2024-03-11 23:19:30,407 INFO  L386   tUnfolder$Statistics]:   existing Event has 34 ancestors and is cut-off event
[2024-03-11 23:19:30,407 INFO  L386   tUnfolder$Statistics]:   existing Event has 31 ancestors and is cut-off event
[2024-03-11 23:19:30,435 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([385] L697-3-->L697: Formula: (= 0 |v_#race~threads_alive~0_7|)  InVars {}  OutVars{#race~threads_alive~0=|v_#race~threads_alive~0_7|}  AuxVars[]  AssignedVars[#race~threads_alive~0][22], [Black: 220#(and (<= 0 |ULTIMATE.start_main_#t~post7#1|) (<= 0 ~threads_alive~0)), Black: 166#(<= 0 ~threads_alive~0), Black: 176#(<= 0 |ULTIMATE.start_main_#t~post7#1|), threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 44#L684true, 162#(<= 1 ~threads_alive~0), Black: 135#true, Black: 143#(= |#race~threads_alive~0| |ULTIMATE.start_main_#t~nondet8#1|), 112#L685-2true, 227#true, Black: 148#(= |#race~data~0| 0), 31#L697true, Black: 154#(= |threadThread1of2ForFork0_#t~nondet2| |#race~data~0|)])
[2024-03-11 23:19:30,435 INFO  L383   tUnfolder$Statistics]: this new event has 35 ancestors and is cut-off event
[2024-03-11 23:19:30,435 INFO  L386   tUnfolder$Statistics]:   existing Event has 35 ancestors and is cut-off event
[2024-03-11 23:19:30,435 INFO  L386   tUnfolder$Statistics]:   existing Event has 32 ancestors and is cut-off event
[2024-03-11 23:19:30,435 INFO  L386   tUnfolder$Statistics]:   existing Event has 32 ancestors and is cut-off event
[2024-03-11 23:19:30,841 INFO  L381   tUnfolder$Statistics]: inserting event number 4 for the transition-marking pair ([564] L698-1-->ULTIMATE.startEXIT: Formula: (and (= |v_ULTIMATE.start_main_#res#1_24| v_~data~0_38) (= |v_ULTIMATE.start_main_#res#1_24| |v_ULTIMATE.start_#t~ret13#1_12|))  InVars {~data~0=v_~data~0_38}  OutVars{ULTIMATE.start_main_#res#1=|v_ULTIMATE.start_main_#res#1_24|, ULTIMATE.start_#t~ret13#1=|v_ULTIMATE.start_#t~ret13#1_12|, ~data~0=v_~data~0_38}  AuxVars[]  AssignedVars[ULTIMATE.start_main_#res#1, ULTIMATE.start_#t~ret13#1][81], [Black: 220#(and (<= 0 |ULTIMATE.start_main_#t~post7#1|) (<= 0 ~threads_alive~0)), Black: 176#(<= 0 |ULTIMATE.start_main_#t~post7#1|), threadThread1of2ForFork0InUse, threadThread2of2ForFork0InUse, 2#ULTIMATE.startEXITtrue, 3#threadEXITtrue, 166#(<= 0 ~threads_alive~0), Black: 135#true, Black: 143#(= |#race~threads_alive~0| |ULTIMATE.start_main_#t~nondet8#1|), 227#true, Black: 146#true, Black: 154#(= |threadThread1of2ForFork0_#t~nondet2| |#race~data~0|), 68#L685-1true])
[2024-03-11 23:19:30,841 INFO  L383   tUnfolder$Statistics]: this new event has 43 ancestors and is cut-off event
[2024-03-11 23:19:30,841 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2024-03-11 23:19:30,842 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2024-03-11 23:19:30,842 INFO  L386   tUnfolder$Statistics]:   existing Event has 43 ancestors and is cut-off event
[2024-03-11 23:19:30,892 INFO  L130       PetriNetUnfolder]: 4048/8545 cut-off events.
[2024-03-11 23:19:30,892 INFO  L131       PetriNetUnfolder]: For 7119/7971 co-relation queries the response was YES.
[2024-03-11 23:19:30,905 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 22925 conditions, 8545 events. 4048/8545 cut-off events. For 7119/7971 co-relation queries the response was YES. Maximal size of possible extension queue 416. Compared 73782 event pairs, 1772 based on Foata normal form. 202/7937 useless extension candidates. Maximal degree in co-relation 19406. Up to 5504 conditions per place. 
[2024-03-11 23:19:30,928 INFO  L137   encePairwiseOnDemand]: 210/218 looper letters, 63 selfloop transitions, 15 changer transitions 0/119 dead transitions.
[2024-03-11 23:19:30,928 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 75 places, 119 transitions, 688 flow
[2024-03-11 23:19:30,929 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:30,929 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:30,930 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 388 transitions.
[2024-03-11 23:19:30,930 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5932721712538226
[2024-03-11 23:19:30,930 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 388 transitions.
[2024-03-11 23:19:30,930 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 388 transitions.
[2024-03-11 23:19:30,930 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:30,930 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 388 transitions.
[2024-03-11 23:19:30,931 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 129.33333333333334) internal successors, (388), 3 states have internal predecessors, (388), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:30,932 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:30,932 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:30,932 INFO  L175             Difference]: Start difference. First operand has 73 places, 95 transitions, 426 flow. Second operand 3 states and 388 transitions.
[2024-03-11 23:19:30,932 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 75 places, 119 transitions, 688 flow
[2024-03-11 23:19:30,936 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 75 places, 119 transitions, 688 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:19:30,937 INFO  L231             Difference]: Finished difference. Result has 76 places, 106 transitions, 549 flow
[2024-03-11 23:19:30,937 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=426, PETRI_DIFFERENCE_MINUEND_PLACES=73, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=95, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=4, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=80, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=549, PETRI_PLACES=76, PETRI_TRANSITIONS=106}
[2024-03-11 23:19:30,938 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 19 predicate places.
[2024-03-11 23:19:30,938 INFO  L495      AbstractCegarLoop]: Abstraction has has 76 places, 106 transitions, 549 flow
[2024-03-11 23:19:30,938 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 119.33333333333333) internal successors, (358), 3 states have internal predecessors, (358), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:30,938 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:30,938 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:30,938 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2024-03-11 23:19:30,938 INFO  L420      AbstractCegarLoop]: === Iteration 7 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:30,938 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:30,939 INFO  L85        PathProgramCache]: Analyzing trace with hash 304011890, now seen corresponding path program 1 times
[2024-03-11 23:19:30,939 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:30,939 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1920376509]
[2024-03-11 23:19:30,939 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:30,939 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:30,948 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:19:30,964 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2024-03-11 23:19:30,964 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:19:30,964 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1920376509]
[2024-03-11 23:19:30,964 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1920376509] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:19:30,964 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:19:30,964 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:19:30,965 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [245894627]
[2024-03-11 23:19:30,965 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:19:30,965 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:19:30,965 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:19:30,965 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:19:30,965 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:19:30,980 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 119 out of 218
[2024-03-11 23:19:30,980 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 76 places, 106 transitions, 549 flow. Second operand  has 3 states, 3 states have (on average 122.66666666666667) internal successors, (368), 3 states have internal predecessors, (368), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:30,980 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:19:30,980 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 119 of 218
[2024-03-11 23:19:30,980 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:19:31,544 INFO  L130       PetriNetUnfolder]: 3785/8061 cut-off events.
[2024-03-11 23:19:31,544 INFO  L131       PetriNetUnfolder]: For 11791/13468 co-relation queries the response was YES.
[2024-03-11 23:19:31,557 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 24408 conditions, 8061 events. 3785/8061 cut-off events. For 11791/13468 co-relation queries the response was YES. Maximal size of possible extension queue 449. Compared 70650 event pairs, 1521 based on Foata normal form. 289/7508 useless extension candidates. Maximal degree in co-relation 20393. Up to 4685 conditions per place. 
[2024-03-11 23:19:31,577 INFO  L137   encePairwiseOnDemand]: 213/218 looper letters, 73 selfloop transitions, 6 changer transitions 0/134 dead transitions.
[2024-03-11 23:19:31,577 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 78 places, 134 transitions, 852 flow
[2024-03-11 23:19:31,577 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:19:31,578 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:19:31,578 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 397 transitions.
[2024-03-11 23:19:31,578 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6070336391437309
[2024-03-11 23:19:31,579 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 397 transitions.
[2024-03-11 23:19:31,579 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 397 transitions.
[2024-03-11 23:19:31,579 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:19:31,579 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 397 transitions.
[2024-03-11 23:19:31,580 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 132.33333333333334) internal successors, (397), 3 states have internal predecessors, (397), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:31,581 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:31,581 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 218.0) internal successors, (872), 4 states have internal predecessors, (872), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:31,581 INFO  L175             Difference]: Start difference. First operand has 76 places, 106 transitions, 549 flow. Second operand 3 states and 397 transitions.
[2024-03-11 23:19:31,581 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 78 places, 134 transitions, 852 flow
[2024-03-11 23:19:31,588 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 77 places, 134 transitions, 833 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-03-11 23:19:31,589 INFO  L231             Difference]: Finished difference. Result has 78 places, 109 transitions, 574 flow
[2024-03-11 23:19:31,589 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=218, PETRI_DIFFERENCE_MINUEND_FLOW=534, PETRI_DIFFERENCE_MINUEND_PLACES=75, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=106, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=3, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=100, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=574, PETRI_PLACES=78, PETRI_TRANSITIONS=109}
[2024-03-11 23:19:31,590 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, 21 predicate places.
[2024-03-11 23:19:31,590 INFO  L495      AbstractCegarLoop]: Abstraction has has 78 places, 109 transitions, 574 flow
[2024-03-11 23:19:31,590 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 122.66666666666667) internal successors, (368), 3 states have internal predecessors, (368), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:19:31,590 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:19:31,590 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:31,590 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2024-03-11 23:19:31,590 INFO  L420      AbstractCegarLoop]: === Iteration 8 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (and 12 more)] ===
[2024-03-11 23:19:31,590 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:19:31,591 INFO  L85        PathProgramCache]: Analyzing trace with hash 1820031444, now seen corresponding path program 1 times
[2024-03-11 23:19:31,591 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:19:31,591 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2014468583]
[2024-03-11 23:19:31,591 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:19:31,591 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:19:31,602 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:19:31,602 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-03-11 23:19:31,608 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:19:31,612 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-03-11 23:19:31,613 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location threadErr1ASSERT_VIOLATIONDATA_RACE (14 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (13 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (12 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr4ASSERT_VIOLATIONDATA_RACE (11 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (10 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (9 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (8 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (7 of 15 remaining)
[2024-03-11 23:19:31,613 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (6 of 15 remaining)
[2024-03-11 23:19:31,614 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (5 of 15 remaining)
[2024-03-11 23:19:31,614 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (4 of 15 remaining)
[2024-03-11 23:19:31,614 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (3 of 15 remaining)
[2024-03-11 23:19:31,614 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 15 remaining)
[2024-03-11 23:19:31,614 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (1 of 15 remaining)
[2024-03-11 23:19:31,614 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (0 of 15 remaining)
[2024-03-11 23:19:31,614 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2024-03-11 23:19:31,614 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:19:31,618 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 2 thread instances
[2024-03-11 23:19:31,618 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2024-03-11 23:19:31,644 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 11.03 11:19:31 BasicIcfg
[2024-03-11 23:19:31,644 INFO  L132        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2024-03-11 23:19:31,644 INFO  L113        PluginConnector]: ------------------------Witness Printer----------------------------
[2024-03-11 23:19:31,644 INFO  L271        PluginConnector]: Initializing Witness Printer...
[2024-03-11 23:19:31,644 INFO  L275        PluginConnector]: Witness Printer initialized
[2024-03-11 23:19:31,645 INFO  L185        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 11.03 11:19:23" (3/4) ...
[2024-03-11 23:19:31,647 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2024-03-11 23:19:31,647 INFO  L132        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2024-03-11 23:19:31,647 INFO  L158              Benchmark]: Toolchain (without parser) took 8902.46ms. Allocated memory was 111.1MB in the beginning and 790.6MB in the end (delta: 679.5MB). Free memory was 81.0MB in the beginning and 387.8MB in the end (delta: -306.8MB). Peak memory consumption was 374.4MB. Max. memory is 16.1GB.
[2024-03-11 23:19:31,648 INFO  L158              Benchmark]: CDTParser took 0.14ms. Allocated memory is still 111.1MB. Free memory is still 88.2MB. There was no memory consumed. Max. memory is 16.1GB.
[2024-03-11 23:19:31,648 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 298.58ms. Allocated memory is still 111.1MB. Free memory was 80.7MB in the beginning and 61.8MB in the end (delta: 18.9MB). Peak memory consumption was 18.9MB. Max. memory is 16.1GB.
[2024-03-11 23:19:31,648 INFO  L158              Benchmark]: Boogie Procedure Inliner took 30.78ms. Allocated memory is still 111.1MB. Free memory was 61.8MB in the beginning and 59.8MB in the end (delta: 2.0MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-03-11 23:19:31,648 INFO  L158              Benchmark]: Boogie Preprocessor took 20.82ms. Allocated memory is still 111.1MB. Free memory was 59.8MB in the beginning and 58.3MB in the end (delta: 1.5MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-03-11 23:19:31,649 INFO  L158              Benchmark]: RCFGBuilder took 361.24ms. Allocated memory was 111.1MB in the beginning and 134.2MB in the end (delta: 23.1MB). Free memory was 58.0MB in the beginning and 102.3MB in the end (delta: -44.3MB). Peak memory consumption was 17.1MB. Max. memory is 16.1GB.
[2024-03-11 23:19:31,649 INFO  L158              Benchmark]: TraceAbstraction took 8183.57ms. Allocated memory was 134.2MB in the beginning and 790.6MB in the end (delta: 656.4MB). Free memory was 101.6MB in the beginning and 387.8MB in the end (delta: -286.2MB). Peak memory consumption was 369.9MB. Max. memory is 16.1GB.
[2024-03-11 23:19:31,649 INFO  L158              Benchmark]: Witness Printer took 2.52ms. Allocated memory is still 790.6MB. Free memory is still 387.8MB. There was no memory consumed. Max. memory is 16.1GB.
[2024-03-11 23:19:31,651 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.14ms. Allocated memory is still 111.1MB. Free memory is still 88.2MB. There was no memory consumed. Max. memory is 16.1GB.
 * CACSL2BoogieTranslator took 298.58ms. Allocated memory is still 111.1MB. Free memory was 80.7MB in the beginning and 61.8MB in the end (delta: 18.9MB). Peak memory consumption was 18.9MB. Max. memory is 16.1GB.
 * Boogie Procedure Inliner took 30.78ms. Allocated memory is still 111.1MB. Free memory was 61.8MB in the beginning and 59.8MB in the end (delta: 2.0MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * Boogie Preprocessor took 20.82ms. Allocated memory is still 111.1MB. Free memory was 59.8MB in the beginning and 58.3MB in the end (delta: 1.5MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * RCFGBuilder took 361.24ms. Allocated memory was 111.1MB in the beginning and 134.2MB in the end (delta: 23.1MB). Free memory was 58.0MB in the beginning and 102.3MB in the end (delta: -44.3MB). Peak memory consumption was 17.1MB. Max. memory is 16.1GB.
 * TraceAbstraction took 8183.57ms. Allocated memory was 134.2MB in the beginning and 790.6MB in the end (delta: 656.4MB). Free memory was 101.6MB in the beginning and 387.8MB in the end (delta: -286.2MB). Peak memory consumption was 369.9MB. Max. memory is 16.1GB.
 * Witness Printer took 2.52ms. Allocated memory is still 790.6MB. Free memory is still 387.8MB. 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: 1.5s, 104 PlacesBefore, 37 PlacesAfterwards, 105 TransitionsBefore, 36 TransitionsAfterwards, 2500 CoEnabledTransitionPairs, 6 FixpointIterations, 29 TrivialSequentialCompositions, 43 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 1 ConcurrentYvCompositions, 2 ChoiceCompositions, 78 TotalNumberOfCompositions, 7962 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 3934, independent: 3606, independent conditional: 0, independent unconditional: 3606, dependent: 328, dependent conditional: 0, dependent unconditional: 328, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 1262, independent: 1205, independent conditional: 0, independent unconditional: 1205, dependent: 57, dependent conditional: 0, dependent unconditional: 57, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 3934, independent: 2401, independent conditional: 0, independent unconditional: 2401, dependent: 271, dependent conditional: 0, dependent unconditional: 271, unknown: 1262, unknown conditional: 0, unknown unconditional: 1262] , Statistics on independence cache: Total cache size (in pairs): 169, Positive cache size: 140, Positive conditional cache size: 0, Positive unconditional cache size: 140, Negative cache size: 29, Negative conditional cache size: 0, Negative unconditional cache size: 29, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 1.4s, 132 PlacesBefore, 57 PlacesAfterwards, 131 TransitionsBefore, 54 TransitionsAfterwards, 6300 CoEnabledTransitionPairs, 6 FixpointIterations, 31 TrivialSequentialCompositions, 50 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 1 ConcurrentYvCompositions, 2 ChoiceCompositions, 87 TotalNumberOfCompositions, 24128 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 7085, independent: 6561, independent conditional: 0, independent unconditional: 6561, dependent: 524, dependent conditional: 0, dependent unconditional: 524, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 2845, independent: 2765, independent conditional: 0, independent unconditional: 2765, dependent: 80, dependent conditional: 0, dependent unconditional: 80, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 7085, independent: 3796, independent conditional: 0, independent unconditional: 3796, dependent: 444, dependent conditional: 0, dependent unconditional: 444, unknown: 2845, unknown conditional: 0, unknown unconditional: 2845] , Statistics on independence cache: Total cache size (in pairs): 373, Positive cache size: 320, Positive conditional cache size: 0, Positive unconditional cache size: 320, Negative cache size: 53, Negative conditional cache size: 0, Negative unconditional cache size: 53, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - DataRaceFoundResult [Line: 685]: Data race detected
    Data race detected
The following path leads to a data race: 
[L678]               0  int threads_alive = 0;
[L679]               0  int data = 0;
[L680]               0  pthread_mutex_t data_mutex = { { 0, 0, 0, PTHREAD_MUTEX_TIMED_NP, 0, { { 0, 0 } } } };
[L689]               0  int breads_total = __VERIFIER_nondet_int();
[L690]  CALL         0  assume_abort_if_not(breads_total >= 0)
[L675]  COND FALSE   0  !(!cond)
[L690]  RET          0  assume_abort_if_not(breads_total >= 0)
[L691]               0  int i = 0;
        VAL             [breads_total=2, data=0, data_mutex={1:0}, i=0, threads_alive=0]
[L691]  COND TRUE    0  i < breads_total
[L692]               0  threads_alive++
[L693]               0  pthread_t tid;
[L694]  FCALL, FORK  0  pthread_create(&tid, ((void *)0), &thread, ((void *)0))
        VAL             [arg={0:0}, breads_total=2, data=0, data_mutex={1:0}, i=0, pthread_create(&tid, ((void *)0), &thread, ((void *)0))=0, threads_alive=1, tid={5:0}]
[L695]  EXPR         0  \read(tid)
[L695]               0  pthread_detach(tid)
[L691]               0  i++
[L691]  COND TRUE    0  i < breads_total
[L692]               0  threads_alive++
        VAL             [arg={0:0}, breads_total=2, data=0, data_mutex={1:0}, i=1, threads_alive=1]
[L683]               1  data = __VERIFIER_nondet_int()
[L685]               1  threads_alive--
        VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, threads_alive=1]
[L692]               0  threads_alive++
        VAL             [arg={0:0}, arg={0:0}, breads_total=2, data=0, data_mutex={1:0}, i=1, threads_alive=2, threads_alive++=1threads_alive++=27]
[L685]               1  threads_alive--
        VAL             [arg={0:0}, arg={0:0}, data=0, data_mutex={1:0}, threads_alive=2]

Now there is a data race on ~threads_alive~0 between 
	C: threads_alive++ [692]
and
	C: threads_alive-- [685]

  - UnprovableResult [Line: 692]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 697]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 698]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 692]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 695]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 694]: 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: 683]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 685]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - StatisticsResult: Ultimate Automizer benchmark data with 1 thread instances
    CFG has 3 procedures, 128 locations, 12 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 2.3s, OverallIterations: 5, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.3s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 1.6s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 107 SdHoareTripleChecker+Valid, 0.1s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 46 mSDsluCounter, 5 SdHoareTripleChecker+Invalid, 0.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 21 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 193 IncrementalHoareTripleChecker+Invalid, 214 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 21 mSolverCounterUnsat, 5 mSDtfsCounter, 193 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 8 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=225occurred in iteration=4, InterpolantAutomatonStates: 12, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.0s SatisfiabilityAnalysisTime, 0.1s InterpolantComputationTime, 44 NumberOfCodeBlocks, 44 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 24 ConstructedInterpolants, 0 QuantifiedInterpolants, 32 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 4 InterpolantComputations, 4 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
  - StatisticsResult: Ultimate Automizer benchmark data with 2 thread instances
    CFG has 4 procedures, 154 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.8s, OverallIterations: 8, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 3.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 1.4s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 360 SdHoareTripleChecker+Valid, 0.5s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 207 mSDsluCounter, 24 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 3 mSDsCounter, 40 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 657 IncrementalHoareTripleChecker+Invalid, 697 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 40 mSolverCounterUnsat, 21 mSDtfsCounter, 657 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 36 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=574occurred in iteration=7, InterpolantAutomatonStates: 25, 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.2s InterpolantComputationTime, 129 NumberOfCodeBlocks, 129 NumberOfCodeBlocksAsserted, 9 NumberOfCheckSat, 99 ConstructedInterpolants, 0 QuantifiedInterpolants, 163 SizeOfPredicates, 2 NumberOfNonLiveVariables, 124 ConjunctsInSsa, 4 ConjunctsInUnsatCore, 8 InterpolantComputations, 7 PerfectInterpolantSequences, 8/9 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2024-03-11 23:19:31,680 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
--- End real Ultimate output ---

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