./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/semaphore-posix-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/semaphore-posix-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 d87a8225f17a9e0b8d5a6edaefcb34036eb1eea97d985b1c80b4cadc5f4bc42e
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2024-02-28 18:38:30,298 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2024-02-28 18:38:30,300 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2024-02-28 18:38:30,320 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2024-02-28 18:38:30,320 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2024-02-28 18:38:30,321 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2024-02-28 18:38:30,322 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2024-02-28 18:38:30,323 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2024-02-28 18:38:30,324 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2024-02-28 18:38:30,325 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2024-02-28 18:38:30,326 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2024-02-28 18:38:30,327 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2024-02-28 18:38:30,327 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2024-02-28 18:38:30,328 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2024-02-28 18:38:30,329 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2024-02-28 18:38:30,330 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2024-02-28 18:38:30,331 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2024-02-28 18:38:30,331 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2024-02-28 18:38:30,332 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2024-02-28 18:38:30,334 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2024-02-28 18:38:30,334 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2024-02-28 18:38:30,335 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2024-02-28 18:38:30,336 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2024-02-28 18:38:30,337 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2024-02-28 18:38:30,339 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2024-02-28 18:38:30,340 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2024-02-28 18:38:30,340 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2024-02-28 18:38:30,340 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2024-02-28 18:38:30,341 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2024-02-28 18:38:30,341 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2024-02-28 18:38:30,342 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2024-02-28 18:38:30,342 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2024-02-28 18:38:30,343 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2024-02-28 18:38:30,343 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2024-02-28 18:38:30,344 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2024-02-28 18:38:30,344 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2024-02-28 18:38:30,344 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2024-02-28 18:38:30,344 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2024-02-28 18:38:30,345 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2024-02-28 18:38:30,345 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2024-02-28 18:38:30,346 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2024-02-28 18:38:30,346 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2024-02-28 18:38:30,364 INFO  L113        SettingsManager]: Loading preferences was successful
[2024-02-28 18:38:30,364 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2024-02-28 18:38:30,364 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2024-02-28 18:38:30,367 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2024-02-28 18:38:30,368 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2024-02-28 18:38:30,368 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2024-02-28 18:38:30,369 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * Use SBE=true
[2024-02-28 18:38:30,369 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * sizeof long=4
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2024-02-28 18:38:30,369 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * sizeof long double=12
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2024-02-28 18:38:30,370 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2024-02-28 18:38:30,370 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2024-02-28 18:38:30,371 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2024-02-28 18:38:30,371 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2024-02-28 18:38:30,371 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2024-02-28 18:38:30,371 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2024-02-28 18:38:30,371 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2024-02-28 18:38:30,371 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2024-02-28 18:38:30,371 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2024-02-28 18:38:30,372 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2024-02-28 18:38:30,372 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2024-02-28 18:38:30,372 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2024-02-28 18:38:30,372 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2024-02-28 18:38:30,372 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2024-02-28 18:38:30,372 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2024-02-28 18:38:30,372 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 -> d87a8225f17a9e0b8d5a6edaefcb34036eb1eea97d985b1c80b4cadc5f4bc42e
[2024-02-28 18:38:30,542 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2024-02-28 18:38:30,572 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2024-02-28 18:38:30,574 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2024-02-28 18:38:30,574 INFO  L271        PluginConnector]: Initializing CDTParser...
[2024-02-28 18:38:30,575 INFO  L275        PluginConnector]: CDTParser initialized
[2024-02-28 18:38:30,576 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/semaphore-posix-race.i
[2024-02-28 18:38:31,585 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2024-02-28 18:38:31,793 INFO  L351              CDTParser]: Found 1 translation units.
[2024-02-28 18:38:31,793 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/semaphore-posix-race.i
[2024-02-28 18:38:31,804 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/5ded29a9f/113e4a0eabff4f7fa05b4ec3c7c2c771/FLAG9553fc9b7
[2024-02-28 18:38:31,814 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/5ded29a9f/113e4a0eabff4f7fa05b4ec3c7c2c771
[2024-02-28 18:38:31,816 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2024-02-28 18:38:31,817 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2024-02-28 18:38:31,817 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2024-02-28 18:38:31,817 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2024-02-28 18:38:31,820 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2024-02-28 18:38:31,820 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 28.02 06:38:31" (1/1) ...
[2024-02-28 18:38:31,821 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@16eda843 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:31, skipping insertion in model container
[2024-02-28 18:38:31,821 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 28.02 06:38:31" (1/1) ...
[2024-02-28 18:38:31,826 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2024-02-28 18:38:31,855 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2024-02-28 18:38:31,965 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2024-02-28 18:38:32,105 WARN  L623        FunctionHandler]: Unknown extern function sem_wait
[2024-02-28 18:38:32,110 WARN  L623        FunctionHandler]: Unknown extern function sem_post
[2024-02-28 18:38:32,112 WARN  L623        FunctionHandler]: Unknown extern function sem_init
[2024-02-28 18:38:32,118 WARN  L623        FunctionHandler]: Unknown extern function sem_post
[2024-02-28 18:38:32,121 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2024-02-28 18:38:32,129 INFO  L203         MainTranslator]: Completed pre-run
[2024-02-28 18:38:32,138 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2024-02-28 18:38:32,159 WARN  L623        FunctionHandler]: Unknown extern function sem_wait
[2024-02-28 18:38:32,160 WARN  L623        FunctionHandler]: Unknown extern function sem_post
[2024-02-28 18:38:32,160 WARN  L623        FunctionHandler]: Unknown extern function sem_init
[2024-02-28 18:38:32,163 WARN  L623        FunctionHandler]: Unknown extern function sem_post
[2024-02-28 18:38:32,166 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2024-02-28 18:38:32,233 INFO  L208         MainTranslator]: Completed translation
[2024-02-28 18:38:32,233 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32 WrapperNode
[2024-02-28 18:38:32,233 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2024-02-28 18:38:32,234 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2024-02-28 18:38:32,234 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2024-02-28 18:38:32,234 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2024-02-28 18:38:32,239 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,254 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,272 INFO  L138                Inliner]: procedures = 278, calls = 37, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 99
[2024-02-28 18:38:32,272 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2024-02-28 18:38:32,272 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2024-02-28 18:38:32,272 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2024-02-28 18:38:32,273 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2024-02-28 18:38:32,280 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,280 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,284 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,284 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,290 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,292 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,294 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,295 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,297 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2024-02-28 18:38:32,298 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2024-02-28 18:38:32,298 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2024-02-28 18:38:32,298 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2024-02-28 18:38:32,299 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (1/1) ...
[2024-02-28 18:38:32,303 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2024-02-28 18:38:32,311 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2024-02-28 18:38:32,325 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-02-28 18:38:32,328 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-02-28 18:38:32,350 INFO  L130     BoogieDeclarations]: Found specification of procedure sem_init
[2024-02-28 18:38:32,350 INFO  L130     BoogieDeclarations]: Found specification of procedure sem_post
[2024-02-28 18:38:32,350 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure sem_wait
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2024-02-28 18:38:32,351 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2024-02-28 18:38:32,351 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2024-02-28 18:38:32,352 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2024-02-28 18:38:32,352 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2024-02-28 18:38:32,353 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2024-02-28 18:38:32,470 INFO  L235             CfgBuilder]: Building ICFG
[2024-02-28 18:38:32,472 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2024-02-28 18:38:32,670 INFO  L276             CfgBuilder]: Performing block encoding
[2024-02-28 18:38:32,677 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2024-02-28 18:38:32,677 INFO  L300             CfgBuilder]: Removed 2 assume(true) statements.
[2024-02-28 18:38:32,679 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.02 06:38:32 BoogieIcfgContainer
[2024-02-28 18:38:32,679 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2024-02-28 18:38:32,681 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2024-02-28 18:38:32,681 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2024-02-28 18:38:32,683 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2024-02-28 18:38:32,683 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 28.02 06:38:31" (1/3) ...
[2024-02-28 18:38:32,684 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5b945235 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.02 06:38:32, skipping insertion in model container
[2024-02-28 18:38:32,684 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 28.02 06:38:32" (2/3) ...
[2024-02-28 18:38:32,684 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5b945235 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.02 06:38:32, skipping insertion in model container
[2024-02-28 18:38:32,684 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.02 06:38:32" (3/3) ...
[2024-02-28 18:38:32,685 INFO  L112   eAbstractionObserver]: Analyzing ICFG semaphore-posix-race.i
[2024-02-28 18:38:32,691 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2024-02-28 18:38:32,698 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2024-02-28 18:38:32,698 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 5 error locations.
[2024-02-28 18:38:32,698 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2024-02-28 18:38:32,736 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2024-02-28 18:38:32,763 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 125 places, 126 transitions, 260 flow
[2024-02-28 18:38:32,824 INFO  L130       PetriNetUnfolder]: 6/175 cut-off events.
[2024-02-28 18:38:32,824 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2024-02-28 18:38:32,828 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 181 conditions, 175 events. 6/175 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 312 event pairs, 0 based on Foata normal form. 0/157 useless extension candidates. Maximal degree in co-relation 95. Up to 4 conditions per place. 
[2024-02-28 18:38:32,828 INFO  L82        GeneralOperation]: Start removeDead. Operand has 125 places, 126 transitions, 260 flow
[2024-02-28 18:38:32,832 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 125 places, 126 transitions, 260 flow
[2024-02-28 18:38:32,834 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-02-28 18:38:32,842 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 125 places, 126 transitions, 260 flow
[2024-02-28 18:38:32,844 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 125 places, 126 transitions, 260 flow
[2024-02-28 18:38:32,844 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 125 places, 126 transitions, 260 flow
[2024-02-28 18:38:32,871 INFO  L130       PetriNetUnfolder]: 6/175 cut-off events.
[2024-02-28 18:38:32,871 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2024-02-28 18:38:32,871 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 181 conditions, 175 events. 6/175 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 312 event pairs, 0 based on Foata normal form. 0/157 useless extension candidates. Maximal degree in co-relation 95. Up to 4 conditions per place. 
[2024-02-28 18:38:32,873 INFO  L119        LiptonReduction]: Number of co-enabled transitions 1904
[2024-02-28 18:38:38,332 INFO  L134        LiptonReduction]: Checked pairs total: 1485
[2024-02-28 18:38:38,332 INFO  L136        LiptonReduction]: Total number of compositions: 129
[2024-02-28 18:38:38,344 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-02-28 18:38:38,349 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;@40775315, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-02-28 18:38:38,349 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 7 error locations.
[2024-02-28 18:38:38,351 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2024-02-28 18:38:38,351 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-02-28 18:38:38,351 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:38,352 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2024-02-28 18:38:38,352 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 4 more)] ===
[2024-02-28 18:38:38,356 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:38,356 INFO  L85        PathProgramCache]: Analyzing trace with hash 14451, now seen corresponding path program 1 times
[2024-02-28 18:38:38,363 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:38,363 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1547164076]
[2024-02-28 18:38:38,364 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:38,364 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:38,439 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:38,486 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 18:38:38,486 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:38,487 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1547164076]
[2024-02-28 18:38:38,487 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1547164076] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:38,488 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:38,488 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2024-02-28 18:38:38,489 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1977619105]
[2024-02-28 18:38:38,489 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:38,494 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2024-02-28 18:38:38,495 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:38,509 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2024-02-28 18:38:38,510 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2024-02-28 18:38:38,512 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 121 out of 255
[2024-02-28 18:38:38,514 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 18 places, 16 transitions, 40 flow. Second operand  has 2 states, 2 states have (on average 122.0) internal successors, (244), 2 states have internal predecessors, (244), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:38,514 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:38,514 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 121 of 255
[2024-02-28 18:38:38,515 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:38,547 INFO  L130       PetriNetUnfolder]: 6/26 cut-off events.
[2024-02-28 18:38:38,547 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2024-02-28 18:38:38,547 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 58 conditions, 26 events. 6/26 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 54 event pairs, 5 based on Foata normal form. 0/20 useless extension candidates. Maximal degree in co-relation 32. Up to 25 conditions per place. 
[2024-02-28 18:38:38,548 INFO  L137   encePairwiseOnDemand]: 250/255 looper letters, 5 selfloop transitions, 0 changer transitions 5/11 dead transitions.
[2024-02-28 18:38:38,548 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 14 places, 11 transitions, 50 flow
[2024-02-28 18:38:38,549 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2024-02-28 18:38:38,551 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2024-02-28 18:38:38,556 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 257 transitions.
[2024-02-28 18:38:38,558 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.503921568627451
[2024-02-28 18:38:38,559 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 257 transitions.
[2024-02-28 18:38:38,559 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 257 transitions.
[2024-02-28 18:38:38,560 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:38,562 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 257 transitions.
[2024-02-28 18:38:38,564 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 128.5) internal successors, (257), 2 states have internal predecessors, (257), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:38,568 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 255.0) internal successors, (765), 3 states have internal predecessors, (765), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:38,568 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 255.0) internal successors, (765), 3 states have internal predecessors, (765), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:38,569 INFO  L175             Difference]: Start difference. First operand has 18 places, 16 transitions, 40 flow. Second operand 2 states and 257 transitions.
[2024-02-28 18:38:38,570 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 14 places, 11 transitions, 50 flow
[2024-02-28 18:38:38,572 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 14 places, 11 transitions, 50 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 18:38:38,572 INFO  L231             Difference]: Finished difference. Result has 14 places, 6 transitions, 17 flow
[2024-02-28 18:38:38,574 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=255, PETRI_DIFFERENCE_MINUEND_FLOW=30, PETRI_DIFFERENCE_MINUEND_PLACES=13, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=11, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=11, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=17, PETRI_PLACES=14, PETRI_TRANSITIONS=6}
[2024-02-28 18:38:38,577 INFO  L288   CegarLoopForPetriNet]: 18 programPoint places, -4 predicate places.
[2024-02-28 18:38:38,577 INFO  L495      AbstractCegarLoop]: Abstraction has has 14 places, 6 transitions, 17 flow
[2024-02-28 18:38:38,577 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 122.0) internal successors, (244), 2 states have internal predecessors, (244), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:38,577 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:38,577 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1]
[2024-02-28 18:38:38,578 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2024-02-28 18:38:38,578 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 4 more)] ===
[2024-02-28 18:38:38,578 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:38,578 INFO  L85        PathProgramCache]: Analyzing trace with hash 469065154, now seen corresponding path program 1 times
[2024-02-28 18:38:38,578 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:38,579 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [258780796]
[2024-02-28 18:38:38,579 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:38,579 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:38,622 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 18:38:38,623 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-02-28 18:38:38,649 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 18:38:38,666 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-02-28 18:38:38,666 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-02-28 18:38:38,667 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (6 of 7 remaining)
[2024-02-28 18:38:38,668 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (5 of 7 remaining)
[2024-02-28 18:38:38,669 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (4 of 7 remaining)
[2024-02-28 18:38:38,669 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (3 of 7 remaining)
[2024-02-28 18:38:38,669 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (2 of 7 remaining)
[2024-02-28 18:38:38,669 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 7 remaining)
[2024-02-28 18:38:38,669 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 7 remaining)
[2024-02-28 18:38:38,669 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2024-02-28 18:38:38,670 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1]
[2024-02-28 18:38:38,671 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-02-28 18:38:38,672 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2024-02-28 18:38:38,686 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2024-02-28 18:38:38,690 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 145 places, 145 transitions, 308 flow
[2024-02-28 18:38:38,720 INFO  L130       PetriNetUnfolder]: 11/293 cut-off events.
[2024-02-28 18:38:38,720 INFO  L131       PetriNetUnfolder]: For 6/6 co-relation queries the response was YES.
[2024-02-28 18:38:38,721 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 307 conditions, 293 events. 11/293 cut-off events. For 6/6 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 653 event pairs, 0 based on Foata normal form. 0/261 useless extension candidates. Maximal degree in co-relation 177. Up to 8 conditions per place. 
[2024-02-28 18:38:38,721 INFO  L82        GeneralOperation]: Start removeDead. Operand has 145 places, 145 transitions, 308 flow
[2024-02-28 18:38:38,722 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 145 places, 145 transitions, 308 flow
[2024-02-28 18:38:38,722 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-02-28 18:38:38,723 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 145 places, 145 transitions, 308 flow
[2024-02-28 18:38:38,723 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 145 places, 145 transitions, 308 flow
[2024-02-28 18:38:38,723 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 145 places, 145 transitions, 308 flow
[2024-02-28 18:38:38,756 INFO  L130       PetriNetUnfolder]: 11/293 cut-off events.
[2024-02-28 18:38:38,756 INFO  L131       PetriNetUnfolder]: For 6/6 co-relation queries the response was YES.
[2024-02-28 18:38:38,756 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 307 conditions, 293 events. 11/293 cut-off events. For 6/6 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 653 event pairs, 0 based on Foata normal form. 0/261 useless extension candidates. Maximal degree in co-relation 177. Up to 8 conditions per place. 
[2024-02-28 18:38:38,759 INFO  L119        LiptonReduction]: Number of co-enabled transitions 4828
[2024-02-28 18:38:43,690 INFO  L134        LiptonReduction]: Checked pairs total: 6140
[2024-02-28 18:38:43,691 INFO  L136        LiptonReduction]: Total number of compositions: 136
[2024-02-28 18:38:43,694 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-02-28 18:38:43,696 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;@40775315, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-02-28 18:38:43,696 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 8 error locations.
[2024-02-28 18:38:43,698 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2024-02-28 18:38:43,698 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-02-28 18:38:43,698 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:43,698 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2024-02-28 18:38:43,699 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 18:38:43,699 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:43,699 INFO  L85        PathProgramCache]: Analyzing trace with hash 24054, now seen corresponding path program 1 times
[2024-02-28 18:38:43,699 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:43,700 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1768071339]
[2024-02-28 18:38:43,700 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:43,700 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:43,710 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:43,723 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 18:38:43,723 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:43,723 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1768071339]
[2024-02-28 18:38:43,723 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1768071339] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:43,723 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:43,723 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2024-02-28 18:38:43,724 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1795186638]
[2024-02-28 18:38:43,724 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:43,724 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2024-02-28 18:38:43,724 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:43,724 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2024-02-28 18:38:43,724 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2024-02-28 18:38:43,725 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 138 out of 281
[2024-02-28 18:38:43,726 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 29 places, 26 transitions, 70 flow. Second operand  has 2 states, 2 states have (on average 139.0) internal successors, (278), 2 states have internal predecessors, (278), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:43,726 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:43,726 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 138 of 281
[2024-02-28 18:38:43,726 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:43,805 INFO  L130       PetriNetUnfolder]: 168/362 cut-off events.
[2024-02-28 18:38:43,806 INFO  L131       PetriNetUnfolder]: For 30/30 co-relation queries the response was YES.
[2024-02-28 18:38:43,806 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 712 conditions, 362 events. 168/362 cut-off events. For 30/30 co-relation queries the response was YES. Maximal size of possible extension queue 29. Compared 1552 event pairs, 162 based on Foata normal form. 0/315 useless extension candidates. Maximal degree in co-relation 147. Up to 315 conditions per place. 
[2024-02-28 18:38:43,808 INFO  L137   encePairwiseOnDemand]: 277/281 looper letters, 17 selfloop transitions, 0 changer transitions 0/22 dead transitions.
[2024-02-28 18:38:43,808 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 26 places, 22 transitions, 96 flow
[2024-02-28 18:38:43,808 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2024-02-28 18:38:43,808 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2024-02-28 18:38:43,809 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 297 transitions.
[2024-02-28 18:38:43,810 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5284697508896797
[2024-02-28 18:38:43,810 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 297 transitions.
[2024-02-28 18:38:43,810 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 297 transitions.
[2024-02-28 18:38:43,810 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:43,811 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 297 transitions.
[2024-02-28 18:38:43,812 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 148.5) internal successors, (297), 2 states have internal predecessors, (297), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:43,813 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 281.0) internal successors, (843), 3 states have internal predecessors, (843), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:43,813 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 281.0) internal successors, (843), 3 states have internal predecessors, (843), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:43,813 INFO  L175             Difference]: Start difference. First operand has 29 places, 26 transitions, 70 flow. Second operand 2 states and 297 transitions.
[2024-02-28 18:38:43,814 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 26 places, 22 transitions, 96 flow
[2024-02-28 18:38:43,814 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 26 places, 22 transitions, 96 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 18:38:43,815 INFO  L231             Difference]: Finished difference. Result has 26 places, 22 transitions, 62 flow
[2024-02-28 18:38:43,815 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=281, PETRI_DIFFERENCE_MINUEND_FLOW=62, PETRI_DIFFERENCE_MINUEND_PLACES=25, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=22, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=22, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=62, PETRI_PLACES=26, PETRI_TRANSITIONS=22}
[2024-02-28 18:38:43,815 INFO  L288   CegarLoopForPetriNet]: 29 programPoint places, -3 predicate places.
[2024-02-28 18:38:43,815 INFO  L495      AbstractCegarLoop]: Abstraction has has 26 places, 22 transitions, 62 flow
[2024-02-28 18:38:43,816 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 139.0) internal successors, (278), 2 states have internal predecessors, (278), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:43,816 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:43,816 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1]
[2024-02-28 18:38:43,816 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2024-02-28 18:38:43,816 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 18:38:43,816 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:43,817 INFO  L85        PathProgramCache]: Analyzing trace with hash 756661494, now seen corresponding path program 1 times
[2024-02-28 18:38:43,817 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:43,817 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1864829814]
[2024-02-28 18:38:43,817 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:43,817 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:43,830 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:43,883 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 18:38:43,883 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:43,883 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1864829814]
[2024-02-28 18:38:43,883 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1864829814] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:43,883 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:43,884 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 18:38:43,884 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1237481751]
[2024-02-28 18:38:43,884 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:43,884 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 18:38:43,884 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:43,885 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 18:38:43,885 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 18:38:43,901 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 132 out of 281
[2024-02-28 18:38:43,902 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 26 places, 22 transitions, 62 flow. Second operand  has 3 states, 3 states have (on average 134.0) internal successors, (402), 3 states have internal predecessors, (402), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:43,902 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:43,902 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 132 of 281
[2024-02-28 18:38:43,902 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:43,994 INFO  L130       PetriNetUnfolder]: 208/427 cut-off events.
[2024-02-28 18:38:43,994 INFO  L131       PetriNetUnfolder]: For 35/35 co-relation queries the response was YES.
[2024-02-28 18:38:43,995 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 850 conditions, 427 events. 208/427 cut-off events. For 35/35 co-relation queries the response was YES. Maximal size of possible extension queue 35. Compared 1875 event pairs, 147 based on Foata normal form. 0/354 useless extension candidates. Maximal degree in co-relation 845. Up to 316 conditions per place. 
[2024-02-28 18:38:43,996 INFO  L137   encePairwiseOnDemand]: 277/281 looper letters, 25 selfloop transitions, 3 changer transitions 2/34 dead transitions.
[2024-02-28 18:38:43,996 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 28 places, 34 transitions, 154 flow
[2024-02-28 18:38:43,997 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 18:38:43,997 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 18:38:43,998 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 427 transitions.
[2024-02-28 18:38:43,998 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5065243179122183
[2024-02-28 18:38:43,999 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 427 transitions.
[2024-02-28 18:38:43,999 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 427 transitions.
[2024-02-28 18:38:43,999 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:43,999 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 427 transitions.
[2024-02-28 18:38:44,000 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 142.33333333333334) internal successors, (427), 3 states have internal predecessors, (427), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,003 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 281.0) internal successors, (1124), 4 states have internal predecessors, (1124), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,003 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 281.0) internal successors, (1124), 4 states have internal predecessors, (1124), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,003 INFO  L175             Difference]: Start difference. First operand has 26 places, 22 transitions, 62 flow. Second operand 3 states and 427 transitions.
[2024-02-28 18:38:44,003 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 28 places, 34 transitions, 154 flow
[2024-02-28 18:38:44,004 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 28 places, 34 transitions, 154 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 18:38:44,005 INFO  L231             Difference]: Finished difference. Result has 29 places, 24 transitions, 81 flow
[2024-02-28 18:38:44,005 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=281, PETRI_DIFFERENCE_MINUEND_FLOW=62, PETRI_DIFFERENCE_MINUEND_PLACES=26, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=22, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=19, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=81, PETRI_PLACES=29, PETRI_TRANSITIONS=24}
[2024-02-28 18:38:44,005 INFO  L288   CegarLoopForPetriNet]: 29 programPoint places, 0 predicate places.
[2024-02-28 18:38:44,005 INFO  L495      AbstractCegarLoop]: Abstraction has has 29 places, 24 transitions, 81 flow
[2024-02-28 18:38:44,006 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 134.0) internal successors, (402), 3 states have internal predecessors, (402), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,006 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:44,006 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 18:38:44,006 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2024-02-28 18:38:44,006 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 18:38:44,007 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:44,007 INFO  L85        PathProgramCache]: Analyzing trace with hash -1681885421, now seen corresponding path program 1 times
[2024-02-28 18:38:44,007 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:44,007 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1890394019]
[2024-02-28 18:38:44,007 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:44,007 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:44,022 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:44,044 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2024-02-28 18:38:44,045 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:44,045 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1890394019]
[2024-02-28 18:38:44,045 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1890394019] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:44,045 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:44,045 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 18:38:44,045 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2041764105]
[2024-02-28 18:38:44,046 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:44,046 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 18:38:44,046 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:44,046 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 18:38:44,047 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 18:38:44,057 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 132 out of 281
[2024-02-28 18:38:44,058 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 29 places, 24 transitions, 81 flow. Second operand  has 3 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-02-28 18:38:44,058 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:44,058 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 132 of 281
[2024-02-28 18:38:44,058 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:44,160 INFO  L130       PetriNetUnfolder]: 217/430 cut-off events.
[2024-02-28 18:38:44,160 INFO  L131       PetriNetUnfolder]: For 139/143 co-relation queries the response was YES.
[2024-02-28 18:38:44,161 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1038 conditions, 430 events. 217/430 cut-off events. For 139/143 co-relation queries the response was YES. Maximal size of possible extension queue 30. Compared 1794 event pairs, 149 based on Foata normal form. 0/353 useless extension candidates. Maximal degree in co-relation 1031. Up to 342 conditions per place. 
[2024-02-28 18:38:44,162 INFO  L137   encePairwiseOnDemand]: 277/281 looper letters, 25 selfloop transitions, 4 changer transitions 2/35 dead transitions.
[2024-02-28 18:38:44,162 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 31 places, 35 transitions, 173 flow
[2024-02-28 18:38:44,162 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 18:38:44,162 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 18:38:44,163 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 426 transitions.
[2024-02-28 18:38:44,163 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.505338078291815
[2024-02-28 18:38:44,164 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 426 transitions.
[2024-02-28 18:38:44,164 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 426 transitions.
[2024-02-28 18:38:44,164 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:44,164 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 426 transitions.
[2024-02-28 18:38:44,165 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 142.0) internal successors, (426), 3 states have internal predecessors, (426), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,167 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 281.0) internal successors, (1124), 4 states have internal predecessors, (1124), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,167 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 281.0) internal successors, (1124), 4 states have internal predecessors, (1124), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:44,167 INFO  L175             Difference]: Start difference. First operand has 29 places, 24 transitions, 81 flow. Second operand 3 states and 426 transitions.
[2024-02-28 18:38:44,167 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 31 places, 35 transitions, 173 flow
[2024-02-28 18:38:44,168 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 30 places, 35 transitions, 169 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-02-28 18:38:44,169 INFO  L231             Difference]: Finished difference. Result has 31 places, 26 transitions, 102 flow
[2024-02-28 18:38:44,169 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=281, PETRI_DIFFERENCE_MINUEND_FLOW=78, PETRI_DIFFERENCE_MINUEND_PLACES=28, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=24, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=20, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=102, PETRI_PLACES=31, PETRI_TRANSITIONS=26}
[2024-02-28 18:38:44,170 INFO  L288   CegarLoopForPetriNet]: 29 programPoint places, 2 predicate places.
[2024-02-28 18:38:44,170 INFO  L495      AbstractCegarLoop]: Abstraction has has 31 places, 26 transitions, 102 flow
[2024-02-28 18:38:44,170 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 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-02-28 18:38:44,170 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:44,170 INFO  L209   CegarLoopForPetriNet]: trace histogram [3, 2, 2, 1, 1, 1, 1]
[2024-02-28 18:38:44,171 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2024-02-28 18:38:44,171 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-02-28 18:38:44,171 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:44,171 INFO  L85        PathProgramCache]: Analyzing trace with hash -603955878, now seen corresponding path program 1 times
[2024-02-28 18:38:44,171 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:44,171 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1665648130]
[2024-02-28 18:38:44,171 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:44,171 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:44,191 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 18:38:44,191 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-02-28 18:38:44,202 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 18:38:44,208 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-02-28 18:38:44,208 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-02-28 18:38:44,208 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (7 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (6 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (5 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (4 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (3 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 8 remaining)
[2024-02-28 18:38:44,209 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 8 remaining)
[2024-02-28 18:38:44,210 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2024-02-28 18:38:44,210 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2024-02-28 18:38:44,210 WARN  L233   ceAbstractionStarter]: 2 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-02-28 18:38:44,210 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 3 thread instances.
[2024-02-28 18:38:44,224 INFO  L144    ThreadInstanceAdder]: Constructed 3 joinOtherThreadTransitions.
[2024-02-28 18:38:44,226 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 165 places, 164 transitions, 358 flow
[2024-02-28 18:38:44,263 INFO  L130       PetriNetUnfolder]: 21/490 cut-off events.
[2024-02-28 18:38:44,263 INFO  L131       PetriNetUnfolder]: For 19/19 co-relation queries the response was YES.
[2024-02-28 18:38:44,264 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 518 conditions, 490 events. 21/490 cut-off events. For 19/19 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 1435 event pairs, 1 based on Foata normal form. 0/434 useless extension candidates. Maximal degree in co-relation 301. Up to 16 conditions per place. 
[2024-02-28 18:38:44,264 INFO  L82        GeneralOperation]: Start removeDead. Operand has 165 places, 164 transitions, 358 flow
[2024-02-28 18:38:44,266 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 165 places, 164 transitions, 358 flow
[2024-02-28 18:38:44,266 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-02-28 18:38:44,266 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 165 places, 164 transitions, 358 flow
[2024-02-28 18:38:44,266 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 165 places, 164 transitions, 358 flow
[2024-02-28 18:38:44,266 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 165 places, 164 transitions, 358 flow
[2024-02-28 18:38:44,302 INFO  L130       PetriNetUnfolder]: 21/490 cut-off events.
[2024-02-28 18:38:44,302 INFO  L131       PetriNetUnfolder]: For 19/19 co-relation queries the response was YES.
[2024-02-28 18:38:44,303 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 518 conditions, 490 events. 21/490 cut-off events. For 19/19 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 1435 event pairs, 1 based on Foata normal form. 0/434 useless extension candidates. Maximal degree in co-relation 301. Up to 16 conditions per place. 
[2024-02-28 18:38:44,310 INFO  L119        LiptonReduction]: Number of co-enabled transitions 8262
[2024-02-28 18:38:49,046 INFO  L134        LiptonReduction]: Checked pairs total: 11545
[2024-02-28 18:38:49,047 INFO  L136        LiptonReduction]: Total number of compositions: 149
[2024-02-28 18:38:49,049 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-02-28 18:38:49,050 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;@40775315, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-02-28 18:38:49,051 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 9 error locations.
[2024-02-28 18:38:49,052 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2024-02-28 18:38:49,052 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-02-28 18:38:49,052 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:49,053 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2024-02-28 18:38:49,053 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 18:38:49,053 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:49,053 INFO  L85        PathProgramCache]: Analyzing trace with hash 34676, now seen corresponding path program 1 times
[2024-02-28 18:38:49,053 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:49,053 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [601010604]
[2024-02-28 18:38:49,053 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:49,054 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:49,061 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:49,068 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 18:38:49,069 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:49,069 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [601010604]
[2024-02-28 18:38:49,069 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [601010604] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:49,069 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:49,069 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2024-02-28 18:38:49,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1141573495]
[2024-02-28 18:38:49,069 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:49,069 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2024-02-28 18:38:49,070 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:49,070 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2024-02-28 18:38:49,070 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2024-02-28 18:38:49,070 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 155 out of 313
[2024-02-28 18:38:49,071 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 36 places, 32 transitions, 94 flow. Second operand  has 2 states, 2 states have (on average 156.0) internal successors, (312), 2 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-02-28 18:38:49,071 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:49,071 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 155 of 313
[2024-02-28 18:38:49,071 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:49,277 INFO  L130       PetriNetUnfolder]: 1241/2159 cut-off events.
[2024-02-28 18:38:49,277 INFO  L131       PetriNetUnfolder]: For 277/277 co-relation queries the response was YES.
[2024-02-28 18:38:49,280 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 4296 conditions, 2159 events. 1241/2159 cut-off events. For 277/277 co-relation queries the response was YES. Maximal size of possible extension queue 108. Compared 11544 event pairs, 1210 based on Foata normal form. 0/1948 useless extension candidates. Maximal degree in co-relation 718. Up to 1932 conditions per place. 
[2024-02-28 18:38:49,286 INFO  L137   encePairwiseOnDemand]: 309/313 looper letters, 22 selfloop transitions, 0 changer transitions 0/28 dead transitions.
[2024-02-28 18:38:49,286 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 33 places, 28 transitions, 130 flow
[2024-02-28 18:38:49,288 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2024-02-28 18:38:49,288 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2024-02-28 18:38:49,289 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 336 transitions.
[2024-02-28 18:38:49,289 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.536741214057508
[2024-02-28 18:38:49,289 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 336 transitions.
[2024-02-28 18:38:49,289 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 336 transitions.
[2024-02-28 18:38:49,289 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:49,289 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 336 transitions.
[2024-02-28 18:38:49,290 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 168.0) internal successors, (336), 2 states have internal predecessors, (336), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,291 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 313.0) internal successors, (939), 3 states have internal predecessors, (939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,292 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 313.0) internal successors, (939), 3 states have internal predecessors, (939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,292 INFO  L175             Difference]: Start difference. First operand has 36 places, 32 transitions, 94 flow. Second operand 2 states and 336 transitions.
[2024-02-28 18:38:49,292 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 33 places, 28 transitions, 130 flow
[2024-02-28 18:38:49,292 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 33 places, 28 transitions, 130 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 18:38:49,293 INFO  L231             Difference]: Finished difference. Result has 33 places, 28 transitions, 86 flow
[2024-02-28 18:38:49,293 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=313, PETRI_DIFFERENCE_MINUEND_FLOW=86, PETRI_DIFFERENCE_MINUEND_PLACES=32, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=28, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=28, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=86, PETRI_PLACES=33, PETRI_TRANSITIONS=28}
[2024-02-28 18:38:49,294 INFO  L288   CegarLoopForPetriNet]: 36 programPoint places, -3 predicate places.
[2024-02-28 18:38:49,294 INFO  L495      AbstractCegarLoop]: Abstraction has has 33 places, 28 transitions, 86 flow
[2024-02-28 18:38:49,294 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 156.0) internal successors, (312), 2 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-02-28 18:38:49,294 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:49,294 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1]
[2024-02-28 18:38:49,294 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2024-02-28 18:38:49,294 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 18:38:49,295 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:49,295 INFO  L85        PathProgramCache]: Analyzing trace with hash 1986149906, now seen corresponding path program 1 times
[2024-02-28 18:38:49,295 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:49,295 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [4818024]
[2024-02-28 18:38:49,295 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:49,295 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:49,304 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:49,318 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-02-28 18:38:49,319 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:49,319 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [4818024]
[2024-02-28 18:38:49,319 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [4818024] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:49,319 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:49,319 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 18:38:49,319 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [18964438]
[2024-02-28 18:38:49,320 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:49,320 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 18:38:49,320 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:49,320 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 18:38:49,320 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 18:38:49,334 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 148 out of 313
[2024-02-28 18:38:49,334 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 33 places, 28 transitions, 86 flow. Second operand  has 3 states, 3 states have (on average 150.0) internal successors, (450), 3 states have internal predecessors, (450), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,334 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:49,334 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 148 of 313
[2024-02-28 18:38:49,334 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:49,599 INFO  L130       PetriNetUnfolder]: 1697/2841 cut-off events.
[2024-02-28 18:38:49,599 INFO  L131       PetriNetUnfolder]: For 348/348 co-relation queries the response was YES.
[2024-02-28 18:38:49,602 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 5693 conditions, 2841 events. 1697/2841 cut-off events. For 348/348 co-relation queries the response was YES. Maximal size of possible extension queue 147. Compared 15605 event pairs, 1246 based on Foata normal form. 0/2446 useless extension candidates. Maximal degree in co-relation 5687. Up to 2214 conditions per place. 
[2024-02-28 18:38:49,610 INFO  L137   encePairwiseOnDemand]: 308/313 looper letters, 36 selfloop transitions, 4 changer transitions 0/45 dead transitions.
[2024-02-28 18:38:49,610 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 35 places, 45 transitions, 218 flow
[2024-02-28 18:38:49,611 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 18:38:49,611 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 18:38:49,613 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 485 transitions.
[2024-02-28 18:38:49,613 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.516506922257721
[2024-02-28 18:38:49,613 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 485 transitions.
[2024-02-28 18:38:49,613 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 485 transitions.
[2024-02-28 18:38:49,614 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:49,614 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 485 transitions.
[2024-02-28 18:38:49,615 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 161.66666666666666) internal successors, (485), 3 states have internal predecessors, (485), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,617 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 313.0) internal successors, (1252), 4 states have internal predecessors, (1252), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,617 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 313.0) internal successors, (1252), 4 states have internal predecessors, (1252), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,617 INFO  L175             Difference]: Start difference. First operand has 33 places, 28 transitions, 86 flow. Second operand 3 states and 485 transitions.
[2024-02-28 18:38:49,617 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 35 places, 45 transitions, 218 flow
[2024-02-28 18:38:49,618 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 35 places, 45 transitions, 218 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-02-28 18:38:49,619 INFO  L231             Difference]: Finished difference. Result has 36 places, 31 transitions, 112 flow
[2024-02-28 18:38:49,619 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=313, PETRI_DIFFERENCE_MINUEND_FLOW=86, PETRI_DIFFERENCE_MINUEND_PLACES=33, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=28, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=24, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=112, PETRI_PLACES=36, PETRI_TRANSITIONS=31}
[2024-02-28 18:38:49,619 INFO  L288   CegarLoopForPetriNet]: 36 programPoint places, 0 predicate places.
[2024-02-28 18:38:49,620 INFO  L495      AbstractCegarLoop]: Abstraction has has 36 places, 31 transitions, 112 flow
[2024-02-28 18:38:49,620 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 150.0) internal successors, (450), 3 states have internal predecessors, (450), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,620 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:49,620 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 18:38:49,620 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2024-02-28 18:38:49,620 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 18:38:49,621 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:49,621 INFO  L85        PathProgramCache]: Analyzing trace with hash 1862432176, now seen corresponding path program 1 times
[2024-02-28 18:38:49,621 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:49,621 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1623314397]
[2024-02-28 18:38:49,621 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:49,621 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:49,640 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-02-28 18:38:49,660 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2024-02-28 18:38:49,661 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-02-28 18:38:49,661 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1623314397]
[2024-02-28 18:38:49,661 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1623314397] provided 1 perfect and 0 imperfect interpolant sequences
[2024-02-28 18:38:49,661 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-02-28 18:38:49,661 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-02-28 18:38:49,661 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [704545897]
[2024-02-28 18:38:49,662 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-02-28 18:38:49,662 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-02-28 18:38:49,662 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-02-28 18:38:49,662 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-02-28 18:38:49,662 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-02-28 18:38:49,676 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 148 out of 313
[2024-02-28 18:38:49,677 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 36 places, 31 transitions, 112 flow. Second operand  has 3 states, 3 states have (on average 150.66666666666666) internal successors, (452), 3 states have internal predecessors, (452), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:49,677 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-02-28 18:38:49,677 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 148 of 313
[2024-02-28 18:38:49,677 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-02-28 18:38:49,982 INFO  L130       PetriNetUnfolder]: 2007/3363 cut-off events.
[2024-02-28 18:38:49,982 INFO  L131       PetriNetUnfolder]: For 1193/1246 co-relation queries the response was YES.
[2024-02-28 18:38:49,986 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 7879 conditions, 3363 events. 2007/3363 cut-off events. For 1193/1246 co-relation queries the response was YES. Maximal size of possible extension queue 184. Compared 19290 event pairs, 1381 based on Foata normal form. 0/2863 useless extension candidates. Maximal degree in co-relation 7871. Up to 2668 conditions per place. 
[2024-02-28 18:38:49,995 INFO  L137   encePairwiseOnDemand]: 308/313 looper letters, 37 selfloop transitions, 5 changer transitions 0/47 dead transitions.
[2024-02-28 18:38:49,995 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 38 places, 47 transitions, 248 flow
[2024-02-28 18:38:50,002 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-02-28 18:38:50,002 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-02-28 18:38:50,003 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 484 transitions.
[2024-02-28 18:38:50,003 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5154419595314164
[2024-02-28 18:38:50,003 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 484 transitions.
[2024-02-28 18:38:50,003 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 484 transitions.
[2024-02-28 18:38:50,003 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-02-28 18:38:50,003 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 484 transitions.
[2024-02-28 18:38:50,005 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 161.33333333333334) internal successors, (484), 3 states have internal predecessors, (484), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:50,008 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 313.0) internal successors, (1252), 4 states have internal predecessors, (1252), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:50,009 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 313.0) internal successors, (1252), 4 states have internal predecessors, (1252), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:50,010 INFO  L175             Difference]: Start difference. First operand has 36 places, 31 transitions, 112 flow. Second operand 3 states and 484 transitions.
[2024-02-28 18:38:50,010 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 38 places, 47 transitions, 248 flow
[2024-02-28 18:38:50,013 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 37 places, 47 transitions, 243 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-02-28 18:38:50,014 INFO  L231             Difference]: Finished difference. Result has 38 places, 34 transitions, 141 flow
[2024-02-28 18:38:50,015 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=313, PETRI_DIFFERENCE_MINUEND_FLOW=108, PETRI_DIFFERENCE_MINUEND_PLACES=35, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=31, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=26, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=141, PETRI_PLACES=38, PETRI_TRANSITIONS=34}
[2024-02-28 18:38:50,016 INFO  L288   CegarLoopForPetriNet]: 36 programPoint places, 2 predicate places.
[2024-02-28 18:38:50,016 INFO  L495      AbstractCegarLoop]: Abstraction has has 38 places, 34 transitions, 141 flow
[2024-02-28 18:38:50,016 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 150.66666666666666) internal successors, (452), 3 states have internal predecessors, (452), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-02-28 18:38:50,016 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-02-28 18:38:50,016 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-02-28 18:38:50,016 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2024-02-28 18:38:50,016 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2024-02-28 18:38:50,017 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-02-28 18:38:50,017 INFO  L85        PathProgramCache]: Analyzing trace with hash -1940880712, now seen corresponding path program 1 times
[2024-02-28 18:38:50,017 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-02-28 18:38:50,017 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1354166766]
[2024-02-28 18:38:50,017 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-02-28 18:38:50,017 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-02-28 18:38:50,036 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 18:38:50,036 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-02-28 18:38:50,046 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-02-28 18:38:50,050 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-02-28 18:38:50,051 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location threadErr0ASSERT_VIOLATIONDATA_RACE (8 of 9 remaining)
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (7 of 9 remaining)
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (6 of 9 remaining)
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (5 of 9 remaining)
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (4 of 9 remaining)
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (3 of 9 remaining)
[2024-02-28 18:38:50,051 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 9 remaining)
[2024-02-28 18:38:50,052 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 9 remaining)
[2024-02-28 18:38:50,052 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 9 remaining)
[2024-02-28 18:38:50,052 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2024-02-28 18:38:50,052 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2024-02-28 18:38:50,055 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 3 thread instances
[2024-02-28 18:38:50,056 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2024-02-28 18:38:50,080 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.02 06:38:50 BasicIcfg
[2024-02-28 18:38:50,080 INFO  L132        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2024-02-28 18:38:50,081 INFO  L113        PluginConnector]: ------------------------Witness Printer----------------------------
[2024-02-28 18:38:50,081 INFO  L271        PluginConnector]: Initializing Witness Printer...
[2024-02-28 18:38:50,081 INFO  L275        PluginConnector]: Witness Printer initialized
[2024-02-28 18:38:50,081 INFO  L185        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.02 06:38:32" (3/4) ...
[2024-02-28 18:38:50,083 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2024-02-28 18:38:50,083 INFO  L132        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2024-02-28 18:38:50,084 INFO  L158              Benchmark]: Toolchain (without parser) took 18267.20ms. Allocated memory was 111.1MB in the beginning and 323.0MB in the end (delta: 211.8MB). Free memory was 66.9MB in the beginning and 213.2MB in the end (delta: -146.3MB). Peak memory consumption was 66.9MB. Max. memory is 16.1GB.
[2024-02-28 18:38:50,084 INFO  L158              Benchmark]: CDTParser took 0.10ms. Allocated memory is still 92.3MB. Free memory is still 64.1MB. There was no memory consumed. Max. memory is 16.1GB.
[2024-02-28 18:38:50,084 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 416.02ms. Allocated memory is still 111.1MB. Free memory was 66.6MB in the beginning and 76.6MB in the end (delta: -10.0MB). Peak memory consumption was 30.0MB. Max. memory is 16.1GB.
[2024-02-28 18:38:50,084 INFO  L158              Benchmark]: Boogie Procedure Inliner took 37.83ms. Allocated memory is still 111.1MB. Free memory was 76.6MB in the beginning and 74.0MB in the end (delta: 2.6MB). There was no memory consumed. Max. memory is 16.1GB.
[2024-02-28 18:38:50,085 INFO  L158              Benchmark]: Boogie Preprocessor took 24.94ms. Allocated memory is still 111.1MB. Free memory was 74.0MB in the beginning and 72.0MB in the end (delta: 2.0MB). Peak memory consumption was 4.2MB. Max. memory is 16.1GB.
[2024-02-28 18:38:50,085 INFO  L158              Benchmark]: RCFGBuilder took 381.34ms. Allocated memory is still 111.1MB. Free memory was 72.0MB in the beginning and 55.2MB in the end (delta: 16.8MB). Peak memory consumption was 16.8MB. Max. memory is 16.1GB.
[2024-02-28 18:38:50,085 INFO  L158              Benchmark]: TraceAbstraction took 17399.65ms. Allocated memory was 111.1MB in the beginning and 323.0MB in the end (delta: 211.8MB). Free memory was 54.3MB in the beginning and 214.3MB in the end (delta: -160.0MB). Peak memory consumption was 51.6MB. Max. memory is 16.1GB.
[2024-02-28 18:38:50,085 INFO  L158              Benchmark]: Witness Printer took 2.70ms. Allocated memory is still 323.0MB. Free memory was 214.3MB in the beginning and 213.2MB in the end (delta: 1.1MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-02-28 18:38:50,087 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.10ms. Allocated memory is still 92.3MB. Free memory is still 64.1MB. There was no memory consumed. Max. memory is 16.1GB.
 * CACSL2BoogieTranslator took 416.02ms. Allocated memory is still 111.1MB. Free memory was 66.6MB in the beginning and 76.6MB in the end (delta: -10.0MB). Peak memory consumption was 30.0MB. Max. memory is 16.1GB.
 * Boogie Procedure Inliner took 37.83ms. Allocated memory is still 111.1MB. Free memory was 76.6MB in the beginning and 74.0MB in the end (delta: 2.6MB). There was no memory consumed. Max. memory is 16.1GB.
 * Boogie Preprocessor took 24.94ms. Allocated memory is still 111.1MB. Free memory was 74.0MB in the beginning and 72.0MB in the end (delta: 2.0MB). Peak memory consumption was 4.2MB. Max. memory is 16.1GB.
 * RCFGBuilder took 381.34ms. Allocated memory is still 111.1MB. Free memory was 72.0MB in the beginning and 55.2MB in the end (delta: 16.8MB). Peak memory consumption was 16.8MB. Max. memory is 16.1GB.
 * TraceAbstraction took 17399.65ms. Allocated memory was 111.1MB in the beginning and 323.0MB in the end (delta: 211.8MB). Free memory was 54.3MB in the beginning and 214.3MB in the end (delta: -160.0MB). Peak memory consumption was 51.6MB. Max. memory is 16.1GB.
 * Witness Printer took 2.70ms. Allocated memory is still 323.0MB. Free memory was 214.3MB in the beginning and 213.2MB in the end (delta: 1.1MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 5.5s, 125 PlacesBefore, 18 PlacesAfterwards, 126 TransitionsBefore, 16 TransitionsAfterwards, 1904 CoEnabledTransitionPairs, 8 FixpointIterations, 51 TrivialSequentialCompositions, 67 ConcurrentSequentialCompositions, 4 TrivialYvCompositions, 4 ConcurrentYvCompositions, 3 ChoiceCompositions, 129 TotalNumberOfCompositions, 1485 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 1485, independent: 1485, independent conditional: 0, independent unconditional: 1485, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 967, independent: 967, independent conditional: 0, independent unconditional: 967, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 1485, independent: 518, independent conditional: 0, independent unconditional: 518, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 967, unknown conditional: 0, unknown unconditional: 967] , Statistics on independence cache: Total cache size (in pairs): 12, Positive cache size: 12, Positive conditional cache size: 0, Positive unconditional cache size: 12, Negative cache size: 0, Negative conditional cache size: 0, Negative unconditional cache size: 0, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 5.0s, 145 PlacesBefore, 29 PlacesAfterwards, 145 TransitionsBefore, 26 TransitionsAfterwards, 4828 CoEnabledTransitionPairs, 7 FixpointIterations, 45 TrivialSequentialCompositions, 79 ConcurrentSequentialCompositions, 5 TrivialYvCompositions, 4 ConcurrentYvCompositions, 3 ChoiceCompositions, 136 TotalNumberOfCompositions, 6140 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 4386, independent: 4295, independent conditional: 0, independent unconditional: 4295, dependent: 91, dependent conditional: 0, dependent unconditional: 91, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 2506, independent: 2494, independent conditional: 0, independent unconditional: 2494, dependent: 12, dependent conditional: 0, dependent unconditional: 12, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 4386, independent: 1801, independent conditional: 0, independent unconditional: 1801, dependent: 79, dependent conditional: 0, dependent unconditional: 79, unknown: 2506, unknown conditional: 0, unknown unconditional: 2506] , Statistics on independence cache: Total cache size (in pairs): 63, Positive cache size: 58, Positive conditional cache size: 0, Positive unconditional cache size: 58, Negative cache size: 5, Negative conditional cache size: 0, Negative unconditional cache size: 5, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 4.8s, 165 PlacesBefore, 36 PlacesAfterwards, 164 TransitionsBefore, 32 TransitionsAfterwards, 8262 CoEnabledTransitionPairs, 7 FixpointIterations, 46 TrivialSequentialCompositions, 92 ConcurrentSequentialCompositions, 4 TrivialYvCompositions, 4 ConcurrentYvCompositions, 3 ChoiceCompositions, 149 TotalNumberOfCompositions, 11545 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 8323, independent: 8181, independent conditional: 0, independent unconditional: 8181, dependent: 142, dependent conditional: 0, dependent unconditional: 142, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 4296, independent: 4271, independent conditional: 0, independent unconditional: 4271, dependent: 25, dependent conditional: 0, dependent unconditional: 25, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 8323, independent: 3910, independent conditional: 0, independent unconditional: 3910, dependent: 117, dependent conditional: 0, dependent unconditional: 117, unknown: 4296, unknown conditional: 0, unknown unconditional: 4296] , Statistics on independence cache: Total cache size (in pairs): 174, Positive cache size: 164, Positive conditional cache size: 0, Positive unconditional cache size: 164, Negative cache size: 10, Negative conditional cache size: 0, Negative unconditional cache size: 10, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - DataRaceFoundResult [Line: 1039]: Data race detected
    Data race detected
The following path leads to a data race: 
[L1035]               0  int data = 0;
[L1036]               0  sem_t data_sem;
[L1045]               0  int threads_total = __VERIFIER_nondet_int();
[L1046]  CALL         0  assume_abort_if_not(threads_total >= 0)
[L1032]  COND FALSE   0  !(!cond)
[L1046]  RET          0  assume_abort_if_not(threads_total >= 0)
[L1047]               0  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
[L1047]               0  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
[L1048]               0  int i = 0;
         VAL             [data=0, data_sem={1:0}, i=0, threads_total=5, tids={17:0}]
[L1048]  COND TRUE    0  i < threads_total
[L1049]  EXPR         0  \read(*tids)
[L1049]  EXPR         0  tids[i]
[L1049]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [\read(*tids)={-3:0}, arg={0:0}, data=0, data_sem={1:0}, i=0, pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))=-2, threads_total=5, tids={17:0}]
[L1048]               0  i++
         VAL             [arg={0:0}, data=0, data_sem={1:0}, i=1, threads_total=5, tids={17:0}]
[L1048]  COND TRUE    0  i < threads_total
[L1049]  EXPR         0  \read(*tids)
[L1049]  EXPR         0  tids[i]
[L1039]               1  data = __VERIFIER_nondet_int()
         VAL             [__VERIFIER_nondet_int()=0, arg={0:0}, arg={0:0}, data=0, data = __VERIFIER_nondet_int()=26, data_sem={1:0}]
[L1049]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [\read(*tids)={-3:0}, __VERIFIER_nondet_int()=0, arg={0:0}, arg={0:0}, data=0, data = __VERIFIER_nondet_int()=26, data_sem={1:0}, i=1, pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))=-1, threads_total=5, tids={17:0}]
[L1039]               2  data = __VERIFIER_nondet_int()
         VAL             [__VERIFIER_nondet_int()=-4, arg={0:0}, arg={0:0}, data=-4, data = __VERIFIER_nondet_int()=22, data_sem={1:0}]

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

  - UnprovableResult [Line: 1049]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1053]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1055]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1053]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1049]: 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. 
  - StatisticsResult: Ultimate Automizer benchmark data with 1 thread instances
    CFG has 3 procedures, 141 locations, 7 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.9s, OverallIterations: 2, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 5.6s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 0 SdHoareTripleChecker+Valid, 0.0s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 0 mSDsluCounter, 0 SdHoareTripleChecker+Invalid, 0.0s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 10 IncrementalHoareTripleChecker+Invalid, 10 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 0 mSDtfsCounter, 10 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 1 GetRequests, 1 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=40occurred in iteration=0, InterpolantAutomatonStates: 2, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.0s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 8 NumberOfCodeBlocks, 8 NumberOfCodeBlocksAsserted, 2 NumberOfCheckSat, 1 ConstructedInterpolants, 0 QuantifiedInterpolants, 1 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 1 InterpolantComputations, 1 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
  - StatisticsResult: Ultimate Automizer benchmark data with 2 thread instances
    CFG has 4 procedures, 159 locations, 8 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 5.5s, OverallIterations: 4, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.3s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 5.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 49 SdHoareTripleChecker+Valid, 0.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 25 mSDsluCounter, 8 SdHoareTripleChecker+Invalid, 0.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 6 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 128 IncrementalHoareTripleChecker+Invalid, 134 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 6 mSolverCounterUnsat, 8 mSDtfsCounter, 128 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 5 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=102occurred in iteration=3, InterpolantAutomatonStates: 8, 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, 29 NumberOfCodeBlocks, 29 NumberOfCodeBlocksAsserted, 4 NumberOfCheckSat, 15 ConstructedInterpolants, 0 QuantifiedInterpolants, 19 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 3 InterpolantComputations, 3 PerfectInterpolantSequences, 2/2 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
  - StatisticsResult: Ultimate Automizer benchmark data with 3 thread instances
    CFG has 5 procedures, 177 locations, 9 error locations. Started 1 CEGAR loops. EmptinessCheckTime: 0.0s, RemoveRedundantFlowTime: 0.0s, RemoveRedundantFlowUnfoldingTime: 0.0s, BackfoldingTime: 0.0s, BackfoldingUnfoldingTime: 0.0s, FlowIncreaseByBackfolding: 0, BasicCegarLoop: OverallTime: 5.8s, OverallIterations: 4, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 4.8s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 79 SdHoareTripleChecker+Valid, 0.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 37 mSDsluCounter, 22 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 6 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 177 IncrementalHoareTripleChecker+Invalid, 183 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 6 mSolverCounterUnsat, 22 mSDtfsCounter, 177 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 5 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=141occurred in iteration=3, InterpolantAutomatonStates: 8, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.0s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 30 NumberOfCodeBlocks, 30 NumberOfCodeBlocksAsserted, 4 NumberOfCheckSat, 15 ConstructedInterpolants, 0 QuantifiedInterpolants, 19 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 3 InterpolantComputations, 3 PerfectInterpolantSequences, 2/2 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2024-02-28 18:38:50,124 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...
--- End real Ultimate output ---

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