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


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


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

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 32bit --witnessprinter.graph.data.programhash efa45410300c0656b5dff15aa94228ada3facf40b9ca1e07e8eddd3745c4a129
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2023-10-27 12:51:26,810 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2023-10-27 12:51:26,830 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2023-10-27 12:51:26,883 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2023-10-27 12:51:26,884 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2023-10-27 12:51:26,886 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2023-10-27 12:51:26,888 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2023-10-27 12:51:26,890 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2023-10-27 12:51:26,891 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2023-10-27 12:51:26,896 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2023-10-27 12:51:26,897 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2023-10-27 12:51:26,898 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2023-10-27 12:51:26,898 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2023-10-27 12:51:26,900 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2023-10-27 12:51:26,901 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2023-10-27 12:51:26,903 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2023-10-27 12:51:26,919 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2023-10-27 12:51:26,919 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2023-10-27 12:51:26,920 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2023-10-27 12:51:26,925 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2023-10-27 12:51:26,927 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2023-10-27 12:51:26,928 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2023-10-27 12:51:26,929 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2023-10-27 12:51:26,929 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2023-10-27 12:51:26,932 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2023-10-27 12:51:26,933 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2023-10-27 12:51:26,933 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2023-10-27 12:51:26,934 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2023-10-27 12:51:26,935 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2023-10-27 12:51:26,935 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2023-10-27 12:51:26,935 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2023-10-27 12:51:26,936 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2023-10-27 12:51:26,938 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2023-10-27 12:51:26,939 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2023-10-27 12:51:26,943 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2023-10-27 12:51:26,944 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2023-10-27 12:51:26,944 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2023-10-27 12:51:26,945 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2023-10-27 12:51:26,945 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2023-10-27 12:51:26,946 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2023-10-27 12:51:26,946 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2023-10-27 12:51:26,952 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2023-10-27 12:51:26,991 INFO  L113        SettingsManager]: Loading preferences was successful
[2023-10-27 12:51:26,991 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2023-10-27 12:51:26,992 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2023-10-27 12:51:26,992 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2023-10-27 12:51:26,992 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2023-10-27 12:51:26,993 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2023-10-27 12:51:26,993 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2023-10-27 12:51:26,993 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2023-10-27 12:51:26,994 INFO  L138        SettingsManager]:  * Use SBE=true
[2023-10-27 12:51:26,994 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2023-10-27 12:51:26,995 INFO  L138        SettingsManager]:  * sizeof long=4
[2023-10-27 12:51:26,995 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2023-10-27 12:51:26,995 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2023-10-27 12:51:26,995 INFO  L138        SettingsManager]:  * sizeof POINTER=4
[2023-10-27 12:51:26,995 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * sizeof long double=12
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2023-10-27 12:51:26,996 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2023-10-27 12:51:26,997 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2023-10-27 12:51:26,997 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2023-10-27 12:51:26,997 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2023-10-27 12:51:26,997 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2023-10-27 12:51:26,997 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-10-27 12:51:26,997 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2023-10-27 12:51:26,998 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2023-10-27 12:51:26,998 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2023-10-27 12:51:26,998 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2023-10-27 12:51:26,998 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2023-10-27 12:51:26,999 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2023-10-27 12:51:26,999 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2023-10-27 12:51:26,999 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2023-10-27 12:51:26,999 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2023-10-27 12:51:27,000 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2023-10-27 12:51:27,000 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 -> efa45410300c0656b5dff15aa94228ada3facf40b9ca1e07e8eddd3745c4a129
[2023-10-27 12:51:27,384 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2023-10-27 12:51:27,405 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2023-10-27 12:51:27,407 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2023-10-27 12:51:27,407 INFO  L271        PluginConnector]: Initializing CDTParser...
[2023-10-27 12:51:27,408 INFO  L275        PluginConnector]: CDTParser initialized
[2023-10-27 12:51:27,409 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value-race.i
[2023-10-27 12:51:29,053 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2023-10-27 12:51:29,452 INFO  L351              CDTParser]: Found 1 translation units.
[2023-10-27 12:51:29,466 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-local-value-race.i
[2023-10-27 12:51:29,491 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/0f48e732f/985f3685ee79461890a8f3eecab1339a/FLAG720c40141
[2023-10-27 12:51:29,530 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/0f48e732f/985f3685ee79461890a8f3eecab1339a
[2023-10-27 12:51:29,532 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2023-10-27 12:51:29,533 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2023-10-27 12:51:29,534 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2023-10-27 12:51:29,534 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2023-10-27 12:51:29,536 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2023-10-27 12:51:29,541 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 27.10 12:51:29" (1/1) ...
[2023-10-27 12:51:29,544 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@20bd921a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:29, skipping insertion in model container
[2023-10-27 12:51:29,544 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 27.10 12:51:29" (1/1) ...
[2023-10-27 12:51:29,558 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2023-10-27 12:51:29,629 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2023-10-27 12:51:29,882 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2023-10-27 12:51:30,240 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-race.i[47870,47883]
[2023-10-27 12:51:30,278 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-10-27 12:51:30,301 INFO  L203         MainTranslator]: Completed pre-run
[2023-10-27 12:51:30,334 WARN  L611        FunctionHandler]: implicit declaration of function __builtin_bswap16
[2023-10-27 12:51:30,364 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-race.i[47870,47883]
[2023-10-27 12:51:30,382 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-10-27 12:51:30,481 INFO  L208         MainTranslator]: Completed translation
[2023-10-27 12:51:30,481 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30 WrapperNode
[2023-10-27 12:51:30,481 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2023-10-27 12:51:30,483 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2023-10-27 12:51:30,483 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2023-10-27 12:51:30,483 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2023-10-27 12:51:30,495 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,541 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,590 INFO  L138                Inliner]: procedures = 274, calls = 32, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 89
[2023-10-27 12:51:30,590 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2023-10-27 12:51:30,591 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2023-10-27 12:51:30,591 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2023-10-27 12:51:30,591 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2023-10-27 12:51:30,598 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,598 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,619 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,620 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,627 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,643 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,647 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,656 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,660 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2023-10-27 12:51:30,670 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2023-10-27 12:51:30,670 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2023-10-27 12:51:30,670 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2023-10-27 12:51:30,671 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (1/1) ...
[2023-10-27 12:51:30,676 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-10-27 12:51:30,692 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-10-27 12:51:30,735 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2023-10-27 12:51:30,766 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2023-10-27 12:51:30,771 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2023-10-27 12:51:30,771 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2023-10-27 12:51:30,771 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2023-10-27 12:51:30,771 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2023-10-27 12:51:30,775 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2023-10-27 12:51:30,775 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2023-10-27 12:51:30,775 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexLock
[2023-10-27 12:51:30,775 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2023-10-27 12:51:30,775 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2023-10-27 12:51:30,776 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~int
[2023-10-27 12:51:30,776 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2023-10-27 12:51:30,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2023-10-27 12:51:30,776 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2023-10-27 12:51:30,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2023-10-27 12:51:30,778 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2023-10-27 12:51:31,008 INFO  L235             CfgBuilder]: Building ICFG
[2023-10-27 12:51:31,010 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2023-10-27 12:51:31,500 INFO  L276             CfgBuilder]: Performing block encoding
[2023-10-27 12:51:31,507 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2023-10-27 12:51:31,524 INFO  L300             CfgBuilder]: Removed 3 assume(true) statements.
[2023-10-27 12:51:31,528 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 27.10 12:51:31 BoogieIcfgContainer
[2023-10-27 12:51:31,528 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2023-10-27 12:51:31,530 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2023-10-27 12:51:31,531 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2023-10-27 12:51:31,534 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2023-10-27 12:51:31,534 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 27.10 12:51:29" (1/3) ...
[2023-10-27 12:51:31,550 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7c1c7d33 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 27.10 12:51:31, skipping insertion in model container
[2023-10-27 12:51:31,550 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 27.10 12:51:30" (2/3) ...
[2023-10-27 12:51:31,550 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7c1c7d33 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 27.10 12:51:31, skipping insertion in model container
[2023-10-27 12:51:31,550 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 27.10 12:51:31" (3/3) ...
[2023-10-27 12:51:31,551 INFO  L112   eAbstractionObserver]: Analyzing ICFG thread-local-value-race.i
[2023-10-27 12:51:31,559 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2023-10-27 12:51:31,566 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2023-10-27 12:51:31,567 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 8 error locations.
[2023-10-27 12:51:31,567 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2023-10-27 12:51:31,688 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2023-10-27 12:51:31,765 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 135 places, 138 transitions, 284 flow
[2023-10-27 12:51:31,909 INFO  L130       PetriNetUnfolder]: 8/184 cut-off events.
[2023-10-27 12:51:31,909 INFO  L131       PetriNetUnfolder]: For 1/2 co-relation queries the response was YES.
[2023-10-27 12:51:31,914 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 190 conditions, 184 events. 8/184 cut-off events. For 1/2 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 354 event pairs, 0 based on Foata normal form. 0/161 useless extension candidates. Maximal degree in co-relation 91. Up to 4 conditions per place. 
[2023-10-27 12:51:31,914 INFO  L82        GeneralOperation]: Start removeDead. Operand has 135 places, 138 transitions, 284 flow
[2023-10-27 12:51:31,921 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 135 places, 138 transitions, 284 flow
[2023-10-27 12:51:31,925 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-27 12:51:31,939 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 135 places, 138 transitions, 284 flow
[2023-10-27 12:51:31,955 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 135 places, 138 transitions, 284 flow
[2023-10-27 12:51:31,956 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 135 places, 138 transitions, 284 flow
[2023-10-27 12:51:32,027 INFO  L130       PetriNetUnfolder]: 8/184 cut-off events.
[2023-10-27 12:51:32,027 INFO  L131       PetriNetUnfolder]: For 1/2 co-relation queries the response was YES.
[2023-10-27 12:51:32,029 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 190 conditions, 184 events. 8/184 cut-off events. For 1/2 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 354 event pairs, 0 based on Foata normal form. 0/161 useless extension candidates. Maximal degree in co-relation 91. Up to 4 conditions per place. 
[2023-10-27 12:51:32,032 INFO  L119        LiptonReduction]: Number of co-enabled transitions 4134
[2023-10-27 12:51:36,534 INFO  L134        LiptonReduction]: Checked pairs total: 18429
[2023-10-27 12:51:36,535 INFO  L136        LiptonReduction]: Total number of compositions: 99
[2023-10-27 12:51:36,556 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-27 12:51:36,575 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;@6daeab77, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-27 12:51:36,576 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 13 error locations.
[2023-10-27 12:51:36,584 INFO  L130       PetriNetUnfolder]: 0/17 cut-off events.
[2023-10-27 12:51:36,584 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:51:36,584 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:36,585 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:51:36,585 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)] ===
[2023-10-27 12:51:36,589 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:36,589 INFO  L85        PathProgramCache]: Analyzing trace with hash -1846690505, now seen corresponding path program 1 times
[2023-10-27 12:51:36,598 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:36,613 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1005835554]
[2023-10-27 12:51:36,614 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:36,614 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:36,858 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:51:37,538 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:51:37,539 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:51:37,539 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1005835554]
[2023-10-27 12:51:37,540 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1005835554] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:51:37,540 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:51:37,540 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:51:37,541 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2046776440]
[2023-10-27 12:51:37,542 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:51:37,548 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:51:37,561 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:51:37,595 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:51:37,596 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:51:37,884 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 102 out of 237
[2023-10-27 12:51:37,888 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 54 places, 53 transitions, 114 flow. Second operand  has 6 states, 6 states have (on average 103.16666666666667) internal successors, (619), 6 states have internal predecessors, (619), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:37,889 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:51:37,889 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 102 of 237
[2023-10-27 12:51:37,890 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:51:38,250 INFO  L130       PetriNetUnfolder]: 391/991 cut-off events.
[2023-10-27 12:51:38,251 INFO  L131       PetriNetUnfolder]: For 1/1 co-relation queries the response was YES.
[2023-10-27 12:51:38,254 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1841 conditions, 991 events. 391/991 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 51. Compared 5750 event pairs, 70 based on Foata normal form. 0/922 useless extension candidates. Maximal degree in co-relation 1762. Up to 559 conditions per place. 
[2023-10-27 12:51:38,275 INFO  L137   encePairwiseOnDemand]: 208/237 looper letters, 64 selfloop transitions, 44 changer transitions 0/119 dead transitions.
[2023-10-27 12:51:38,275 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 55 places, 119 transitions, 459 flow
[2023-10-27 12:51:38,276 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2023-10-27 12:51:38,278 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2023-10-27 12:51:38,288 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 732 transitions.
[2023-10-27 12:51:38,300 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5147679324894515
[2023-10-27 12:51:38,301 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 732 transitions.
[2023-10-27 12:51:38,317 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 732 transitions.
[2023-10-27 12:51:38,321 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:51:38,323 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 732 transitions.
[2023-10-27 12:51:38,328 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 122.0) internal successors, (732), 6 states have internal predecessors, (732), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:38,338 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 237.0) internal successors, (1659), 7 states have internal predecessors, (1659), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:38,339 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 237.0) internal successors, (1659), 7 states have internal predecessors, (1659), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:38,340 INFO  L175             Difference]: Start difference. First operand has 54 places, 53 transitions, 114 flow. Second operand 6 states and 732 transitions.
[2023-10-27 12:51:38,341 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 55 places, 119 transitions, 459 flow
[2023-10-27 12:51:38,350 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 55 places, 119 transitions, 459 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-27 12:51:38,353 INFO  L231             Difference]: Finished difference. Result has 60 places, 92 transitions, 417 flow
[2023-10-27 12:51:38,354 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=237, PETRI_DIFFERENCE_MINUEND_FLOW=101, PETRI_DIFFERENCE_MINUEND_PLACES=50, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=48, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=7, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=25, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=417, PETRI_PLACES=60, PETRI_TRANSITIONS=92}
[2023-10-27 12:51:38,371 INFO  L288   CegarLoopForPetriNet]: 54 programPoint places, 6 predicate places.
[2023-10-27 12:51:38,371 INFO  L495      AbstractCegarLoop]: Abstraction has has 60 places, 92 transitions, 417 flow
[2023-10-27 12:51:38,372 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 103.16666666666667) internal successors, (619), 6 states have internal predecessors, (619), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:38,373 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:38,373 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:51:38,375 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2023-10-27 12:51:38,375 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 10 more)] ===
[2023-10-27 12:51:38,376 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:38,376 INFO  L85        PathProgramCache]: Analyzing trace with hash -2012571814, now seen corresponding path program 1 times
[2023-10-27 12:51:38,376 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:38,377 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [45214057]
[2023-10-27 12:51:38,378 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:38,378 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:38,422 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:51:38,875 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:51:38,876 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:51:38,876 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [45214057]
[2023-10-27 12:51:38,876 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [45214057] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:51:38,876 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:51:38,876 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:51:38,877 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [550042268]
[2023-10-27 12:51:38,877 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:51:38,881 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:51:38,881 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:51:38,882 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:51:38,882 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:51:39,189 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 112 out of 237
[2023-10-27 12:51:39,190 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 60 places, 92 transitions, 417 flow. Second operand  has 6 states, 6 states have (on average 113.33333333333333) internal successors, (680), 6 states have internal predecessors, (680), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:39,190 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:51:39,190 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 112 of 237
[2023-10-27 12:51:39,190 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:51:39,532 INFO  L130       PetriNetUnfolder]: 425/1083 cut-off events.
[2023-10-27 12:51:39,535 INFO  L131       PetriNetUnfolder]: For 489/508 co-relation queries the response was YES.
[2023-10-27 12:51:39,537 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 2776 conditions, 1083 events. 425/1083 cut-off events. For 489/508 co-relation queries the response was YES. Maximal size of possible extension queue 57. Compared 6385 event pairs, 67 based on Foata normal form. 0/1043 useless extension candidates. Maximal degree in co-relation 2678. Up to 583 conditions per place. 
[2023-10-27 12:51:39,540 INFO  L137   encePairwiseOnDemand]: 223/237 looper letters, 71 selfloop transitions, 65 changer transitions 0/172 dead transitions.
[2023-10-27 12:51:39,553 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 65 places, 172 transitions, 1033 flow
[2023-10-27 12:51:39,553 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2023-10-27 12:51:39,554 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2023-10-27 12:51:39,557 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 751 transitions.
[2023-10-27 12:51:39,558 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5281293952180028
[2023-10-27 12:51:39,558 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 751 transitions.
[2023-10-27 12:51:39,558 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 751 transitions.
[2023-10-27 12:51:39,559 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:51:39,559 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 751 transitions.
[2023-10-27 12:51:39,560 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 125.16666666666667) internal successors, (751), 6 states have internal predecessors, (751), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:39,563 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 237.0) internal successors, (1659), 7 states have internal predecessors, (1659), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:39,563 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 237.0) internal successors, (1659), 7 states have internal predecessors, (1659), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:39,563 INFO  L175             Difference]: Start difference. First operand has 60 places, 92 transitions, 417 flow. Second operand 6 states and 751 transitions.
[2023-10-27 12:51:39,564 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 65 places, 172 transitions, 1033 flow
[2023-10-27 12:51:39,584 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 65 places, 172 transitions, 1033 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-27 12:51:39,587 INFO  L231             Difference]: Finished difference. Result has 70 places, 156 transitions, 1029 flow
[2023-10-27 12:51:39,587 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=237, PETRI_DIFFERENCE_MINUEND_FLOW=417, PETRI_DIFFERENCE_MINUEND_PLACES=60, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=92, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=16, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=72, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=1029, PETRI_PLACES=70, PETRI_TRANSITIONS=156}
[2023-10-27 12:51:39,588 INFO  L288   CegarLoopForPetriNet]: 54 programPoint places, 16 predicate places.
[2023-10-27 12:51:39,588 INFO  L495      AbstractCegarLoop]: Abstraction has has 70 places, 156 transitions, 1029 flow
[2023-10-27 12:51:39,589 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 113.33333333333333) internal successors, (680), 6 states have internal predecessors, (680), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:39,589 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:39,589 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:51:39,589 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2023-10-27 12:51:39,590 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 10 more)] ===
[2023-10-27 12:51:39,590 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:39,590 INFO  L85        PathProgramCache]: Analyzing trace with hash -1034764589, now seen corresponding path program 1 times
[2023-10-27 12:51:39,590 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:39,590 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [686147086]
[2023-10-27 12:51:39,591 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:39,591 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:39,625 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:51:39,974 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:51:39,974 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:51:39,974 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [686147086]
[2023-10-27 12:51:39,975 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [686147086] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:51:39,975 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:51:39,975 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:51:39,976 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [934081037]
[2023-10-27 12:51:39,976 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:51:39,976 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:51:39,976 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:51:39,977 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:51:39,980 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:51:40,121 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 101 out of 237
[2023-10-27 12:51:40,122 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 70 places, 156 transitions, 1029 flow. Second operand  has 6 states, 6 states have (on average 103.16666666666667) internal successors, (619), 6 states have internal predecessors, (619), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:40,122 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:51:40,122 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 101 of 237
[2023-10-27 12:51:40,123 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:51:40,549 INFO  L130       PetriNetUnfolder]: 585/1391 cut-off events.
[2023-10-27 12:51:40,565 INFO  L131       PetriNetUnfolder]: For 1062/1071 co-relation queries the response was YES.
[2023-10-27 12:51:40,567 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 4568 conditions, 1391 events. 585/1391 cut-off events. For 1062/1071 co-relation queries the response was YES. Maximal size of possible extension queue 70. Compared 8382 event pairs, 99 based on Foata normal form. 0/1319 useless extension candidates. Maximal degree in co-relation 4435. Up to 1066 conditions per place. 
[2023-10-27 12:51:40,573 INFO  L137   encePairwiseOnDemand]: 215/237 looper letters, 160 selfloop transitions, 80 changer transitions 0/254 dead transitions.
[2023-10-27 12:51:40,573 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 75 places, 254 transitions, 1921 flow
[2023-10-27 12:51:40,574 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2023-10-27 12:51:40,574 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2023-10-27 12:51:40,575 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 736 transitions.
[2023-10-27 12:51:40,589 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.5175808720112518
[2023-10-27 12:51:40,590 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 736 transitions.
[2023-10-27 12:51:40,590 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 736 transitions.
[2023-10-27 12:51:40,590 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:51:40,590 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 736 transitions.
[2023-10-27 12:51:40,592 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 122.66666666666667) internal successors, (736), 6 states have internal predecessors, (736), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:40,594 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 237.0) internal successors, (1659), 7 states have internal predecessors, (1659), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:40,595 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 237.0) internal successors, (1659), 7 states have internal predecessors, (1659), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:40,595 INFO  L175             Difference]: Start difference. First operand has 70 places, 156 transitions, 1029 flow. Second operand 6 states and 736 transitions.
[2023-10-27 12:51:40,595 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 75 places, 254 transitions, 1921 flow
[2023-10-27 12:51:40,603 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 75 places, 254 transitions, 1921 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-27 12:51:40,620 INFO  L231             Difference]: Finished difference. Result has 79 places, 230 transitions, 1688 flow
[2023-10-27 12:51:40,621 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=237, PETRI_DIFFERENCE_MINUEND_FLOW=1029, PETRI_DIFFERENCE_MINUEND_PLACES=70, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=156, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=22, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=124, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=1688, PETRI_PLACES=79, PETRI_TRANSITIONS=230}
[2023-10-27 12:51:40,622 INFO  L288   CegarLoopForPetriNet]: 54 programPoint places, 25 predicate places.
[2023-10-27 12:51:40,622 INFO  L495      AbstractCegarLoop]: Abstraction has has 79 places, 230 transitions, 1688 flow
[2023-10-27 12:51:40,623 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 103.16666666666667) internal successors, (619), 6 states have internal predecessors, (619), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:40,623 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:40,623 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1]
[2023-10-27 12:51:40,623 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2023-10-27 12:51:40,623 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 10 more)] ===
[2023-10-27 12:51:40,624 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:40,624 INFO  L85        PathProgramCache]: Analyzing trace with hash -883199818, now seen corresponding path program 1 times
[2023-10-27 12:51:40,624 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:40,624 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1850028442]
[2023-10-27 12:51:40,624 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:40,625 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:40,674 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:51:40,674 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-27 12:51:40,691 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:51:40,730 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-27 12:51:40,741 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-27 12:51:40,742 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (12 of 13 remaining)
[2023-10-27 12:51:40,744 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (11 of 13 remaining)
[2023-10-27 12:51:40,745 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (10 of 13 remaining)
[2023-10-27 12:51:40,746 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (9 of 13 remaining)
[2023-10-27 12:51:40,746 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (8 of 13 remaining)
[2023-10-27 12:51:40,746 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (7 of 13 remaining)
[2023-10-27 12:51:40,746 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (6 of 13 remaining)
[2023-10-27 12:51:40,747 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (5 of 13 remaining)
[2023-10-27 12:51:40,747 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (4 of 13 remaining)
[2023-10-27 12:51:40,747 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (3 of 13 remaining)
[2023-10-27 12:51:40,751 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (2 of 13 remaining)
[2023-10-27 12:51:40,751 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (1 of 13 remaining)
[2023-10-27 12:51:40,751 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (0 of 13 remaining)
[2023-10-27 12:51:40,751 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2023-10-27 12:51:40,752 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2023-10-27 12:51:40,756 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-10-27 12:51:40,756 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2023-10-27 12:51:40,799 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2023-10-27 12:51:40,812 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 175 places, 179 transitions, 376 flow
[2023-10-27 12:51:40,872 INFO  L130       PetriNetUnfolder]: 15/321 cut-off events.
[2023-10-27 12:51:40,873 INFO  L131       PetriNetUnfolder]: For 6/8 co-relation queries the response was YES.
[2023-10-27 12:51:40,875 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 335 conditions, 321 events. 15/321 cut-off events. For 6/8 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 839 event pairs, 0 based on Foata normal form. 0/279 useless extension candidates. Maximal degree in co-relation 186. Up to 8 conditions per place. 
[2023-10-27 12:51:40,875 INFO  L82        GeneralOperation]: Start removeDead. Operand has 175 places, 179 transitions, 376 flow
[2023-10-27 12:51:40,877 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 175 places, 179 transitions, 376 flow
[2023-10-27 12:51:40,877 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-27 12:51:40,877 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 175 places, 179 transitions, 376 flow
[2023-10-27 12:51:40,877 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 175 places, 179 transitions, 376 flow
[2023-10-27 12:51:40,877 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 175 places, 179 transitions, 376 flow
[2023-10-27 12:51:40,931 INFO  L130       PetriNetUnfolder]: 15/321 cut-off events.
[2023-10-27 12:51:40,931 INFO  L131       PetriNetUnfolder]: For 6/8 co-relation queries the response was YES.
[2023-10-27 12:51:40,932 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 335 conditions, 321 events. 15/321 cut-off events. For 6/8 co-relation queries the response was YES. Maximal size of possible extension queue 8. Compared 839 event pairs, 0 based on Foata normal form. 0/279 useless extension candidates. Maximal degree in co-relation 186. Up to 8 conditions per place. 
[2023-10-27 12:51:40,946 INFO  L119        LiptonReduction]: Number of co-enabled transitions 12324
[2023-10-27 12:51:44,395 INFO  L134        LiptonReduction]: Checked pairs total: 68953
[2023-10-27 12:51:44,395 INFO  L136        LiptonReduction]: Total number of compositions: 98
[2023-10-27 12:51:44,397 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-27 12:51:44,397 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;@6daeab77, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-27 12:51:44,397 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 17 error locations.
[2023-10-27 12:51:44,401 INFO  L130       PetriNetUnfolder]: 0/17 cut-off events.
[2023-10-27 12:51:44,401 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:51:44,401 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:44,401 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:51:44,402 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)] ===
[2023-10-27 12:51:44,402 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:44,402 INFO  L85        PathProgramCache]: Analyzing trace with hash -1994008606, now seen corresponding path program 1 times
[2023-10-27 12:51:44,405 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:44,405 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [762141678]
[2023-10-27 12:51:44,405 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:44,405 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:44,430 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:51:44,750 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:51:44,751 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:51:44,751 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [762141678]
[2023-10-27 12:51:44,751 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [762141678] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:51:44,751 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:51:44,751 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:51:44,752 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [873989050]
[2023-10-27 12:51:44,752 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:51:44,752 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:51:44,752 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:51:44,753 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:51:44,753 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:51:45,011 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 131 out of 277
[2023-10-27 12:51:45,012 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 93 places, 92 transitions, 202 flow. Second operand  has 6 states, 6 states have (on average 132.16666666666666) internal successors, (793), 6 states have internal predecessors, (793), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:45,012 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:51:45,012 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 131 of 277
[2023-10-27 12:51:45,012 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:51:50,364 INFO  L130       PetriNetUnfolder]: 18676/34023 cut-off events.
[2023-10-27 12:51:50,385 INFO  L131       PetriNetUnfolder]: For 295/295 co-relation queries the response was YES.
[2023-10-27 12:51:50,510 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 63117 conditions, 34023 events. 18676/34023 cut-off events. For 295/295 co-relation queries the response was YES. Maximal size of possible extension queue 875. Compared 291138 event pairs, 5099 based on Foata normal form. 0/31822 useless extension candidates. Maximal degree in co-relation 27782. Up to 18880 conditions per place. 
[2023-10-27 12:51:50,808 INFO  L137   encePairwiseOnDemand]: 241/277 looper letters, 127 selfloop transitions, 79 changer transitions 0/236 dead transitions.
[2023-10-27 12:51:50,813 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 94 places, 236 transitions, 901 flow
[2023-10-27 12:51:50,814 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2023-10-27 12:51:50,814 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2023-10-27 12:51:50,816 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 1005 transitions.
[2023-10-27 12:51:50,828 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6046931407942239
[2023-10-27 12:51:50,828 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 1005 transitions.
[2023-10-27 12:51:50,828 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 1005 transitions.
[2023-10-27 12:51:50,829 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:51:50,829 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 1005 transitions.
[2023-10-27 12:51:50,832 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 167.5) internal successors, (1005), 6 states have internal predecessors, (1005), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:50,834 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 277.0) internal successors, (1939), 7 states have internal predecessors, (1939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:50,835 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 277.0) internal successors, (1939), 7 states have internal predecessors, (1939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:50,835 INFO  L175             Difference]: Start difference. First operand has 93 places, 92 transitions, 202 flow. Second operand 6 states and 1005 transitions.
[2023-10-27 12:51:50,835 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 94 places, 236 transitions, 901 flow
[2023-10-27 12:51:50,839 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 94 places, 236 transitions, 899 flow, removed 1 selfloop flow, removed 0 redundant places.
[2023-10-27 12:51:50,859 INFO  L231             Difference]: Finished difference. Result has 99 places, 165 transitions, 724 flow
[2023-10-27 12:51:50,859 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=182, PETRI_DIFFERENCE_MINUEND_PLACES=89, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=86, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=16, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=55, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=724, PETRI_PLACES=99, PETRI_TRANSITIONS=165}
[2023-10-27 12:51:50,861 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 6 predicate places.
[2023-10-27 12:51:50,861 INFO  L495      AbstractCegarLoop]: Abstraction has has 99 places, 165 transitions, 724 flow
[2023-10-27 12:51:50,861 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 132.16666666666666) internal successors, (793), 6 states have internal predecessors, (793), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:50,861 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:50,862 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:51:50,862 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2023-10-27 12:51:50,862 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:51:50,862 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:50,862 INFO  L85        PathProgramCache]: Analyzing trace with hash 1726378141, now seen corresponding path program 1 times
[2023-10-27 12:51:50,863 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:50,865 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [916908389]
[2023-10-27 12:51:50,865 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:50,865 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:50,875 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:51:50,901 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:51:50,901 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:51:50,902 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [916908389]
[2023-10-27 12:51:50,902 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [916908389] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:51:50,902 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:51:50,902 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:51:50,902 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [952400871]
[2023-10-27 12:51:50,902 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:51:50,903 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:51:50,905 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:51:50,906 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:51:50,906 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:51:50,921 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 160 out of 277
[2023-10-27 12:51:50,928 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 99 places, 165 transitions, 724 flow. Second operand  has 3 states, 3 states have (on average 162.0) internal successors, (486), 3 states have internal predecessors, (486), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:50,928 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:51:50,928 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 160 of 277
[2023-10-27 12:51:50,928 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:51:54,057 INFO  L130       PetriNetUnfolder]: 10491/22763 cut-off events.
[2023-10-27 12:51:54,057 INFO  L131       PetriNetUnfolder]: For 7214/8174 co-relation queries the response was YES.
[2023-10-27 12:51:54,135 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 51153 conditions, 22763 events. 10491/22763 cut-off events. For 7214/8174 co-relation queries the response was YES. Maximal size of possible extension queue 798. Compared 216556 event pairs, 3394 based on Foata normal form. 24/20864 useless extension candidates. Maximal degree in co-relation 21620. Up to 8686 conditions per place. 
[2023-10-27 12:51:54,349 INFO  L137   encePairwiseOnDemand]: 271/277 looper letters, 67 selfloop transitions, 5 changer transitions 0/190 dead transitions.
[2023-10-27 12:51:54,349 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 101 places, 190 transitions, 953 flow
[2023-10-27 12:51:54,350 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:51:54,350 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:51:54,351 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 530 transitions.
[2023-10-27 12:51:54,351 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6377858002406739
[2023-10-27 12:51:54,351 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 530 transitions.
[2023-10-27 12:51:54,351 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 530 transitions.
[2023-10-27 12:51:54,351 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:51:54,352 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 530 transitions.
[2023-10-27 12:51:54,353 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 176.66666666666666) internal successors, (530), 3 states have internal predecessors, (530), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:54,354 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:54,354 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:54,354 INFO  L175             Difference]: Start difference. First operand has 99 places, 165 transitions, 724 flow. Second operand 3 states and 530 transitions.
[2023-10-27 12:51:54,354 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 101 places, 190 transitions, 953 flow
[2023-10-27 12:51:54,506 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 101 places, 190 transitions, 953 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-27 12:51:54,510 INFO  L231             Difference]: Finished difference. Result has 103 places, 169 transitions, 762 flow
[2023-10-27 12:51:54,510 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=724, PETRI_DIFFERENCE_MINUEND_PLACES=99, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=165, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=160, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=762, PETRI_PLACES=103, PETRI_TRANSITIONS=169}
[2023-10-27 12:51:54,513 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 10 predicate places.
[2023-10-27 12:51:54,514 INFO  L495      AbstractCegarLoop]: Abstraction has has 103 places, 169 transitions, 762 flow
[2023-10-27 12:51:54,514 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 162.0) internal successors, (486), 3 states have internal predecessors, (486), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:54,514 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:51:54,514 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:51:54,514 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2023-10-27 12:51:54,514 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:51:54,515 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:51:54,515 INFO  L85        PathProgramCache]: Analyzing trace with hash 1170541659, now seen corresponding path program 1 times
[2023-10-27 12:51:54,515 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:51:54,516 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1667293885]
[2023-10-27 12:51:54,516 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:51:54,516 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:51:54,526 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:51:54,807 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:51:54,807 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:51:54,807 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1667293885]
[2023-10-27 12:51:54,808 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1667293885] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:51:54,809 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:51:54,809 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:51:54,811 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1018409208]
[2023-10-27 12:51:54,811 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:51:54,811 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:51:54,811 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:51:54,812 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:51:54,812 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:51:55,122 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 141 out of 277
[2023-10-27 12:51:55,123 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 103 places, 169 transitions, 762 flow. Second operand  has 6 states, 6 states have (on average 142.33333333333334) internal successors, (854), 6 states have internal predecessors, (854), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:55,124 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:51:55,124 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 141 of 277
[2023-10-27 12:51:55,124 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:51:59,600 INFO  L130       PetriNetUnfolder]: 20387/36781 cut-off events.
[2023-10-27 12:51:59,600 INFO  L131       PetriNetUnfolder]: For 22307/23288 co-relation queries the response was YES.
[2023-10-27 12:51:59,682 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 95645 conditions, 36781 events. 20387/36781 cut-off events. For 22307/23288 co-relation queries the response was YES. Maximal size of possible extension queue 970. Compared 315307 event pairs, 6623 based on Foata normal form. 0/34655 useless extension candidates. Maximal degree in co-relation 62761. Up to 22846 conditions per place. 
[2023-10-27 12:51:59,933 INFO  L137   encePairwiseOnDemand]: 255/277 looper letters, 175 selfloop transitions, 133 changer transitions 0/365 dead transitions.
[2023-10-27 12:51:59,933 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 108 places, 365 transitions, 2218 flow
[2023-10-27 12:51:59,933 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2023-10-27 12:51:59,934 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2023-10-27 12:51:59,937 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 1016 transitions.
[2023-10-27 12:51:59,938 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6113116726835138
[2023-10-27 12:51:59,938 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 1016 transitions.
[2023-10-27 12:51:59,938 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 1016 transitions.
[2023-10-27 12:51:59,939 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:51:59,939 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 1016 transitions.
[2023-10-27 12:51:59,940 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 169.33333333333334) internal successors, (1016), 6 states have internal predecessors, (1016), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:59,942 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 277.0) internal successors, (1939), 7 states have internal predecessors, (1939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:59,943 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 277.0) internal successors, (1939), 7 states have internal predecessors, (1939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:51:59,943 INFO  L175             Difference]: Start difference. First operand has 103 places, 169 transitions, 762 flow. Second operand 6 states and 1016 transitions.
[2023-10-27 12:51:59,943 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 108 places, 365 transitions, 2218 flow
[2023-10-27 12:52:00,121 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 106 places, 365 transitions, 2184 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:52:00,150 INFO  L231             Difference]: Finished difference. Result has 111 places, 301 transitions, 2006 flow
[2023-10-27 12:52:00,151 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=752, PETRI_DIFFERENCE_MINUEND_PLACES=101, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=169, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=33, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=132, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=2006, PETRI_PLACES=111, PETRI_TRANSITIONS=301}
[2023-10-27 12:52:00,152 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 18 predicate places.
[2023-10-27 12:52:00,152 INFO  L495      AbstractCegarLoop]: Abstraction has has 111 places, 301 transitions, 2006 flow
[2023-10-27 12:52:00,153 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 142.33333333333334) internal successors, (854), 6 states have internal predecessors, (854), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:00,153 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:00,153 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:00,153 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2023-10-27 12:52:00,153 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting threadErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:00,153 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:00,154 INFO  L85        PathProgramCache]: Analyzing trace with hash -1205354157, now seen corresponding path program 1 times
[2023-10-27 12:52:00,154 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:00,154 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [468981354]
[2023-10-27 12:52:00,154 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:00,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:00,180 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:00,194 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:52:00,194 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:00,195 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [468981354]
[2023-10-27 12:52:00,195 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [468981354] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:52:00,195 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:52:00,195 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:52:00,195 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [891532006]
[2023-10-27 12:52:00,195 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:52:00,196 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:52:00,196 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:00,196 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:52:00,196 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:52:00,220 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 160 out of 277
[2023-10-27 12:52:00,222 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 111 places, 301 transitions, 2006 flow. Second operand  has 3 states, 3 states have (on average 162.66666666666666) internal successors, (488), 3 states have internal predecessors, (488), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:00,222 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:00,222 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 160 of 277
[2023-10-27 12:52:00,222 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:52:04,456 INFO  L130       PetriNetUnfolder]: 17572/36718 cut-off events.
[2023-10-27 12:52:04,457 INFO  L131       PetriNetUnfolder]: For 36036/39647 co-relation queries the response was YES.
[2023-10-27 12:52:04,591 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 102434 conditions, 36718 events. 17572/36718 cut-off events. For 36036/39647 co-relation queries the response was YES. Maximal size of possible extension queue 1238. Compared 365853 event pairs, 2721 based on Foata normal form. 256/35086 useless extension candidates. Maximal degree in co-relation 90480. Up to 15007 conditions per place. 
[2023-10-27 12:52:04,850 INFO  L137   encePairwiseOnDemand]: 269/277 looper letters, 141 selfloop transitions, 7 changer transitions 0/365 dead transitions.
[2023-10-27 12:52:04,851 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 113 places, 365 transitions, 2691 flow
[2023-10-27 12:52:04,862 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:52:04,862 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:52:04,864 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 542 transitions.
[2023-10-27 12:52:04,864 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6522262334536703
[2023-10-27 12:52:04,864 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 542 transitions.
[2023-10-27 12:52:04,864 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 542 transitions.
[2023-10-27 12:52:04,865 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:52:04,865 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 542 transitions.
[2023-10-27 12:52:04,866 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 180.66666666666666) internal successors, (542), 3 states have internal predecessors, (542), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:04,867 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:04,868 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:04,868 INFO  L175             Difference]: Start difference. First operand has 111 places, 301 transitions, 2006 flow. Second operand 3 states and 542 transitions.
[2023-10-27 12:52:04,868 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 113 places, 365 transitions, 2691 flow
[2023-10-27 12:52:05,577 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 113 places, 365 transitions, 2691 flow, removed 0 selfloop flow, removed 0 redundant places.
[2023-10-27 12:52:05,595 INFO  L231             Difference]: Finished difference. Result has 115 places, 307 transitions, 2068 flow
[2023-10-27 12:52:05,595 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=2006, PETRI_DIFFERENCE_MINUEND_PLACES=111, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=301, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=294, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=2068, PETRI_PLACES=115, PETRI_TRANSITIONS=307}
[2023-10-27 12:52:05,596 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 22 predicate places.
[2023-10-27 12:52:05,596 INFO  L495      AbstractCegarLoop]: Abstraction has has 115 places, 307 transitions, 2068 flow
[2023-10-27 12:52:05,597 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 162.66666666666666) internal successors, (488), 3 states have internal predecessors, (488), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:05,597 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:05,597 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:05,597 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2023-10-27 12:52:05,597 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:05,597 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:05,598 INFO  L85        PathProgramCache]: Analyzing trace with hash 1551336595, now seen corresponding path program 1 times
[2023-10-27 12:52:05,598 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:05,598 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [341586735]
[2023-10-27 12:52:05,598 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:05,598 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:05,620 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:05,648 INFO  L134       CoverageAnalysis]: Checked inductivity of 8 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2023-10-27 12:52:05,649 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:05,649 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [341586735]
[2023-10-27 12:52:05,649 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [341586735] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:52:05,649 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:52:05,649 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2023-10-27 12:52:05,649 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1545749897]
[2023-10-27 12:52:05,649 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:52:05,650 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:52:05,650 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:05,650 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:52:05,650 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:52:05,665 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 160 out of 277
[2023-10-27 12:52:05,665 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 115 places, 307 transitions, 2068 flow. Second operand  has 3 states, 3 states have (on average 163.0) internal successors, (489), 3 states have internal predecessors, (489), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:05,665 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:05,665 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 160 of 277
[2023-10-27 12:52:05,665 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:52:09,745 INFO  L130       PetriNetUnfolder]: 17561/36822 cut-off events.
[2023-10-27 12:52:09,746 INFO  L131       PetriNetUnfolder]: For 40782/45418 co-relation queries the response was YES.
[2023-10-27 12:52:09,919 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 105196 conditions, 36822 events. 17561/36822 cut-off events. For 40782/45418 co-relation queries the response was YES. Maximal size of possible extension queue 1323. Compared 371243 event pairs, 4014 based on Foata normal form. 216/34959 useless extension candidates. Maximal degree in co-relation 92929. Up to 15285 conditions per place. 
[2023-10-27 12:52:10,157 INFO  L137   encePairwiseOnDemand]: 272/277 looper letters, 114 selfloop transitions, 6 changer transitions 0/342 dead transitions.
[2023-10-27 12:52:10,177 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 117 places, 342 transitions, 2516 flow
[2023-10-27 12:52:10,177 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:52:10,178 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:52:10,178 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 526 transitions.
[2023-10-27 12:52:10,179 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6329723225030084
[2023-10-27 12:52:10,179 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 526 transitions.
[2023-10-27 12:52:10,179 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 526 transitions.
[2023-10-27 12:52:10,179 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:52:10,179 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 526 transitions.
[2023-10-27 12:52:10,180 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 175.33333333333334) internal successors, (526), 3 states have internal predecessors, (526), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:10,181 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:10,182 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:10,182 INFO  L175             Difference]: Start difference. First operand has 115 places, 307 transitions, 2068 flow. Second operand 3 states and 526 transitions.
[2023-10-27 12:52:10,182 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 117 places, 342 transitions, 2516 flow
[2023-10-27 12:52:10,646 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 115 places, 342 transitions, 2500 flow, removed 0 selfloop flow, removed 2 redundant places.
[2023-10-27 12:52:10,649 INFO  L231             Difference]: Finished difference. Result has 116 places, 310 transitions, 2092 flow
[2023-10-27 12:52:10,663 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=2054, PETRI_DIFFERENCE_MINUEND_PLACES=113, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=307, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=3, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=301, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=2092, PETRI_PLACES=116, PETRI_TRANSITIONS=310}
[2023-10-27 12:52:10,665 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 23 predicate places.
[2023-10-27 12:52:10,666 INFO  L495      AbstractCegarLoop]: Abstraction has has 116 places, 310 transitions, 2092 flow
[2023-10-27 12:52:10,666 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 163.0) internal successors, (489), 3 states have internal predecessors, (489), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:10,666 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:10,666 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:10,666 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2023-10-27 12:52:10,666 INFO  L420      AbstractCegarLoop]: === Iteration 6 === Targeting threadErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:10,667 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:10,667 INFO  L85        PathProgramCache]: Analyzing trace with hash -748181148, now seen corresponding path program 1 times
[2023-10-27 12:52:10,667 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:10,667 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [371855907]
[2023-10-27 12:52:10,667 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:10,667 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:10,682 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:11,002 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:52:11,003 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:11,003 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [371855907]
[2023-10-27 12:52:11,003 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [371855907] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:52:11,004 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:52:11,004 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:52:11,004 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [828307708]
[2023-10-27 12:52:11,013 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:52:11,014 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:52:11,014 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:11,014 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:52:11,014 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:52:11,209 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 128 out of 277
[2023-10-27 12:52:11,210 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 116 places, 310 transitions, 2092 flow. Second operand  has 6 states, 6 states have (on average 130.83333333333334) internal successors, (785), 6 states have internal predecessors, (785), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:11,210 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:11,210 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 128 of 277
[2023-10-27 12:52:11,210 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:52:19,884 INFO  L130       PetriNetUnfolder]: 42153/72844 cut-off events.
[2023-10-27 12:52:19,884 INFO  L131       PetriNetUnfolder]: For 74087/78508 co-relation queries the response was YES.
[2023-10-27 12:52:20,199 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 233922 conditions, 72844 events. 42153/72844 cut-off events. For 74087/78508 co-relation queries the response was YES. Maximal size of possible extension queue 1791. Compared 640889 event pairs, 13222 based on Foata normal form. 1140/70728 useless extension candidates. Maximal degree in co-relation 211028. Up to 57333 conditions per place. 
[2023-10-27 12:52:20,452 INFO  L137   encePairwiseOnDemand]: 245/277 looper letters, 361 selfloop transitions, 187 changer transitions 0/584 dead transitions.
[2023-10-27 12:52:20,452 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 121 places, 584 transitions, 4656 flow
[2023-10-27 12:52:20,453 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2023-10-27 12:52:20,453 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2023-10-27 12:52:20,454 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 999 transitions.
[2023-10-27 12:52:20,456 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.6010830324909747
[2023-10-27 12:52:20,456 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 999 transitions.
[2023-10-27 12:52:20,456 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 999 transitions.
[2023-10-27 12:52:20,466 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:52:20,466 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 999 transitions.
[2023-10-27 12:52:20,475 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 166.5) internal successors, (999), 6 states have internal predecessors, (999), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:20,477 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 277.0) internal successors, (1939), 7 states have internal predecessors, (1939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:20,477 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 277.0) internal successors, (1939), 7 states have internal predecessors, (1939), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:20,478 INFO  L175             Difference]: Start difference. First operand has 116 places, 310 transitions, 2092 flow. Second operand 6 states and 999 transitions.
[2023-10-27 12:52:20,478 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 121 places, 584 transitions, 4656 flow
[2023-10-27 12:52:21,335 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 120 places, 584 transitions, 4646 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-10-27 12:52:21,340 INFO  L231             Difference]: Finished difference. Result has 124 places, 488 transitions, 3823 flow
[2023-10-27 12:52:21,340 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=2086, PETRI_DIFFERENCE_MINUEND_PLACES=115, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=310, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=53, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=242, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=3823, PETRI_PLACES=124, PETRI_TRANSITIONS=488}
[2023-10-27 12:52:21,341 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 31 predicate places.
[2023-10-27 12:52:21,342 INFO  L495      AbstractCegarLoop]: Abstraction has has 124 places, 488 transitions, 3823 flow
[2023-10-27 12:52:21,343 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 130.83333333333334) internal successors, (785), 6 states have internal predecessors, (785), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:21,343 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:21,343 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:21,343 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2023-10-27 12:52:21,343 INFO  L420      AbstractCegarLoop]: === Iteration 7 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:21,344 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:21,344 INFO  L85        PathProgramCache]: Analyzing trace with hash 1137170375, now seen corresponding path program 1 times
[2023-10-27 12:52:21,344 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:21,344 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1286404146]
[2023-10-27 12:52:21,344 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:21,344 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:21,388 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:21,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 8 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2023-10-27 12:52:21,465 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:21,465 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1286404146]
[2023-10-27 12:52:21,465 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1286404146] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:52:21,465 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:52:21,465 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [3] imperfect sequences [] total 3
[2023-10-27 12:52:21,465 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1591004898]
[2023-10-27 12:52:21,465 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:52:21,466 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 3 states
[2023-10-27 12:52:21,466 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:21,466 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 3 interpolants.
[2023-10-27 12:52:21,466 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=3, Invalid=3, Unknown=0, NotChecked=0, Total=6
[2023-10-27 12:52:21,481 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 159 out of 277
[2023-10-27 12:52:21,482 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 124 places, 488 transitions, 3823 flow. Second operand  has 3 states, 3 states have (on average 162.0) internal successors, (486), 3 states have internal predecessors, (486), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:21,482 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:21,482 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 159 of 277
[2023-10-27 12:52:21,482 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:52:24,556 INFO  L130       PetriNetUnfolder]: 13289/26638 cut-off events.
[2023-10-27 12:52:24,557 INFO  L131       PetriNetUnfolder]: For 41774/45605 co-relation queries the response was YES.
[2023-10-27 12:52:24,644 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 88093 conditions, 26638 events. 13289/26638 cut-off events. For 41774/45605 co-relation queries the response was YES. Maximal size of possible extension queue 723. Compared 236169 event pairs, 1531 based on Foata normal form. 818/26418 useless extension candidates. Maximal degree in co-relation 78663. Up to 11159 conditions per place. 
[2023-10-27 12:52:24,732 INFO  L137   encePairwiseOnDemand]: 269/277 looper letters, 126 selfloop transitions, 8 changer transitions 0/469 dead transitions.
[2023-10-27 12:52:24,732 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 122 places, 469 transitions, 3865 flow
[2023-10-27 12:52:24,733 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2023-10-27 12:52:24,733 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 3 states.
[2023-10-27 12:52:24,734 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3 states to 3 states and 525 transitions.
[2023-10-27 12:52:24,735 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.631768953068592
[2023-10-27 12:52:24,735 INFO  L72            ComplementDD]: Start complementDD. Operand 3 states and 525 transitions.
[2023-10-27 12:52:24,735 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 3 states and 525 transitions.
[2023-10-27 12:52:24,735 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:52:24,735 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 3 states and 525 transitions.
[2023-10-27 12:52:24,736 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 4 states, 3 states have (on average 175.0) internal successors, (525), 3 states have internal predecessors, (525), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:24,738 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:24,739 INFO  L81            ComplementDD]: Finished complementDD. Result  has 4 states, 4 states have (on average 277.0) internal successors, (1108), 4 states have internal predecessors, (1108), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:24,739 INFO  L175             Difference]: Start difference. First operand has 124 places, 488 transitions, 3823 flow. Second operand 3 states and 525 transitions.
[2023-10-27 12:52:24,739 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 122 places, 469 transitions, 3865 flow
[2023-10-27 12:52:25,744 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 118 places, 469 transitions, 3721 flow, removed 66 selfloop flow, removed 4 redundant places.
[2023-10-27 12:52:25,749 INFO  L231             Difference]: Finished difference. Result has 118 places, 431 transitions, 3220 flow
[2023-10-27 12:52:25,750 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=3204, PETRI_DIFFERENCE_MINUEND_PLACES=116, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=431, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=8, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=423, PETRI_DIFFERENCE_SUBTRAHEND_STATES=3, PETRI_FLOW=3220, PETRI_PLACES=118, PETRI_TRANSITIONS=431}
[2023-10-27 12:52:25,754 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 25 predicate places.
[2023-10-27 12:52:25,754 INFO  L495      AbstractCegarLoop]: Abstraction has has 118 places, 431 transitions, 3220 flow
[2023-10-27 12:52:25,754 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 3 states, 3 states have (on average 162.0) internal successors, (486), 3 states have internal predecessors, (486), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:25,754 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:25,755 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:25,755 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2023-10-27 12:52:25,755 INFO  L420      AbstractCegarLoop]: === Iteration 8 === Targeting ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:25,755 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:25,755 INFO  L85        PathProgramCache]: Analyzing trace with hash 2098377104, now seen corresponding path program 1 times
[2023-10-27 12:52:25,755 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:25,756 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1925215109]
[2023-10-27 12:52:25,756 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:25,763 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:25,827 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:26,247 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2023-10-27 12:52:26,247 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:26,247 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1925215109]
[2023-10-27 12:52:26,247 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1925215109] provided 0 perfect and 1 imperfect interpolant sequences
[2023-10-27 12:52:26,248 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2020209893]
[2023-10-27 12:52:26,248 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:26,248 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2023-10-27 12:52:26,248 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-10-27 12:52:26,263 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2023-10-27 12:52:26,292 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2023-10-27 12:52:26,423 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:26,426 INFO  L263         TraceCheckSpWp]: Trace formula consists of 214 conjuncts, 28 conjunts are in the unsatisfiable core
[2023-10-27 12:52:26,428 INFO  L286         TraceCheckSpWp]: Computing forward predicates...
[2023-10-27 12:52:26,576 INFO  L321             Elim1Store]: treesize reduction 4, result has 50.0 percent of original size
[2023-10-27 12:52:26,577 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 11 treesize of output 11
[2023-10-27 12:52:26,828 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 11 treesize of output 7
[2023-10-27 12:52:26,880 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:26,881 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 21 treesize of output 20
[2023-10-27 12:52:26,940 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:26,941 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:26,942 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 2 select indices, 2 select index equivalence classes, 4 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 0 case distinctions, treesize of input 30 treesize of output 32
[2023-10-27 12:52:27,001 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:27,002 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:27,002 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:27,004 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 7 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 0 case distinctions, treesize of input 39 treesize of output 44
[2023-10-27 12:52:27,080 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 41 treesize of output 37
[2023-10-27 12:52:27,124 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2023-10-27 12:52:27,124 INFO  L328         TraceCheckSpWp]: Computing backward predicates...
[2023-10-27 12:52:27,158 WARN  L837   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store |c_#race| c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ |c_ULTIMATE.start_main_~#tids~0#1.offset| 1)) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store |c_#race| c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ 2 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store |c_#race| c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store |c_#race| c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ 3 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) 0))) is different from false
[2023-10-27 12:52:27,196 WARN  L837   $PredicateComparison]: unable to prove that (let ((.cse1 (+ 3 |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (let ((.cse0 (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| (store (select |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse1 0)))) (and (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ 2 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ |c_ULTIMATE.start_main_~#tids~0#1.offset| 1)) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse1) 0))))) is different from false
[2023-10-27 12:52:27,234 WARN  L837   $PredicateComparison]: unable to prove that (let ((.cse2 (+ 2 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) (.cse1 (+ 3 |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (let ((.cse0 (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| (store (store (select |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse2 0) .cse1 0)))) (and (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse1) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ |c_ULTIMATE.start_main_~#tids~0#1.offset| 1)) 0)) (forall ((v_ArrVal_384 (Array Int Int))) (= (select (select (store .cse0 c_~ptr~0.base v_ArrVal_384) |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse2) 0))))) is different from false
[2023-10-27 12:52:27,344 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 3 refuted. 0 times theorem prover too weak. 1 trivial. 2 not checked.
[2023-10-27 12:52:27,344 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2020209893] provided 0 perfect and 2 imperfect interpolant sequences
[2023-10-27 12:52:27,345 INFO  L184   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2023-10-27 12:52:27,345 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 18
[2023-10-27 12:52:27,345 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1564345630]
[2023-10-27 12:52:27,345 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2023-10-27 12:52:27,345 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2023-10-27 12:52:27,345 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:27,346 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2023-10-27 12:52:27,346 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=79, Invalid=202, Unknown=3, NotChecked=96, Total=380
[2023-10-27 12:52:27,348 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 103 out of 277
[2023-10-27 12:52:27,349 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 118 places, 431 transitions, 3220 flow. Second operand  has 20 states, 20 states have (on average 105.85) internal successors, (2117), 20 states have internal predecessors, (2117), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:27,349 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:27,349 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 103 of 277
[2023-10-27 12:52:27,349 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:52:34,154 INFO  L130       PetriNetUnfolder]: 29043/47835 cut-off events.
[2023-10-27 12:52:34,154 INFO  L131       PetriNetUnfolder]: For 59411/59411 co-relation queries the response was YES.
[2023-10-27 12:52:34,296 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 170099 conditions, 47835 events. 29043/47835 cut-off events. For 59411/59411 co-relation queries the response was YES. Maximal size of possible extension queue 950. Compared 360786 event pairs, 10523 based on Foata normal form. 624/45197 useless extension candidates. Maximal degree in co-relation 148855. Up to 44000 conditions per place. 
[2023-10-27 12:52:34,468 INFO  L137   encePairwiseOnDemand]: 255/277 looper letters, 500 selfloop transitions, 16 changer transitions 11/540 dead transitions.
[2023-10-27 12:52:34,468 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 125 places, 540 transitions, 4887 flow
[2023-10-27 12:52:34,469 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2023-10-27 12:52:34,469 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 11 states.
[2023-10-27 12:52:34,471 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 11 states to 11 states and 1292 transitions.
[2023-10-27 12:52:34,483 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.42402362979980307
[2023-10-27 12:52:34,483 INFO  L72            ComplementDD]: Start complementDD. Operand 11 states and 1292 transitions.
[2023-10-27 12:52:34,483 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 11 states and 1292 transitions.
[2023-10-27 12:52:34,484 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:52:34,484 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 11 states and 1292 transitions.
[2023-10-27 12:52:34,488 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 12 states, 11 states have (on average 117.45454545454545) internal successors, (1292), 11 states have internal predecessors, (1292), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:34,499 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 12 states, 12 states have (on average 277.0) internal successors, (3324), 12 states have internal predecessors, (3324), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:34,500 INFO  L81            ComplementDD]: Finished complementDD. Result  has 12 states, 12 states have (on average 277.0) internal successors, (3324), 12 states have internal predecessors, (3324), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:34,500 INFO  L175             Difference]: Start difference. First operand has 118 places, 431 transitions, 3220 flow. Second operand 11 states and 1292 transitions.
[2023-10-27 12:52:34,500 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 125 places, 540 transitions, 4887 flow
[2023-10-27 12:52:35,624 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 124 places, 540 transitions, 4871 flow, removed 0 selfloop flow, removed 1 redundant places.
[2023-10-27 12:52:35,631 INFO  L231             Difference]: Finished difference. Result has 132 places, 441 transitions, 3354 flow
[2023-10-27 12:52:35,632 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=3200, PETRI_DIFFERENCE_MINUEND_PLACES=114, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=428, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=3, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=415, PETRI_DIFFERENCE_SUBTRAHEND_STATES=11, PETRI_FLOW=3354, PETRI_PLACES=132, PETRI_TRANSITIONS=441}
[2023-10-27 12:52:35,632 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 39 predicate places.
[2023-10-27 12:52:35,632 INFO  L495      AbstractCegarLoop]: Abstraction has has 132 places, 441 transitions, 3354 flow
[2023-10-27 12:52:35,633 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 20 states have (on average 105.85) internal successors, (2117), 20 states have internal predecessors, (2117), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:35,633 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:35,633 INFO  L209   CegarLoopForPetriNet]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:35,640 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2023-10-27 12:52:35,838 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2023-10-27 12:52:35,838 INFO  L420      AbstractCegarLoop]: === Iteration 9 === Targeting threadErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:35,839 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:35,839 INFO  L85        PathProgramCache]: Analyzing trace with hash -135029521, now seen corresponding path program 1 times
[2023-10-27 12:52:35,839 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:35,839 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1203731477]
[2023-10-27 12:52:35,839 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:35,839 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:35,891 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:36,257 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2023-10-27 12:52:36,257 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:36,258 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1203731477]
[2023-10-27 12:52:36,258 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1203731477] provided 0 perfect and 1 imperfect interpolant sequences
[2023-10-27 12:52:36,258 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2068605946]
[2023-10-27 12:52:36,258 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:36,258 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2023-10-27 12:52:36,258 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-10-27 12:52:36,259 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2023-10-27 12:52:36,299 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2023-10-27 12:52:36,422 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:36,423 INFO  L263         TraceCheckSpWp]: Trace formula consists of 214 conjuncts, 30 conjunts are in the unsatisfiable core
[2023-10-27 12:52:36,426 INFO  L286         TraceCheckSpWp]: Computing forward predicates...
[2023-10-27 12:52:36,450 INFO  L321             Elim1Store]: treesize reduction 4, result has 50.0 percent of original size
[2023-10-27 12:52:36,450 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 11 treesize of output 11
[2023-10-27 12:52:36,593 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 11 treesize of output 7
[2023-10-27 12:52:36,641 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:36,642 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 21 treesize of output 20
[2023-10-27 12:52:36,703 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:36,704 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:36,705 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 2 select indices, 2 select index equivalence classes, 3 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 0 case distinctions, treesize of input 30 treesize of output 32
[2023-10-27 12:52:36,764 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:36,765 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:36,767 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2023-10-27 12:52:36,768 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 6 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 0 case distinctions, treesize of input 39 treesize of output 44
[2023-10-27 12:52:36,870 INFO  L350             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 41 treesize of output 37
[2023-10-27 12:52:36,899 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2023-10-27 12:52:36,900 INFO  L328         TraceCheckSpWp]: Computing backward predicates...
[2023-10-27 12:52:36,932 WARN  L837   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_475 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet7| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) (+ c_~ptr~0.offset 2)))) (forall ((v_ArrVal_475 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet7| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) c_~ptr~0.offset))) (forall ((v_ArrVal_475 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet7| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) (+ c_~ptr~0.offset 1)))) (forall ((v_ArrVal_475 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) (+ c_~ptr~0.offset 3)) |c_threadThread1of2ForFork0_#t~nondet7|))) is different from false
[2023-10-27 12:52:36,964 WARN  L837   $PredicateComparison]: unable to prove that (let ((.cse1 (+ c_~ptr~0.offset 3))) (let ((.cse0 (store |c_#race| c_~ptr~0.base (store (select |c_#race| c_~ptr~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet7|)))) (and (forall ((v_ArrVal_475 (Array Int Int))) (= (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) .cse1) |c_threadThread1of2ForFork0_#t~nondet7|)) (forall ((v_ArrVal_475 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet7| (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) (+ c_~ptr~0.offset 1)))) (forall ((v_ArrVal_475 (Array Int Int))) (= (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) (+ c_~ptr~0.offset 2)) |c_threadThread1of2ForFork0_#t~nondet7|)) (forall ((v_ArrVal_475 (Array Int Int))) (= (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_475) c_~ptr~0.base) c_~ptr~0.offset) |c_threadThread1of2ForFork0_#t~nondet7|))))) is different from false
[2023-10-27 12:52:37,049 INFO  L134       CoverageAnalysis]: Checked inductivity of 2 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 1 not checked.
[2023-10-27 12:52:37,049 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2068605946] provided 0 perfect and 2 imperfect interpolant sequences
[2023-10-27 12:52:37,049 INFO  L184   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2023-10-27 12:52:37,050 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 17
[2023-10-27 12:52:37,050 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1943879454]
[2023-10-27 12:52:37,050 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2023-10-27 12:52:37,052 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2023-10-27 12:52:37,052 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:37,052 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2023-10-27 12:52:37,052 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=77, Invalid=201, Unknown=2, NotChecked=62, Total=342
[2023-10-27 12:52:37,273 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 101 out of 277
[2023-10-27 12:52:37,275 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 132 places, 441 transitions, 3354 flow. Second operand  has 19 states, 19 states have (on average 103.94736842105263) internal successors, (1975), 19 states have internal predecessors, (1975), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:37,275 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:37,275 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 101 of 277
[2023-10-27 12:52:37,275 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2023-10-27 12:52:47,964 INFO  L130       PetriNetUnfolder]: 45416/74294 cut-off events.
[2023-10-27 12:52:47,965 INFO  L131       PetriNetUnfolder]: For 115079/115079 co-relation queries the response was YES.
[2023-10-27 12:52:48,530 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 273395 conditions, 74294 events. 45416/74294 cut-off events. For 115079/115079 co-relation queries the response was YES. Maximal size of possible extension queue 1613. Compared 589913 event pairs, 10253 based on Foata normal form. 389/69551 useless extension candidates. Maximal degree in co-relation 265911. Up to 24543 conditions per place. 
[2023-10-27 12:52:48,780 INFO  L137   encePairwiseOnDemand]: 234/277 looper letters, 1050 selfloop transitions, 318 changer transitions 0/1381 dead transitions.
[2023-10-27 12:52:48,780 INFO  L142   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 141 places, 1381 transitions, 12658 flow
[2023-10-27 12:52:48,780 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2023-10-27 12:52:48,780 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 12 states.
[2023-10-27 12:52:48,796 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 12 states to 12 states and 1640 transitions.
[2023-10-27 12:52:48,798 INFO  L523   CegarLoopForPetriNet]: DFA transition density 0.49338146811071
[2023-10-27 12:52:48,799 INFO  L72            ComplementDD]: Start complementDD. Operand 12 states and 1640 transitions.
[2023-10-27 12:52:48,799 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 12 states and 1640 transitions.
[2023-10-27 12:52:48,799 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2023-10-27 12:52:48,799 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 12 states and 1640 transitions.
[2023-10-27 12:52:48,802 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 13 states, 12 states have (on average 136.66666666666666) internal successors, (1640), 12 states have internal predecessors, (1640), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:48,805 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 13 states, 13 states have (on average 277.0) internal successors, (3601), 13 states have internal predecessors, (3601), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:48,805 INFO  L81            ComplementDD]: Finished complementDD. Result  has 13 states, 13 states have (on average 277.0) internal successors, (3601), 13 states have internal predecessors, (3601), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:48,806 INFO  L175             Difference]: Start difference. First operand has 132 places, 441 transitions, 3354 flow. Second operand 12 states and 1640 transitions.
[2023-10-27 12:52:48,806 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 141 places, 1381 transitions, 12658 flow
[2023-10-27 12:52:52,759 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 138 places, 1381 transitions, 12537 flow, removed 51 selfloop flow, removed 3 redundant places.
[2023-10-27 12:52:52,770 INFO  L231             Difference]: Finished difference. Result has 147 places, 713 transitions, 6805 flow
[2023-10-27 12:52:52,770 INFO  L271   CegarLoopForPetriNet]: {PETRI_ALPHABET=277, PETRI_DIFFERENCE_MINUEND_FLOW=3332, PETRI_DIFFERENCE_MINUEND_PLACES=127, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=441, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=92, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=272, PETRI_DIFFERENCE_SUBTRAHEND_STATES=12, PETRI_FLOW=6805, PETRI_PLACES=147, PETRI_TRANSITIONS=713}
[2023-10-27 12:52:52,771 INFO  L288   CegarLoopForPetriNet]: 93 programPoint places, 54 predicate places.
[2023-10-27 12:52:52,771 INFO  L495      AbstractCegarLoop]: Abstraction has has 147 places, 713 transitions, 6805 flow
[2023-10-27 12:52:52,785 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 19 states have (on average 103.94736842105263) internal successors, (1975), 19 states have internal predecessors, (1975), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:52,786 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:52,786 INFO  L209   CegarLoopForPetriNet]: trace histogram [3, 3, 3, 3, 3, 3, 3, 2, 2, 1, 1, 1, 1]
[2023-10-27 12:52:52,797 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2023-10-27 12:52:52,990 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12,3 /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2023-10-27 12:52:52,991 INFO  L420      AbstractCegarLoop]: === Iteration 10 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (and 14 more)] ===
[2023-10-27 12:52:52,991 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:52,992 INFO  L85        PathProgramCache]: Analyzing trace with hash -316743641, now seen corresponding path program 1 times
[2023-10-27 12:52:52,992 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:52,992 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1144225973]
[2023-10-27 12:52:52,993 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:52,993 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:53,028 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:52:53,034 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2023-10-27 12:52:53,060 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2023-10-27 12:52:53,069 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2023-10-27 12:52:53,071 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2023-10-27 12:52:53,071 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (16 of 17 remaining)
[2023-10-27 12:52:53,071 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (15 of 17 remaining)
[2023-10-27 12:52:53,071 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (14 of 17 remaining)
[2023-10-27 12:52:53,071 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (13 of 17 remaining)
[2023-10-27 12:52:53,071 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (12 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (11 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (10 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (9 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (8 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (7 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (6 of 17 remaining)
[2023-10-27 12:52:53,072 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (5 of 17 remaining)
[2023-10-27 12:52:53,073 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (4 of 17 remaining)
[2023-10-27 12:52:53,073 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (3 of 17 remaining)
[2023-10-27 12:52:53,073 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr1ASSERT_VIOLATIONDATA_RACE (2 of 17 remaining)
[2023-10-27 12:52:53,073 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr2ASSERT_VIOLATIONDATA_RACE (1 of 17 remaining)
[2023-10-27 12:52:53,073 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr3ASSERT_VIOLATIONDATA_RACE (0 of 17 remaining)
[2023-10-27 12:52:53,073 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2023-10-27 12:52:53,073 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:53,074 WARN  L233   ceAbstractionStarter]: 2 thread instances were not sufficient, I will increase this number and restart the analysis
[2023-10-27 12:52:53,074 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 3 thread instances.
[2023-10-27 12:52:53,110 INFO  L144    ThreadInstanceAdder]: Constructed 3 joinOtherThreadTransitions.
[2023-10-27 12:52:53,112 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 215 places, 220 transitions, 470 flow
[2023-10-27 12:52:53,193 INFO  L130       PetriNetUnfolder]: 27/537 cut-off events.
[2023-10-27 12:52:53,209 INFO  L131       PetriNetUnfolder]: For 19/22 co-relation queries the response was YES.
[2023-10-27 12:52:53,214 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 565 conditions, 537 events. 27/537 cut-off events. For 19/22 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 1728 event pairs, 1 based on Foata normal form. 0/466 useless extension candidates. Maximal degree in co-relation 329. Up to 16 conditions per place. 
[2023-10-27 12:52:53,214 INFO  L82        GeneralOperation]: Start removeDead. Operand has 215 places, 220 transitions, 470 flow
[2023-10-27 12:52:53,216 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 215 places, 220 transitions, 470 flow
[2023-10-27 12:52:53,216 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-10-27 12:52:53,217 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 215 places, 220 transitions, 470 flow
[2023-10-27 12:52:53,217 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 215 places, 220 transitions, 470 flow
[2023-10-27 12:52:53,217 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 215 places, 220 transitions, 470 flow
[2023-10-27 12:52:53,283 INFO  L130       PetriNetUnfolder]: 27/537 cut-off events.
[2023-10-27 12:52:53,284 INFO  L131       PetriNetUnfolder]: For 19/22 co-relation queries the response was YES.
[2023-10-27 12:52:53,301 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 565 conditions, 537 events. 27/537 cut-off events. For 19/22 co-relation queries the response was YES. Maximal size of possible extension queue 10. Compared 1728 event pairs, 1 based on Foata normal form. 0/466 useless extension candidates. Maximal degree in co-relation 329. Up to 16 conditions per place. 
[2023-10-27 12:52:53,332 INFO  L119        LiptonReduction]: Number of co-enabled transitions 23400
[2023-10-27 12:52:57,155 INFO  L134        LiptonReduction]: Checked pairs total: 136722
[2023-10-27 12:52:57,155 INFO  L136        LiptonReduction]: Total number of compositions: 109
[2023-10-27 12:52:57,156 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2023-10-27 12:52:57,156 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;@6daeab77, mLbeIndependenceSettings=[IndependenceType=SYNTACTIC, AbstractionType=NONE, UseConditional=<UNSUPPORTED>, UseSemiCommutativity=<UNSUPPORTED>, Solver=<NOT_USED>, SolverTimeout=<NOT_USED>]
[2023-10-27 12:52:57,156 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 21 error locations.
[2023-10-27 12:52:57,157 INFO  L130       PetriNetUnfolder]: 0/17 cut-off events.
[2023-10-27 12:52:57,158 INFO  L131       PetriNetUnfolder]: For 0/0 co-relation queries the response was YES.
[2023-10-27 12:52:57,158 INFO  L201   CegarLoopForPetriNet]: Found error trace
[2023-10-27 12:52:57,158 INFO  L209   CegarLoopForPetriNet]: trace histogram [1, 1, 1, 1, 1, 1, 1]
[2023-10-27 12:52:57,158 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)] ===
[2023-10-27 12:52:57,158 INFO  L144       PredicateUnifier]: Initialized classic predicate unifier
[2023-10-27 12:52:57,158 INFO  L85        PathProgramCache]: Analyzing trace with hash -2023808160, now seen corresponding path program 1 times
[2023-10-27 12:52:57,158 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2023-10-27 12:52:57,158 INFO  L333   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1220093106]
[2023-10-27 12:52:57,158 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2023-10-27 12:52:57,158 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2023-10-27 12:52:57,189 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2023-10-27 12:52:57,349 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2023-10-27 12:52:57,350 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2023-10-27 12:52:57,350 INFO  L333   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1220093106]
[2023-10-27 12:52:57,350 INFO  L157   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1220093106] provided 1 perfect and 0 imperfect interpolant sequences
[2023-10-27 12:52:57,350 INFO  L184   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2023-10-27 12:52:57,350 INFO  L197   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2023-10-27 12:52:57,350 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2059311066]
[2023-10-27 12:52:57,351 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2023-10-27 12:52:57,351 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2023-10-27 12:52:57,351 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2023-10-27 12:52:57,351 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2023-10-27 12:52:57,352 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2023-10-27 12:52:57,587 INFO  L478   CegarLoopForPetriNet]: Number of universal loopers: 160 out of 329
[2023-10-27 12:52:57,588 INFO  L100   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 121 places, 120 transitions, 270 flow. Second operand  has 6 states, 6 states have (on average 161.16666666666666) internal successors, (967), 6 states have internal predecessors, (967), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2023-10-27 12:52:57,588 INFO  L109   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2023-10-27 12:52:57,588 INFO  L110   encePairwiseOnDemand]: Number of universal subtrahend loopers: 160 of 329
[2023-10-27 12:52:57,588 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
