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


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


Checking for data races
Using default analysis
Version 0e0057cc
Calling Ultimate with: /usr/lib/jvm/java-11-openjdk-amd64/bin/java -Dosgi.configuration.area=/mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data -tc /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/config/AutomizerReach.xml -i /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-struct.i -s /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf --cacsl2boogietranslator.entry.function main --witnessprinter.witness.directory /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux --witnessprinter.witness.filename witness --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 da4059ae5015b9b2b5411cafd8d7f66dfcf43ca14cb85e33016c9817b7004fc6
--- Real Ultimate output ---
This is Ultimate 0.2.4-dev-0e0057c
[2024-03-09 06:22:49,381 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2024-03-09 06:22:49,423 INFO  L114        SettingsManager]: Loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/config/svcomp-DataRace-32bit-Automizer_Default.epf
[2024-03-09 06:22:49,426 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2024-03-09 06:22:49,427 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2024-03-09 06:22:49,442 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2024-03-09 06:22:49,443 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2024-03-09 06:22:49,443 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2024-03-09 06:22:49,444 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2024-03-09 06:22:49,444 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2024-03-09 06:22:49,444 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2024-03-09 06:22:49,445 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2024-03-09 06:22:49,445 INFO  L153        SettingsManager]:  * Use SBE=true
[2024-03-09 06:22:49,445 INFO  L151        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2024-03-09 06:22:49,446 INFO  L153        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2024-03-09 06:22:49,446 INFO  L153        SettingsManager]:  * sizeof long=4
[2024-03-09 06:22:49,447 INFO  L153        SettingsManager]:  * Overapproximate operations on floating types=true
[2024-03-09 06:22:49,447 INFO  L153        SettingsManager]:  * sizeof POINTER=4
[2024-03-09 06:22:49,447 INFO  L153        SettingsManager]:  * Check division by zero=IGNORE
[2024-03-09 06:22:49,447 INFO  L153        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2024-03-09 06:22:49,448 INFO  L153        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2024-03-09 06:22:49,448 INFO  L153        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2024-03-09 06:22:49,448 INFO  L153        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2024-03-09 06:22:49,449 INFO  L153        SettingsManager]:  * Check unreachability of reach_error function=false
[2024-03-09 06:22:49,449 INFO  L153        SettingsManager]:  * sizeof long double=12
[2024-03-09 06:22:49,449 INFO  L153        SettingsManager]:  * Check if freed pointer was valid=false
[2024-03-09 06:22:49,449 INFO  L153        SettingsManager]:  * Use constant arrays=true
[2024-03-09 06:22:49,450 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2024-03-09 06:22:49,450 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2024-03-09 06:22:49,450 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2024-03-09 06:22:49,450 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000
[2024-03-09 06:22:49,451 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2024-03-09 06:22:49,451 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2024-03-09 06:22:49,451 INFO  L153        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopHeads
[2024-03-09 06:22:49,451 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2024-03-09 06:22:49,452 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2024-03-09 06:22:49,452 INFO  L153        SettingsManager]:  * Apply one-shot large block encoding in concurrent analysis=false
[2024-03-09 06:22:49,452 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2024-03-09 06:22:49,452 INFO  L153        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2024-03-09 06:22:49,453 INFO  L153        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2024-03-09 06:22:49,453 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2024-03-09 06:22:49,453 INFO  L153        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-pldi24/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-pldi24/UAutomizer-linux
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness filename -> witness
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 -> da4059ae5015b9b2b5411cafd8d7f66dfcf43ca14cb85e33016c9817b7004fc6
[2024-03-09 06:22:49,627 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2024-03-09 06:22:49,659 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2024-03-09 06:22:49,661 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2024-03-09 06:22:49,662 INFO  L270        PluginConnector]: Initializing CDTParser...
[2024-03-09 06:22:49,663 INFO  L274        PluginConnector]: CDTParser initialized
[2024-03-09 06:22:49,663 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-struct.i
[2024-03-09 06:22:50,709 INFO  L533              CDTParser]: Created temporary CDT project at NULL
[2024-03-09 06:22:50,942 INFO  L384              CDTParser]: Found 1 translation units.
[2024-03-09 06:22:50,942 INFO  L180              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-struct.i
[2024-03-09 06:22:50,954 INFO  L427              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data/6bc8a2d84/8b4b6943140a4a43a29be675811919fa/FLAGecadb26a0
[2024-03-09 06:22:50,964 INFO  L435              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/data/6bc8a2d84/8b4b6943140a4a43a29be675811919fa
[2024-03-09 06:22:50,971 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2024-03-09 06:22:50,972 INFO  L133        ToolchainWalker]: Walking toolchain with 6 elements.
[2024-03-09 06:22:50,974 INFO  L112        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2024-03-09 06:22:50,974 INFO  L270        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2024-03-09 06:22:50,980 INFO  L274        PluginConnector]: CACSL2BoogieTranslator initialized
[2024-03-09 06:22:50,980 INFO  L184        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 09.03 06:22:50" (1/1) ...
[2024-03-09 06:22:50,981 INFO  L204        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@38729c3f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:50, skipping insertion in model container
[2024-03-09 06:22:50,981 INFO  L184        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 09.03 06:22:50" (1/1) ...
[2024-03-09 06:22:51,016 INFO  L177         MainTranslator]: Built tables and reachable declarations
[2024-03-09 06:22:51,268 INFO  L209          PostProcessor]: Analyzing one entry point: main
[2024-03-09 06:22:51,276 INFO  L202         MainTranslator]: Completed pre-run
[2024-03-09 06:22:51,307 INFO  L209          PostProcessor]: Analyzing one entry point: main
[2024-03-09 06:22:51,375 INFO  L206         MainTranslator]: Completed translation
[2024-03-09 06:22:51,376 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51 WrapperNode
[2024-03-09 06:22:51,376 INFO  L131        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2024-03-09 06:22:51,377 INFO  L112        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2024-03-09 06:22:51,377 INFO  L270        PluginConnector]: Initializing Boogie Procedure Inliner...
[2024-03-09 06:22:51,377 INFO  L274        PluginConnector]: Boogie Procedure Inliner initialized
[2024-03-09 06:22:51,383 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,398 INFO  L184        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,416 INFO  L138                Inliner]: procedures = 265, calls = 18, calls flagged for inlining = 3, calls inlined = 3, statements flattened = 79
[2024-03-09 06:22:51,417 INFO  L131        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2024-03-09 06:22:51,418 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2024-03-09 06:22:51,418 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2024-03-09 06:22:51,418 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2024-03-09 06:22:51,425 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,426 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,429 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,429 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,436 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,438 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,440 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,441 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,443 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2024-03-09 06:22:51,444 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2024-03-09 06:22:51,444 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2024-03-09 06:22:51,444 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2024-03-09 06:22:51,445 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (1/1) ...
[2024-03-09 06:22:51,449 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000
[2024-03-09 06:22:51,457 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:22:51,467 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000 (exit command is (exit), workingDir is null)
[2024-03-09 06:22:51,486 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:4000 (1)] Waiting until timeout for monitored process
[2024-03-09 06:22:51,526 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2024-03-09 06:22:51,526 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2024-03-09 06:22:51,527 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2024-03-09 06:22:51,527 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2024-03-09 06:22:51,527 INFO  L130     BoogieDeclarations]: Found specification of procedure read~int
[2024-03-09 06:22:51,528 INFO  L130     BoogieDeclarations]: Found specification of procedure write~int
[2024-03-09 06:22:51,528 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2024-03-09 06:22:51,528 INFO  L130     BoogieDeclarations]: Found specification of procedure thread
[2024-03-09 06:22:51,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure thread
[2024-03-09 06:22:51,528 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2024-03-09 06:22:51,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2024-03-09 06:22:51,529 WARN  L213             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to OneNontrivialStatement
[2024-03-09 06:22:51,680 INFO  L241             CfgBuilder]: Building ICFG
[2024-03-09 06:22:51,682 INFO  L267             CfgBuilder]: Building CFG for each procedure with an implementation
[2024-03-09 06:22:51,849 INFO  L282             CfgBuilder]: Performing block encoding
[2024-03-09 06:22:51,857 INFO  L304             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2024-03-09 06:22:51,857 INFO  L309             CfgBuilder]: Removed 2 assume(true) statements.
[2024-03-09 06:22:51,858 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 09.03 06:22:51 BoogieIcfgContainer
[2024-03-09 06:22:51,858 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2024-03-09 06:22:51,860 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2024-03-09 06:22:51,860 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2024-03-09 06:22:51,863 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2024-03-09 06:22:51,863 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 09.03 06:22:50" (1/3) ...
[2024-03-09 06:22:51,863 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@22ae6392 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 09.03 06:22:51, skipping insertion in model container
[2024-03-09 06:22:51,864 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 09.03 06:22:51" (2/3) ...
[2024-03-09 06:22:51,864 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@22ae6392 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 09.03 06:22:51, skipping insertion in model container
[2024-03-09 06:22:51,864 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 09.03 06:22:51" (3/3) ...
[2024-03-09 06:22:51,865 INFO  L112   eAbstractionObserver]: Analyzing ICFG per-thread-struct.i
[2024-03-09 06:22:51,871 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2024-03-09 06:22:51,878 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2024-03-09 06:22:51,878 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 5 error locations.
[2024-03-09 06:22:51,878 INFO  L514   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2024-03-09 06:22:51,918 INFO  L144    ThreadInstanceAdder]: Constructed 1 joinOtherThreadTransitions.
[2024-03-09 06:22:51,942 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 102 places, 103 transitions, 213 flow
[2024-03-09 06:22:52,046 INFO  L124   PetriNetUnfolderBase]: 6/154 cut-off events.
[2024-03-09 06:22:52,047 INFO  L125   PetriNetUnfolderBase]: For 1/1 co-relation queries the response was YES.
[2024-03-09 06:22:52,051 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 159 conditions, 154 events. 6/154 cut-off events. For 1/1 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 304 event pairs, 0 based on Foata normal form. 0/136 useless extension candidates. Maximal degree in co-relation 74. Up to 4 conditions per place. 
[2024-03-09 06:22:52,051 INFO  L82        GeneralOperation]: Start removeDead. Operand has 102 places, 103 transitions, 213 flow
[2024-03-09 06:22:52,055 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 102 places, 103 transitions, 213 flow
[2024-03-09 06:22:52,062 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-09 06:22:52,068 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=LoopHeads, 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;@72815bf9, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2024-03-09 06:22:52,068 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 7 error locations.
[2024-03-09 06:22:52,077 INFO  L185   PetriNetUnfolderBase]: Found word, exiting Unfolder.
[2024-03-09 06:22:52,077 INFO  L124   PetriNetUnfolderBase]: 3/48 cut-off events.
[2024-03-09 06:22:52,078 INFO  L125   PetriNetUnfolderBase]: For 0/0 co-relation queries the response was YES.
[2024-03-09 06:22:52,078 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:52,078 INFO  L208   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, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:52,079 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 4 more)] ===
[2024-03-09 06:22:52,083 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:52,083 INFO  L85        PathProgramCache]: Analyzing trace with hash 1739621941, now seen corresponding path program 1 times
[2024-03-09 06:22:52,090 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:52,090 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1707492712]
[2024-03-09 06:22:52,090 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:52,091 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:52,181 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:52,341 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:52,342 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:52,342 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1707492712]
[2024-03-09 06:22:52,343 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1707492712] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:52,343 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:52,343 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:52,344 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1416876921]
[2024-03-09 06:22:52,345 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:52,352 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2024-03-09 06:22:52,356 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:52,375 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2024-03-09 06:22:52,375 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=8, Invalid=12, Unknown=0, NotChecked=0, Total=20
[2024-03-09 06:22:52,442 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 87 out of 103
[2024-03-09 06:22:52,444 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 102 places, 103 transitions, 213 flow. Second operand  has 5 states, 5 states have (on average 88.4) internal successors, (442), 5 states have internal predecessors, (442), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:52,445 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:52,445 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 87 of 103
[2024-03-09 06:22:52,446 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:52,497 INFO  L124   PetriNetUnfolderBase]: 1/165 cut-off events.
[2024-03-09 06:22:52,497 INFO  L125   PetriNetUnfolderBase]: For 4/4 co-relation queries the response was YES.
[2024-03-09 06:22:52,498 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 192 conditions, 165 events. 1/165 cut-off events. For 4/4 co-relation queries the response was YES. Maximal size of possible extension queue 6. Compared 265 event pairs, 0 based on Foata normal form. 2/156 useless extension candidates. Maximal degree in co-relation 40. Up to 16 conditions per place. 
[2024-03-09 06:22:52,499 INFO  L140   encePairwiseOnDemand]: 92/103 looper letters, 11 selfloop transitions, 6 changer transitions 2/105 dead transitions.
[2024-03-09 06:22:52,499 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 107 places, 105 transitions, 253 flow
[2024-03-09 06:22:52,500 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:52,502 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:52,508 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 546 transitions.
[2024-03-09 06:22:52,511 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.883495145631068
[2024-03-09 06:22:52,511 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 546 transitions.
[2024-03-09 06:22:52,512 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 546 transitions.
[2024-03-09 06:22:52,514 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:52,515 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 546 transitions.
[2024-03-09 06:22:52,519 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 91.0) internal successors, (546), 6 states have internal predecessors, (546), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:52,523 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 103.0) internal successors, (721), 7 states have internal predecessors, (721), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:52,524 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 103.0) internal successors, (721), 7 states have internal predecessors, (721), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:52,525 INFO  L175             Difference]: Start difference. First operand has 102 places, 103 transitions, 213 flow. Second operand 6 states and 546 transitions.
[2024-03-09 06:22:52,526 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 107 places, 105 transitions, 253 flow
[2024-03-09 06:22:52,528 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 107 places, 105 transitions, 253 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-09 06:22:52,531 INFO  L231             Difference]: Finished difference. Result has 111 places, 103 transitions, 247 flow
[2024-03-09 06:22:52,532 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=103, PETRI_DIFFERENCE_MINUEND_FLOW=207, PETRI_DIFFERENCE_MINUEND_PLACES=102, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=100, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=2, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=94, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=247, PETRI_PLACES=111, PETRI_TRANSITIONS=103}
[2024-03-09 06:22:52,535 INFO  L281   CegarLoopForPetriNet]: 102 programPoint places, 9 predicate places.
[2024-03-09 06:22:52,536 INFO  L495      AbstractCegarLoop]: Abstraction has has 111 places, 103 transitions, 247 flow
[2024-03-09 06:22:52,536 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 5 states have (on average 88.4) internal successors, (442), 5 states have internal predecessors, (442), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:52,536 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:52,536 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:52,537 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable0
[2024-03-09 06:22:52,537 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 4 more)] ===
[2024-03-09 06:22:52,537 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:52,538 INFO  L85        PathProgramCache]: Analyzing trace with hash 2126181978, now seen corresponding path program 1 times
[2024-03-09 06:22:52,538 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:52,538 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [538511161]
[2024-03-09 06:22:52,538 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:52,539 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:52,567 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:52,814 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:52,814 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:52,815 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [538511161]
[2024-03-09 06:22:52,815 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [538511161] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:52,815 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:52,815 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:52,815 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [939594118]
[2024-03-09 06:22:52,816 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:52,816 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-03-09 06:22:52,817 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:52,817 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-03-09 06:22:52,818 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-03-09 06:22:53,021 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 72 out of 103
[2024-03-09 06:22:53,022 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 111 places, 103 transitions, 247 flow. Second operand  has 6 states, 6 states have (on average 73.16666666666667) internal successors, (439), 6 states have internal predecessors, (439), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,022 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:53,023 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 72 of 103
[2024-03-09 06:22:53,023 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:53,228 INFO  L124   PetriNetUnfolderBase]: 116/602 cut-off events.
[2024-03-09 06:22:53,229 INFO  L125   PetriNetUnfolderBase]: For 15/15 co-relation queries the response was YES.
[2024-03-09 06:22:53,231 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 951 conditions, 602 events. 116/602 cut-off events. For 15/15 co-relation queries the response was YES. Maximal size of possible extension queue 39. Compared 3361 event pairs, 9 based on Foata normal form. 0/557 useless extension candidates. Maximal degree in co-relation 861. Up to 195 conditions per place. 
[2024-03-09 06:22:53,233 INFO  L140   encePairwiseOnDemand]: 80/103 looper letters, 38 selfloop transitions, 29 changer transitions 4/142 dead transitions.
[2024-03-09 06:22:53,234 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 115 places, 142 transitions, 462 flow
[2024-03-09 06:22:53,234 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:53,234 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:53,236 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 502 transitions.
[2024-03-09 06:22:53,237 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8122977346278317
[2024-03-09 06:22:53,237 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 502 transitions.
[2024-03-09 06:22:53,238 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 502 transitions.
[2024-03-09 06:22:53,238 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:53,238 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 502 transitions.
[2024-03-09 06:22:53,239 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 83.66666666666667) internal successors, (502), 6 states have internal predecessors, (502), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,241 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 103.0) internal successors, (721), 7 states have internal predecessors, (721), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,241 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 103.0) internal successors, (721), 7 states have internal predecessors, (721), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,242 INFO  L175             Difference]: Start difference. First operand has 111 places, 103 transitions, 247 flow. Second operand 6 states and 502 transitions.
[2024-03-09 06:22:53,242 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 115 places, 142 transitions, 462 flow
[2024-03-09 06:22:53,244 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 114 places, 142 transitions, 460 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-03-09 06:22:53,246 INFO  L231             Difference]: Finished difference. Result has 119 places, 128 transitions, 441 flow
[2024-03-09 06:22:53,247 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=103, PETRI_DIFFERENCE_MINUEND_FLOW=245, PETRI_DIFFERENCE_MINUEND_PLACES=109, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=103, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=3, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=83, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=441, PETRI_PLACES=119, PETRI_TRANSITIONS=128}
[2024-03-09 06:22:53,247 INFO  L281   CegarLoopForPetriNet]: 102 programPoint places, 17 predicate places.
[2024-03-09 06:22:53,248 INFO  L495      AbstractCegarLoop]: Abstraction has has 119 places, 128 transitions, 441 flow
[2024-03-09 06:22:53,248 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 73.16666666666667) internal successors, (439), 6 states have internal predecessors, (439), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,248 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:53,248 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:53,249 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2024-03-09 06:22:53,249 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 4 more)] ===
[2024-03-09 06:22:53,249 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:53,250 INFO  L85        PathProgramCache]: Analyzing trace with hash 382970382, now seen corresponding path program 1 times
[2024-03-09 06:22:53,250 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:53,250 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [857148100]
[2024-03-09 06:22:53,250 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:53,251 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:53,272 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:53,517 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:53,517 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:53,517 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [857148100]
[2024-03-09 06:22:53,518 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [857148100] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:53,518 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:53,518 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:53,518 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [289177893]
[2024-03-09 06:22:53,518 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:53,519 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-03-09 06:22:53,519 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:53,519 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-03-09 06:22:53,520 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-03-09 06:22:53,618 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 73 out of 103
[2024-03-09 06:22:53,619 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 119 places, 128 transitions, 441 flow. Second operand  has 6 states, 6 states have (on average 75.0) internal successors, (450), 6 states have internal predecessors, (450), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,619 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:53,619 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 73 of 103
[2024-03-09 06:22:53,619 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:53,901 INFO  L124   PetriNetUnfolderBase]: 337/1201 cut-off events.
[2024-03-09 06:22:53,901 INFO  L125   PetriNetUnfolderBase]: For 446/544 co-relation queries the response was YES.
[2024-03-09 06:22:53,905 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 2766 conditions, 1201 events. 337/1201 cut-off events. For 446/544 co-relation queries the response was YES. Maximal size of possible extension queue 83. Compared 8525 event pairs, 67 based on Foata normal form. 15/1149 useless extension candidates. Maximal degree in co-relation 2579. Up to 597 conditions per place. 
[2024-03-09 06:22:53,908 INFO  L140   encePairwiseOnDemand]: 80/103 looper letters, 49 selfloop transitions, 79 changer transitions 5/209 dead transitions.
[2024-03-09 06:22:53,908 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 121 places, 209 transitions, 1043 flow
[2024-03-09 06:22:53,909 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:53,909 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:53,910 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 535 transitions.
[2024-03-09 06:22:53,911 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8656957928802589
[2024-03-09 06:22:53,911 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 535 transitions.
[2024-03-09 06:22:53,911 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 535 transitions.
[2024-03-09 06:22:53,911 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:53,911 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 535 transitions.
[2024-03-09 06:22:53,913 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 89.16666666666667) internal successors, (535), 6 states have internal predecessors, (535), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,914 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 103.0) internal successors, (721), 7 states have internal predecessors, (721), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,915 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 103.0) internal successors, (721), 7 states have internal predecessors, (721), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,915 INFO  L175             Difference]: Start difference. First operand has 119 places, 128 transitions, 441 flow. Second operand 6 states and 535 transitions.
[2024-03-09 06:22:53,915 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 121 places, 209 transitions, 1043 flow
[2024-03-09 06:22:53,921 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 117 places, 209 transitions, 1031 flow, removed 5 selfloop flow, removed 4 redundant places.
[2024-03-09 06:22:53,924 INFO  L231             Difference]: Finished difference. Result has 122 places, 204 transitions, 1119 flow
[2024-03-09 06:22:53,924 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=103, PETRI_DIFFERENCE_MINUEND_FLOW=429, PETRI_DIFFERENCE_MINUEND_PLACES=112, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=128, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=17, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=97, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=1119, PETRI_PLACES=122, PETRI_TRANSITIONS=204}
[2024-03-09 06:22:53,924 INFO  L281   CegarLoopForPetriNet]: 102 programPoint places, 20 predicate places.
[2024-03-09 06:22:53,925 INFO  L495      AbstractCegarLoop]: Abstraction has has 122 places, 204 transitions, 1119 flow
[2024-03-09 06:22:53,925 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 75.0) internal successors, (450), 6 states have internal predecessors, (450), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:53,925 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:53,926 INFO  L208   CegarLoopForPetriNet]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1]
[2024-03-09 06:22:53,926 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2024-03-09 06:22:53,926 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 4 more)] ===
[2024-03-09 06:22:53,926 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:53,927 INFO  L85        PathProgramCache]: Analyzing trace with hash 1331419043, now seen corresponding path program 1 times
[2024-03-09 06:22:53,927 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:53,927 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1359010655]
[2024-03-09 06:22:53,927 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:53,928 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:53,950 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-09 06:22:53,951 INFO  L356             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2024-03-09 06:22:53,961 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is sat
[2024-03-09 06:22:53,979 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2024-03-09 06:22:53,979 INFO  L360         BasicCegarLoop]: Counterexample is feasible
[2024-03-09 06:22:53,980 INFO  L805   garLoopResultBuilder]: Registering result UNSAFE for location ULTIMATE.startErr0INUSE_VIOLATIONSUFFICIENT_THREAD_INSTANCES (6 of 7 remaining)
[2024-03-09 06:22:53,982 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE (5 of 7 remaining)
[2024-03-09 06:22:53,982 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE (4 of 7 remaining)
[2024-03-09 06:22:53,982 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (3 of 7 remaining)
[2024-03-09 06:22:53,982 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE (2 of 7 remaining)
[2024-03-09 06:22:53,983 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (1 of 7 remaining)
[2024-03-09 06:22:53,983 INFO  L805   garLoopResultBuilder]: Registering result UNKNOWN for location threadErr0ASSERT_VIOLATIONDATA_RACE (0 of 7 remaining)
[2024-03-09 06:22:53,983 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2024-03-09 06:22:53,983 INFO  L445         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1]
[2024-03-09 06:22:53,985 WARN  L233   ceAbstractionStarter]: 1 thread instances were not sufficient, I will increase this number and restart the analysis
[2024-03-09 06:22:53,985 INFO  L514   ceAbstractionStarter]: Constructing petrified ICFG for 2 thread instances.
[2024-03-09 06:22:54,000 INFO  L144    ThreadInstanceAdder]: Constructed 2 joinOtherThreadTransitions.
[2024-03-09 06:22:54,002 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 122 places, 122 transitions, 260 flow
[2024-03-09 06:22:54,021 INFO  L124   PetriNetUnfolderBase]: 11/275 cut-off events.
[2024-03-09 06:22:54,021 INFO  L125   PetriNetUnfolderBase]: For 6/6 co-relation queries the response was YES.
[2024-03-09 06:22:54,022 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 287 conditions, 275 events. 11/275 cut-off events. For 6/6 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 632 event pairs, 0 based on Foata normal form. 0/243 useless extension candidates. Maximal degree in co-relation 156. Up to 8 conditions per place. 
[2024-03-09 06:22:54,022 INFO  L82        GeneralOperation]: Start removeDead. Operand has 122 places, 122 transitions, 260 flow
[2024-03-09 06:22:54,023 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 122 places, 122 transitions, 260 flow
[2024-03-09 06:22:54,024 INFO  L356      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2024-03-09 06:22:54,025 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=LoopHeads, 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;@72815bf9, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2024-03-09 06:22:54,025 INFO  L358      AbstractCegarLoop]: Starting to check reachability of 8 error locations.
[2024-03-09 06:22:54,028 INFO  L185   PetriNetUnfolderBase]: Found word, exiting Unfolder.
[2024-03-09 06:22:54,028 INFO  L124   PetriNetUnfolderBase]: 3/48 cut-off events.
[2024-03-09 06:22:54,028 INFO  L125   PetriNetUnfolderBase]: For 0/0 co-relation queries the response was YES.
[2024-03-09 06:22:54,028 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:54,028 INFO  L208   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, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:54,028 INFO  L420      AbstractCegarLoop]: === Iteration 1 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:22:54,029 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:54,029 INFO  L85        PathProgramCache]: Analyzing trace with hash 67653935, now seen corresponding path program 1 times
[2024-03-09 06:22:54,029 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:54,029 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [496723572]
[2024-03-09 06:22:54,029 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:54,030 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:54,038 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:54,074 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:54,074 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:54,074 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [496723572]
[2024-03-09 06:22:54,074 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [496723572] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:54,075 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:54,075 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:54,075 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [552546059]
[2024-03-09 06:22:54,075 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:54,076 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2024-03-09 06:22:54,076 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:54,076 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2024-03-09 06:22:54,076 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=8, Invalid=12, Unknown=0, NotChecked=0, Total=20
[2024-03-09 06:22:54,123 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 104 out of 122
[2024-03-09 06:22:54,124 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 122 places, 122 transitions, 260 flow. Second operand  has 5 states, 5 states have (on average 105.4) internal successors, (527), 5 states have internal predecessors, (527), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:54,124 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:54,125 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 104 of 122
[2024-03-09 06:22:54,125 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:54,166 INFO  L124   PetriNetUnfolderBase]: 3/283 cut-off events.
[2024-03-09 06:22:54,167 INFO  L125   PetriNetUnfolderBase]: For 17/17 co-relation queries the response was YES.
[2024-03-09 06:22:54,167 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 333 conditions, 283 events. 3/283 cut-off events. For 17/17 co-relation queries the response was YES. Maximal size of possible extension queue 7. Compared 685 event pairs, 0 based on Foata normal form. 2/266 useless extension candidates. Maximal degree in co-relation 188. Up to 32 conditions per place. 
[2024-03-09 06:22:54,168 INFO  L140   encePairwiseOnDemand]: 111/122 looper letters, 14 selfloop transitions, 6 changer transitions 2/125 dead transitions.
[2024-03-09 06:22:54,168 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 127 places, 125 transitions, 308 flow
[2024-03-09 06:22:54,168 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:54,168 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:54,169 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 651 transitions.
[2024-03-09 06:22:54,170 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.889344262295082
[2024-03-09 06:22:54,170 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 651 transitions.
[2024-03-09 06:22:54,170 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 651 transitions.
[2024-03-09 06:22:54,170 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:54,171 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 651 transitions.
[2024-03-09 06:22:54,172 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 108.5) internal successors, (651), 6 states have internal predecessors, (651), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:54,173 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:54,174 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:54,174 INFO  L175             Difference]: Start difference. First operand has 122 places, 122 transitions, 260 flow. Second operand 6 states and 651 transitions.
[2024-03-09 06:22:54,174 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 127 places, 125 transitions, 308 flow
[2024-03-09 06:22:54,175 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 127 places, 125 transitions, 308 flow, removed 0 selfloop flow, removed 0 redundant places.
[2024-03-09 06:22:54,176 INFO  L231             Difference]: Finished difference. Result has 131 places, 123 transitions, 298 flow
[2024-03-09 06:22:54,176 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=254, PETRI_DIFFERENCE_MINUEND_PLACES=122, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=119, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=113, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=298, PETRI_PLACES=131, PETRI_TRANSITIONS=123}
[2024-03-09 06:22:54,177 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 9 predicate places.
[2024-03-09 06:22:54,181 INFO  L495      AbstractCegarLoop]: Abstraction has has 131 places, 123 transitions, 298 flow
[2024-03-09 06:22:54,181 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 5 states have (on average 105.4) internal successors, (527), 5 states have internal predecessors, (527), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:54,182 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:54,182 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:54,182 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2024-03-09 06:22:54,185 INFO  L420      AbstractCegarLoop]: === Iteration 2 === Targeting ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:22:54,185 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:54,185 INFO  L85        PathProgramCache]: Analyzing trace with hash 1834781466, now seen corresponding path program 1 times
[2024-03-09 06:22:54,185 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:54,186 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1652872139]
[2024-03-09 06:22:54,186 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:54,186 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:54,194 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:54,324 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:54,325 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:54,325 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1652872139]
[2024-03-09 06:22:54,325 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1652872139] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:54,325 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:54,325 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:54,326 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1625005192]
[2024-03-09 06:22:54,326 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:54,326 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-03-09 06:22:54,326 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:54,327 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-03-09 06:22:54,327 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-03-09 06:22:54,494 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 85 out of 122
[2024-03-09 06:22:54,494 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 131 places, 123 transitions, 298 flow. Second operand  has 6 states, 6 states have (on average 86.16666666666667) internal successors, (517), 6 states have internal predecessors, (517), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:54,494 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:54,495 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 85 of 122
[2024-03-09 06:22:54,495 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:55,097 INFO  L124   PetriNetUnfolderBase]: 1709/5076 cut-off events.
[2024-03-09 06:22:55,097 INFO  L125   PetriNetUnfolderBase]: For 163/163 co-relation queries the response was YES.
[2024-03-09 06:22:55,103 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 8275 conditions, 5076 events. 1709/5076 cut-off events. For 163/163 co-relation queries the response was YES. Maximal size of possible extension queue 238. Compared 42960 event pairs, 275 based on Foata normal form. 0/4719 useless extension candidates. Maximal degree in co-relation 8184. Up to 2240 conditions per place. 
[2024-03-09 06:22:55,118 INFO  L140   encePairwiseOnDemand]: 95/122 looper letters, 46 selfloop transitions, 48 changer transitions 4/183 dead transitions.
[2024-03-09 06:22:55,119 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 135 places, 183 transitions, 617 flow
[2024-03-09 06:22:55,120 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:55,120 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:55,121 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 607 transitions.
[2024-03-09 06:22:55,121 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8292349726775956
[2024-03-09 06:22:55,121 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 607 transitions.
[2024-03-09 06:22:55,121 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 607 transitions.
[2024-03-09 06:22:55,122 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:55,122 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 607 transitions.
[2024-03-09 06:22:55,123 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 101.16666666666667) internal successors, (607), 6 states have internal predecessors, (607), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:55,124 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:55,124 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:55,124 INFO  L175             Difference]: Start difference. First operand has 131 places, 123 transitions, 298 flow. Second operand 6 states and 607 transitions.
[2024-03-09 06:22:55,124 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 135 places, 183 transitions, 617 flow
[2024-03-09 06:22:55,128 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 134 places, 183 transitions, 615 flow, removed 0 selfloop flow, removed 1 redundant places.
[2024-03-09 06:22:55,131 INFO  L231             Difference]: Finished difference. Result has 139 places, 167 transitions, 614 flow
[2024-03-09 06:22:55,131 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=296, PETRI_DIFFERENCE_MINUEND_PLACES=129, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=123, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=8, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=99, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=614, PETRI_PLACES=139, PETRI_TRANSITIONS=167}
[2024-03-09 06:22:55,134 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 17 predicate places.
[2024-03-09 06:22:55,134 INFO  L495      AbstractCegarLoop]: Abstraction has has 139 places, 167 transitions, 614 flow
[2024-03-09 06:22:55,134 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 86.16666666666667) internal successors, (517), 6 states have internal predecessors, (517), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:55,134 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:55,134 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:55,134 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2024-03-09 06:22:55,135 INFO  L420      AbstractCegarLoop]: === Iteration 3 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:22:55,135 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:55,135 INFO  L85        PathProgramCache]: Analyzing trace with hash -1475656483, now seen corresponding path program 1 times
[2024-03-09 06:22:55,136 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:55,136 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1708108500]
[2024-03-09 06:22:55,136 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:55,136 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:55,160 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:55,368 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:55,368 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:55,368 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1708108500]
[2024-03-09 06:22:55,369 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1708108500] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:55,369 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:55,369 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:55,369 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [885130497]
[2024-03-09 06:22:55,369 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:55,370 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-03-09 06:22:55,370 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:55,371 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-03-09 06:22:55,371 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-03-09 06:22:55,513 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 86 out of 122
[2024-03-09 06:22:55,514 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 139 places, 167 transitions, 614 flow. Second operand  has 6 states, 6 states have (on average 88.0) internal successors, (528), 6 states have internal predecessors, (528), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:55,514 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:55,514 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 86 of 122
[2024-03-09 06:22:55,515 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:56,802 INFO  L124   PetriNetUnfolderBase]: 4894/11954 cut-off events.
[2024-03-09 06:22:56,803 INFO  L125   PetriNetUnfolderBase]: For 5307/7433 co-relation queries the response was YES.
[2024-03-09 06:22:56,851 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 29122 conditions, 11954 events. 4894/11954 cut-off events. For 5307/7433 co-relation queries the response was YES. Maximal size of possible extension queue 458. Compared 108963 event pairs, 1132 based on Foata normal form. 46/11284 useless extension candidates. Maximal degree in co-relation 7823. Up to 6769 conditions per place. 
[2024-03-09 06:22:56,904 INFO  L140   encePairwiseOnDemand]: 95/122 looper letters, 80 selfloop transitions, 142 changer transitions 0/312 dead transitions.
[2024-03-09 06:22:56,904 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 141 places, 312 transitions, 1722 flow
[2024-03-09 06:22:56,904 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:56,905 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:56,906 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 643 transitions.
[2024-03-09 06:22:56,906 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8784153005464481
[2024-03-09 06:22:56,906 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 643 transitions.
[2024-03-09 06:22:56,906 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 643 transitions.
[2024-03-09 06:22:56,907 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:56,907 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 643 transitions.
[2024-03-09 06:22:56,908 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 107.16666666666667) internal successors, (643), 6 states have internal predecessors, (643), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:56,909 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:56,910 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:56,910 INFO  L175             Difference]: Start difference. First operand has 139 places, 167 transitions, 614 flow. Second operand 6 states and 643 transitions.
[2024-03-09 06:22:56,910 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 141 places, 312 transitions, 1722 flow
[2024-03-09 06:22:56,922 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 138 places, 312 transitions, 1712 flow, removed 5 selfloop flow, removed 3 redundant places.
[2024-03-09 06:22:56,926 INFO  L231             Difference]: Finished difference. Result has 143 places, 304 transitions, 1902 flow
[2024-03-09 06:22:56,926 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=604, PETRI_DIFFERENCE_MINUEND_PLACES=133, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=167, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=32, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=106, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=1902, PETRI_PLACES=143, PETRI_TRANSITIONS=304}
[2024-03-09 06:22:56,927 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 21 predicate places.
[2024-03-09 06:22:56,927 INFO  L495      AbstractCegarLoop]: Abstraction has has 143 places, 304 transitions, 1902 flow
[2024-03-09 06:22:56,927 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 88.0) internal successors, (528), 6 states have internal predecessors, (528), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:56,928 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:56,928 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:56,928 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2024-03-09 06:22:56,928 INFO  L420      AbstractCegarLoop]: === Iteration 4 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:22:56,928 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:56,928 INFO  L85        PathProgramCache]: Analyzing trace with hash 1192601189, now seen corresponding path program 1 times
[2024-03-09 06:22:56,929 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:56,929 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [77031908]
[2024-03-09 06:22:56,929 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:56,929 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:56,944 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:57,136 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2024-03-09 06:22:57,136 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:57,136 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [77031908]
[2024-03-09 06:22:57,137 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [77031908] provided 1 perfect and 0 imperfect interpolant sequences
[2024-03-09 06:22:57,137 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2024-03-09 06:22:57,137 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2024-03-09 06:22:57,137 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1124479527]
[2024-03-09 06:22:57,137 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2024-03-09 06:22:57,138 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2024-03-09 06:22:57,138 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:57,138 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2024-03-09 06:22:57,139 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=15, Unknown=0, NotChecked=0, Total=30
[2024-03-09 06:22:57,418 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 94 out of 122
[2024-03-09 06:22:57,419 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 143 places, 304 transitions, 1902 flow. Second operand  has 6 states, 6 states have (on average 95.5) internal successors, (573), 6 states have internal predecessors, (573), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:57,419 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:57,419 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 94 of 122
[2024-03-09 06:22:57,419 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:22:58,645 INFO  L124   PetriNetUnfolderBase]: 5008/11995 cut-off events.
[2024-03-09 06:22:58,645 INFO  L125   PetriNetUnfolderBase]: For 14303/14924 co-relation queries the response was YES.
[2024-03-09 06:22:58,673 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 37507 conditions, 11995 events. 5008/11995 cut-off events. For 14303/14924 co-relation queries the response was YES. Maximal size of possible extension queue 458. Compared 107231 event pairs, 575 based on Foata normal form. 47/11606 useless extension candidates. Maximal degree in co-relation 19773. Up to 5158 conditions per place. 
[2024-03-09 06:22:58,712 INFO  L140   encePairwiseOnDemand]: 107/122 looper letters, 120 selfloop transitions, 124 changer transitions 0/425 dead transitions.
[2024-03-09 06:22:58,712 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 148 places, 425 transitions, 3306 flow
[2024-03-09 06:22:58,713 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2024-03-09 06:22:58,713 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 6 states.
[2024-03-09 06:22:58,714 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6 states to 6 states and 629 transitions.
[2024-03-09 06:22:58,714 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.8592896174863388
[2024-03-09 06:22:58,714 INFO  L72            ComplementDD]: Start complementDD. Operand 6 states and 629 transitions.
[2024-03-09 06:22:58,714 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 6 states and 629 transitions.
[2024-03-09 06:22:58,715 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:22:58,715 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 6 states and 629 transitions.
[2024-03-09 06:22:58,716 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 7 states, 6 states have (on average 104.83333333333333) internal successors, (629), 6 states have internal predecessors, (629), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:58,717 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:58,717 INFO  L81            ComplementDD]: Finished complementDD. Result  has 7 states, 7 states have (on average 122.0) internal successors, (854), 7 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)
[2024-03-09 06:22:58,717 INFO  L175             Difference]: Start difference. First operand has 143 places, 304 transitions, 1902 flow. Second operand 6 states and 629 transitions.
[2024-03-09 06:22:58,717 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 148 places, 425 transitions, 3306 flow
[2024-03-09 06:22:58,766 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 148 places, 425 transitions, 3252 flow, removed 27 selfloop flow, removed 0 redundant places.
[2024-03-09 06:22:58,770 INFO  L231             Difference]: Finished difference. Result has 153 places, 423 transitions, 3346 flow
[2024-03-09 06:22:58,771 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=1848, PETRI_DIFFERENCE_MINUEND_PLACES=143, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=304, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=29, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=252, PETRI_DIFFERENCE_SUBTRAHEND_STATES=6, PETRI_FLOW=3346, PETRI_PLACES=153, PETRI_TRANSITIONS=423}
[2024-03-09 06:22:58,771 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 31 predicate places.
[2024-03-09 06:22:58,771 INFO  L495      AbstractCegarLoop]: Abstraction has has 153 places, 423 transitions, 3346 flow
[2024-03-09 06:22:58,772 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 6 states have (on average 95.5) internal successors, (573), 6 states have internal predecessors, (573), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:58,772 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:22:58,772 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:22:58,772 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2024-03-09 06:22:58,772 INFO  L420      AbstractCegarLoop]: === Iteration 5 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:22:58,773 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:22:58,773 INFO  L85        PathProgramCache]: Analyzing trace with hash 929046158, now seen corresponding path program 1 times
[2024-03-09 06:22:58,773 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:22:58,773 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1126241221]
[2024-03-09 06:22:58,773 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:58,773 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:22:58,790 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:59,137 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:59,137 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:22:59,137 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1126241221]
[2024-03-09 06:22:59,137 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1126241221] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:22:59,138 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [86565616]
[2024-03-09 06:22:59,138 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:22:59,138 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:22:59,138 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:22:59,144 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:22:59,146 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2024-03-09 06:22:59,242 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:22:59,253 INFO  L262         TraceCheckSpWp]: Trace formula consists of 182 conjuncts, 24 conjunts are in the unsatisfiable core
[2024-03-09 06:22:59,259 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:22:59,419 INFO  L378             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
[2024-03-09 06:22:59,450 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 0 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
[2024-03-09 06:22:59,495 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:22:59,495 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 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 30 treesize of output 32
[2024-03-09 06:22:59,540 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:22:59,540 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 0 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 3 case distinctions, treesize of input 39 treesize of output 44
[2024-03-09 06:22:59,605 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:22:59,606 INFO  L378             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 43 treesize of output 32
[2024-03-09 06:22:59,615 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:59,615 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:22:59,641 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_269 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_269 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 3)))) (forall ((v_ArrVal_269 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))) (forall ((v_ArrVal_269 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset)))) is different from false
[2024-03-09 06:22:59,661 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_269 (Array Int Int))) (= (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) .cse1) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_269 (Array Int Int))) (= (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_269 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_269 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_269) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2))))))) is different from false
[2024-03-09 06:22:59,852 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:22:59,852 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [86565616] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:22:59,852 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:22:59,852 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 28
[2024-03-09 06:22:59,852 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1809300463]
[2024-03-09 06:22:59,852 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:22:59,853 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 29 states
[2024-03-09 06:22:59,853 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:22:59,854 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 29 interpolants.
[2024-03-09 06:22:59,854 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=105, Invalid=603, Unknown=2, NotChecked=102, Total=812
[2024-03-09 06:22:59,883 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 58 out of 122
[2024-03-09 06:22:59,884 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 153 places, 423 transitions, 3346 flow. Second operand  has 29 states, 29 states have (on average 60.3448275862069) internal successors, (1750), 29 states have internal predecessors, (1750), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:22:59,884 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:22:59,884 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 58 of 122
[2024-03-09 06:22:59,884 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:23:05,763 INFO  L124   PetriNetUnfolderBase]: 15326/30554 cut-off events.
[2024-03-09 06:23:05,763 INFO  L125   PetriNetUnfolderBase]: For 45508/45728 co-relation queries the response was YES.
[2024-03-09 06:23:05,832 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 105642 conditions, 30554 events. 15326/30554 cut-off events. For 45508/45728 co-relation queries the response was YES. Maximal size of possible extension queue 994. Compared 276992 event pairs, 2325 based on Foata normal form. 385/29475 useless extension candidates. Maximal degree in co-relation 85703. Up to 11501 conditions per place. 
[2024-03-09 06:23:05,931 INFO  L140   encePairwiseOnDemand]: 98/122 looper letters, 762 selfloop transitions, 485 changer transitions 1/1307 dead transitions.
[2024-03-09 06:23:05,932 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 180 places, 1307 transitions, 12210 flow
[2024-03-09 06:23:05,932 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 28 states. 
[2024-03-09 06:23:05,932 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 28 states.
[2024-03-09 06:23:05,935 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 2094 transitions.
[2024-03-09 06:23:05,936 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.6129976580796253
[2024-03-09 06:23:05,937 INFO  L72            ComplementDD]: Start complementDD. Operand 28 states and 2094 transitions.
[2024-03-09 06:23:05,937 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 28 states and 2094 transitions.
[2024-03-09 06:23:05,938 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:23:05,938 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 28 states and 2094 transitions.
[2024-03-09 06:23:05,941 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 29 states, 28 states have (on average 74.78571428571429) internal successors, (2094), 28 states have internal predecessors, (2094), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:05,945 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 29 states, 29 states have (on average 122.0) internal successors, (3538), 29 states have internal predecessors, (3538), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:05,946 INFO  L81            ComplementDD]: Finished complementDD. Result  has 29 states, 29 states have (on average 122.0) internal successors, (3538), 29 states have internal predecessors, (3538), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:05,946 INFO  L175             Difference]: Start difference. First operand has 153 places, 423 transitions, 3346 flow. Second operand 28 states and 2094 transitions.
[2024-03-09 06:23:05,946 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 180 places, 1307 transitions, 12210 flow
[2024-03-09 06:23:06,276 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 180 places, 1307 transitions, 12174 flow, removed 18 selfloop flow, removed 0 redundant places.
[2024-03-09 06:23:06,287 INFO  L231             Difference]: Finished difference. Result has 197 places, 870 transitions, 9261 flow
[2024-03-09 06:23:06,287 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=3310, PETRI_DIFFERENCE_MINUEND_PLACES=153, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=423, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=160, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=244, PETRI_DIFFERENCE_SUBTRAHEND_STATES=28, PETRI_FLOW=9261, PETRI_PLACES=197, PETRI_TRANSITIONS=870}
[2024-03-09 06:23:06,288 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 75 predicate places.
[2024-03-09 06:23:06,288 INFO  L495      AbstractCegarLoop]: Abstraction has has 197 places, 870 transitions, 9261 flow
[2024-03-09 06:23:06,289 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 29 states, 29 states have (on average 60.3448275862069) internal successors, (1750), 29 states have internal predecessors, (1750), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:06,289 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:23:06,289 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:23:06,301 INFO  L540       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2024-03-09 06:23:06,494 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,2 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:23:06,495 INFO  L420      AbstractCegarLoop]: === Iteration 6 === Targeting ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:23:06,496 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:23:06,496 INFO  L85        PathProgramCache]: Analyzing trace with hash -16778054, now seen corresponding path program 1 times
[2024-03-09 06:23:06,497 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:23:06,497 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1936551147]
[2024-03-09 06:23:06,497 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:23:06,497 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:23:06,519 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:23:06,820 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:23:06,821 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:23:06,821 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1936551147]
[2024-03-09 06:23:06,821 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1936551147] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:23:06,821 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2123838382]
[2024-03-09 06:23:06,821 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:23:06,821 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:23:06,821 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:23:06,822 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:23:06,837 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2024-03-09 06:23:06,957 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:23:06,958 INFO  L262         TraceCheckSpWp]: Trace formula consists of 182 conjuncts, 22 conjunts are in the unsatisfiable core
[2024-03-09 06:23:06,961 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:23:07,215 INFO  L378             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
[2024-03-09 06:23:07,249 INFO  L378             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 19 treesize of output 18
[2024-03-09 06:23:07,290 INFO  L378             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 26 treesize of output 28
[2024-03-09 06:23:07,343 INFO  L378             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 33 treesize of output 38
[2024-03-09 06:23:07,408 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:23:07,409 INFO  L378             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 37 treesize of output 26
[2024-03-09 06:23:07,446 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:23:07,447 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:23:07,474 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store |c_#race| c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ 2 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store |c_#race| c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ |c_ULTIMATE.start_main_~#tids~0#1.offset| 1)) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store |c_#race| c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ 3 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store |c_#race| c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0))) is different from false
[2024-03-09 06:23:07,493 WARN  L854   $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_348 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ 2 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ |c_ULTIMATE.start_main_~#tids~0#1.offset| 1)) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse1) 0))))) is different from false
[2024-03-09 06:23:07,519 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (+ 2 |c_ULTIMATE.start_main_~#tids~0#1.offset|)) (.cse2 (+ 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|) .cse1 0) .cse2 0)))) (and (forall ((v_ArrVal_348 (Array Int Int))) (= 0 (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (forall ((v_ArrVal_348 (Array Int Int))) (= 0 (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse1))) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) (+ |c_ULTIMATE.start_main_~#tids~0#1.offset| 1)) 0)) (forall ((v_ArrVal_348 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_348) |c_ULTIMATE.start_main_~#tids~0#1.base|) .cse2) 0))))) is different from false
[2024-03-09 06:23:07,773 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:23:07,773 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2123838382] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:23:07,774 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:23:07,774 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 31
[2024-03-09 06:23:07,774 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [316549858]
[2024-03-09 06:23:07,774 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:23:07,774 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 32 states
[2024-03-09 06:23:07,775 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:23:07,775 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 32 interpolants.
[2024-03-09 06:23:07,775 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=115, Invalid=706, Unknown=3, NotChecked=168, Total=992
[2024-03-09 06:23:07,862 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 60 out of 122
[2024-03-09 06:23:07,864 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 197 places, 870 transitions, 9261 flow. Second operand  has 32 states, 32 states have (on average 62.15625) internal successors, (1989), 32 states have internal predecessors, (1989), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:07,864 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:23:07,864 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 60 of 122
[2024-03-09 06:23:07,864 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:23:16,212 INFO  L124   PetriNetUnfolderBase]: 18104/34974 cut-off events.
[2024-03-09 06:23:16,213 INFO  L125   PetriNetUnfolderBase]: For 161490/161877 co-relation queries the response was YES.
[2024-03-09 06:23:16,345 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 168670 conditions, 34974 events. 18104/34974 cut-off events. For 161490/161877 co-relation queries the response was YES. Maximal size of possible extension queue 1173. Compared 313328 event pairs, 1885 based on Foata normal form. 383/33613 useless extension candidates. Maximal degree in co-relation 163550. Up to 10633 conditions per place. 
[2024-03-09 06:23:16,476 INFO  L140   encePairwiseOnDemand]: 91/122 looper letters, 999 selfloop transitions, 771 changer transitions 0/1839 dead transitions.
[2024-03-09 06:23:16,476 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 227 places, 1839 transitions, 22645 flow
[2024-03-09 06:23:16,476 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 31 states. 
[2024-03-09 06:23:16,476 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 31 states.
[2024-03-09 06:23:16,480 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 2323 transitions.
[2024-03-09 06:23:16,480 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.6142252776308831
[2024-03-09 06:23:16,481 INFO  L72            ComplementDD]: Start complementDD. Operand 31 states and 2323 transitions.
[2024-03-09 06:23:16,481 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 31 states and 2323 transitions.
[2024-03-09 06:23:16,482 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:23:16,482 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 31 states and 2323 transitions.
[2024-03-09 06:23:16,486 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 32 states, 31 states have (on average 74.93548387096774) internal successors, (2323), 31 states have internal predecessors, (2323), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:16,489 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 32 states, 32 states have (on average 122.0) internal successors, (3904), 32 states have internal predecessors, (3904), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:16,490 INFO  L81            ComplementDD]: Finished complementDD. Result  has 32 states, 32 states have (on average 122.0) internal successors, (3904), 32 states have internal predecessors, (3904), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:16,490 INFO  L175             Difference]: Start difference. First operand has 197 places, 870 transitions, 9261 flow. Second operand 31 states and 2323 transitions.
[2024-03-09 06:23:16,490 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 227 places, 1839 transitions, 22645 flow
[2024-03-09 06:23:17,936 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 226 places, 1839 transitions, 22156 flow, removed 243 selfloop flow, removed 1 redundant places.
[2024-03-09 06:23:17,954 INFO  L231             Difference]: Finished difference. Result has 242 places, 1321 transitions, 17501 flow
[2024-03-09 06:23:17,955 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=9011, PETRI_DIFFERENCE_MINUEND_PLACES=196, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=870, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=383, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=344, PETRI_DIFFERENCE_SUBTRAHEND_STATES=31, PETRI_FLOW=17501, PETRI_PLACES=242, PETRI_TRANSITIONS=1321}
[2024-03-09 06:23:17,956 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 120 predicate places.
[2024-03-09 06:23:17,956 INFO  L495      AbstractCegarLoop]: Abstraction has has 242 places, 1321 transitions, 17501 flow
[2024-03-09 06:23:17,957 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 32 states, 32 states have (on average 62.15625) internal successors, (1989), 32 states have internal predecessors, (1989), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:17,957 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:23:17,957 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:23:17,963 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2024-03-09 06:23:18,158 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 3 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2024-03-09 06:23:18,159 INFO  L420      AbstractCegarLoop]: === Iteration 7 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:23:18,160 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:23:18,160 INFO  L85        PathProgramCache]: Analyzing trace with hash -818786000, now seen corresponding path program 1 times
[2024-03-09 06:23:18,160 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:23:18,160 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1381385277]
[2024-03-09 06:23:18,161 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:23:18,161 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:23:18,186 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:23:18,927 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:23:18,928 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:23:18,928 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1381385277]
[2024-03-09 06:23:18,928 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1381385277] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:23:18,928 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1449429290]
[2024-03-09 06:23:18,928 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:23:18,928 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:23:18,928 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:23:18,929 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:23:18,931 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2024-03-09 06:23:19,040 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:23:19,041 INFO  L262         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 46 conjunts are in the unsatisfiable core
[2024-03-09 06:23:19,047 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:23:19,074 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 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 6 treesize of output 5
[2024-03-09 06:23:19,155 INFO  L349             Elim1Store]: treesize reduction 4, result has 66.7 percent of original size
[2024-03-09 06:23:19,156 INFO  L378             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 15 treesize of output 15
[2024-03-09 06:23:19,333 INFO  L349             Elim1Store]: treesize reduction 19, result has 20.8 percent of original size
[2024-03-09 06:23:19,334 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 34 treesize of output 33
[2024-03-09 06:23:19,476 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:23:19,477 INFO  L378             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 26 treesize of output 19
[2024-03-09 06:23:19,506 INFO  L378             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
[2024-03-09 06:23:19,573 INFO  L378             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
[2024-03-09 06:23:19,658 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:23:19,658 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 2 select indices, 2 select index equivalence classes, 1 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 30 treesize of output 32
[2024-03-09 06:23:19,901 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 25 treesize of output 13
[2024-03-09 06:23:19,953 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:23:19,953 INFO  L378             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 34 treesize of output 25
[2024-03-09 06:23:19,971 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:23:19,972 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 1 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 3 case distinctions, treesize of input 39 treesize of output 44
[2024-03-09 06:23:20,031 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:23:20,032 INFO  L378             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 43 treesize of output 32
[2024-03-09 06:23:20,060 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:23:20,061 INFO  L378             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 43 treesize of output 32
[2024-03-09 06:23:20,084 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:23:20,085 INFO  L378             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 43 treesize of output 32
[2024-03-09 06:23:20,120 INFO  L378             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 43 treesize of output 32
[2024-03-09 06:23:20,132 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:23:20,132 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:23:20,155 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_452 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_452 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_452 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 3)) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_452 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)) |c_threadThread1of2ForFork0_#t~nondet4|))) is different from false
[2024-03-09 06:23:36,589 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) .cse1) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (forall ((v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2))))))) is different from false
[2024-03-09 06:23:36,615 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse0 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (and (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) .cse0) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))))) is different from false
[2024-03-09 06:23:36,647 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse0 (+ c_threadThread1of2ForFork0_~t~0.offset 3)) (.cse1 (select (select |c_#memory_$Pointer$.base| |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (and (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse1 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) .cse0))) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse1 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse1 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse0 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse1 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))))) is different from false
[2024-03-09 06:23:36,843 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse3 (+ c_threadThread1of2ForFork0_~t~0.offset 2))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse3 |c_threadThread1of2ForFork0_#t~nondet4|))) (.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3)) (.cse2 (select (select |c_#memory_$Pointer$.base| |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (and (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse2 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) .cse1))) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse2 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) .cse3))) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse2 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_446 (Array Int Int)) (v_ArrVal_452 (Array Int Int)) (v_ArrVal_451 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_446) c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)) |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_451) .cse2 v_ArrVal_452) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset)))))) is different from false
[2024-03-09 06:23:37,478 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 62 treesize of output 46
[2024-03-09 06:23:37,598 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:23:37,598 INFO  L378             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 35 treesize of output 40
[2024-03-09 06:23:37,665 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 1 not checked.
[2024-03-09 06:23:37,666 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1449429290] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:23:37,666 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:23:37,666 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 17, 19] total 43
[2024-03-09 06:23:37,666 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [556545377]
[2024-03-09 06:23:37,666 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:23:37,668 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 44 states
[2024-03-09 06:23:37,670 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:23:37,670 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 44 interpolants.
[2024-03-09 06:23:37,672 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=154, Invalid=1320, Unknown=28, NotChecked=390, Total=1892
[2024-03-09 06:23:37,761 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 49 out of 122
[2024-03-09 06:23:37,765 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 242 places, 1321 transitions, 17501 flow. Second operand  has 44 states, 44 states have (on average 51.15909090909091) internal successors, (2251), 44 states have internal predecessors, (2251), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:23:37,765 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:23:37,765 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 49 of 122
[2024-03-09 06:23:37,766 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:24:02,667 INFO  L124   PetriNetUnfolderBase]: 29178/57089 cut-off events.
[2024-03-09 06:24:02,667 INFO  L125   PetriNetUnfolderBase]: For 444823/444917 co-relation queries the response was YES.
[2024-03-09 06:24:03,224 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 290929 conditions, 57089 events. 29178/57089 cut-off events. For 444823/444917 co-relation queries the response was YES. Maximal size of possible extension queue 1878. Compared 556720 event pairs, 3673 based on Foata normal form. 140/54930 useless extension candidates. Maximal degree in co-relation 285115. Up to 27466 conditions per place. 
[2024-03-09 06:24:03,455 INFO  L140   encePairwiseOnDemand]: 76/122 looper letters, 2239 selfloop transitions, 591 changer transitions 58/2937 dead transitions.
[2024-03-09 06:24:03,455 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 294 places, 2937 transitions, 40408 flow
[2024-03-09 06:24:03,456 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 53 states. 
[2024-03-09 06:24:03,456 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 53 states.
[2024-03-09 06:24:03,460 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 3253 transitions.
[2024-03-09 06:24:03,461 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.5030931023816888
[2024-03-09 06:24:03,461 INFO  L72            ComplementDD]: Start complementDD. Operand 53 states and 3253 transitions.
[2024-03-09 06:24:03,461 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 53 states and 3253 transitions.
[2024-03-09 06:24:03,462 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:24:03,462 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 53 states and 3253 transitions.
[2024-03-09 06:24:03,467 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 54 states, 53 states have (on average 61.37735849056604) internal successors, (3253), 53 states have internal predecessors, (3253), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:03,473 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 54 states, 54 states have (on average 122.0) internal successors, (6588), 54 states have internal predecessors, (6588), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:03,474 INFO  L81            ComplementDD]: Finished complementDD. Result  has 54 states, 54 states have (on average 122.0) internal successors, (6588), 54 states have internal predecessors, (6588), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:03,474 INFO  L175             Difference]: Start difference. First operand has 242 places, 1321 transitions, 17501 flow. Second operand 53 states and 3253 transitions.
[2024-03-09 06:24:03,474 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 294 places, 2937 transitions, 40408 flow
[2024-03-09 06:24:06,838 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 287 places, 2937 transitions, 40281 flow, removed 28 selfloop flow, removed 7 redundant places.
[2024-03-09 06:24:06,869 INFO  L231             Difference]: Finished difference. Result has 329 places, 1825 transitions, 26121 flow
[2024-03-09 06:24:06,869 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=17409, PETRI_DIFFERENCE_MINUEND_PLACES=235, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=1321, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=130, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=939, PETRI_DIFFERENCE_SUBTRAHEND_STATES=53, PETRI_FLOW=26121, PETRI_PLACES=329, PETRI_TRANSITIONS=1825}
[2024-03-09 06:24:06,870 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 207 predicate places.
[2024-03-09 06:24:06,870 INFO  L495      AbstractCegarLoop]: Abstraction has has 329 places, 1825 transitions, 26121 flow
[2024-03-09 06:24:06,871 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 44 states, 44 states have (on average 51.15909090909091) internal successors, (2251), 44 states have internal predecessors, (2251), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:06,871 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:24:06,871 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:24:06,875 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2024-03-09 06:24:07,075 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,4 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:24:07,076 INFO  L420      AbstractCegarLoop]: === Iteration 8 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:24:07,076 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:24:07,077 INFO  L85        PathProgramCache]: Analyzing trace with hash -267500672, now seen corresponding path program 2 times
[2024-03-09 06:24:07,077 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:24:07,077 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2136011322]
[2024-03-09 06:24:07,077 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:24:07,078 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:24:07,099 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:24:07,792 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:24:07,792 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:24:07,792 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2136011322]
[2024-03-09 06:24:07,792 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2136011322] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:24:07,793 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1646694577]
[2024-03-09 06:24:07,793 INFO  L93    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2024-03-09 06:24:07,793 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:24:07,793 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:24:07,794 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:24:07,796 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2024-03-09 06:24:07,915 INFO  L228   tOrderPrioritization]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2024-03-09 06:24:07,915 INFO  L229   tOrderPrioritization]: Conjunction of SSA is unsat
[2024-03-09 06:24:07,917 INFO  L262         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 67 conjunts are in the unsatisfiable core
[2024-03-09 06:24:07,923 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:24:08,048 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 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 6 treesize of output 5
[2024-03-09 06:24:08,103 INFO  L349             Elim1Store]: treesize reduction 18, result has 35.7 percent of original size
[2024-03-09 06:24:08,103 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 2 case distinctions, treesize of input 17 treesize of output 21
[2024-03-09 06:24:08,239 INFO  L349             Elim1Store]: treesize reduction 8, result has 61.9 percent of original size
[2024-03-09 06:24:08,240 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 3 select indices, 3 select index equivalence classes, 1 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 2 case distinctions, treesize of input 20 treesize of output 22
[2024-03-09 06:24:08,551 INFO  L349             Elim1Store]: treesize reduction 19, result has 20.8 percent of original size
[2024-03-09 06:24:08,552 INFO  L378             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 2 new quantified variables, introduced 1 case distinctions, treesize of input 33 treesize of output 32
[2024-03-09 06:24:08,770 INFO  L378             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 25 treesize of output 18
[2024-03-09 06:24:08,839 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 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
[2024-03-09 06:24:08,907 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 19 treesize of output 18
[2024-03-09 06:24:09,293 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 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 24 treesize of output 12
[2024-03-09 06:24:09,370 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 2 select indices, 2 select index equivalence classes, 5 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 0 case distinctions, treesize of input 26 treesize of output 28
[2024-03-09 06:24:09,458 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 8 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 0 case distinctions, treesize of input 33 treesize of output 38
[2024-03-09 06:24:09,572 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 37 treesize of output 26
[2024-03-09 06:24:09,599 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 37 treesize of output 26
[2024-03-09 06:24:09,623 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 37 treesize of output 26
[2024-03-09 06:24:09,639 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 37 treesize of output 26
[2024-03-09 06:24:09,732 INFO  L378             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 37 treesize of output 26
[2024-03-09 06:24:09,799 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:24:09,800 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:24:09,827 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_557 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_557 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 3)))) (forall ((v_ArrVal_557 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (forall ((v_ArrVal_557 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1))))) is different from false
[2024-03-09 06:24:09,863 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 3)))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1))))) is different from false
[2024-03-09 06:24:09,921 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) .cse1))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset) |c_threadThread1of2ForFork0_#t~nondet4|))))) is different from false
[2024-03-09 06:24:09,943 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse2 (+ c_threadThread1of2ForFork0_~t~0.offset 2)) (.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse2 |c_threadThread1of2ForFork0_#t~nondet4|) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) .cse1))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) .cse2) |c_threadThread1of2ForFork0_#t~nondet4|)) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset) |c_threadThread1of2ForFork0_#t~nondet4|))))) is different from false
[2024-03-09 06:24:09,968 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse3 (+ c_threadThread1of2ForFork0_~t~0.offset 2)) (.cse2 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse3 |c_threadThread1of2ForFork0_#t~nondet4|) .cse2 |c_threadThread1of2ForFork0_#t~nondet4|))) (.cse1 (select (select |c_#memory_$Pointer$.base| |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (and (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) .cse1 v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) .cse1 v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) .cse1 v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) .cse2))) (forall ((v_ArrVal_557 (Array Int Int)) (v_ArrVal_556 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_556) .cse1 v_ArrVal_557) c_threadThread1of2ForFork0_~t~0.base) .cse3)))))) is different from false
[2024-03-09 06:24:10,594 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:24:10,595 INFO  L378             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 1 new quantified variables, introduced 4 case distinctions, treesize of input 42 treesize of output 58
[2024-03-09 06:24:10,603 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:24:10,603 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 4 select indices, 4 select index equivalence classes, 0 disjoint index pairs (out of 6 index pairs), introduced 4 new quantified variables, introduced 6 case distinctions, treesize of input 248 treesize of output 154
[2024-03-09 06:24:10,612 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 21 treesize of output 17
[2024-03-09 06:24:10,615 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 32 treesize of output 24
[2024-03-09 06:24:10,649 INFO  L349             Elim1Store]: treesize reduction 38, result has 2.6 percent of original size
[2024-03-09 06:24:10,649 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 4 case distinctions, treesize of input 42 treesize of output 1
[2024-03-09 06:24:10,656 INFO  L349             Elim1Store]: treesize reduction 38, result has 2.6 percent of original size
[2024-03-09 06:24:10,657 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 4 case distinctions, treesize of input 40 treesize of output 1
[2024-03-09 06:24:10,665 INFO  L349             Elim1Store]: treesize reduction 38, result has 2.6 percent of original size
[2024-03-09 06:24:10,666 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 4 case distinctions, treesize of input 42 treesize of output 1
[2024-03-09 06:24:11,453 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 51 treesize of output 35
[2024-03-09 06:24:11,466 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 8 treesize of output 6
[2024-03-09 06:24:11,665 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:24:11,665 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1646694577] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:24:11,665 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:24:11,665 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 22, 20] total 57
[2024-03-09 06:24:11,666 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2067508712]
[2024-03-09 06:24:11,666 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:24:11,666 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 58 states
[2024-03-09 06:24:11,667 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:24:11,667 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 58 interpolants.
[2024-03-09 06:24:11,668 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=233, Invalid=2534, Unknown=9, NotChecked=530, Total=3306
[2024-03-09 06:24:11,755 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 33 out of 122
[2024-03-09 06:24:11,757 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 329 places, 1825 transitions, 26121 flow. Second operand  has 58 states, 58 states have (on average 35.224137931034484) internal successors, (2043), 58 states have internal predecessors, (2043), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:11,757 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:24:11,757 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 33 of 122
[2024-03-09 06:24:11,757 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:24:51,154 INFO  L124   PetriNetUnfolderBase]: 33468/64830 cut-off events.
[2024-03-09 06:24:51,154 INFO  L125   PetriNetUnfolderBase]: For 669666/670254 co-relation queries the response was YES.
[2024-03-09 06:24:51,957 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 371953 conditions, 64830 events. 33468/64830 cut-off events. For 669666/670254 co-relation queries the response was YES. Maximal size of possible extension queue 1985. Compared 631256 event pairs, 3641 based on Foata normal form. 365/62528 useless extension candidates. Maximal degree in co-relation 370347. Up to 30614 conditions per place. 
[2024-03-09 06:24:52,216 INFO  L140   encePairwiseOnDemand]: 65/122 looper letters, 2692 selfloop transitions, 971 changer transitions 49/3746 dead transitions.
[2024-03-09 06:24:52,217 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 402 places, 3746 transitions, 56670 flow
[2024-03-09 06:24:52,218 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 74 states. 
[2024-03-09 06:24:52,218 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 74 states.
[2024-03-09 06:24:52,220 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 3368 transitions.
[2024-03-09 06:24:52,221 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.3730615861763403
[2024-03-09 06:24:52,221 INFO  L72            ComplementDD]: Start complementDD. Operand 74 states and 3368 transitions.
[2024-03-09 06:24:52,221 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 74 states and 3368 transitions.
[2024-03-09 06:24:52,222 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:24:52,222 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 74 states and 3368 transitions.
[2024-03-09 06:24:52,226 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 75 states, 74 states have (on average 45.513513513513516) internal successors, (3368), 74 states have internal predecessors, (3368), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:52,233 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 75 states, 75 states have (on average 122.0) internal successors, (9150), 75 states have internal predecessors, (9150), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:52,234 INFO  L81            ComplementDD]: Finished complementDD. Result  has 75 states, 75 states have (on average 122.0) internal successors, (9150), 75 states have internal predecessors, (9150), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:24:52,234 INFO  L175             Difference]: Start difference. First operand has 329 places, 1825 transitions, 26121 flow. Second operand 74 states and 3368 transitions.
[2024-03-09 06:24:52,234 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 402 places, 3746 transitions, 56670 flow
[2024-03-09 06:25:03,094 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 396 places, 3746 transitions, 56586 flow, removed 36 selfloop flow, removed 6 redundant places.
[2024-03-09 06:25:03,136 INFO  L231             Difference]: Finished difference. Result has 417 places, 2381 transitions, 37825 flow
[2024-03-09 06:25:03,137 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=26059, PETRI_DIFFERENCE_MINUEND_PLACES=323, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=1825, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=490, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=1190, PETRI_DIFFERENCE_SUBTRAHEND_STATES=74, PETRI_FLOW=37825, PETRI_PLACES=417, PETRI_TRANSITIONS=2381}
[2024-03-09 06:25:03,137 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 295 predicate places.
[2024-03-09 06:25:03,138 INFO  L495      AbstractCegarLoop]: Abstraction has has 417 places, 2381 transitions, 37825 flow
[2024-03-09 06:25:03,138 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 58 states, 58 states have (on average 35.224137931034484) internal successors, (2043), 58 states have internal predecessors, (2043), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:25:03,138 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:25:03,138 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:25:03,148 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2024-03-09 06:25:03,339 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2024-03-09 06:25:03,339 INFO  L420      AbstractCegarLoop]: === Iteration 9 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:25:03,340 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:25:03,340 INFO  L85        PathProgramCache]: Analyzing trace with hash -1160744244, now seen corresponding path program 3 times
[2024-03-09 06:25:03,341 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:25:03,341 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1219400120]
[2024-03-09 06:25:03,341 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:25:03,341 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:25:03,364 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:25:04,044 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:25:04,044 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:25:04,044 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1219400120]
[2024-03-09 06:25:04,044 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1219400120] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:25:04,044 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2041418299]
[2024-03-09 06:25:04,045 INFO  L93    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2024-03-09 06:25:04,045 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:25:04,045 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:25:04,046 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:25:04,048 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2024-03-09 06:25:04,177 INFO  L228   tOrderPrioritization]: Assert order OUTSIDE_LOOP_FIRST2 issued 2 check-sat command(s)
[2024-03-09 06:25:04,177 INFO  L229   tOrderPrioritization]: Conjunction of SSA is unsat
[2024-03-09 06:25:04,178 INFO  L262         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 70 conjunts are in the unsatisfiable core
[2024-03-09 06:25:04,182 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:25:04,306 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 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 6 treesize of output 5
[2024-03-09 06:25:04,365 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:25:04,366 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 2 select indices, 2 select index equivalence classes, 1 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 0 case distinctions, treesize of input 17 treesize of output 17
[2024-03-09 06:25:04,528 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:25:04,544 INFO  L349             Elim1Store]: treesize reduction 8, result has 61.9 percent of original size
[2024-03-09 06:25:04,545 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 3 select indices, 3 select index equivalence classes, 1 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 2 case distinctions, treesize of input 20 treesize of output 22
[2024-03-09 06:25:04,905 INFO  L349             Elim1Store]: treesize reduction 17, result has 22.7 percent of original size
[2024-03-09 06:25:04,906 INFO  L378             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 1 case distinctions, treesize of input 33 treesize of output 24
[2024-03-09 06:25:05,206 INFO  L378             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 26 treesize of output 19
[2024-03-09 06:25:05,368 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 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
[2024-03-09 06:25:05,648 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 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 25 treesize of output 13
[2024-03-09 06:25:05,721 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 19 treesize of output 18
[2024-03-09 06:25:05,804 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 2 select indices, 2 select index equivalence classes, 5 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 0 case distinctions, treesize of input 26 treesize of output 28
[2024-03-09 06:25:05,894 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 8 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 0 case distinctions, treesize of input 33 treesize of output 38
[2024-03-09 06:25:05,994 INFO  L378             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 37 treesize of output 26
[2024-03-09 06:25:06,041 INFO  L378             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 37 treesize of output 26
[2024-03-09 06:25:06,072 INFO  L378             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 37 treesize of output 26
[2024-03-09 06:25:06,108 INFO  L378             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 37 treesize of output 26
[2024-03-09 06:25:06,279 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:25:06,280 INFO  L378             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 44 treesize of output 36
[2024-03-09 06:25:06,390 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:25:06,390 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:25:06,419 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))) (forall ((v_ArrVal_662 (Array Int Int))) (= (select (select (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 3)) |c_threadThread1of2ForFork0_#t~nondet4|))) is different from false
[2024-03-09 06:25:06,595 WARN  L854   $PredicateComparison]: unable to prove that (and (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 3)))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_662 (Array Int Int))) (= (select (select (store (store |c_#race| |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)) |c_threadThread1of2ForFork0_#t~nondet4|))))) is different from false
[2024-03-09 06:25:06,743 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset) |c_threadThread1of2ForFork0_#t~nondet4|)) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 2)))))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse1))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0))))))) is different from false
[2024-03-09 06:25:06,781 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 2)) (.cse2 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|) .cse2 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse1) |c_threadThread1of2ForFork0_#t~nondet4|)) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) (+ c_threadThread1of2ForFork0_~t~0.offset 1)))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse2))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0))))))) is different from false
[2024-03-09 06:25:06,826 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse2 (+ c_threadThread1of2ForFork0_~t~0.offset 1)) (.cse3 (+ c_threadThread1of2ForFork0_~t~0.offset 2)) (.cse1 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (store (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse2 |c_threadThread1of2ForFork0_#t~nondet4|) .cse3 |c_threadThread1of2ForFork0_#t~nondet4|) .cse1 |c_threadThread1of2ForFork0_#t~nondet4|)))) (and (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse1))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse2))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)) (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) |c_ULTIMATE.start_main_#t~mem13#1.base| v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse3)))))))) is different from false
[2024-03-09 06:25:06,871 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse3 (+ c_threadThread1of2ForFork0_~t~0.offset 1)) (.cse2 (+ c_threadThread1of2ForFork0_~t~0.offset 2)) (.cse4 (+ c_threadThread1of2ForFork0_~t~0.offset 3))) (let ((.cse0 (store |c_#race| c_threadThread1of2ForFork0_~t~0.base (store (store (store (select |c_#race| c_threadThread1of2ForFork0_~t~0.base) .cse3 |c_threadThread1of2ForFork0_#t~nondet4|) .cse2 |c_threadThread1of2ForFork0_#t~nondet4|) .cse4 |c_threadThread1of2ForFork0_#t~nondet4|))) (.cse1 (select (select |c_#memory_$Pointer$.base| |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|))) (and (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) .cse1 v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse2))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) .cse1 v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse3))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= |c_threadThread1of2ForFork0_#t~nondet4| (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) .cse1 v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) c_threadThread1of2ForFork0_~t~0.offset))) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0)))) (forall ((v_ArrVal_661 (Array Int Int))) (or (forall ((v_ArrVal_662 (Array Int Int))) (= (select (select (store (store .cse0 |c_ULTIMATE.start_main_~#tids~0#1.base| v_ArrVal_661) .cse1 v_ArrVal_662) c_threadThread1of2ForFork0_~t~0.base) .cse4) |c_threadThread1of2ForFork0_#t~nondet4|)) (not (= (select v_ArrVal_661 |c_ULTIMATE.start_main_~#tids~0#1.offset|) 0))))))) is different from false
[2024-03-09 06:25:07,328 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:25:07,328 INFO  L378             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 1 new quantified variables, introduced 4 case distinctions, treesize of input 40 treesize of output 56
[2024-03-09 06:25:07,335 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:25:07,335 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 4 select indices, 4 select index equivalence classes, 0 disjoint index pairs (out of 6 index pairs), introduced 4 new quantified variables, introduced 6 case distinctions, treesize of input 138 treesize of output 76
[2024-03-09 06:25:07,342 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 52 treesize of output 48
[2024-03-09 06:25:07,351 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:25:07,351 INFO  L378             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 37 treesize of output 41
[2024-03-09 06:25:07,402 INFO  L349             Elim1Store]: treesize reduction 38, result has 2.6 percent of original size
[2024-03-09 06:25:07,402 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 4 case distinctions, treesize of input 42 treesize of output 1
[2024-03-09 06:25:07,414 INFO  L349             Elim1Store]: treesize reduction 38, result has 2.6 percent of original size
[2024-03-09 06:25:07,414 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 4 case distinctions, treesize of input 42 treesize of output 1
[2024-03-09 06:25:07,425 INFO  L349             Elim1Store]: treesize reduction 38, result has 2.6 percent of original size
[2024-03-09 06:25:07,425 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 0 select indices, 0 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 4 case distinctions, treesize of input 42 treesize of output 1
[2024-03-09 06:25:08,355 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 52 treesize of output 40
[2024-03-09 06:25:08,361 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 22
[2024-03-09 06:25:08,595 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:25:08,596 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2041418299] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:25:08,596 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:25:08,596 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 22, 21] total 58
[2024-03-09 06:25:08,596 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [522408747]
[2024-03-09 06:25:08,596 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:25:08,596 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 59 states
[2024-03-09 06:25:08,597 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:25:08,597 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 59 interpolants.
[2024-03-09 06:25:08,598 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=220, Invalid=2553, Unknown=7, NotChecked=642, Total=3422
[2024-03-09 06:25:08,996 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 33 out of 122
[2024-03-09 06:25:08,999 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 417 places, 2381 transitions, 37825 flow. Second operand  has 59 states, 59 states have (on average 35.186440677966104) internal successors, (2076), 59 states have internal predecessors, (2076), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:25:08,999 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:25:08,999 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 33 of 122
[2024-03-09 06:25:08,999 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:25:59,147 INFO  L124   PetriNetUnfolderBase]: 35798/68895 cut-off events.
[2024-03-09 06:25:59,147 INFO  L125   PetriNetUnfolderBase]: For 967376/968006 co-relation queries the response was YES.
[2024-03-09 06:26:00,348 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 448612 conditions, 68895 events. 35798/68895 cut-off events. For 967376/968006 co-relation queries the response was YES. Maximal size of possible extension queue 2114. Compared 669975 event pairs, 3763 based on Foata normal form. 392/66890 useless extension candidates. Maximal degree in co-relation 448098. Up to 31094 conditions per place. 
[2024-03-09 06:26:00,653 INFO  L140   encePairwiseOnDemand]: 61/122 looper letters, 2977 selfloop transitions, 1408 changer transitions 38/4457 dead transitions.
[2024-03-09 06:26:00,653 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 497 places, 4457 transitions, 74066 flow
[2024-03-09 06:26:00,654 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 82 states. 
[2024-03-09 06:26:00,654 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 82 states.
[2024-03-09 06:26:00,657 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 3700 transitions.
[2024-03-09 06:26:00,660 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.36985205917632946
[2024-03-09 06:26:00,660 INFO  L72            ComplementDD]: Start complementDD. Operand 82 states and 3700 transitions.
[2024-03-09 06:26:00,660 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 82 states and 3700 transitions.
[2024-03-09 06:26:00,661 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:26:00,661 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 82 states and 3700 transitions.
[2024-03-09 06:26:00,666 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 83 states, 82 states have (on average 45.1219512195122) internal successors, (3700), 82 states have internal predecessors, (3700), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:26:00,677 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 83 states, 83 states have (on average 122.0) internal successors, (10126), 83 states have internal predecessors, (10126), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:26:00,678 INFO  L81            ComplementDD]: Finished complementDD. Result  has 83 states, 83 states have (on average 122.0) internal successors, (10126), 83 states have internal predecessors, (10126), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:26:00,678 INFO  L175             Difference]: Start difference. First operand has 417 places, 2381 transitions, 37825 flow. Second operand 82 states and 3700 transitions.
[2024-03-09 06:26:00,678 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 497 places, 4457 transitions, 74066 flow
[2024-03-09 06:26:25,075 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 467 places, 4457 transitions, 72619 flow, removed 624 selfloop flow, removed 30 redundant places.
[2024-03-09 06:26:25,129 INFO  L231             Difference]: Finished difference. Result has 498 places, 3003 transitions, 52663 flow
[2024-03-09 06:26:25,130 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=36716, PETRI_DIFFERENCE_MINUEND_PLACES=386, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=2381, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=824, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=1404, PETRI_DIFFERENCE_SUBTRAHEND_STATES=82, PETRI_FLOW=52663, PETRI_PLACES=498, PETRI_TRANSITIONS=3003}
[2024-03-09 06:26:25,130 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 376 predicate places.
[2024-03-09 06:26:25,130 INFO  L495      AbstractCegarLoop]: Abstraction has has 498 places, 3003 transitions, 52663 flow
[2024-03-09 06:26:25,131 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 59 states, 59 states have (on average 35.186440677966104) internal successors, (2076), 59 states have internal predecessors, (2076), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:26:25,131 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:26:25,131 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:26:25,138 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2024-03-09 06:26:25,332 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12,6 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:26:25,333 INFO  L420      AbstractCegarLoop]: === Iteration 10 === Targeting threadErr0ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:26:25,333 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:26:25,334 INFO  L85        PathProgramCache]: Analyzing trace with hash 186194082, now seen corresponding path program 4 times
[2024-03-09 06:26:25,334 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:26:25,334 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [509443666]
[2024-03-09 06:26:25,334 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:26:25,334 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:26:25,363 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:26:25,964 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:26:25,965 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:26:25,965 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [509443666]
[2024-03-09 06:26:25,965 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [509443666] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:26:25,965 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [765421533]
[2024-03-09 06:26:25,965 INFO  L93    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2024-03-09 06:26:25,965 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:26:25,965 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:26:25,967 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:26:25,968 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2024-03-09 06:26:26,152 INFO  L228   tOrderPrioritization]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 0 check-sat command(s)
[2024-03-09 06:26:26,153 INFO  L229   tOrderPrioritization]: Conjunction of SSA is unsat
[2024-03-09 06:26:26,156 INFO  L262         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 67 conjunts are in the unsatisfiable core
[2024-03-09 06:26:26,162 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:26:26,203 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 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 6 treesize of output 5
[2024-03-09 06:26:26,381 INFO  L349             Elim1Store]: treesize reduction 4, result has 66.7 percent of original size
[2024-03-09 06:26:26,381 INFO  L378             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 15 treesize of output 15
[2024-03-09 06:26:26,784 INFO  L349             Elim1Store]: treesize reduction 19, result has 20.8 percent of original size
[2024-03-09 06:26:26,785 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 50 treesize of output 45
[2024-03-09 06:26:26,797 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:26:26,799 INFO  L378             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 24 treesize of output 11
[2024-03-09 06:26:27,088 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:26:27,090 INFO  L378             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 16 treesize of output 11
[2024-03-09 06:26:27,096 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:26:27,097 INFO  L378             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 26 treesize of output 19
[2024-03-09 06:26:27,370 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 25 treesize of output 13
[2024-03-09 06:26:27,381 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 7 treesize of output 3
[2024-03-09 06:26:27,503 INFO  L378             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
[2024-03-09 06:26:27,561 INFO  L378             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 19 treesize of output 18
[2024-03-09 06:26:27,634 INFO  L378             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 26 treesize of output 28
[2024-03-09 06:26:27,707 INFO  L378             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 33 treesize of output 38
[2024-03-09 06:26:27,797 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 4 select indices, 4 select index equivalence classes, 7 disjoint index pairs (out of 6 index pairs), introduced 4 new quantified variables, introduced 0 case distinctions, treesize of input 44 treesize of output 52
[2024-03-09 06:26:27,889 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:26:27,890 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:26:29,979 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 180 treesize of output 132
[2024-03-09 06:26:29,996 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 60 treesize of output 52
[2024-03-09 06:26:30,010 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 52 treesize of output 48
[2024-03-09 06:26:30,022 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 56 treesize of output 52
[2024-03-09 06:26:30,032 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 48 treesize of output 46
[2024-03-09 06:26:30,041 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 26 treesize of output 24
[2024-03-09 06:26:30,261 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:26:30,262 INFO  L378             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 35 treesize of output 40
[2024-03-09 06:26:30,336 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:26:30,337 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [765421533] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:26:30,337 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:26:30,337 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [17, 17, 19] total 50
[2024-03-09 06:26:30,338 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1756684590]
[2024-03-09 06:26:30,338 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:26:30,338 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 51 states
[2024-03-09 06:26:30,339 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:26:30,340 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 51 interpolants.
[2024-03-09 06:26:30,341 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=226, Invalid=2298, Unknown=26, NotChecked=0, Total=2550
[2024-03-09 06:26:35,008 WARN  L539   Checker$ProtectedHtc]: IncrementalHoareTripleChecker took 4.00s for a HTC check with result UNKNOWN. Formula has sorts [Array, Bool, Int], hasArrays=true, hasNonlinArith=false, quantifiers [1]
[2024-03-09 06:26:38,500 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 43 out of 122
[2024-03-09 06:26:38,503 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 498 places, 3003 transitions, 52663 flow. Second operand  has 51 states, 51 states have (on average 45.15686274509804) internal successors, (2303), 51 states have internal predecessors, (2303), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:26:38,503 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:26:38,503 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 43 of 122
[2024-03-09 06:26:38,504 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:26:58,282 WARN  L539   Checker$ProtectedHtc]: IncrementalHoareTripleChecker took 4.01s for a HTC check with result UNKNOWN. Formula has sorts [Array, Bool, Int], hasArrays=true, hasNonlinArith=false, quantifiers [0]
[2024-03-09 06:27:02,427 WARN  L539   Checker$ProtectedHtc]: IncrementalHoareTripleChecker took 4.00s for a HTC check with result UNKNOWN. Formula has sorts [Array, Bool, Int], hasArrays=true, hasNonlinArith=false, quantifiers [0]
[2024-03-09 06:27:07,012 WARN  L539   Checker$ProtectedHtc]: IncrementalHoareTripleChecker took 4.00s for a HTC check with result UNKNOWN. Formula has sorts [Array, Bool, Int], hasArrays=true, hasNonlinArith=false, quantifiers [0]
[2024-03-09 06:27:51,465 WARN  L539   Checker$ProtectedHtc]: IncrementalHoareTripleChecker took 4.00s for a HTC check with result UNKNOWN. Formula has sorts [Array, Bool, Int], hasArrays=true, hasNonlinArith=false, quantifiers [0]
[2024-03-09 06:28:18,967 WARN  L539   Checker$ProtectedHtc]: IncrementalHoareTripleChecker took 4.00s for a HTC check with result UNKNOWN. Formula has sorts [Array, Bool, Int], hasArrays=true, hasNonlinArith=false, quantifiers [0]
[2024-03-09 06:28:25,446 INFO  L124   PetriNetUnfolderBase]: 65070/123648 cut-off events.
[2024-03-09 06:28:25,446 INFO  L125   PetriNetUnfolderBase]: For 2444996/2446014 co-relation queries the response was YES.
[2024-03-09 06:28:28,324 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 903477 conditions, 123648 events. 65070/123648 cut-off events. For 2444996/2446014 co-relation queries the response was YES. Maximal size of possible extension queue 4030. Compared 1303830 event pairs, 6901 based on Foata normal form. 1035/120275 useless extension candidates. Maximal degree in co-relation 902732. Up to 35802 conditions per place. 
[2024-03-09 06:28:28,939 INFO  L140   encePairwiseOnDemand]: 68/122 looper letters, 5103 selfloop transitions, 3518 changer transitions 62/8726 dead transitions.
[2024-03-09 06:28:28,939 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 580 places, 8726 transitions, 168620 flow
[2024-03-09 06:28:28,940 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 83 states. 
[2024-03-09 06:28:28,940 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 83 states.
[2024-03-09 06:28:28,944 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 83 states to 83 states and 4911 transitions.
[2024-03-09 06:28:28,946 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.4849891368753703
[2024-03-09 06:28:28,946 INFO  L72            ComplementDD]: Start complementDD. Operand 83 states and 4911 transitions.
[2024-03-09 06:28:28,946 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 83 states and 4911 transitions.
[2024-03-09 06:28:28,947 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:28:28,947 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 83 states and 4911 transitions.
[2024-03-09 06:28:28,952 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 84 states, 83 states have (on average 59.16867469879518) internal successors, (4911), 83 states have internal predecessors, (4911), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:28:28,959 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 84 states, 84 states have (on average 122.0) internal successors, (10248), 84 states have internal predecessors, (10248), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:28:28,959 INFO  L81            ComplementDD]: Finished complementDD. Result  has 84 states, 84 states have (on average 122.0) internal successors, (10248), 84 states have internal predecessors, (10248), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:28:28,959 INFO  L175             Difference]: Start difference. First operand has 498 places, 3003 transitions, 52663 flow. Second operand 83 states and 4911 transitions.
[2024-03-09 06:28:28,959 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 580 places, 8726 transitions, 168620 flow
[2024-03-09 06:30:06,535 INFO  L88        GeneralOperation]: Finished removeRedundantFlow, result has has 542 places, 8726 transitions, 166200 flow, removed 1028 selfloop flow, removed 38 redundant places.
[2024-03-09 06:30:06,646 INFO  L231             Difference]: Finished difference. Result has 584 places, 5906 transitions, 123352 flow
[2024-03-09 06:30:06,648 INFO  L264   CegarLoopForPetriNet]: {PETRI_ALPHABET=122, PETRI_DIFFERENCE_MINUEND_FLOW=51430, PETRI_DIFFERENCE_MINUEND_PLACES=460, PETRI_DIFFERENCE_MINUEND_TRANSITIONS=3003, PETRI_DIFFERENCE_SUBTRAHEND_LETTERS_WITH_MORE_CHANGERS_THAN_LOOPERS=1186, PETRI_DIFFERENCE_SUBTRAHEND_LOOPER_ONLY_LETTERS=1512, PETRI_DIFFERENCE_SUBTRAHEND_STATES=83, PETRI_FLOW=123352, PETRI_PLACES=584, PETRI_TRANSITIONS=5906}
[2024-03-09 06:30:06,648 INFO  L281   CegarLoopForPetriNet]: 122 programPoint places, 462 predicate places.
[2024-03-09 06:30:06,649 INFO  L495      AbstractCegarLoop]: Abstraction has has 584 places, 5906 transitions, 123352 flow
[2024-03-09 06:30:06,649 INFO  L496      AbstractCegarLoop]: INTERPOLANT automaton has  has 51 states, 51 states have (on average 45.15686274509804) internal successors, (2303), 51 states have internal predecessors, (2303), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:30:06,649 INFO  L200   CegarLoopForPetriNet]: Found error trace
[2024-03-09 06:30:06,649 INFO  L208   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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2024-03-09 06:30:06,657 INFO  L552       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2024-03-09 06:30:06,850 WARN  L477      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable13
[2024-03-09 06:30:06,850 INFO  L420      AbstractCegarLoop]: === Iteration 11 === Targeting ULTIMATE.startErr2ASSERT_VIOLATIONDATA_RACE === [ULTIMATE.startErr1ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr3ASSERT_VIOLATIONDATA_RACE, ULTIMATE.startErr0ASSERT_VIOLATIONDATA_RACE (and 5 more)] ===
[2024-03-09 06:30:06,851 INFO  L160       PredicateUnifier]: Initialized classic predicate unifier
[2024-03-09 06:30:06,851 INFO  L85        PathProgramCache]: Analyzing trace with hash 1391990736, now seen corresponding path program 1 times
[2024-03-09 06:30:06,852 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2024-03-09 06:30:06,852 INFO  L334   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [533817868]
[2024-03-09 06:30:06,852 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:30:06,852 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2024-03-09 06:30:06,871 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:30:07,586 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:30:07,587 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2024-03-09 06:30:07,587 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [533817868]
[2024-03-09 06:30:07,587 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [533817868] provided 0 perfect and 1 imperfect interpolant sequences
[2024-03-09 06:30:07,587 INFO  L334   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [41796403]
[2024-03-09 06:30:07,588 INFO  L95    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2024-03-09 06:30:07,588 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2024-03-09 06:30:07,588 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3
[2024-03-09 06:30:07,590 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2024-03-09 06:30:07,592 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi24/UAutomizer-linux/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2024-03-09 06:30:07,730 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2024-03-09 06:30:07,732 INFO  L262         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 38 conjunts are in the unsatisfiable core
[2024-03-09 06:30:07,735 INFO  L285         TraceCheckSpWp]: Computing forward predicates...
[2024-03-09 06:30:07,744 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 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 6 treesize of output 5
[2024-03-09 06:30:07,773 INFO  L349             Elim1Store]: treesize reduction 18, result has 35.7 percent of original size
[2024-03-09 06:30:07,773 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 2 case distinctions, treesize of input 17 treesize of output 21
[2024-03-09 06:30:07,915 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:30:07,927 INFO  L349             Elim1Store]: treesize reduction 4, result has 66.7 percent of original size
[2024-03-09 06:30:07,928 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 3 select indices, 3 select index equivalence classes, 2 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 1 case distinctions, treesize of input 20 treesize of output 18
[2024-03-09 06:30:08,153 INFO  L349             Elim1Store]: treesize reduction 19, result has 20.8 percent of original size
[2024-03-09 06:30:08,153 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 33 treesize of output 32
[2024-03-09 06:30:08,336 INFO  L190   IndexEqualityManager]: detected not equals via solver
[2024-03-09 06:30:08,337 INFO  L378             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 25 treesize of output 18
[2024-03-09 06:30:08,433 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 12
[2024-03-09 06:30:08,474 INFO  L378             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 15 treesize of output 11
[2024-03-09 06:30:08,484 INFO  L378             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 28 treesize of output 27
[2024-03-09 06:30:08,502 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:30:08,502 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 2 select indices, 2 select index equivalence classes, 1 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 40 treesize of output 42
[2024-03-09 06:30:08,520 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:30:08,521 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 1 stores, 3 select indices, 3 select index equivalence classes, 1 disjoint index pairs (out of 3 index pairs), introduced 3 new quantified variables, introduced 3 case distinctions, treesize of input 52 treesize of output 57
[2024-03-09 06:30:08,544 INFO  L378             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 56 treesize of output 45
[2024-03-09 06:30:08,559 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:30:08,560 INFO  L327         TraceCheckSpWp]: Computing backward predicates...
[2024-03-09 06:30:08,938 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (* |c_ULTIMATE.start_main_~i~1#1| 4))) (let ((.cse3 (+ 2 |c_ULTIMATE.start_main_#t~mem13#1.offset| .cse1)) (.cse2 (+ 3 |c_ULTIMATE.start_main_#t~mem13#1.offset| .cse1))) (let ((.cse0 (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| (store (store (select |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse3 0) .cse2 0)))) (and (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) (+ |c_ULTIMATE.start_main_#t~mem13#1.offset| 1 .cse1)) 0)) (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse2) 0)) (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) (+ |c_ULTIMATE.start_main_#t~mem13#1.offset| .cse1)) 0)) (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse3) 0)))))) is different from false
[2024-03-09 06:30:08,966 WARN  L854   $PredicateComparison]: unable to prove that (let ((.cse1 (* |c_ULTIMATE.start_main_~i~1#1| 4))) (let ((.cse4 (+ |c_ULTIMATE.start_main_#t~mem13#1.offset| 1 .cse1)) (.cse3 (+ 2 |c_ULTIMATE.start_main_#t~mem13#1.offset| .cse1)) (.cse2 (+ 3 |c_ULTIMATE.start_main_#t~mem13#1.offset| .cse1))) (let ((.cse0 (store |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base| (store (store (store (select |c_#race| |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse4 0) .cse3 0) .cse2 0)))) (and (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) (+ |c_ULTIMATE.start_main_#t~mem13#1.offset| .cse1)) 0)) (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse2) 0)) (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse3) 0)) (forall ((v_ArrVal_861 (Array Int Int))) (= (select (select (store .cse0 c_threadThread1of2ForFork0_~t~0.base v_ArrVal_861) |c_ULTIMATE.start_main_#t~mem13#1.base|) .cse4) 0)))))) is different from false
[2024-03-09 06:30:08,991 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:30:08,991 INFO  L378             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 1 new quantified variables, introduced 4 case distinctions, treesize of input 50 treesize of output 66
[2024-03-09 06:30:08,998 INFO  L349             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2024-03-09 06:30:08,999 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 4 select indices, 4 select index equivalence classes, 0 disjoint index pairs (out of 6 index pairs), introduced 4 new quantified variables, introduced 6 case distinctions, treesize of input 81 treesize of output 38
[2024-03-09 06:30:09,013 INFO  L349             Elim1Store]: treesize reduction 51, result has 1.9 percent of original size
[2024-03-09 06:30:09,013 INFO  L378             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 1 new quantified variables, introduced 4 case distinctions, treesize of input 51 treesize of output 1
[2024-03-09 06:30:09,021 INFO  L349             Elim1Store]: treesize reduction 51, result has 1.9 percent of original size
[2024-03-09 06:30:09,021 INFO  L378             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 1 new quantified variables, introduced 4 case distinctions, treesize of input 51 treesize of output 1
[2024-03-09 06:30:09,030 INFO  L349             Elim1Store]: treesize reduction 51, result has 1.9 percent of original size
[2024-03-09 06:30:09,030 INFO  L378             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 1 new quantified variables, introduced 4 case distinctions, treesize of input 51 treesize of output 1
[2024-03-09 06:30:09,146 WARN  L854   $PredicateComparison]: unable to prove that (forall ((v_ArrVal_856 (Array Int Int))) (not (= c_threadThread1of2ForFork0_~arg.base (select (select (store |c_#memory_$Pointer$.base| c_threadThread1of2ForFork0_~arg.base v_ArrVal_856) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|)))) is different from false
[2024-03-09 06:30:13,507 WARN  L854   $PredicateComparison]: unable to prove that (forall ((v_ArrVal_856 (Array Int Int)) (v_ArrVal_855 (Array Int Int))) (not (= |c_ULTIMATE.start_main_#t~malloc8#1.base| (select (select (store (store |c_#memory_$Pointer$.base| (select (select |c_#memory_$Pointer$.base| |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|) v_ArrVal_855) |c_ULTIMATE.start_main_#t~malloc8#1.base| v_ArrVal_856) |c_ULTIMATE.start_main_~#tids~0#1.base|) |c_ULTIMATE.start_main_~#tids~0#1.offset|)))) is different from false
[2024-03-09 06:30:13,632 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 2, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 73 treesize of output 57
[2024-03-09 06:30:13,640 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 52 treesize of output 48
[2024-03-09 06:30:13,646 INFO  L378             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 48 treesize of output 46
[2024-03-09 06:30:13,884 INFO  L134       CoverageAnalysis]: Checked inductivity of 1 backedges. 0 proven. 1 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2024-03-09 06:30:13,885 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [41796403] provided 0 perfect and 2 imperfect interpolant sequences
[2024-03-09 06:30:13,885 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2024-03-09 06:30:13,885 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 16, 18] total 40
[2024-03-09 06:30:13,886 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [83361119]
[2024-03-09 06:30:13,886 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2024-03-09 06:30:13,887 INFO  L571      AbstractCegarLoop]: INTERPOLANT automaton has 41 states
[2024-03-09 06:30:13,888 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2024-03-09 06:30:13,888 INFO  L143   InterpolantAutomaton]: Constructing interpolant automaton starting with 41 interpolants.
[2024-03-09 06:30:13,889 INFO  L145   InterpolantAutomaton]: CoverageRelationStatistics Valid=137, Invalid=1144, Unknown=67, NotChecked=292, Total=1640
[2024-03-09 06:30:14,138 INFO  L471   CegarLoopForPetriNet]: Number of universal loopers: 45 out of 122
[2024-03-09 06:30:14,140 INFO  L103   encePairwiseOnDemand]: Start differencePairwiseOnDemand. First operand has 584 places, 5906 transitions, 123352 flow. Second operand  has 41 states, 41 states have (on average 47.02439024390244) internal successors, (1928), 41 states have internal predecessors, (1928), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:30:14,140 INFO  L112   encePairwiseOnDemand]: Universal subtrahend loopers provided by user.
[2024-03-09 06:30:14,140 INFO  L113   encePairwiseOnDemand]: Number of universal subtrahend loopers: 45 of 122
[2024-03-09 06:30:14,140 INFO  L73            FinitePrefix]: Start finitePrefix. Operand will be constructed on-demand
[2024-03-09 06:32:12,996 INFO  L124   PetriNetUnfolderBase]: 62590/121092 cut-off events.
[2024-03-09 06:32:12,996 INFO  L125   PetriNetUnfolderBase]: For 3675526/3677230 co-relation queries the response was YES.
[2024-03-09 06:32:16,678 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 1035548 conditions, 121092 events. 62590/121092 cut-off events. For 3675526/3677230 co-relation queries the response was YES. Maximal size of possible extension queue 4032. Compared 1302118 event pairs, 7188 based on Foata normal form. 1068/117577 useless extension candidates. Maximal degree in co-relation 1033920. Up to 36262 conditions per place. 
[2024-03-09 06:32:17,355 INFO  L140   encePairwiseOnDemand]: 88/122 looper letters, 5257 selfloop transitions, 2919 changer transitions 28/8624 dead transitions.
[2024-03-09 06:32:17,355 INFO  L145   encePairwiseOnDemand]: Finished differencePairwiseOnDemand. Result has 627 places, 8624 transitions, 197679 flow
[2024-03-09 06:32:17,357 INFO  L141   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 45 states. 
[2024-03-09 06:32:17,357 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand 45 states.
[2024-03-09 06:32:17,358 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 2652 transitions.
[2024-03-09 06:32:17,359 INFO  L516   CegarLoopForPetriNet]: DFA transition density 0.4830601092896175
[2024-03-09 06:32:17,360 INFO  L72            ComplementDD]: Start complementDD. Operand 45 states and 2652 transitions.
[2024-03-09 06:32:17,360 INFO  L73         IsDeterministic]: Start isDeterministic. Operand 45 states and 2652 transitions.
[2024-03-09 06:32:17,360 INFO  L80         IsDeterministic]: Finished isDeterministic. Operand is deterministic.
[2024-03-09 06:32:17,360 INFO  L117    ReachableStatesCopy]: Start reachableStatesCopy. Operand 45 states and 2652 transitions.
[2024-03-09 06:32:17,363 INFO  L343    DoubleDeckerVisitor]: Before removal of dead ends  has 46 states, 45 states have (on average 58.93333333333333) internal successors, (2652), 45 states have internal predecessors, (2652), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:32:17,367 INFO  L131    ReachableStatesCopy]: Finished reachableStatesCopy Result  has 46 states, 46 states have (on average 122.0) internal successors, (5612), 46 states have internal predecessors, (5612), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:32:17,367 INFO  L81            ComplementDD]: Finished complementDD. Result  has 46 states, 46 states have (on average 122.0) internal successors, (5612), 46 states have internal predecessors, (5612), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2024-03-09 06:32:17,367 INFO  L175             Difference]: Start difference. First operand has 584 places, 5906 transitions, 123352 flow. Second operand 45 states and 2652 transitions.
[2024-03-09 06:32:17,367 INFO  L82        GeneralOperation]: Start removeRedundantFlow. Operand has 627 places, 8624 transitions, 197679 flow
Killed by 15
