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


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


Checking for data races
Using default analysis
Version 2329fc70
Calling Ultimate with: /usr/lib/jvm/java-11-openjdk-amd64/bin/java -Dosgi.configuration.area=/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data -tc /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/AutomizerReach.xml -i /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value.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 3bf538699ff4830766ccfb2585b1925332e310c88598164afbd78ddc90cc3e5f
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2024-03-11 23:23:09,025 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2024-03-11 23:23:09,027 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2024-03-11 23:23:09,046 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2024-03-11 23:23:09,047 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2024-03-11 23:23:09,047 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2024-03-11 23:23:09,048 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2024-03-11 23:23:09,049 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2024-03-11 23:23:09,050 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2024-03-11 23:23:09,051 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2024-03-11 23:23:09,052 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2024-03-11 23:23:09,052 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2024-03-11 23:23:09,053 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2024-03-11 23:23:09,053 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2024-03-11 23:23:09,054 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2024-03-11 23:23:09,055 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2024-03-11 23:23:09,055 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2024-03-11 23:23:09,056 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2024-03-11 23:23:09,057 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2024-03-11 23:23:09,058 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2024-03-11 23:23:09,059 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2024-03-11 23:23:09,060 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2024-03-11 23:23:09,065 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2024-03-11 23:23:09,066 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2024-03-11 23:23:09,069 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2024-03-11 23:23:09,069 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2024-03-11 23:23:09,070 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2024-03-11 23:23:09,071 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2024-03-11 23:23:09,071 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2024-03-11 23:23:09,072 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2024-03-11 23:23:09,072 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2024-03-11 23:23:09,073 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2024-03-11 23:23:09,074 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2024-03-11 23:23:09,075 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2024-03-11 23:23:09,076 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2024-03-11 23:23:09,076 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2024-03-11 23:23:09,077 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2024-03-11 23:23:09,077 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2024-03-11 23:23:09,078 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2024-03-11 23:23:09,079 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2024-03-11 23:23:09,079 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2024-03-11 23:23:09,080 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2024-03-11 23:23:09,101 INFO  L113        SettingsManager]: Loading preferences was successful
[2024-03-11 23:23:09,101 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2024-03-11 23:23:09,102 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2024-03-11 23:23:09,102 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2024-03-11 23:23:09,102 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2024-03-11 23:23:09,102 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2024-03-11 23:23:09,103 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2024-03-11 23:23:09,103 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2024-03-11 23:23:09,103 INFO  L138        SettingsManager]:  * Use SBE=true
[2024-03-11 23:23:09,103 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2024-03-11 23:23:09,103 INFO  L138        SettingsManager]:  * sizeof long=4
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2024-03-11 23:23:09,104 INFO  L138        SettingsManager]:  * sizeof long double=12
[2024-03-11 23:23:09,105 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2024-03-11 23:23:09,105 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2024-03-11 23:23:09,105 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2024-03-11 23:23:09,105 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2024-03-11 23:23:09,105 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2024-03-11 23:23:09,105 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2024-03-11 23:23:09,105 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2024-03-11 23:23:09,105 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2024-03-11 23:23:09,106 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2024-03-11 23:23:09,107 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 -> 3bf538699ff4830766ccfb2585b1925332e310c88598164afbd78ddc90cc3e5f
[2024-03-11 23:23:09,268 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2024-03-11 23:23:09,286 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2024-03-11 23:23:09,287 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2024-03-11 23:23:09,288 INFO  L271        PluginConnector]: Initializing CDTParser...
[2024-03-11 23:23:09,289 INFO  L275        PluginConnector]: CDTParser initialized
[2024-03-11 23:23:09,290 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value.i
[2024-03-11 23:23:10,371 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2024-03-11 23:23:10,578 INFO  L351              CDTParser]: Found 1 translation units.
[2024-03-11 23:23:10,579 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value.i
[2024-03-11 23:23:10,589 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/65ad5bcdc/2ddac2d7f34b4943b84b3e12896b8681/FLAG2a5d61a02
[2024-03-11 23:23:10,599 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/65ad5bcdc/2ddac2d7f34b4943b84b3e12896b8681
[2024-03-11 23:23:10,601 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2024-03-11 23:23:10,602 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2024-03-11 23:23:10,603 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2024-03-11 23:23:10,603 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2024-03-11 23:23:10,606 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2024-03-11 23:23:10,607 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:10,607 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@17195198 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10, skipping insertion in model container
[2024-03-11 23:23:10,608 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:10,613 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2024-03-11 23:23:10,643 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2024-03-11 23:23:10,756 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2024-03-11 23:23:10,905 WARN  L237   ndardFunctionHandler]: Function reach_error is already implemented but we override the implementation for the call at /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value.i[47765,47778]
[2024-03-11 23:23:10,918 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2024-03-11 23:23:10,923 INFO  L203         MainTranslator]: Completed pre-run
[2024-03-11 23:23:10,933 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2024-03-11 23:23:10,949 WARN  L237   ndardFunctionHandler]: Function reach_error is already implemented but we override the implementation for the call at /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value.i[47765,47778]
[2024-03-11 23:23:10,955 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2024-03-11 23:23:10,990 INFO  L208         MainTranslator]: Completed translation
[2024-03-11 23:23:10,990 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10 WrapperNode
[2024-03-11 23:23:10,991 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2024-03-11 23:23:10,991 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2024-03-11 23:23:10,992 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2024-03-11 23:23:10,992 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2024-03-11 23:23:10,996 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,010 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,028 INFO  L138                Inliner]: procedures = 273, calls = 23, calls flagged for inlining = 6, calls inlined = 6, statements flattened = 114
[2024-03-11 23:23:11,029 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2024-03-11 23:23:11,029 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2024-03-11 23:23:11,029 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2024-03-11 23:23:11,029 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2024-03-11 23:23:11,036 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,036 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,040 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,040 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,046 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,049 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,050 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,051 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,053 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2024-03-11 23:23:11,054 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2024-03-11 23:23:11,054 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2024-03-11 23:23:11,054 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2024-03-11 23:23:11,054 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (1/1) ...
[2024-03-11 23:23:11,059 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2024-03-11 23:23:11,067 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2024-03-11 23:23:11,083 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2024-03-11 23:23:11,086 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2024-03-11 23:23:11,127 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2024-03-11 23:23:11,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2024-03-11 23:23:11,128 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2024-03-11 23:23:11,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2024-03-11 23:23:11,129 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2024-03-11 23:23:11,263 INFO  L235             CfgBuilder]: Building ICFG
[2024-03-11 23:23:11,264 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2024-03-11 23:23:11,443 INFO  L276             CfgBuilder]: Performing block encoding
[2024-03-11 23:23:11,449 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2024-03-11 23:23:11,450 INFO  L300             CfgBuilder]: Removed 2 assume(true) statements.
[2024-03-11 23:23:11,451 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 11.03 11:23:11 BoogieIcfgContainer
[2024-03-11 23:23:11,451 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2024-03-11 23:23:11,453 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2024-03-11 23:23:11,453 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2024-03-11 23:23:11,455 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2024-03-11 23:23:11,455 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 11.03 11:23:10" (1/3) ...
[2024-03-11 23:23:11,455 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@279d7d8e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 11.03 11:23:11, skipping insertion in model container
[2024-03-11 23:23:11,455 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 11.03 11:23:10" (2/3) ...
[2024-03-11 23:23:11,456 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@279d7d8e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 11.03 11:23:11, skipping insertion in model container
[2024-03-11 23:23:11,456 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 11.03 11:23:11" (3/3) ...
[2024-03-11 23:23:11,457 INFO  L112   eAbstractionObserver]: Analyzing ICFG thread-local-value.i
[2024-03-11 23:23:11,462 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2024-03-11 23:23:11,469 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2024-03-11 23:23:11,469 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 8 error locations.
[2024-03-11 23:23:11,469 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2024-03-11 23:23:11,510 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2024-03-11 23:23:11,536 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 130 places, 134 transitions, 276 flow
[2024-03-11 23:23:11,585 INFO  L130       PetriNetUnfolder]: 9/180 cut-off events.
[2024-03-11 23:23:11,585 INFO  L131       PetriNetUnfolder]: For 1/2 co-relation queries the response was YES.
[2024-03-11 23:23:11,590 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 186 conditions, 180 events. 9/180 cut-off events. For 1/2 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 365 event pairs, 0 based on Foata normal form. 0/156 useless extension candidates. Maximal degree in co-relation 97. Up to 4 conditions per place. 
[2024-03-11 23:23:11,590 INFO  L82        GeneralOperation]: Start removeDead. Operand has 130 places, 134 transitions, 276 flow
[2024-03-11 23:23:11,594 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 130 places, 134 transitions, 276 flow
[2024-03-11 23:23:11,596 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-03-11 23:23:11,604 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 130 places, 134 transitions, 276 flow
[2024-03-11 23:23:11,606 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 130 places, 134 transitions, 276 flow
[2024-03-11 23:23:11,606 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 130 places, 134 transitions, 276 flow
[2024-03-11 23:23:11,633 INFO  L130       PetriNetUnfolder]: 9/180 cut-off events.
[2024-03-11 23:23:11,633 INFO  L131       PetriNetUnfolder]: For 1/2 co-relation queries the response was YES.
[2024-03-11 23:23:11,634 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 186 conditions, 180 events. 9/180 cut-off events. For 1/2 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 365 event pairs, 0 based on Foata normal form. 0/156 useless extension candidates. Maximal degree in co-relation 97. Up to 4 conditions per place. 
[2024-03-11 23:23:11,636 INFO  L119        LiptonReduction]: Number of co-enabled transitions 4770
[2024-03-11 23:23:15,804 INFO  L134        LiptonReduction]: Checked pairs total: 3997
[2024-03-11 23:23:15,805 INFO  L136        LiptonReduction]: Total number of compositions: 148
[2024-03-11 23:23:15,816 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-11 23:23:15,820 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;@4074ab47, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-03-11 23:23:15,821 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 13 error locations.
[2024-03-11 23:23:15,822 INFO  L130       PetriNetUnfolder]: 0/3 cut-off events.
[2024-03-11 23:23:15,823 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:23:15,823 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:15,823 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2024-03-11 23:23:15,823 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 10 more)] ===
[2024-03-11 23:23:15,827 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:15,827 INFO  L85        PathProgramCache]: Analyzing trace with hash 16907, now seen corresponding path program 1 times
[2024-03-11 23:23:15,833 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:15,834 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [36570538]
[2024-03-11 23:23:15,834 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:15,834 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:15,911 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:15,951 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:15,951 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:15,951 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [36570538]
[2024-03-11 23:23:15,952 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [36570538] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:15,952 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:15,952 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2024-03-11 23:23:15,953 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [948033830]
[2024-03-11 23:23:15,954 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:15,959 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2024-03-11 23:23:15,959 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:15,974 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2024-03-11 23:23:15,975 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2024-03-11 23:23:15,977 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 123 out of 282
[2024-03-11 23:23:15,979 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 21 places, 19 transitions, 46 flow. Second operand  has 2 states, 2 states have (on average 124.0) internal successors, (248), 2 states have internal predecessors, (248), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:15,979 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:15,979 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 123 of 282
[2024-03-11 23:23:15,980 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:16,020 INFO  L130       PetriNetUnfolder]: 6/26 cut-off events.
[2024-03-11 23:23:16,021 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2024-03-11 23:23:16,021 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 58 conditions, 26 events. 6/26 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 52 event pairs, 5 based on Foata normal form. 0/20 useless extension candidates. Maximal degree in co-relation 32. Up to 25 conditions per place. 
[2024-03-11 23:23:16,022 INFO  L137   encePairwiseOnDemand]: 274/282 looper letters, 5 selfloop transitions, 0 changer transitions 5/11 dead transitions.
[2024-03-11 23:23:16,022 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 14 places, 11 transitions, 50 flow
[2024-03-11 23:23:16,023 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2024-03-11 23:23:16,024 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2024-03-11 23:23:16,030 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 264 transitions.
[2024-03-11 23:23:16,032 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.46808510638297873
[2024-03-11 23:23:16,032 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 264 transitions.
[2024-03-11 23:23:16,033 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 264 transitions.
[2024-03-11 23:23:16,034 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:16,035 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 264 transitions.
[2024-03-11 23:23:16,037 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 132.0) internal successors, (264), 2 states have internal predecessors, (264), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:16,043 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 282.0) internal successors, (846), 3 states have internal predecessors, (846), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:16,043 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 282.0) internal successors, (846), 3 states have internal predecessors, (846), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:16,045 INFO  L175             Difference]: Start difference. First operand has 21 places, 19 transitions, 46 flow. Second operand 2 states and 264 transitions.
[2024-03-11 23:23:16,046 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 14 places, 11 transitions, 50 flow
[2024-03-11 23:23:16,047 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 14 places, 11 transitions, 50 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:23:16,048 INFO  L231             Difference]: Finished difference. Result has 14 places, 6 transitions, 17 flow
[2024-03-11 23:23:16,049 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=282, PETRI_DIFFERENCE_MINUEND_FLOW=30, PETRI_DIFFERENCE_MINUEND_PLACES=13, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=11, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=11, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=17, PETRI_PLACES=14, PETRI_TRANSITIONS=6}
[2024-03-11 23:23:16,052 INFO  L288   CegarLoopForPetriNet]: 21 programPoint places, -7 predicate places.
[2024-03-11 23:23:16,052 INFO  L495      AbstractCegarLoop]: Abstraction has has 14 places, 6 transitions, 17 flow
[2024-03-11 23:23:16,052 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 124.0) internal successors, (248), 2 states have internal predecessors, (248), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:16,053 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:16,053 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1]
[2024-03-11 23:23:16,053 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2024-03-11 23:23:16,053 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 10 more)] ===
[2024-03-11 23:23:16,053 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:16,054 INFO  L85        PathProgramCache]: Analyzing trace with hash -1553961339, now seen corresponding path program 1 times
[2024-03-11 23:23:16,054 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:16,054 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [216173953]
[2024-03-11 23:23:16,054 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:16,054 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:16,092 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:23:16,092 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-03-11 23:23:16,112 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:23:16,128 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-03-11 23:23:16,128 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-03-11 23:23:16,130 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (12 of 13 remaining)
[2024-03-11 23:23:16,131 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (11 of 13 remaining)
[2024-03-11 23:23:16,131 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (10 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (9 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (8 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (7 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (6 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (5 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (4 of 13 remaining)
[2024-03-11 23:23:16,132 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (3 of 13 remaining)
[2024-03-11 23:23:16,133 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (2 of 13 remaining)
[2024-03-11 23:23:16,133 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (1 of 13 remaining)
[2024-03-11 23:23:16,133 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (0 of 13 remaining)
[2024-03-11 23:23:16,133 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2024-03-11 23:23:16,133 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1]
[2024-03-11 23:23:16,135 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-03-11 23:23:16,135 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2024-03-11 23:23:16,153 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2024-03-11 23:23:16,157 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 175 places, 181 transitions, 380 flow
[2024-03-11 23:23:16,202 INFO  L130       PetriNetUnfolder]: 17/323 cut-off events.
[2024-03-11 23:23:16,202 INFO  L131       PetriNetUnfolder]: For 6/8 co-relation queries the response was YES.
[2024-03-11 23:23:16,205 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 337 conditions, 323 events. 17/323 cut-off events. For 6/8 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 864 event pairs, 0 based on Foata normal form. 0/279 useless extension candidates. Maximal degree in co-relation 182. Up to 8 conditions per place. 
[2024-03-11 23:23:16,205 INFO  L82        GeneralOperation]: Start removeDead. Operand has 175 places, 181 transitions, 380 flow
[2024-03-11 23:23:16,207 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 175 places, 181 transitions, 380 flow
[2024-03-11 23:23:16,207 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-03-11 23:23:16,207 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 175 places, 181 transitions, 380 flow
[2024-03-11 23:23:16,208 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 175 places, 181 transitions, 380 flow
[2024-03-11 23:23:16,208 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 175 places, 181 transitions, 380 flow
[2024-03-11 23:23:16,245 INFO  L130       PetriNetUnfolder]: 17/323 cut-off events.
[2024-03-11 23:23:16,246 INFO  L131       PetriNetUnfolder]: For 6/8 co-relation queries the response was YES.
[2024-03-11 23:23:16,248 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 337 conditions, 323 events. 17/323 cut-off events. For 6/8 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 864 event pairs, 0 based on Foata normal form. 0/279 useless extension candidates. Maximal degree in co-relation 182. Up to 8 conditions per place. 
[2024-03-11 23:23:16,259 INFO  L119        LiptonReduction]: Number of co-enabled transitions 14760
[2024-03-11 23:23:19,768 INFO  L134        LiptonReduction]: Checked pairs total: 29674
[2024-03-11 23:23:19,768 INFO  L136        LiptonReduction]: Total number of compositions: 170
[2024-03-11 23:23:19,770 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-11 23:23:19,771 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;@4074ab47, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-03-11 23:23:19,771 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 17 error locations.
[2024-03-11 23:23:19,772 INFO  L130       PetriNetUnfolder]: 0/2 cut-off events.
[2024-03-11 23:23:19,772 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:23:19,772 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:19,772 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2024-03-11 23:23:19,772 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2024-03-11 23:23:19,772 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:19,772 INFO  L85        PathProgramCache]: Analyzing trace with hash 29771, now seen corresponding path program 1 times
[2024-03-11 23:23:19,773 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:19,773 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [586531621]
[2024-03-11 23:23:19,773 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:19,773 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:19,788 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:19,802 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:19,802 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:19,802 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [586531621]
[2024-03-11 23:23:19,802 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [586531621] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:19,802 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:19,802 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2024-03-11 23:23:19,802 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [972805109]
[2024-03-11 23:23:19,802 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:19,803 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2024-03-11 23:23:19,803 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:19,803 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2024-03-11 23:23:19,803 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2024-03-11 23:23:19,804 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 162 out of 351
[2024-03-11 23:23:19,804 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 57 places, 59 transitions, 136 flow. Second operand  has 2 states, 2 states have (on average 163.0) internal successors, (326), 2 states have internal predecessors, (326), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:19,804 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:19,804 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 162 of 351
[2024-03-11 23:23:19,805 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:20,016 INFO  L130       PetriNetUnfolder]: 1323/2650 cut-off events.
[2024-03-11 23:23:20,016 INFO  L131       PetriNetUnfolder]: For 64/64 co-relation queries the response was YES.
[2024-03-11 23:23:20,018 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 4895 conditions, 2650 events. 1323/2650 cut-off events. For 64/64 co-relation queries the response was YES. Maximal size of possible extension queue 113. Compared 16666 event pairs, 1310 based on Foata normal form. 146/2271 useless extension candidates. Maximal degree in co-relation 3647. Up to 2177 conditions per place. 
[2024-03-11 23:23:20,027 INFO  L137   encePairwiseOnDemand]: 342/351 looper letters, 31 selfloop transitions, 0 changer transitions 0/47 dead transitions.
[2024-03-11 23:23:20,027 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 51 places, 47 transitions, 174 flow
[2024-03-11 23:23:20,028 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2024-03-11 23:23:20,028 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2024-03-11 23:23:20,029 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 364 transitions.
[2024-03-11 23:23:20,030 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5185185185185185
[2024-03-11 23:23:20,030 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 364 transitions.
[2024-03-11 23:23:20,030 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 364 transitions.
[2024-03-11 23:23:20,030 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:20,030 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 364 transitions.
[2024-03-11 23:23:20,032 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 182.0) internal successors, (364), 2 states have internal predecessors, (364), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,033 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 351.0) internal successors, (1053), 3 states have internal predecessors, (1053), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,034 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 351.0) internal successors, (1053), 3 states have internal predecessors, (1053), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,034 INFO  L175             Difference]: Start difference. First operand has 57 places, 59 transitions, 136 flow. Second operand 2 states and 364 transitions.
[2024-03-11 23:23:20,034 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 51 places, 47 transitions, 174 flow
[2024-03-11 23:23:20,035 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 51 places, 47 transitions, 174 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:23:20,036 INFO  L231             Difference]: Finished difference. Result has 51 places, 47 transitions, 112 flow
[2024-03-11 23:23:20,036 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=351, PETRI_DIFFERENCE_MINUEND_FLOW=112, PETRI_DIFFERENCE_MINUEND_PLACES=50, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=47, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=47, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=112, PETRI_PLACES=51, PETRI_TRANSITIONS=47}
[2024-03-11 23:23:20,036 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, -6 predicate places.
[2024-03-11 23:23:20,037 INFO  L495      AbstractCegarLoop]: Abstraction has has 51 places, 47 transitions, 112 flow
[2024-03-11 23:23:20,037 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 163.0) internal successors, (326), 2 states have internal predecessors, (326), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,037 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:20,037 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1]
[2024-03-11 23:23:20,037 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2024-03-11 23:23:20,037 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2024-03-11 23:23:20,037 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:20,038 INFO  L85        PathProgramCache]: Analyzing trace with hash 887661955, now seen corresponding path program 1 times
[2024-03-11 23:23:20,038 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:20,038 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1721762401]
[2024-03-11 23:23:20,038 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:20,038 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:20,056 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:20,078 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:20,078 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:20,078 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1721762401]
[2024-03-11 23:23:20,078 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1721762401] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:20,078 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:20,078 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:23:20,079 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [716976471]
[2024-03-11 23:23:20,079 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:20,079 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:23:20,079 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:20,079 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:23:20,079 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:23:20,107 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 142 out of 351
[2024-03-11 23:23:20,108 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 51 places, 47 transitions, 112 flow. Second operand  has 3 states, 3 states have (on average 143.66666666666666) internal successors, (431), 3 states have internal predecessors, (431), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,108 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:20,108 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 142 of 351
[2024-03-11 23:23:20,108 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:20,469 INFO  L130       PetriNetUnfolder]: 2438/4270 cut-off events.
[2024-03-11 23:23:20,470 INFO  L131       PetriNetUnfolder]: For 106/106 co-relation queries the response was YES.
[2024-03-11 23:23:20,472 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 8508 conditions, 4270 events. 2438/4270 cut-off events. For 106/106 co-relation queries the response was YES. Maximal size of possible extension queue 147. Compared 25124 event pairs, 900 based on Foata normal form. 0/3512 useless extension candidates. Maximal degree in co-relation 8503. Up to 3438 conditions per place. 
[2024-03-11 23:23:20,482 INFO  L137   encePairwiseOnDemand]: 331/351 looper letters, 60 selfloop transitions, 14 changer transitions 0/80 dead transitions.
[2024-03-11 23:23:20,483 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 53 places, 80 transitions, 337 flow
[2024-03-11 23:23:20,484 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:23:20,485 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:23:20,486 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 506 transitions.
[2024-03-11 23:23:20,486 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.4805318138651472
[2024-03-11 23:23:20,487 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 506 transitions.
[2024-03-11 23:23:20,487 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 506 transitions.
[2024-03-11 23:23:20,487 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:20,487 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 506 transitions.
[2024-03-11 23:23:20,488 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 168.66666666666666) internal successors, (506), 3 states have internal predecessors, (506), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,491 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 351.0) internal successors, (1404), 4 states have internal predecessors, (1404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,491 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 351.0) internal successors, (1404), 4 states have internal predecessors, (1404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,491 INFO  L175             Difference]: Start difference. First operand has 51 places, 47 transitions, 112 flow. Second operand 3 states and 506 transitions.
[2024-03-11 23:23:20,491 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 53 places, 80 transitions, 337 flow
[2024-03-11 23:23:20,492 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 53 places, 80 transitions, 337 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:23:20,493 INFO  L231             Difference]: Finished difference. Result has 55 places, 61 transitions, 236 flow
[2024-03-11 23:23:20,494 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=351, PETRI_DIFFERENCE_MINUEND_FLOW=112, PETRI_DIFFERENCE_MINUEND_PLACES=51, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=47, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=33, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=236, PETRI_PLACES=55, PETRI_TRANSITIONS=61}
[2024-03-11 23:23:20,494 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, -2 predicate places.
[2024-03-11 23:23:20,494 INFO  L495      AbstractCegarLoop]: Abstraction has has 55 places, 61 transitions, 236 flow
[2024-03-11 23:23:20,495 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 143.66666666666666) internal successors, (431), 3 states have internal predecessors, (431), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,495 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:20,495 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:23:20,495 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2024-03-11 23:23:20,495 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2024-03-11 23:23:20,495 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:20,495 INFO  L85        PathProgramCache]: Analyzing trace with hash -1632366107, now seen corresponding path program 1 times
[2024-03-11 23:23:20,496 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:20,496 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1676399325]
[2024-03-11 23:23:20,496 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:20,496 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:20,505 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:20,524 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:20,524 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:20,524 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1676399325]
[2024-03-11 23:23:20,524 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1676399325] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:20,524 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:20,524 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:23:20,524 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1743668326]
[2024-03-11 23:23:20,524 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:20,525 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:23:20,525 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:20,525 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:23:20,525 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:23:20,549 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 150 out of 351
[2024-03-11 23:23:20,549 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 55 places, 61 transitions, 236 flow. Second operand  has 3 states, 3 states have (on average 152.66666666666666) internal successors, (458), 3 states have internal predecessors, (458), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,549 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:20,549 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 150 of 351
[2024-03-11 23:23:20,549 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:20,940 INFO  L130       PetriNetUnfolder]: 2312/4245 cut-off events.
[2024-03-11 23:23:20,940 INFO  L131       PetriNetUnfolder]: For 1306/1354 co-relation queries the response was YES.
[2024-03-11 23:23:20,944 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 10188 conditions, 4245 events. 2312/4245 cut-off events. For 1306/1354 co-relation queries the response was YES. Maximal size of possible extension queue 160. Compared 26428 event pairs, 1715 based on Foata normal form. 24/3517 useless extension candidates. Maximal degree in co-relation 10181. Up to 3542 conditions per place. 
[2024-03-11 23:23:20,955 INFO  L137   encePairwiseOnDemand]: 344/351 looper letters, 54 selfloop transitions, 9 changer transitions 2/82 dead transitions.
[2024-03-11 23:23:20,955 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 57 places, 82 transitions, 444 flow
[2024-03-11 23:23:20,956 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:23:20,956 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:23:20,957 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 503 transitions.
[2024-03-11 23:23:20,957 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.47768281101614435
[2024-03-11 23:23:20,957 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 503 transitions.
[2024-03-11 23:23:20,957 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 503 transitions.
[2024-03-11 23:23:20,957 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:20,958 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 503 transitions.
[2024-03-11 23:23:20,959 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 167.66666666666666) internal successors, (503), 3 states have internal predecessors, (503), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,961 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 351.0) internal successors, (1404), 4 states have internal predecessors, (1404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,961 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 351.0) internal successors, (1404), 4 states have internal predecessors, (1404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,961 INFO  L175             Difference]: Start difference. First operand has 55 places, 61 transitions, 236 flow. Second operand 3 states and 503 transitions.
[2024-03-11 23:23:20,961 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 57 places, 82 transitions, 444 flow
[2024-03-11 23:23:20,968 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 55 places, 82 transitions, 404 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:23:20,969 INFO  L231             Difference]: Finished difference. Result has 56 places, 68 transitions, 277 flow
[2024-03-11 23:23:20,969 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=351, PETRI_DIFFERENCE_MINUEND_FLOW=208, PETRI_DIFFERENCE_MINUEND_PLACES=53, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=61, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=52, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=277, PETRI_PLACES=56, PETRI_TRANSITIONS=68}
[2024-03-11 23:23:20,969 INFO  L288   CegarLoopForPetriNet]: 57 programPoint places, -1 predicate places.
[2024-03-11 23:23:20,970 INFO  L495      AbstractCegarLoop]: Abstraction has has 56 places, 68 transitions, 277 flow
[2024-03-11 23:23:20,970 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 152.66666666666666) internal successors, (458), 3 states have internal predecessors, (458), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:20,970 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:20,970 INFO  L209   CegarLoopForPetriNet]: trace histogram [3, 2, 2, 1, 1, 1, 1]
[2024-03-11 23:23:20,970 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2024-03-11 23:23:20,970 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2024-03-11 23:23:20,970 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:20,971 INFO  L85        PathProgramCache]: Analyzing trace with hash -158530784, now seen corresponding path program 1 times
[2024-03-11 23:23:20,971 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:20,971 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [751749449]
[2024-03-11 23:23:20,971 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:20,971 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:21,041 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:23:21,042 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-03-11 23:23:21,053 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:23:21,057 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-03-11 23:23:21,058 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-03-11 23:23:21,058 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (16 of 17 remaining)
[2024-03-11 23:23:21,058 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (15 of 17 remaining)
[2024-03-11 23:23:21,058 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (14 of 17 remaining)
[2024-03-11 23:23:21,058 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (13 of 17 remaining)
[2024-03-11 23:23:21,058 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (12 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (11 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (10 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (9 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (8 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (7 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (6 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (5 of 17 remaining)
[2024-03-11 23:23:21,059 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (4 of 17 remaining)
[2024-03-11 23:23:21,060 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (3 of 17 remaining)
[2024-03-11 23:23:21,060 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (2 of 17 remaining)
[2024-03-11 23:23:21,060 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (1 of 17 remaining)
[2024-03-11 23:23:21,060 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (0 of 17 remaining)
[2024-03-11 23:23:21,060 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2024-03-11 23:23:21,060 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2024-03-11 23:23:21,060 WARN  L233   ceAbstractionStarter]: 2 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-03-11 23:23:21,061 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 3 thread instances.
[2024-03-11 23:23:21,075 INFO  L144    ThreadInstanceAdder]: Constructed 3 joinOtherThreadTransitions.
[2024-03-11 23:23:21,077 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 220 places, 228 transitions, 486 flow
[2024-03-11 23:23:21,123 INFO  L130       PetriNetUnfolder]: 30/545 cut-off events.
[2024-03-11 23:23:21,123 INFO  L131       PetriNetUnfolder]: For 19/22 co-relation queries the response was YES.
[2024-03-11 23:23:21,126 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 573 conditions, 545 events. 30/545 cut-off events. For 19/22 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 1813 event pairs, 1 based on Foata normal form. 0/471 useless extension candidates. Maximal degree in co-relation 331. Up to 16 conditions per place. 
[2024-03-11 23:23:21,126 INFO  L82        GeneralOperation]: Start removeDead. Operand has 220 places, 228 transitions, 486 flow
[2024-03-11 23:23:21,128 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 220 places, 228 transitions, 486 flow
[2024-03-11 23:23:21,129 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2024-03-11 23:23:21,129 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 220 places, 228 transitions, 486 flow
[2024-03-11 23:23:21,129 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 220 places, 228 transitions, 486 flow
[2024-03-11 23:23:21,129 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 220 places, 228 transitions, 486 flow
[2024-03-11 23:23:21,197 INFO  L130       PetriNetUnfolder]: 30/545 cut-off events.
[2024-03-11 23:23:21,197 INFO  L131       PetriNetUnfolder]: For 19/22 co-relation queries the response was YES.
[2024-03-11 23:23:21,199 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 573 conditions, 545 events. 30/545 cut-off events. For 19/22 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 1813 event pairs, 1 based on Foata normal form. 0/471 useless extension candidates. Maximal degree in co-relation 331. Up to 16 conditions per place. 
[2024-03-11 23:23:21,212 INFO  L119        LiptonReduction]: Number of co-enabled transitions 28620
[2024-03-11 23:23:24,526 INFO  L134        LiptonReduction]: Checked pairs total: 66452
[2024-03-11 23:23:24,527 INFO  L136        LiptonReduction]: Total number of compositions: 211
[2024-03-11 23:23:24,529 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-11 23:23:24,531 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;@4074ab47, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2024-03-11 23:23:24,531 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 21 error locations.
[2024-03-11 23:23:24,533 INFO  L130       PetriNetUnfolder]: 0/2 cut-off events.
[2024-03-11 23:23:24,533 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2024-03-11 23:23:24,533 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:24,533 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1]
[2024-03-11 23:23:24,533 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 18 more)] ===
[2024-03-11 23:23:24,534 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:24,534 INFO  L85        PathProgramCache]: Analyzing trace with hash 45341, now seen corresponding path program 1 times
[2024-03-11 23:23:24,534 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:24,534 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [869995987]
[2024-03-11 23:23:24,534 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:24,534 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:24,551 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:24,558 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:24,558 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:24,558 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [869995987]
[2024-03-11 23:23:24,558 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [869995987] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:24,558 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:24,559 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [1] imperfect sequences [] total 1
[2024-03-11 23:23:24,559 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [204345053]
[2024-03-11 23:23:24,559 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:24,559 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2024-03-11 23:23:24,559 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:24,559 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2024-03-11 23:23:24,559 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2024-03-11 23:23:24,560 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 201 out of 439
[2024-03-11 23:23:24,560 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 78 places, 81 transitions, 192 flow. Second operand  has 2 states, 2 states have (on average 202.0) internal successors, (404), 2 states have internal predecessors, (404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:24,560 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:24,560 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 201 of 439
[2024-03-11 23:23:24,560 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:26,653 INFO  L130       PetriNetUnfolder]: 21892/36027 cut-off events.
[2024-03-11 23:23:26,654 INFO  L131       PetriNetUnfolder]: For 1405/1405 co-relation queries the response was YES.
[2024-03-11 23:23:26,690 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 68006 conditions, 36027 events. 21892/36027 cut-off events. For 1405/1405 co-relation queries the response was YES. Maximal size of possible extension queue 1107. Compared 290167 event pairs, 21748 based on Foata normal form. 2380/31422 useless extension candidates. Maximal degree in co-relation 18690. Up to 31011 conditions per place. 
[2024-03-11 23:23:26,841 INFO  L137   encePairwiseOnDemand]: 428/439 looper letters, 42 selfloop transitions, 0 changer transitions 0/67 dead transitions.
[2024-03-11 23:23:26,842 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 72 places, 67 transitions, 248 flow
[2024-03-11 23:23:26,842 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2024-03-11 23:23:26,842 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 2 states.
[2024-03-11 23:23:26,843 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2 states to 2 states and 455 transitions.
[2024-03-11 23:23:26,843 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5182232346241458
[2024-03-11 23:23:26,843 INFO  L72            ComplementDD]: Start complementDD. Operand 2 states and 455 transitions.
[2024-03-11 23:23:26,843 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 2 states and 455 transitions.
[2024-03-11 23:23:26,844 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:26,844 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 2 states and 455 transitions.
[2024-03-11 23:23:26,845 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 3 states, 2 states have (on average 227.5) internal successors, (455), 2 states have internal predecessors, (455), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:26,846 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 3 states, 3 states have (on average 439.0) internal successors, (1317), 3 states have internal predecessors, (1317), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:26,847 INFO  L81            ComplementDD]: Finished complementDD. Result  has 3 states, 3 states have (on average 439.0) internal successors, (1317), 3 states have internal predecessors, (1317), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:26,847 INFO  L175             Difference]: Start difference. First operand has 78 places, 81 transitions, 192 flow. Second operand 2 states and 455 transitions.
[2024-03-11 23:23:26,847 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 72 places, 67 transitions, 248 flow
[2024-03-11 23:23:26,848 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 72 places, 67 transitions, 248 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:23:26,849 INFO  L231             Difference]: Finished difference. Result has 72 places, 67 transitions, 164 flow
[2024-03-11 23:23:26,849 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=439, PETRI_DIFFERENCE_MINUEND_FLOW=164, PETRI_DIFFERENCE_MINUEND_PLACES=71, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=67, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=67, PETRI_DIFFERENCE_SUBTRAHEND_STATES=2, PETRI_FLOW=164, PETRI_PLACES=72, PETRI_TRANSITIONS=67}
[2024-03-11 23:23:26,850 INFO  L288   CegarLoopForPetriNet]: 78 programPoint places, -6 predicate places.
[2024-03-11 23:23:26,850 INFO  L495      AbstractCegarLoop]: Abstraction has has 72 places, 67 transitions, 164 flow
[2024-03-11 23:23:26,850 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 202.0) internal successors, (404), 2 states have internal predecessors, (404), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:26,850 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:26,850 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1]
[2024-03-11 23:23:26,850 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2024-03-11 23:23:26,850 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 18 more)] ===
[2024-03-11 23:23:26,851 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:26,851 INFO  L85        PathProgramCache]: Analyzing trace with hash 1351889551, now seen corresponding path program 1 times
[2024-03-11 23:23:26,851 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:26,851 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [965767392]
[2024-03-11 23:23:26,851 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:26,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:26,858 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:26,871 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:26,871 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:26,871 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [965767392]
[2024-03-11 23:23:26,871 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [965767392] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:26,871 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:26,871 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:23:26,872 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1866187512]
[2024-03-11 23:23:26,872 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:26,872 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:23:26,872 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:26,872 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:23:26,872 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:23:26,904 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 171 out of 439
[2024-03-11 23:23:26,905 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 72 places, 67 transitions, 164 flow. Second operand  has 3 states, 3 states have (on average 172.66666666666666) internal successors, (518), 3 states have internal predecessors, (518), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:26,905 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:26,905 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 171 of 439
[2024-03-11 23:23:26,905 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:32,416 INFO  L130       PetriNetUnfolder]: 65889/102980 cut-off events.
[2024-03-11 23:23:32,417 INFO  L131       PetriNetUnfolder]: For 3145/3145 co-relation queries the response was YES.
[2024-03-11 23:23:32,525 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 201315 conditions, 102980 events. 65889/102980 cut-off events. For 3145/3145 co-relation queries the response was YES. Maximal size of possible extension queue 2597. Compared 835829 event pairs, 31598 based on Foata normal form. 0/82682 useless extension candidates. Maximal degree in co-relation 201309. Up to 82506 conditions per place. 
[2024-03-11 23:23:32,792 INFO  L137   encePairwiseOnDemand]: 409/439 looper letters, 84 selfloop transitions, 21 changer transitions 0/114 dead transitions.
[2024-03-11 23:23:32,793 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 74 places, 114 transitions, 489 flow
[2024-03-11 23:23:32,793 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:23:32,794 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:23:32,795 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 627 transitions.
[2024-03-11 23:23:32,795 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.4760820045558087
[2024-03-11 23:23:32,795 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 627 transitions.
[2024-03-11 23:23:32,795 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 627 transitions.
[2024-03-11 23:23:32,795 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:32,795 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 627 transitions.
[2024-03-11 23:23:32,797 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 209.0) internal successors, (627), 3 states have internal predecessors, (627), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:32,799 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 439.0) internal successors, (1756), 4 states have internal predecessors, (1756), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:32,799 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 439.0) internal successors, (1756), 4 states have internal predecessors, (1756), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:32,799 INFO  L175             Difference]: Start difference. First operand has 72 places, 67 transitions, 164 flow. Second operand 3 states and 627 transitions.
[2024-03-11 23:23:32,799 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 74 places, 114 transitions, 489 flow
[2024-03-11 23:23:32,801 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 74 places, 114 transitions, 489 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-11 23:23:32,802 INFO  L231             Difference]: Finished difference. Result has 76 places, 88 transitions, 350 flow
[2024-03-11 23:23:32,802 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=439, PETRI_DIFFERENCE_MINUEND_FLOW=164, PETRI_DIFFERENCE_MINUEND_PLACES=72, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=67, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=0, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=46, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=350, PETRI_PLACES=76, PETRI_TRANSITIONS=88}
[2024-03-11 23:23:32,803 INFO  L288   CegarLoopForPetriNet]: 78 programPoint places, -2 predicate places.
[2024-03-11 23:23:32,803 INFO  L495      AbstractCegarLoop]: Abstraction has has 76 places, 88 transitions, 350 flow
[2024-03-11 23:23:32,803 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 172.66666666666666) internal successors, (518), 3 states have internal predecessors, (518), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:32,803 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:32,803 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:23:32,804 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2024-03-11 23:23:32,804 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 18 more)] ===
[2024-03-11 23:23:32,804 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:32,804 INFO  L85        PathProgramCache]: Analyzing trace with hash -1317181706, now seen corresponding path program 1 times
[2024-03-11 23:23:32,804 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:32,804 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1271628321]
[2024-03-11 23:23:32,804 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:32,804 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:32,812 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:32,827 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-11 23:23:32,828 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:32,828 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1271628321]
[2024-03-11 23:23:32,828 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1271628321] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:32,828 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:32,828 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:23:32,828 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1749324014]
[2024-03-11 23:23:32,828 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:32,828 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:23:32,828 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:32,829 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:23:32,829 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:23:32,878 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 185 out of 439
[2024-03-11 23:23:32,879 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 76 places, 88 transitions, 350 flow. Second operand  has 3 states, 3 states have (on average 187.66666666666666) internal successors, (563), 3 states have internal predecessors, (563), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:32,879 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:32,879 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 185 of 439
[2024-03-11 23:23:32,879 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:39,440 INFO  L130       PetriNetUnfolder]: 75261/117272 cut-off events.
[2024-03-11 23:23:39,440 INFO  L131       PetriNetUnfolder]: For 46283/47995 co-relation queries the response was YES.
[2024-03-11 23:23:39,626 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 288266 conditions, 117272 events. 75261/117272 cut-off events. For 46283/47995 co-relation queries the response was YES. Maximal size of possible extension queue 3064. Compared 975538 event pairs, 51023 based on Foata normal form. 120/95153 useless extension candidates. Maximal degree in co-relation 288258. Up to 89778 conditions per place. 
[2024-03-11 23:23:39,950 INFO  L137   encePairwiseOnDemand]: 427/439 looper letters, 86 selfloop transitions, 21 changer transitions 0/133 dead transitions.
[2024-03-11 23:23:39,950 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 78 places, 133 transitions, 744 flow
[2024-03-11 23:23:39,951 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:23:39,951 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:23:39,952 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 635 transitions.
[2024-03-11 23:23:39,952 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.48215641609719057
[2024-03-11 23:23:39,952 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 635 transitions.
[2024-03-11 23:23:39,953 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 635 transitions.
[2024-03-11 23:23:39,953 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:39,953 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 635 transitions.
[2024-03-11 23:23:39,954 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 211.66666666666666) internal successors, (635), 3 states have internal predecessors, (635), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:39,956 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 439.0) internal successors, (1756), 4 states have internal predecessors, (1756), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:39,957 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 439.0) internal successors, (1756), 4 states have internal predecessors, (1756), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:39,957 INFO  L175             Difference]: Start difference. First operand has 76 places, 88 transitions, 350 flow. Second operand 3 states and 635 transitions.
[2024-03-11 23:23:39,957 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 78 places, 133 transitions, 744 flow
[2024-03-11 23:23:40,098 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 76 places, 133 transitions, 678 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:23:40,100 INFO  L231             Difference]: Finished difference. Result has 78 places, 107 transitions, 506 flow
[2024-03-11 23:23:40,100 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=439, PETRI_DIFFERENCE_MINUEND_FLOW=308, PETRI_DIFFERENCE_MINUEND_PLACES=74, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=88, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=67, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=506, PETRI_PLACES=78, PETRI_TRANSITIONS=107}
[2024-03-11 23:23:40,100 INFO  L288   CegarLoopForPetriNet]: 78 programPoint places, 0 predicate places.
[2024-03-11 23:23:40,101 INFO  L495      AbstractCegarLoop]: Abstraction has has 78 places, 107 transitions, 506 flow
[2024-03-11 23:23:40,101 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 187.66666666666666) internal successors, (563), 3 states have internal predecessors, (563), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:40,101 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:40,101 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:23:40,101 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2024-03-11 23:23:40,101 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 18 more)] ===
[2024-03-11 23:23:40,102 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:40,102 INFO  L85        PathProgramCache]: Analyzing trace with hash 27076088, now seen corresponding path program 1 times
[2024-03-11 23:23:40,102 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:40,102 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1011615115]
[2024-03-11 23:23:40,102 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:40,102 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:40,113 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-11 23:23:40,128 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2024-03-11 23:23:40,128 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-11 23:23:40,129 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1011615115]
[2024-03-11 23:23:40,129 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1011615115] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-11 23:23:40,129 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-11 23:23:40,129 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2024-03-11 23:23:40,129 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2047132992]
[2024-03-11 23:23:40,129 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-11 23:23:40,129 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2024-03-11 23:23:40,129 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-11 23:23:40,129 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2024-03-11 23:23:40,130 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2024-03-11 23:23:40,174 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 185 out of 439
[2024-03-11 23:23:40,175 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 78 places, 107 transitions, 506 flow. Second operand  has 3 states, 3 states have (on average 188.66666666666666) internal successors, (566), 3 states have internal predecessors, (566), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:40,175 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-11 23:23:40,175 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 185 of 439
[2024-03-11 23:23:40,175 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-11 23:23:48,551 INFO  L130       PetriNetUnfolder]: 88396/135405 cut-off events.
[2024-03-11 23:23:48,552 INFO  L131       PetriNetUnfolder]: For 120417/128310 co-relation queries the response was YES.
[2024-03-11 23:23:48,768 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 370943 conditions, 135405 events. 88396/135405 cut-off events. For 120417/128310 co-relation queries the response was YES. Maximal size of possible extension queue 3607. Compared 1118553 event pairs, 55628 based on Foata normal form. 1451/109366 useless extension candidates. Maximal degree in co-relation 370934. Up to 105719 conditions per place. 
[2024-03-11 23:23:49,151 INFO  L137   encePairwiseOnDemand]: 427/439 looper letters, 97 selfloop transitions, 33 changer transitions 0/157 dead transitions.
[2024-03-11 23:23:49,152 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 80 places, 157 transitions, 1007 flow
[2024-03-11 23:23:49,152 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2024-03-11 23:23:49,152 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2024-03-11 23:23:49,154 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 633 transitions.
[2024-03-11 23:23:49,154 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.4806378132118451
[2024-03-11 23:23:49,154 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 633 transitions.
[2024-03-11 23:23:49,154 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 633 transitions.
[2024-03-11 23:23:49,154 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-11 23:23:49,155 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 633 transitions.
[2024-03-11 23:23:49,156 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 211.0) internal successors, (633), 3 states have internal predecessors, (633), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:49,157 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 439.0) internal successors, (1756), 4 states have internal predecessors, (1756), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:49,158 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 439.0) internal successors, (1756), 4 states have internal predecessors, (1756), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:49,158 INFO  L175             Difference]: Start difference. First operand has 78 places, 107 transitions, 506 flow. Second operand 3 states and 633 transitions.
[2024-03-11 23:23:49,158 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 80 places, 157 transitions, 1007 flow
[2024-03-11 23:23:50,393 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 78 places, 157 transitions, 941 flow, removed 0 selfloop flow, removed 2 redundant places.
[2024-03-11 23:23:50,395 INFO  L231             Difference]: Finished difference. Result has 80 places, 134 transitions, 802 flow
[2024-03-11 23:23:50,395 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=439, PETRI_DIFFERENCE_MINUEND_FLOW=464, PETRI_DIFFERENCE_MINUEND_PLACES=76, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=107, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=6, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=74, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=802, PETRI_PLACES=80, PETRI_TRANSITIONS=134}
[2024-03-11 23:23:50,396 INFO  L288   CegarLoopForPetriNet]: 78 programPoint places, 2 predicate places.
[2024-03-11 23:23:50,396 INFO  L495      AbstractCegarLoop]: Abstraction has has 80 places, 134 transitions, 802 flow
[2024-03-11 23:23:50,396 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 188.66666666666666) internal successors, (566), 3 states have internal predecessors, (566), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-11 23:23:50,396 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2024-03-11 23:23:50,396 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-11 23:23:50,396 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2024-03-11 23:23:50,397 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 18 more)] ===
[2024-03-11 23:23:50,397 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-11 23:23:50,397 INFO  L85        PathProgramCache]: Analyzing trace with hash -1159829118, now seen corresponding path program 1 times
[2024-03-11 23:23:50,397 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-11 23:23:50,397 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1612428287]
[2024-03-11 23:23:50,397 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-11 23:23:50,398 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-11 23:23:50,410 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:23:50,410 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-03-11 23:23:50,417 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-11 23:23:50,421 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-03-11 23:23:50,421 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location threadErr0ASSERT_VIOLATIONDATA_RACE (20 of 21 remaining)
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (19 of 21 remaining)
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (18 of 21 remaining)
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (17 of 21 remaining)
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (16 of 21 remaining)
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (15 of 21 remaining)
[2024-03-11 23:23:50,422 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (14 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (13 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (12 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (11 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (10 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (9 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (8 of 21 remaining)
[2024-03-11 23:23:50,423 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (7 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (6 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (5 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (4 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (3 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (2 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (1 of 21 remaining)
[2024-03-11 23:23:50,424 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (0 of 21 remaining)
[2024-03-11 23:23:50,425 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2024-03-11 23:23:50,425 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2024-03-11 23:23:50,428 INFO  L228   ceAbstractionStarter]: Analysis of concurrent program completed with 3 thread instances
[2024-03-11 23:23:50,428 INFO  L178   ceAbstractionStarter]: Computing trace abstraction results
[2024-03-11 23:23:50,454 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 11.03 11:23:50 BasicIcfg
[2024-03-11 23:23:50,454 INFO  L132        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2024-03-11 23:23:50,454 INFO  L113        PluginConnector]: ------------------------Witness Printer----------------------------
[2024-03-11 23:23:50,454 INFO  L271        PluginConnector]: Initializing Witness Printer...
[2024-03-11 23:23:50,455 INFO  L275        PluginConnector]: Witness Printer initialized
[2024-03-11 23:23:50,455 INFO  L185        PluginConnector]: Executing the observer RCFGCatcher from plugin Witness Printer for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 11.03 11:23:11" (3/4) ...
[2024-03-11 23:23:50,457 INFO  L140         WitnessPrinter]: No result that supports witness generation found
[2024-03-11 23:23:50,457 INFO  L132        PluginConnector]: ------------------------ END Witness Printer----------------------------
[2024-03-11 23:23:50,457 INFO  L158              Benchmark]: Toolchain (without parser) took 39855.32ms. Allocated memory was 123.7MB in the beginning and 8.7GB in the end (delta: 8.6GB). Free memory was 80.7MB in the beginning and 6.0GB in the end (delta: -5.9GB). Peak memory consumption was 2.7GB. Max. memory is 16.1GB.
[2024-03-11 23:23:50,458 INFO  L158              Benchmark]: CDTParser took 0.11ms. Allocated memory is still 123.7MB. Free memory is still 90.9MB. There was no memory consumed. Max. memory is 16.1GB.
[2024-03-11 23:23:50,458 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 387.85ms. Allocated memory is still 123.7MB. Free memory was 80.4MB in the beginning and 52.0MB in the end (delta: 28.4MB). Peak memory consumption was 29.4MB. Max. memory is 16.1GB.
[2024-03-11 23:23:50,458 INFO  L158              Benchmark]: Boogie Procedure Inliner took 37.40ms. Allocated memory is still 123.7MB. Free memory was 52.0MB in the beginning and 49.2MB in the end (delta: 2.8MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-03-11 23:23:50,459 INFO  L158              Benchmark]: Boogie Preprocessor took 24.03ms. Allocated memory is still 123.7MB. Free memory was 49.2MB in the beginning and 47.5MB in the end (delta: 1.7MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
[2024-03-11 23:23:50,459 INFO  L158              Benchmark]: RCFGBuilder took 397.39ms. Allocated memory is still 123.7MB. Free memory was 47.5MB in the beginning and 82.1MB in the end (delta: -34.5MB). Peak memory consumption was 9.2MB. Max. memory is 16.1GB.
[2024-03-11 23:23:50,459 INFO  L158              Benchmark]: TraceAbstraction took 39001.31ms. Allocated memory was 123.7MB in the beginning and 8.7GB in the end (delta: 8.6GB). Free memory was 81.2MB in the beginning and 6.0GB in the end (delta: -5.9GB). Peak memory consumption was 2.7GB. Max. memory is 16.1GB.
[2024-03-11 23:23:50,459 INFO  L158              Benchmark]: Witness Printer took 2.68ms. Allocated memory is still 8.7GB. Free memory is still 6.0GB. There was no memory consumed. Max. memory is 16.1GB.
[2024-03-11 23:23:50,461 INFO  L339   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.11ms. Allocated memory is still 123.7MB. Free memory is still 90.9MB. There was no memory consumed. Max. memory is 16.1GB.
 * CACSL2BoogieTranslator took 387.85ms. Allocated memory is still 123.7MB. Free memory was 80.4MB in the beginning and 52.0MB in the end (delta: 28.4MB). Peak memory consumption was 29.4MB. Max. memory is 16.1GB.
 * Boogie Procedure Inliner took 37.40ms. Allocated memory is still 123.7MB. Free memory was 52.0MB in the beginning and 49.2MB in the end (delta: 2.8MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * Boogie Preprocessor took 24.03ms. Allocated memory is still 123.7MB. Free memory was 49.2MB in the beginning and 47.5MB in the end (delta: 1.7MB). Peak memory consumption was 2.1MB. Max. memory is 16.1GB.
 * RCFGBuilder took 397.39ms. Allocated memory is still 123.7MB. Free memory was 47.5MB in the beginning and 82.1MB in the end (delta: -34.5MB). Peak memory consumption was 9.2MB. Max. memory is 16.1GB.
 * TraceAbstraction took 39001.31ms. Allocated memory was 123.7MB in the beginning and 8.7GB in the end (delta: 8.6GB). Free memory was 81.2MB in the beginning and 6.0GB in the end (delta: -5.9GB). Peak memory consumption was 2.7GB. Max. memory is 16.1GB.
 * Witness Printer took 2.68ms. Allocated memory is still 8.7GB. Free memory is still 6.0GB. There was no memory consumed. Max. memory is 16.1GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 4.2s, 130 PlacesBefore, 21 PlacesAfterwards, 134 TransitionsBefore, 19 TransitionsAfterwards, 4770 CoEnabledTransitionPairs, 8 FixpointIterations, 31 TrivialSequentialCompositions, 94 ConcurrentSequentialCompositions, 4 TrivialYvCompositions, 13 ConcurrentYvCompositions, 6 ChoiceCompositions, 148 TotalNumberOfCompositions, 3997 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 3997, independent: 3997, independent conditional: 0, independent unconditional: 3997, 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: 2555, independent: 2555, independent conditional: 0, independent unconditional: 2555, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 3997, independent: 1442, independent conditional: 0, independent unconditional: 1442, dependent: 0, dependent conditional: 0, dependent unconditional: 0, unknown: 2555, unknown conditional: 0, unknown unconditional: 2555] , Statistics on independence cache: Total cache size (in pairs): 18, Positive cache size: 18, Positive conditional cache size: 0, Positive unconditional cache size: 18, 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: 3.6s, 175 PlacesBefore, 57 PlacesAfterwards, 181 TransitionsBefore, 59 TransitionsAfterwards, 14760 CoEnabledTransitionPairs, 6 FixpointIterations, 27 TrivialSequentialCompositions, 113 ConcurrentSequentialCompositions, 3 TrivialYvCompositions, 23 ConcurrentYvCompositions, 4 ChoiceCompositions, 170 TotalNumberOfCompositions, 29674 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 15632, independent: 15277, independent conditional: 0, independent unconditional: 15277, dependent: 355, dependent conditional: 0, dependent unconditional: 355, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 8384, independent: 8313, independent conditional: 0, independent unconditional: 8313, dependent: 71, dependent conditional: 0, dependent unconditional: 71, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 15632, independent: 6964, independent conditional: 0, independent unconditional: 6964, dependent: 284, dependent conditional: 0, dependent unconditional: 284, unknown: 8384, unknown conditional: 0, unknown unconditional: 8384] , Statistics on independence cache: Total cache size (in pairs): 456, Positive cache size: 419, Positive conditional cache size: 0, Positive unconditional cache size: 419, Negative cache size: 37, Negative conditional cache size: 0, Negative unconditional cache size: 37, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - StatisticsResult: PetriNetLargeBlockEncoding benchmarks
    Lipton Reduction Statistics: ReductionTime: 3.4s, 220 PlacesBefore, 78 PlacesAfterwards, 228 TransitionsBefore, 81 TransitionsAfterwards, 28620 CoEnabledTransitionPairs, 6 FixpointIterations, 30 TrivialSequentialCompositions, 138 ConcurrentSequentialCompositions, 5 TrivialYvCompositions, 33 ConcurrentYvCompositions, 5 ChoiceCompositions, 211 TotalNumberOfCompositions, 66452 MoverChecksTotal, Independence Relation Statistics: CachedIndependenceRelation.Independence Queries: [ total: 27932, independent: 27377, independent conditional: 0, independent unconditional: 27377, dependent: 555, dependent conditional: 0, dependent unconditional: 555, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , CachedIndependenceRelation.Statistics on underlying relation: SyntacticIndependenceRelation.Independence Queries: [ total: 15302, independent: 15177, independent conditional: 0, independent unconditional: 15177, dependent: 125, dependent conditional: 0, dependent unconditional: 125, unknown: 0, unknown conditional: 0, unknown unconditional: 0] , Cache Queries: [ total: 27932, independent: 12200, independent conditional: 0, independent unconditional: 12200, dependent: 430, dependent conditional: 0, dependent unconditional: 430, unknown: 15302, unknown conditional: 0, unknown unconditional: 15302] , Statistics on independence cache: Total cache size (in pairs): 684, Positive cache size: 632, Positive conditional cache size: 0, Positive unconditional cache size: 632, Negative cache size: 52, Negative conditional cache size: 0, Negative unconditional cache size: 52, Unknown cache size: 0, Unknown conditional cache size: 0, Unknown unconditional cache size: 0
  - DataRaceFoundResult [Line: 1031]: Data race detected
    Data race detected
The following path leads to a data race: 
[L1029]               0  int data = 0;
[L1038]               0  int breads_total = __VERIFIER_nondet_int();
[L1039]  CALL         0  assume_abort_if_not(breads_total >= 0)
[L1009]  COND FALSE   0  !(!cond)
[L1039]  RET          0  assume_abort_if_not(breads_total >= 0)
[L1040]               0  pthread_t *tids = malloc(breads_total * sizeof(pthread_t));
[L1040]               0  pthread_t *tids = malloc(breads_total * sizeof(pthread_t));
[L1041]               0  int i = 0;
         VAL             [breads_total=2, data=0, i=0, tids={5:0}]
[L1041]  COND TRUE    0  i < breads_total
[L1042]  EXPR         0  \read(*tids)
[L1042]  EXPR         0  tids[i]
[L1042]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [\read(*tids)={-3:0}, breads_total=2, data=0, i=0, pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))=-2, tids={5:0}]
[L1041]               0  i++
         VAL             [breads_total=2, data=0, i=1, tids={5:0}]
[L1041]  COND TRUE    0  i < breads_total
[L1042]  EXPR         0  \read(*tids)
[L1042]  EXPR         0  tids[i]
[L1031]  EXPR         1  data == 0
         VAL             [arg={0:0}, arg={0:0}, data=0]
[L1031]  CALL         1  __VERIFIER_assert(data == 0)
[L1042]  FCALL, FORK  0  pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))
         VAL             [\read(*tids)={-3:0}, breads_total=2, data=0, i=1, pthread_create(&tids[i], ((void *)0), &thread, ((void *)0))=-1, tids={5:0}]
[L1023]  COND FALSE   1  !(!(cond))
[L1031]  RET          1  __VERIFIER_assert(data == 0)
[L1032]               1  data = 1
         VAL             [arg={0:0}, arg={0:0}, data=1]
[L1031]               2  data == 0
         VAL             [arg={0:0}, arg={0:0}, data=1]
[L1032]               1  data = 1
         VAL             [arg={0:0}, arg={0:0}, data=1, data = 1=53]
[L1031]               2  data == 0
         VAL             [arg={0:0}, arg={0:0}, data=1, data = 1=53]

Now there is a data race on ~data~0 between 
	C: data = 1 [1032]
and
	C: data == 0 [1031]

  - UnprovableResult [Line: 1042]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1045]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1047]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1045]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1042]: Unable to prove that petrification did provide enough thread instances (tool internal message, not intended for end users)
    Unable to prove that petrification did provide enough thread instances (tool internal message, not intended for end users)
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1032]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1033]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - UnprovableResult [Line: 1034]: Unable to prove that there are no data races
    Unable to prove that there are no data races
 Reason: Not analyzed. 
  - StatisticsResult: Ultimate Automizer benchmark data with 1 thread instances
    CFG has 3 procedures, 171 locations, 13 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: 4.6s, OverallIterations: 2, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 4.3s, 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=46occurred in iteration=0, InterpolantAutomatonStates: 2, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.0s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 8 NumberOfCodeBlocks, 8 NumberOfCodeBlocksAsserted, 2 NumberOfCheckSat, 1 ConstructedInterpolants, 0 QuantifiedInterpolants, 1 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 1 InterpolantComputations, 1 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
  - StatisticsResult: Ultimate Automizer benchmark data with 2 thread instances
    CFG has 4 procedures, 214 locations, 17 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: 4.9s, OverallIterations: 4, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 3.6s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 130 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 68 mSDsluCounter, 13 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 38 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 238 IncrementalHoareTripleChecker+Invalid, 276 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 38 mSolverCounterUnsat, 13 mSDtfsCounter, 238 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=277occurred in iteration=3, InterpolantAutomatonStates: 8, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.0s SatisfiabilityAnalysisTime, 0.1s InterpolantComputationTime, 27 NumberOfCodeBlocks, 27 NumberOfCodeBlocksAsserted, 4 NumberOfCheckSat, 13 ConstructedInterpolants, 0 QuantifiedInterpolants, 17 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 3 InterpolantComputations, 3 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 3 thread instances
    CFG has 5 procedures, 257 locations, 21 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: 29.3s, OverallIterations: 5, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 25.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 3.5s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 317 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 137 mSDsluCounter, 38 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 0 mSDsCounter, 50 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 518 IncrementalHoareTripleChecker+Invalid, 568 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 50 mSolverCounterUnsat, 38 mSDtfsCounter, 518 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=802occurred in iteration=4, InterpolantAutomatonStates: 11, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.0s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 43 NumberOfCodeBlocks, 43 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 25 ConstructedInterpolants, 0 QuantifiedInterpolants, 31 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 4 InterpolantComputations, 4 PerfectInterpolantSequences, 2/2 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2024-03-11 23:23:50,497 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
--- End real Ultimate output ---

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