./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.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.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 1fa6b4da7764e7ec13c8a1bf3f9645c63415d6ef4dca1ba158e75f911cb201ac
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2023-10-26 08:55:33,413 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2023-10-26 08:55:33,415 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2023-10-26 08:55:33,449 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2023-10-26 08:55:33,465 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2023-10-26 08:55:33,471 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2023-10-26 08:55:33,485 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2023-10-26 08:55:33,488 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2023-10-26 08:55:33,490 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2023-10-26 08:55:33,494 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2023-10-26 08:55:33,495 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2023-10-26 08:55:33,497 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2023-10-26 08:55:33,497 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2023-10-26 08:55:33,501 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2023-10-26 08:55:33,503 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2023-10-26 08:55:33,505 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2023-10-26 08:55:33,506 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2023-10-26 08:55:33,506 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2023-10-26 08:55:33,507 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2023-10-26 08:55:33,526 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2023-10-26 08:55:33,527 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2023-10-26 08:55:33,528 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2023-10-26 08:55:33,529 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2023-10-26 08:55:33,529 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2023-10-26 08:55:33,537 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2023-10-26 08:55:33,537 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2023-10-26 08:55:33,537 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2023-10-26 08:55:33,538 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2023-10-26 08:55:33,539 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2023-10-26 08:55:33,539 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2023-10-26 08:55:33,540 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2023-10-26 08:55:33,540 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2023-10-26 08:55:33,542 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2023-10-26 08:55:33,542 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2023-10-26 08:55:33,543 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2023-10-26 08:55:33,543 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2023-10-26 08:55:33,544 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2023-10-26 08:55:33,544 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2023-10-26 08:55:33,544 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2023-10-26 08:55:33,545 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2023-10-26 08:55:33,545 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2023-10-26 08:55:33,546 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2023-10-26 08:55:33,595 INFO  L113        SettingsManager]: Loading preferences was successful
[2023-10-26 08:55:33,595 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2023-10-26 08:55:33,596 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2023-10-26 08:55:33,596 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2023-10-26 08:55:33,596 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2023-10-26 08:55:33,596 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2023-10-26 08:55:33,597 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2023-10-26 08:55:33,597 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2023-10-26 08:55:33,597 INFO  L138        SettingsManager]:  * Use SBE=true
[2023-10-26 08:55:33,597 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2023-10-26 08:55:33,598 INFO  L138        SettingsManager]:  * sizeof long=4
[2023-10-26 08:55:33,598 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2023-10-26 08:55:33,598 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2023-10-26 08:55:33,599 INFO  L138        SettingsManager]:  * sizeof long double=12
[2023-10-26 08:55:33,600 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2023-10-26 08:55:33,600 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2023-10-26 08:55:33,600 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2023-10-26 08:55:33,600 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2023-10-26 08:55:33,600 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2023-10-26 08:55:33,600 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2023-10-26 08:55:33,601 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-10-26 08:55:33,601 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2023-10-26 08:55:33,601 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2023-10-26 08:55:33,601 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2023-10-26 08:55:33,601 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2023-10-26 08:55:33,601 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2023-10-26 08:55:33,602 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2023-10-26 08:55:33,602 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2023-10-26 08:55:33,602 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2023-10-26 08:55:33,603 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2023-10-26 08:55:33,603 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2023-10-26 08:55:33,603 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 -> 1fa6b4da7764e7ec13c8a1bf3f9645c63415d6ef4dca1ba158e75f911cb201ac
[2023-10-26 08:55:33,959 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2023-10-26 08:55:33,997 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2023-10-26 08:55:33,999 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2023-10-26 08:55:34,000 INFO  L271        PluginConnector]: Initializing CDTParser...
[2023-10-26 08:55:34,001 INFO  L275        PluginConnector]: CDTParser initialized
[2023-10-26 08:55:34,002 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/semaphore-posix.i
[2023-10-26 08:55:35,718 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2023-10-26 08:55:36,151 INFO  L351              CDTParser]: Found 1 translation units.
[2023-10-26 08:55:36,152 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/semaphore-posix.i
[2023-10-26 08:55:36,178 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/d6128dd55/9c2e1b3e62a64bfa8d21a187445f89bd/FLAGceee9cacf
[2023-10-26 08:55:36,209 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/d6128dd55/9c2e1b3e62a64bfa8d21a187445f89bd
[2023-10-26 08:55:36,212 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2023-10-26 08:55:36,213 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2023-10-26 08:55:36,214 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2023-10-26 08:55:36,214 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2023-10-26 08:55:36,216 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2023-10-26 08:55:36,217 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 26.10 08:55:36" (1/1) ...
[2023-10-26 08:55:36,223 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@44798523 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:36, skipping insertion in model container
[2023-10-26 08:55:36,223 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 26.10 08:55:36" (1/1) ...
[2023-10-26 08:55:36,236 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2023-10-26 08:55:36,308 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2023-10-26 08:55:36,567 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2023-10-26 08:55:36,896 WARN  L623        FunctionHandler]: Unknown extern function sem_wait
[2023-10-26 08:55:36,914 WARN  L623        FunctionHandler]: Unknown extern function sem_post
[2023-10-26 08:55:36,915 WARN  L623        FunctionHandler]: Unknown extern function sem_init
[2023-10-26 08:55:36,943 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-10-26 08:55:36,958 INFO  L203         MainTranslator]: Completed pre-run
[2023-10-26 08:55:36,989 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2023-10-26 08:55:37,019 WARN  L623        FunctionHandler]: Unknown extern function sem_wait
[2023-10-26 08:55:37,020 WARN  L623        FunctionHandler]: Unknown extern function sem_post
[2023-10-26 08:55:37,021 WARN  L623        FunctionHandler]: Unknown extern function sem_init
[2023-10-26 08:55:37,050 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-10-26 08:55:37,132 INFO  L208         MainTranslator]: Completed translation
[2023-10-26 08:55:37,146 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37 WrapperNode
[2023-10-26 08:55:37,146 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2023-10-26 08:55:37,147 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2023-10-26 08:55:37,147 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2023-10-26 08:55:37,147 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2023-10-26 08:55:37,154 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,190 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,234 INFO  L138                Inliner]: procedures = 278, calls = 36, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 96
[2023-10-26 08:55:37,236 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2023-10-26 08:55:37,236 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2023-10-26 08:55:37,236 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2023-10-26 08:55:37,236 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2023-10-26 08:55:37,246 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,246 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,265 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,266 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,282 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,306 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,307 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,308 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,311 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2023-10-26 08:55:37,311 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2023-10-26 08:55:37,311 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2023-10-26 08:55:37,311 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2023-10-26 08:55:37,312 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (1/1) ...
[2023-10-26 08:55:37,329 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-10-26 08:55:37,348 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-10-26 08:55:37,363 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2023-10-26 08:55:37,383 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2023-10-26 08:55:37,416 INFO  L130     BoogieDeclarations]: Found specification of procedure sem_init
[2023-10-26 08:55:37,416 INFO  L130     BoogieDeclarations]: Found specification of procedure sem_post
[2023-10-26 08:55:37,417 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2023-10-26 08:55:37,417 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2023-10-26 08:55:37,417 INFO  L130     BoogieDeclarations]: Found specification of procedure sem_wait
[2023-10-26 08:55:37,417 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2023-10-26 08:55:37,417 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2023-10-26 08:55:37,417 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2023-10-26 08:55:37,423 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2023-10-26 08:55:37,423 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2023-10-26 08:55:37,423 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2023-10-26 08:55:37,423 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2023-10-26 08:55:37,423 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2023-10-26 08:55:37,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2023-10-26 08:55:37,424 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2023-10-26 08:55:37,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2023-10-26 08:55:37,425 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2023-10-26 08:55:37,663 INFO  L235             CfgBuilder]: Building ICFG
[2023-10-26 08:55:37,665 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2023-10-26 08:55:38,095 INFO  L276             CfgBuilder]: Performing block encoding
[2023-10-26 08:55:38,101 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2023-10-26 08:55:38,121 INFO  L300             CfgBuilder]: Removed 2 assume(true) statements.
[2023-10-26 08:55:38,124 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 26.10 08:55:38 BoogieIcfgContainer
[2023-10-26 08:55:38,124 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2023-10-26 08:55:38,126 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2023-10-26 08:55:38,127 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2023-10-26 08:55:38,130 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2023-10-26 08:55:38,130 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 26.10 08:55:36" (1/3) ...
[2023-10-26 08:55:38,132 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@53b66ba6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 26.10 08:55:38, skipping insertion in model container
[2023-10-26 08:55:38,132 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 26.10 08:55:37" (2/3) ...
[2023-10-26 08:55:38,132 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@53b66ba6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 26.10 08:55:38, skipping insertion in model container
[2023-10-26 08:55:38,137 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 26.10 08:55:38" (3/3) ...
[2023-10-26 08:55:38,139 INFO  L112   eAbstractionObserver]: Analyzing ICFG semaphore-posix.i
[2023-10-26 08:55:38,161 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2023-10-26 08:55:38,168 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2023-10-26 08:55:38,168 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 5 error locations.
[2023-10-26 08:55:38,168 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2023-10-26 08:55:38,263 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2023-10-26 08:55:38,310 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 122 places, 123 transitions, 254 flow
[2023-10-26 08:55:38,459 INFO  L130       PetriNetUnfolder]: 6/169 cut-off events.
[2023-10-26 08:55:38,460 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2023-10-26 08:55:38,463 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 175 conditions, 169 events. 6/169 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 296 event pairs, 0 based on Foata normal form. 0/151 useless extension candidates. Maximal degree in co-relation 92. Up to 4 conditions per place. 
[2023-10-26 08:55:38,464 INFO  L82        GeneralOperation]: Start removeDead. Operand has 122 places, 123 transitions, 254 flow
[2023-10-26 08:55:38,466 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 122 places, 123 transitions, 254 flow
[2023-10-26 08:55:38,483 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-26 08:55:38,504 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 122 places, 123 transitions, 254 flow
[2023-10-26 08:55:38,507 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 122 places, 123 transitions, 254 flow
[2023-10-26 08:55:38,508 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 122 places, 123 transitions, 254 flow
[2023-10-26 08:55:38,563 INFO  L130       PetriNetUnfolder]: 6/169 cut-off events.
[2023-10-26 08:55:38,563 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2023-10-26 08:55:38,577 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 175 conditions, 169 events. 6/169 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 296 event pairs, 0 based on Foata normal form. 0/151 useless extension candidates. Maximal degree in co-relation 92. Up to 4 conditions per place. 
[2023-10-26 08:55:38,584 INFO  L119        LiptonReduction]: Number of co-enabled transitions 1802
[2023-10-26 08:55:44,960 INFO  L134        LiptonReduction]: Checked pairs total: 1369
[2023-10-26 08:55:44,961 INFO  L136        LiptonReduction]: Total number of compositions: 125
[2023-10-26 08:55:44,981 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-26 08:55:45,007 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;@69ed0b9a, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-26 08:55:45,007 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 7 error locations.
[2023-10-26 08:55:45,009 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2023-10-26 08:55:45,010 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-26 08:55:45,011 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:45,011 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2023-10-26 08:55:45,016 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)] ===
[2023-10-26 08:55:45,028 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:45,028 INFO  L85        PathProgramCache]: Analyzing trace with hash 14131, now seen corresponding path program 1 times
[2023-10-26 08:55:45,035 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:45,036 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1870084817]
[2023-10-26 08:55:45,036 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:45,037 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:45,201 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:45,330 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-26 08:55:45,331 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:45,331 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1870084817]
[2023-10-26 08:55:45,332 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1870084817] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:45,332 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:45,332 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2023-10-26 08:55:45,333 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1961136691]
[2023-10-26 08:55:45,334 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:45,340 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2023-10-26 08:55:45,347 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:45,387 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2023-10-26 08:55:45,395 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2023-10-26 08:55:45,397 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 118 out of 248
[2023-10-26 08:55:45,399 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 18 places, 16 transitions, 40 flow. Second operand  has 2 states, 2 states have (on average 119.0) internal successors, (238), 2 states have internal predecessors, (238), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:45,399 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:45,399 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 118 of 248
[2023-10-26 08:55:45,400 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:45,458 INFO  L130       PetriNetUnfolder]: 6/25 cut-off events.
[2023-10-26 08:55:45,459 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2023-10-26 08:55:45,460 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 56 conditions, 25 events. 6/25 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 42 event pairs, 5 based on Foata normal form. 0/19 useless extension candidates. Maximal degree in co-relation 32. Up to 25 conditions per place. 
[2023-10-26 08:55:45,461 INFO  L137   encePairwiseOnDemand]: 243/248 looper letters, 5 selfloop transitions, 0 changer transitions 5/11 dead transitions.
[2023-10-26 08:55:45,461 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 14 places, 11 transitions, 50 flow
[2023-10-26 08:55:45,462 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2023-10-26 08:55:45,463 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2023-10-26 08:55:45,486 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 251 transitions.
[2023-10-26 08:55:45,488 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5060483870967742
[2023-10-26 08:55:45,489 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 251 transitions.
[2023-10-26 08:55:45,489 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 251 transitions.
[2023-10-26 08:55:45,491 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:45,492 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 251 transitions.
[2023-10-26 08:55:45,496 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 125.5) internal successors, (251), 2 states have internal predecessors, (251), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:45,507 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 248.0) internal successors, (744), 3 states have internal predecessors, (744), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:45,508 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 248.0) internal successors, (744), 3 states have internal predecessors, (744), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:45,510 INFO  L175             Difference]: Start difference. First operand has 18 places, 16 transitions, 40 flow. Second operand 2 states and 251 transitions.
[2023-10-26 08:55:45,510 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 14 places, 11 transitions, 50 flow
[2023-10-26 08:55:45,512 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 14 places, 11 transitions, 50 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-26 08:55:45,514 INFO  L231             Difference]: Finished difference. Result has 14 places, 6 transitions, 17 flow
[2023-10-26 08:55:45,517 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=248, PETRI_DIFFERENCE_MINUEND_FLOW=30, PETRI_DIFFERENCE_MINUEND_PLACES=13, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=11, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=11, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=17, PETRI_PLACES=14, PETRI_TRANSITIONS=6}
[2023-10-26 08:55:45,541 INFO  L288   CegarLoopForPetriNet]: 18 programPoint places, -4 predicate places.
[2023-10-26 08:55:45,541 INFO  L495      AbstractCegarLoop]: Abstraction has has 14 places, 6 transitions, 17 flow
[2023-10-26 08:55:45,541 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 119.0) internal successors, (238), 2 states have internal predecessors, (238), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:45,542 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:45,542 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1]
[2023-10-26 08:55:45,543 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2023-10-26 08:55:45,543 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)] ===
[2023-10-26 08:55:45,544 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:45,547 INFO  L85        PathProgramCache]: Analyzing trace with hash 173350723, now seen corresponding path program 1 times
[2023-10-26 08:55:45,548 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:45,548 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2089860775]
[2023-10-26 08:55:45,548 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:45,548 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:45,661 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-26 08:55:45,661 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-26 08:55:45,719 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-26 08:55:45,760 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-26 08:55:45,760 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-26 08:55:45,762 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (6 of 7 remaining)
[2023-10-26 08:55:45,763 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (5 of 7 remaining)
[2023-10-26 08:55:45,763 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (4 of 7 remaining)
[2023-10-26 08:55:45,763 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (3 of 7 remaining)
[2023-10-26 08:55:45,764 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (2 of 7 remaining)
[2023-10-26 08:55:45,767 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 7 remaining)
[2023-10-26 08:55:45,767 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 7 remaining)
[2023-10-26 08:55:45,768 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2023-10-26 08:55:45,768 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1]
[2023-10-26 08:55:45,771 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-10-26 08:55:45,771 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2023-10-26 08:55:45,813 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2023-10-26 08:55:45,823 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 142 places, 142 transitions, 302 flow
[2023-10-26 08:55:45,897 INFO  L130       PetriNetUnfolder]: 11/284 cut-off events.
[2023-10-26 08:55:45,898 INFO  L131       PetriNetUnfolder]: For 6/6 co-relation queries the response was YES.
[2023-10-26 08:55:45,900 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 298 conditions, 284 events. 11/284 cut-off events. For 6/6 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 617 event pairs, 0 based on Foata normal form. 0/252 useless extension candidates. Maximal degree in co-relation 171. Up to 8 conditions per place. 
[2023-10-26 08:55:45,900 INFO  L82        GeneralOperation]: Start removeDead. Operand has 142 places, 142 transitions, 302 flow
[2023-10-26 08:55:45,901 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 142 places, 142 transitions, 302 flow
[2023-10-26 08:55:45,901 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-26 08:55:45,902 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 142 places, 142 transitions, 302 flow
[2023-10-26 08:55:45,902 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 142 places, 142 transitions, 302 flow
[2023-10-26 08:55:45,902 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 142 places, 142 transitions, 302 flow
[2023-10-26 08:55:45,951 INFO  L130       PetriNetUnfolder]: 11/284 cut-off events.
[2023-10-26 08:55:45,965 INFO  L131       PetriNetUnfolder]: For 6/6 co-relation queries the response was YES.
[2023-10-26 08:55:45,966 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 298 conditions, 284 events. 11/284 cut-off events. For 6/6 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 617 event pairs, 0 based on Foata normal form. 0/252 useless extension candidates. Maximal degree in co-relation 171. Up to 8 conditions per place. 
[2023-10-26 08:55:45,970 INFO  L119        LiptonReduction]: Number of co-enabled transitions 4624
[2023-10-26 08:55:51,582 INFO  L134        LiptonReduction]: Checked pairs total: 6221
[2023-10-26 08:55:51,584 INFO  L136        LiptonReduction]: Total number of compositions: 136
[2023-10-26 08:55:51,585 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-26 08:55:51,586 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;@69ed0b9a, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-26 08:55:51,588 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 8 error locations.
[2023-10-26 08:55:51,590 INFO  L130       PetriNetUnfolder]: 0/2 cut-off events.
[2023-10-26 08:55:51,590 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-26 08:55:51,590 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:51,591 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2023-10-26 08:55:51,591 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)] ===
[2023-10-26 08:55:51,592 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:51,595 INFO  L85        PathProgramCache]: Analyzing trace with hash 23637, now seen corresponding path program 1 times
[2023-10-26 08:55:51,595 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:51,596 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1285165530]
[2023-10-26 08:55:51,596 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:51,596 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:51,614 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:51,632 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-26 08:55:51,648 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:51,648 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1285165530]
[2023-10-26 08:55:51,649 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1285165530] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:51,649 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:51,649 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2023-10-26 08:55:51,649 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [235659873]
[2023-10-26 08:55:51,649 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:51,650 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2023-10-26 08:55:51,650 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:51,650 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2023-10-26 08:55:51,650 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2023-10-26 08:55:51,651 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 135 out of 278
[2023-10-26 08:55:51,652 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 29 places, 26 transitions, 70 flow. Second operand  has 2 states, 2 states have (on average 136.0) internal successors, (272), 2 states have internal predecessors, (272), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:51,652 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:51,652 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 135 of 278
[2023-10-26 08:55:51,652 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:51,784 INFO  L130       PetriNetUnfolder]: 168/362 cut-off events.
[2023-10-26 08:55:51,784 INFO  L131       PetriNetUnfolder]: For 30/30 co-relation queries the response was YES.
[2023-10-26 08:55:51,787 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 1557 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. 
[2023-10-26 08:55:51,788 INFO  L137   encePairwiseOnDemand]: 274/278 looper letters, 17 selfloop transitions, 0 changer transitions 0/22 dead transitions.
[2023-10-26 08:55:51,788 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 26 places, 22 transitions, 96 flow
[2023-10-26 08:55:51,788 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2023-10-26 08:55:51,788 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2023-10-26 08:55:51,791 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 291 transitions.
[2023-10-26 08:55:51,792 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5233812949640287
[2023-10-26 08:55:51,792 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 291 transitions.
[2023-10-26 08:55:51,793 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 291 transitions.
[2023-10-26 08:55:51,793 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:51,793 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 291 transitions.
[2023-10-26 08:55:51,794 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 145.5) internal successors, (291), 2 states have internal predecessors, (291), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:51,796 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 278.0) internal successors, (834), 3 states have internal predecessors, (834), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:51,797 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 278.0) internal successors, (834), 3 states have internal predecessors, (834), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:51,797 INFO  L175             Difference]: Start difference. First operand has 29 places, 26 transitions, 70 flow. Second operand 2 states and 291 transitions.
[2023-10-26 08:55:51,797 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 26 places, 22 transitions, 96 flow
[2023-10-26 08:55:51,798 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 26 places, 22 transitions, 96 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-26 08:55:51,798 INFO  L231             Difference]: Finished difference. Result has 26 places, 22 transitions, 62 flow
[2023-10-26 08:55:51,798 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, 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}
[2023-10-26 08:55:51,799 INFO  L288   CegarLoopForPetriNet]: 29 programPoint places, -3 predicate places.
[2023-10-26 08:55:51,799 INFO  L495      AbstractCegarLoop]: Abstraction has has 26 places, 22 transitions, 62 flow
[2023-10-26 08:55:51,800 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 136.0) internal successors, (272), 2 states have internal predecessors, (272), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:51,800 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:51,800 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1]
[2023-10-26 08:55:51,800 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2023-10-26 08:55:51,800 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2023-10-26 08:55:51,800 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:51,801 INFO  L85        PathProgramCache]: Analyzing trace with hash 373009728, now seen corresponding path program 1 times
[2023-10-26 08:55:51,801 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:51,801 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [884754619]
[2023-10-26 08:55:51,801 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:51,817 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:51,843 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:51,891 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-26 08:55:51,892 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:51,892 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [884754619]
[2023-10-26 08:55:51,894 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [884754619] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:51,895 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:51,909 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-26 08:55:51,909 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1872370642]
[2023-10-26 08:55:51,910 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:51,911 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-26 08:55:51,911 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:51,911 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-26 08:55:51,911 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-26 08:55:51,926 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 129 out of 278
[2023-10-26 08:55:51,928 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 26 places, 22 transitions, 62 flow. Second operand  has 3 states, 3 states have (on average 131.0) internal successors, (393), 3 states have internal predecessors, (393), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:51,929 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:51,929 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 129 of 278
[2023-10-26 08:55:51,929 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:52,193 INFO  L130       PetriNetUnfolder]: 208/427 cut-off events.
[2023-10-26 08:55:52,205 INFO  L131       PetriNetUnfolder]: For 35/35 co-relation queries the response was YES.
[2023-10-26 08:55:52,206 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 1866 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. 
[2023-10-26 08:55:52,207 INFO  L137   encePairwiseOnDemand]: 274/278 looper letters, 25 selfloop transitions, 3 changer transitions 2/34 dead transitions.
[2023-10-26 08:55:52,207 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 28 places, 34 transitions, 154 flow
[2023-10-26 08:55:52,208 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-26 08:55:52,208 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-26 08:55:52,209 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 418 transitions.
[2023-10-26 08:55:52,210 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5011990407673861
[2023-10-26 08:55:52,210 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 418 transitions.
[2023-10-26 08:55:52,210 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 418 transitions.
[2023-10-26 08:55:52,210 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:52,210 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 418 transitions.
[2023-10-26 08:55:52,211 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 139.33333333333334) internal successors, (418), 3 states have internal predecessors, (418), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,213 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,213 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,214 INFO  L175             Difference]: Start difference. First operand has 26 places, 22 transitions, 62 flow. Second operand 3 states and 418 transitions.
[2023-10-26 08:55:52,214 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 28 places, 34 transitions, 154 flow
[2023-10-26 08:55:52,215 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 28 places, 34 transitions, 154 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-26 08:55:52,215 INFO  L231             Difference]: Finished difference. Result has 29 places, 24 transitions, 81 flow
[2023-10-26 08:55:52,216 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, 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}
[2023-10-26 08:55:52,217 INFO  L288   CegarLoopForPetriNet]: 29 programPoint places, 0 predicate places.
[2023-10-26 08:55:52,218 INFO  L495      AbstractCegarLoop]: Abstraction has has 29 places, 24 transitions, 81 flow
[2023-10-26 08:55:52,218 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 131.0) internal successors, (393), 3 states have internal predecessors, (393), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,218 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:52,218 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-26 08:55:52,218 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2023-10-26 08:55:52,219 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2023-10-26 08:55:52,219 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:52,219 INFO  L85        PathProgramCache]: Analyzing trace with hash -962849307, now seen corresponding path program 1 times
[2023-10-26 08:55:52,219 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:52,220 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1245995756]
[2023-10-26 08:55:52,220 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:52,221 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:52,257 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:52,310 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2023-10-26 08:55:52,311 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:52,311 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1245995756]
[2023-10-26 08:55:52,311 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1245995756] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:52,311 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:52,311 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-26 08:55:52,311 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [432791627]
[2023-10-26 08:55:52,312 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:52,312 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-26 08:55:52,312 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:52,313 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-26 08:55:52,313 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-26 08:55:52,326 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 129 out of 278
[2023-10-26 08:55:52,326 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 29 places, 24 transitions, 81 flow. Second operand  has 3 states, 3 states have (on average 131.66666666666666) internal successors, (395), 3 states have internal predecessors, (395), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,327 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:52,327 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 129 of 278
[2023-10-26 08:55:52,327 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:52,461 INFO  L130       PetriNetUnfolder]: 217/430 cut-off events.
[2023-10-26 08:55:52,462 INFO  L131       PetriNetUnfolder]: For 139/143 co-relation queries the response was YES.
[2023-10-26 08:55:52,462 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 1791 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. 
[2023-10-26 08:55:52,463 INFO  L137   encePairwiseOnDemand]: 274/278 looper letters, 25 selfloop transitions, 4 changer transitions 2/35 dead transitions.
[2023-10-26 08:55:52,464 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 31 places, 35 transitions, 173 flow
[2023-10-26 08:55:52,464 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-26 08:55:52,464 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-26 08:55:52,465 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 417 transitions.
[2023-10-26 08:55:52,465 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5
[2023-10-26 08:55:52,465 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 417 transitions.
[2023-10-26 08:55:52,465 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 417 transitions.
[2023-10-26 08:55:52,466 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:52,466 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 417 transitions.
[2023-10-26 08:55:52,467 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 139.0) internal successors, (417), 3 states have internal predecessors, (417), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,468 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,468 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 278.0) internal successors, (1112), 4 states have internal predecessors, (1112), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,468 INFO  L175             Difference]: Start difference. First operand has 29 places, 24 transitions, 81 flow. Second operand 3 states and 417 transitions.
[2023-10-26 08:55:52,468 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 31 places, 35 transitions, 173 flow
[2023-10-26 08:55:52,471 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 30 places, 35 transitions, 169 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-10-26 08:55:52,472 INFO  L231             Difference]: Finished difference. Result has 31 places, 26 transitions, 102 flow
[2023-10-26 08:55:52,472 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=278, 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}
[2023-10-26 08:55:52,474 INFO  L288   CegarLoopForPetriNet]: 29 programPoint places, 2 predicate places.
[2023-10-26 08:55:52,476 INFO  L495      AbstractCegarLoop]: Abstraction has has 31 places, 26 transitions, 102 flow
[2023-10-26 08:55:52,477 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 131.66666666666666) internal successors, (395), 3 states have internal predecessors, (395), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:52,477 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:52,477 INFO  L209   CegarLoopForPetriNet]: trace histogram [3, 2, 2, 1, 1, 1, 1]
[2023-10-26 08:55:52,478 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2023-10-26 08:55:52,478 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)] ===
[2023-10-26 08:55:52,479 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:52,480 INFO  L85        PathProgramCache]: Analyzing trace with hash 210819786, now seen corresponding path program 1 times
[2023-10-26 08:55:52,480 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:52,480 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [652661535]
[2023-10-26 08:55:52,480 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:52,480 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:52,536 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-26 08:55:52,549 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-26 08:55:52,567 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-26 08:55:52,582 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-26 08:55:52,582 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-26 08:55:52,583 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (7 of 8 remaining)
[2023-10-26 08:55:52,583 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (6 of 8 remaining)
[2023-10-26 08:55:52,583 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (5 of 8 remaining)
[2023-10-26 08:55:52,584 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (4 of 8 remaining)
[2023-10-26 08:55:52,586 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (3 of 8 remaining)
[2023-10-26 08:55:52,586 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 8 remaining)
[2023-10-26 08:55:52,586 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 8 remaining)
[2023-10-26 08:55:52,586 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 8 remaining)
[2023-10-26 08:55:52,587 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2023-10-26 08:55:52,587 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2023-10-26 08:55:52,587 WARN  L233   ceAbstractionStarter]: 2 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-10-26 08:55:52,587 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 3 thread instances.
[2023-10-26 08:55:52,616 INFO  L144    ThreadInstanceAdder]: Constructed 3 joinOtherThreadTransitions.
[2023-10-26 08:55:52,619 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 162 places, 161 transitions, 352 flow
[2023-10-26 08:55:52,691 INFO  L130       PetriNetUnfolder]: 21/478 cut-off events.
[2023-10-26 08:55:52,705 INFO  L131       PetriNetUnfolder]: For 19/19 co-relation queries the response was YES.
[2023-10-26 08:55:52,706 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 506 conditions, 478 events. 21/478 cut-off events. For 19/19 co-relation queries the response was YES. Maximal size of possible extension queue 9. Compared 1345 event pairs, 1 based on Foata normal form. 0/422 useless extension candidates. Maximal degree in co-relation 292. Up to 16 conditions per place. 
[2023-10-26 08:55:52,706 INFO  L82        GeneralOperation]: Start removeDead. Operand has 162 places, 161 transitions, 352 flow
[2023-10-26 08:55:52,707 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 162 places, 161 transitions, 352 flow
[2023-10-26 08:55:52,707 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-26 08:55:52,708 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 162 places, 161 transitions, 352 flow
[2023-10-26 08:55:52,709 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 162 places, 161 transitions, 352 flow
[2023-10-26 08:55:52,709 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 162 places, 161 transitions, 352 flow
[2023-10-26 08:55:52,772 INFO  L130       PetriNetUnfolder]: 21/478 cut-off events.
[2023-10-26 08:55:52,777 INFO  L131       PetriNetUnfolder]: For 19/19 co-relation queries the response was YES.
[2023-10-26 08:55:52,778 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 506 conditions, 478 events. 21/478 cut-off events. For 19/19 co-relation queries the response was YES. Maximal size of possible extension queue 9. Compared 1345 event pairs, 1 based on Foata normal form. 0/422 useless extension candidates. Maximal degree in co-relation 292. Up to 16 conditions per place. 
[2023-10-26 08:55:52,784 INFO  L119        LiptonReduction]: Number of co-enabled transitions 7956
[2023-10-26 08:55:58,096 INFO  L134        LiptonReduction]: Checked pairs total: 11320
[2023-10-26 08:55:58,097 INFO  L136        LiptonReduction]: Total number of compositions: 147
[2023-10-26 08:55:58,098 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-26 08:55:58,101 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;@69ed0b9a, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-26 08:55:58,103 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 9 error locations.
[2023-10-26 08:55:58,104 INFO  L130       PetriNetUnfolder]: 0/2 cut-off events.
[2023-10-26 08:55:58,104 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-26 08:55:58,104 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:58,104 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2023-10-26 08:55:58,104 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)] ===
[2023-10-26 08:55:58,105 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:58,105 INFO  L85        PathProgramCache]: Analyzing trace with hash 34096, now seen corresponding path program 1 times
[2023-10-26 08:55:58,105 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:58,105 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1768600682]
[2023-10-26 08:55:58,105 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:58,105 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:58,114 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:58,135 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-26 08:55:58,135 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:58,135 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1768600682]
[2023-10-26 08:55:58,135 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1768600682] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:58,135 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:58,136 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2023-10-26 08:55:58,136 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1552840853]
[2023-10-26 08:55:58,136 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:58,136 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2023-10-26 08:55:58,136 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:58,137 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2023-10-26 08:55:58,137 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2023-10-26 08:55:58,137 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 152 out of 308
[2023-10-26 08:55:58,138 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 36 places, 32 transitions, 94 flow. Second operand  has 2 states, 2 states have (on average 153.0) internal successors, (306), 2 states have internal predecessors, (306), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:58,138 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:58,138 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 152 of 308
[2023-10-26 08:55:58,138 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:58,455 INFO  L130       PetriNetUnfolder]: 1241/2159 cut-off events.
[2023-10-26 08:55:58,455 INFO  L131       PetriNetUnfolder]: For 277/277 co-relation queries the response was YES.
[2023-10-26 08:55:58,457 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 11479 event pairs, 1210 based on Foata normal form. 0/1945 useless extension candidates. Maximal degree in co-relation 718. Up to 1932 conditions per place. 
[2023-10-26 08:55:58,469 INFO  L137   encePairwiseOnDemand]: 304/308 looper letters, 22 selfloop transitions, 0 changer transitions 0/28 dead transitions.
[2023-10-26 08:55:58,470 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 33 places, 28 transitions, 130 flow
[2023-10-26 08:55:58,470 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2023-10-26 08:55:58,470 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2023-10-26 08:55:58,471 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 330 transitions.
[2023-10-26 08:55:58,471 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5357142857142857
[2023-10-26 08:55:58,485 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 330 transitions.
[2023-10-26 08:55:58,485 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 330 transitions.
[2023-10-26 08:55:58,485 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:58,486 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 330 transitions.
[2023-10-26 08:55:58,486 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 165.0) internal successors, (330), 2 states have internal predecessors, (330), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:58,487 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 308.0) internal successors, (924), 3 states have internal predecessors, (924), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:58,488 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 308.0) internal successors, (924), 3 states have internal predecessors, (924), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:58,488 INFO  L175             Difference]: Start difference. First operand has 36 places, 32 transitions, 94 flow. Second operand 2 states and 330 transitions.
[2023-10-26 08:55:58,488 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 33 places, 28 transitions, 130 flow
[2023-10-26 08:55:58,490 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 33 places, 28 transitions, 130 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-26 08:55:58,491 INFO  L231             Difference]: Finished difference. Result has 33 places, 28 transitions, 86 flow
[2023-10-26 08:55:58,491 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=308, 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}
[2023-10-26 08:55:58,495 INFO  L288   CegarLoopForPetriNet]: 36 programPoint places, -3 predicate places.
[2023-10-26 08:55:58,497 INFO  L495      AbstractCegarLoop]: Abstraction has has 33 places, 28 transitions, 86 flow
[2023-10-26 08:55:58,497 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 153.0) internal successors, (306), 2 states have internal predecessors, (306), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:58,497 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:58,497 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1]
[2023-10-26 08:55:58,498 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2023-10-26 08:55:58,498 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2023-10-26 08:55:58,498 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:58,498 INFO  L85        PathProgramCache]: Analyzing trace with hash 1451858380, now seen corresponding path program 1 times
[2023-10-26 08:55:58,498 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:58,498 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [411747918]
[2023-10-26 08:55:58,499 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:58,499 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:58,508 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:58,536 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-26 08:55:58,536 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:58,537 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [411747918]
[2023-10-26 08:55:58,537 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [411747918] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:58,537 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:58,537 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-26 08:55:58,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1714278658]
[2023-10-26 08:55:58,541 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:58,541 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-26 08:55:58,542 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:58,542 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-26 08:55:58,542 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-26 08:55:58,572 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 145 out of 308
[2023-10-26 08:55:58,573 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 33 places, 28 transitions, 86 flow. Second operand  has 3 states, 3 states have (on average 147.0) internal successors, (441), 3 states have internal predecessors, (441), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:58,573 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:58,573 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 145 of 308
[2023-10-26 08:55:58,573 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:59,097 INFO  L130       PetriNetUnfolder]: 1697/2841 cut-off events.
[2023-10-26 08:55:59,097 INFO  L131       PetriNetUnfolder]: For 348/348 co-relation queries the response was YES.
[2023-10-26 08:55:59,099 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 146. Compared 15510 event pairs, 1246 based on Foata normal form. 0/2443 useless extension candidates. Maximal degree in co-relation 5687. Up to 2214 conditions per place. 
[2023-10-26 08:55:59,107 INFO  L137   encePairwiseOnDemand]: 303/308 looper letters, 36 selfloop transitions, 4 changer transitions 0/45 dead transitions.
[2023-10-26 08:55:59,121 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 35 places, 45 transitions, 218 flow
[2023-10-26 08:55:59,121 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-26 08:55:59,122 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-26 08:55:59,122 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 476 transitions.
[2023-10-26 08:55:59,123 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5151515151515151
[2023-10-26 08:55:59,123 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 476 transitions.
[2023-10-26 08:55:59,123 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 476 transitions.
[2023-10-26 08:55:59,123 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:59,123 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 476 transitions.
[2023-10-26 08:55:59,124 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 158.66666666666666) internal successors, (476), 3 states have internal predecessors, (476), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,126 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 308.0) internal successors, (1232), 4 states have internal predecessors, (1232), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,126 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 308.0) internal successors, (1232), 4 states have internal predecessors, (1232), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,127 INFO  L175             Difference]: Start difference. First operand has 33 places, 28 transitions, 86 flow. Second operand 3 states and 476 transitions.
[2023-10-26 08:55:59,127 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 35 places, 45 transitions, 218 flow
[2023-10-26 08:55:59,128 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 35 places, 45 transitions, 218 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-26 08:55:59,129 INFO  L231             Difference]: Finished difference. Result has 36 places, 31 transitions, 112 flow
[2023-10-26 08:55:59,129 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=308, 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}
[2023-10-26 08:55:59,130 INFO  L288   CegarLoopForPetriNet]: 36 programPoint places, 0 predicate places.
[2023-10-26 08:55:59,131 INFO  L495      AbstractCegarLoop]: Abstraction has has 36 places, 31 transitions, 112 flow
[2023-10-26 08:55:59,131 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 147.0) internal successors, (441), 3 states have internal predecessors, (441), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,131 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:59,145 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-26 08:55:59,145 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2023-10-26 08:55:59,145 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2023-10-26 08:55:59,146 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:59,146 INFO  L85        PathProgramCache]: Analyzing trace with hash 1478039782, now seen corresponding path program 1 times
[2023-10-26 08:55:59,146 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:59,146 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [617272850]
[2023-10-26 08:55:59,146 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:59,146 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:59,157 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-26 08:55:59,205 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2023-10-26 08:55:59,205 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-26 08:55:59,206 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [617272850]
[2023-10-26 08:55:59,206 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [617272850] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-26 08:55:59,206 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-26 08:55:59,206 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-26 08:55:59,206 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [800140991]
[2023-10-26 08:55:59,206 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-26 08:55:59,207 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-26 08:55:59,207 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-26 08:55:59,207 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-26 08:55:59,207 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-26 08:55:59,241 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 145 out of 308
[2023-10-26 08:55:59,241 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 36 places, 31 transitions, 112 flow. Second operand  has 3 states, 3 states have (on average 147.66666666666666) internal successors, (443), 3 states have internal predecessors, (443), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,242 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-26 08:55:59,242 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 145 of 308
[2023-10-26 08:55:59,242 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-26 08:55:59,836 INFO  L130       PetriNetUnfolder]: 2007/3363 cut-off events.
[2023-10-26 08:55:59,837 INFO  L131       PetriNetUnfolder]: For 1193/1246 co-relation queries the response was YES.
[2023-10-26 08:55:59,840 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 183. Compared 19131 event pairs, 1381 based on Foata normal form. 0/2858 useless extension candidates. Maximal degree in co-relation 7871. Up to 2668 conditions per place. 
[2023-10-26 08:55:59,858 INFO  L137   encePairwiseOnDemand]: 303/308 looper letters, 37 selfloop transitions, 5 changer transitions 0/47 dead transitions.
[2023-10-26 08:55:59,858 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 38 places, 47 transitions, 248 flow
[2023-10-26 08:55:59,858 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-26 08:55:59,859 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-26 08:55:59,860 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 475 transitions.
[2023-10-26 08:55:59,860 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5140692640692641
[2023-10-26 08:55:59,860 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 475 transitions.
[2023-10-26 08:55:59,860 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 475 transitions.
[2023-10-26 08:55:59,860 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-26 08:55:59,860 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 475 transitions.
[2023-10-26 08:55:59,861 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 158.33333333333334) internal successors, (475), 3 states have internal predecessors, (475), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,878 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 308.0) internal successors, (1232), 4 states have internal predecessors, (1232), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,879 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 308.0) internal successors, (1232), 4 states have internal predecessors, (1232), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,879 INFO  L175             Difference]: Start difference. First operand has 36 places, 31 transitions, 112 flow. Second operand 3 states and 475 transitions.
[2023-10-26 08:55:59,879 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 38 places, 47 transitions, 248 flow
[2023-10-26 08:55:59,885 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 37 places, 47 transitions, 243 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-10-26 08:55:59,886 INFO  L231             Difference]: Finished difference. Result has 38 places, 34 transitions, 141 flow
[2023-10-26 08:55:59,886 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=308, 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}
[2023-10-26 08:55:59,887 INFO  L288   CegarLoopForPetriNet]: 36 programPoint places, 2 predicate places.
[2023-10-26 08:55:59,887 INFO  L495      AbstractCegarLoop]: Abstraction has has 38 places, 34 transitions, 141 flow
[2023-10-26 08:55:59,887 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 147.66666666666666) internal successors, (443), 3 states have internal predecessors, (443), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-26 08:55:59,887 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-26 08:55:59,887 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-26 08:55:59,887 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2023-10-26 08:55:59,888 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 6 more)] ===
[2023-10-26 08:55:59,888 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-26 08:55:59,888 INFO  L85        PathProgramCache]: Analyzing trace with hash -2087485646, now seen corresponding path program 1 times
[2023-10-26 08:55:59,888 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-26 08:55:59,888 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [443763427]
[2023-10-26 08:55:59,888 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-26 08:55:59,889 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-26 08:55:59,931 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-26 08:55:59,931 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-26 08:55:59,944 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-26 08:55:59,964 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-26 08:55:59,964 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-26 08:55:59,965 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location threadErr0ASSERT_VIOLATIONDATA_RACE (8 of 9 remaining)
[2023-10-26 08:55:59,965 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (7 of 9 remaining)
[2023-10-26 08:55:59,965 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (6 of 9 remaining)
[2023-10-26 08:55:59,965 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (5 of 9 remaining)
[2023-10-26 08:55:59,966 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (4 of 9 remaining)
[2023-10-26 08:55:59,966 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (3 of 9 remaining)
[2023-10-26 08:55:59,966 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (2 of 9 remaining)
[2023-10-26 08:55:59,966 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 9 remaining)
[2023-10-26 08:55:59,966 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 9 remaining)
[2023-10-26 08:55:59,966 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2023-10-26 08:55:59,966 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2023-10-26 08:55:59,970 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 3 thread instances
[2023-10-26 08:55:59,985 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2023-10-26 08:56:00,041 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 26.10 08:56:00 BasicIcfg
[2023-10-26 08:56:00,041 INFO  L132        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2023-10-26 08:56:00,041 INFO  L113        PluginConnector]: ------------------------Witness Printer----------------------------
[2023-10-26 08:56:00,041 INFO  L271        PluginConnector]: Initializing Witness Printer...
[2023-10-26 08:56:00,042 INFO  L275        PluginConnector]: Witness Printer initialized
[2023-10-26 08:56:00,042 INFO  L185        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 26.10 08:55:38" (3/4) ...
[2023-10-26 08:56:00,044 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2023-10-26 08:56:00,057 INFO  L132        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2023-10-26 08:56:00,058 INFO  L158              Benchmark]: Toolchain (without parser) took 23844.63ms. Allocated memory was 45.9MB in the beginning and 96.0MB in the end (delta: 50.1MB). Free memory was 14.6MB in the beginning and 26.5MB in the end (delta: -11.9MB). Peak memory consumption was 38.3MB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,058 INFO  L158              Benchmark]: CDTParser took 0.14ms. Allocated memory is still 40.8MB. Free memory was 15.7MB in the beginning and 15.7MB in the end (delta: 31.6kB). Peak memory consumption was 31.6kB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,058 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 932.39ms. Allocated memory is still 45.9MB. Free memory was 14.4MB in the beginning and 19.0MB in the end (delta: -4.7MB). Peak memory consumption was 5.1MB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,059 INFO  L158              Benchmark]: Boogie Procedure Inliner took 88.69ms. Allocated memory is still 45.9MB. Free memory was 19.0MB in the beginning and 16.3MB in the end (delta: 2.7MB). Peak memory consumption was 2.7MB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,059 INFO  L158              Benchmark]: Boogie Preprocessor took 74.60ms. Allocated memory is still 45.9MB. Free memory was 16.3MB in the beginning and 14.3MB in the end (delta: 2.0MB). Peak memory consumption was 2.0MB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,060 INFO  L158              Benchmark]: RCFGBuilder took 813.28ms. Allocated memory is still 45.9MB. Free memory was 14.3MB in the beginning and 8.9MB in the end (delta: 5.4MB). Peak memory consumption was 6.3MB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,060 INFO  L158              Benchmark]: TraceAbstraction took 21915.20ms. Allocated memory was 45.9MB in the beginning and 96.0MB in the end (delta: 50.1MB). Free memory was 8.2MB in the beginning and 27.0MB in the end (delta: -18.8MB). Peak memory consumption was 31.3MB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,060 INFO  L158              Benchmark]: Witness Printer took 15.81ms. Allocated memory is still 96.0MB. Free memory was 27.0MB in the beginning and 26.5MB in the end (delta: 560.4kB). Peak memory consumption was 560.4kB. Max. memory is 15.6GB.
[2023-10-26 08:56:00,062 INFO  L339   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.14ms. Allocated memory is still 40.8MB. Free memory was 15.7MB in the beginning and 15.7MB in the end (delta: 31.6kB). Peak memory consumption was 31.6kB. Max. memory is 15.6GB.
 * CACSL2BoogieTranslator took 932.39ms. Allocated memory is still 45.9MB. Free memory was 14.4MB in the beginning and 19.0MB in the end (delta: -4.7MB). Peak memory consumption was 5.1MB. Max. memory is 15.6GB.
 * Boogie Procedure Inliner took 88.69ms. Allocated memory is still 45.9MB. Free memory was 19.0MB in the beginning and 16.3MB in the end (delta: 2.7MB). Peak memory consumption was 2.7MB. Max. memory is 15.6GB.
 * Boogie Preprocessor took 74.60ms. Allocated memory is still 45.9MB. Free memory was 16.3MB in the beginning and 14.3MB in the end (delta: 2.0MB). Peak memory consumption was 2.0MB. Max. memory is 15.6GB.
 * RCFGBuilder took 813.28ms. Allocated memory is still 45.9MB. Free memory was 14.3MB in the beginning and 8.9MB in the end (delta: 5.4MB). Peak memory consumption was 6.3MB. Max. memory is 15.6GB.
 * TraceAbstraction took 21915.20ms. Allocated memory was 45.9MB in the beginning and 96.0MB in the end (delta: 50.1MB). Free memory was 8.2MB in the beginning and 27.0MB in the end (delta: -18.8MB). Peak memory consumption was 31.3MB. Max. memory is 15.6GB.
 * Witness Printer took 15.81ms. Allocated memory is still 96.0MB. Free memory was 27.0MB in the beginning and 26.5MB in the end (delta: 560.4kB). Peak memory consumption was 560.4kB. Max. memory is 15.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 6.5s, 122 PlacesBefore, 18 PlacesAfterwards, 123 TransitionsBefore, 16 TransitionsAfterwards, 1802 CoEnabledTransitionPairs, 7 FixpointIterations, 47 TrivialSequentialCompositions, 66 ConcurrentSequentialCompositions, 5 TrivialYvCompositions, 4 ConcurrentYvCompositions, 3 ChoiceCompositions, 125 TotalNumberOfCompositions, 1369 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 1369, independent: 1369, independent conditional: 0, independent unconditional: 1369, 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: 928, independent: 928, independent conditional: 0, independent unconditional: 928, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 1369, independent: 441, independent conditional: 0, independent unconditional: 441, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 928, unknown conditional: 0, unknown unconditional: 928] , 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.7s, 142 PlacesBefore, 29 PlacesAfterwards, 142 TransitionsBefore, 26 TransitionsAfterwards, 4624 CoEnabledTransitionPairs, 7 FixpointIterations, 48 TrivialSequentialCompositions, 77 ConcurrentSequentialCompositions, 4 TrivialYvCompositions, 4 ConcurrentYvCompositions, 3 ChoiceCompositions, 136 TotalNumberOfCompositions, 6221 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 4276, independent: 4176, independent conditional: 0, independent unconditional: 4176, dependent: 100, dependent conditional: 0, dependent unconditional: 100, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 2399, independent: 2387, independent conditional: 0, independent unconditional: 2387, dependent: 12, dependent conditional: 0, dependent unconditional: 12, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 4276, independent: 1789, independent conditional: 0, independent unconditional: 1789, dependent: 88, dependent conditional: 0, dependent unconditional: 88, unknown: 2399, unknown conditional: 0, unknown unconditional: 2399] , Statistics on independence cache: Total cache size (in pairs): 72, Positive cache size: 67, Positive conditional cache size: 0, Positive unconditional cache size: 67, 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: 5.4s, 162 PlacesBefore, 36 PlacesAfterwards, 161 TransitionsBefore, 32 TransitionsAfterwards, 7956 CoEnabledTransitionPairs, 7 FixpointIterations, 46 TrivialSequentialCompositions, 90 ConcurrentSequentialCompositions, 4 TrivialYvCompositions, 4 ConcurrentYvCompositions, 3 ChoiceCompositions, 147 TotalNumberOfCompositions, 11320 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 7497, independent: 7353, independent conditional: 0, independent unconditional: 7353, dependent: 144, dependent conditional: 0, dependent unconditional: 144, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 4126, independent: 4102, independent conditional: 0, independent unconditional: 4102, dependent: 24, dependent conditional: 0, dependent unconditional: 24, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 7497, independent: 3251, independent conditional: 0, independent unconditional: 3251, dependent: 120, dependent conditional: 0, dependent unconditional: 120, unknown: 4126, unknown conditional: 0, unknown unconditional: 4126] , Statistics on independence cache: Total cache size (in pairs): 147, Positive cache size: 137, Positive conditional cache size: 0, Positive unconditional cache size: 137, 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()=-4, arg={0:0}, arg={0:0}, data=-4, 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()=-4, arg={0:0}, arg={0:0}, data=-4, 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()=0, arg={0:0}, arg={0:0}, data=0, 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: 1052]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1054]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1052]: 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, 138 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: 7.5s, OverallIterations: 2, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.2s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 6.7s, 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.1s SatisfiabilityAnalysisTime, 0.1s 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, 156 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: 6.8s, OverallIterations: 4, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 5.8s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 55 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 25 mSDsluCounter, 16 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, 16 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.1s 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, 174 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: 7.3s, OverallIterations: 4, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 5.5s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 61 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 39 mSDsluCounter, 2 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 8 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 173 IncrementalHoareTripleChecker+Invalid, 181 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 8 mSolverCounterUnsat, 2 mSDtfsCounter, 173 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.1s SatisfiabilityAnalysisTime, 0.1s 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!
[2023-10-26 08:56:00,159 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
