./Ultimate.py --spec /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp --file /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c --full-output --architecture 64bit


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


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

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 64bit --witnessprinter.graph.data.programhash 763c6e5a3782c55a2e41fc4f81c1466e8bf5aee1c5345c80fb3017b494ccd6c9
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2023-11-13 05:24:27,008 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2023-11-13 05:24:27,010 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2023-11-13 05:24:27,032 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2023-11-13 05:24:27,032 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2023-11-13 05:24:27,033 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2023-11-13 05:24:27,034 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2023-11-13 05:24:27,035 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2023-11-13 05:24:27,036 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2023-11-13 05:24:27,037 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2023-11-13 05:24:27,037 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2023-11-13 05:24:27,038 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2023-11-13 05:24:27,039 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2023-11-13 05:24:27,039 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2023-11-13 05:24:27,040 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2023-11-13 05:24:27,041 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2023-11-13 05:24:27,041 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2023-11-13 05:24:27,042 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2023-11-13 05:24:27,043 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2023-11-13 05:24:27,044 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2023-11-13 05:24:27,045 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2023-11-13 05:24:27,047 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2023-11-13 05:24:27,047 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2023-11-13 05:24:27,048 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2023-11-13 05:24:27,050 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2023-11-13 05:24:27,051 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2023-11-13 05:24:27,051 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2023-11-13 05:24:27,051 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2023-11-13 05:24:27,052 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2023-11-13 05:24:27,052 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2023-11-13 05:24:27,053 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2023-11-13 05:24:27,053 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2023-11-13 05:24:27,054 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2023-11-13 05:24:27,054 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2023-11-13 05:24:27,055 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2023-11-13 05:24:27,055 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2023-11-13 05:24:27,055 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2023-11-13 05:24:27,056 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2023-11-13 05:24:27,056 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2023-11-13 05:24:27,056 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2023-11-13 05:24:27,057 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2023-11-13 05:24:27,058 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-64bit-Automizer_Default.epf
[2023-11-13 05:24:27,073 INFO  L113        SettingsManager]: Loading preferences was successful
[2023-11-13 05:24:27,073 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2023-11-13 05:24:27,073 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2023-11-13 05:24:27,073 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2023-11-13 05:24:27,074 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2023-11-13 05:24:27,074 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2023-11-13 05:24:27,074 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2023-11-13 05:24:27,074 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2023-11-13 05:24:27,074 INFO  L138        SettingsManager]:  * Use SBE=true
[2023-11-13 05:24:27,075 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Overapproximate operations on floating types=true
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2023-11-13 05:24:27,075 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2023-11-13 05:24:27,076 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-11-13 05:24:27,076 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2023-11-13 05:24:27,076 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Trace refinement strategy=CAMEL
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2023-11-13 05:24:27,077 INFO  L138        SettingsManager]:  * Looper check in Petri net analysis=SEMANTIC
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1 (file:/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/com.sun.xml.bind_2.2.0.v201505121915.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int)
WARNING: Please consider reporting this to the maintainers of com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
Applying setting for plugin de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: Entry function -> main
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness directory -> /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness filename -> witness.graphml
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Write witness besides input file -> false
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data specification -> CHECK( init(main()), LTL(G ! data-race) )


Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data producer -> Automizer
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data architecture -> 64bit
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data programhash -> 763c6e5a3782c55a2e41fc4f81c1466e8bf5aee1c5345c80fb3017b494ccd6c9
[2023-11-13 05:24:27,293 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2023-11-13 05:24:27,317 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2023-11-13 05:24:27,319 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2023-11-13 05:24:27,319 INFO  L271        PluginConnector]: Initializing CDTParser...
[2023-11-13 05:24:27,320 INFO  L275        PluginConnector]: CDTParser initialized
[2023-11-13 05:24:27,322 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c
[2023-11-13 05:24:28,299 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2023-11-13 05:24:28,557 INFO  L351              CDTParser]: Found 1 translation units.
[2023-11-13 05:24:28,558 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c
[2023-11-13 05:24:28,572 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/a2388430d/bb66c29798a14fc6882f7d007ba34a01/FLAG6d1110bd9
[2023-11-13 05:24:28,867 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/a2388430d/bb66c29798a14fc6882f7d007ba34a01
[2023-11-13 05:24:28,870 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2023-11-13 05:24:28,871 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2023-11-13 05:24:28,872 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2023-11-13 05:24:28,872 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2023-11-13 05:24:28,876 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2023-11-13 05:24:28,876 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 13.11 05:24:28" (1/1) ...
[2023-11-13 05:24:28,877 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@7036fa3f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:28, skipping insertion in model container
[2023-11-13 05:24:28,877 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 13.11 05:24:28" (1/1) ...
[2023-11-13 05:24:28,882 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2023-11-13 05:24:28,931 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2023-11-13 05:24:29,136 WARN  L623        FunctionHandler]: Unknown extern function vfprintf
[2023-11-13 05:24:29,147 WARN  L623        FunctionHandler]: Unknown extern function getc
[2023-11-13 05:24:29,154 WARN  L623        FunctionHandler]: Unknown extern function __uflow
[2023-11-13 05:24:29,165 WARN  L623        FunctionHandler]: Unknown extern function __uflow
[2023-11-13 05:24:29,169 WARN  L623        FunctionHandler]: Unknown extern function putc
[2023-11-13 05:24:29,173 WARN  L623        FunctionHandler]: Unknown extern function __overflow
[2023-11-13 05:24:29,179 WARN  L623        FunctionHandler]: Unknown extern function __overflow
[2023-11-13 05:24:29,183 WARN  L623        FunctionHandler]: Unknown extern function __getdelim
[2023-11-13 05:24:29,196 WARN  L623        FunctionHandler]: Unknown extern function strtol
[2023-11-13 05:24:29,197 WARN  L623        FunctionHandler]: Unknown extern function strtol
[2023-11-13 05:24:29,198 WARN  L623        FunctionHandler]: Unknown extern function strtoll
[2023-11-13 05:24:29,212 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:29,214 WARN  L623        FunctionHandler]: Unknown extern function __ctype_toupper_loc
[2023-11-13 05:24:29,230 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:29,237 WARN  L623        FunctionHandler]: Unknown extern function isatty
[2023-11-13 05:24:29,239 WARN  L623        FunctionHandler]: Unknown extern function isatty
[2023-11-13 05:24:29,255 WARN  L623        FunctionHandler]: Unknown extern function toupper
[2023-11-13 05:24:29,255 WARN  L623        FunctionHandler]: Unknown extern function __ctype_toupper_loc
[2023-11-13 05:24:29,257 WARN  L623        FunctionHandler]: Unknown extern function strpbrk
[2023-11-13 05:24:29,266 WARN  L623        FunctionHandler]: Unknown extern function tolower
[2023-11-13 05:24:29,267 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:29,269 WARN  L623        FunctionHandler]: Unknown extern function tolower
[2023-11-13 05:24:29,270 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:29,275 FATAL L?                        ?]: The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator has thrown an exception:
java.lang.UnsupportedOperationException: createNanOrInfinity is unsupported in non-bitprecise translation
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.IntegerTranslation.createNanOrInfinity(IntegerTranslation.java:795)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.standardfunctions.StandardFunctionHandler.handleNaNOrInfinity(StandardFunctionHandler.java:2055)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.standardfunctions.StandardFunctionHandler.lambda$63(StandardFunctionHandler.java:430)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.standardfunctions.StandardFunctionHandler.translateStandardFunction(StandardFunctionHandler.java:242)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:1470)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:267)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:728)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:282)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:1420)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:220)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:1094)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:232)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:1094)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:232)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.FunctionHandler.handleFunctionDefinition(FunctionHandler.java:371)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:1496)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:155)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.processTUchild(CHandler.java:3320)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:2395)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.visit(CHandler.java:600)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.PRDispatcher.dispatch(PRDispatcher.java:134)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.MainTranslator.translate(MainTranslator.java:192)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.MainTranslator.run(MainTranslator.java:115)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.MainTranslator.<init>(MainTranslator.java:93)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.CACSL2BoogieTranslatorObserver.finish(CACSL2BoogieTranslatorObserver.java:128)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:168)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:151)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:128)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:232)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:226)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:142)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:104)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:320)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
[2023-11-13 05:24:29,280 INFO  L158              Benchmark]: Toolchain (without parser) took 407.39ms. Allocated memory is still 184.5MB. Free memory was 151.5MB in the beginning and 144.5MB in the end (delta: 7.0MB). Peak memory consumption was 12.6MB. Max. memory is 16.1GB.
[2023-11-13 05:24:29,281 INFO  L158              Benchmark]: CDTParser took 0.24ms. Allocated memory is still 184.5MB. Free memory is still 156.0MB. There was no memory consumed. Max. memory is 16.1GB.
[2023-11-13 05:24:29,282 INFO  L158              Benchmark]: CACSL2BoogieTranslator took 405.90ms. Allocated memory is still 184.5MB. Free memory was 151.5MB in the beginning and 144.5MB in the end (delta: 7.0MB). Peak memory consumption was 12.6MB. Max. memory is 16.1GB.
[2023-11-13 05:24:29,284 INFO  L339   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.24ms. Allocated memory is still 184.5MB. Free memory is still 156.0MB. There was no memory consumed. Max. memory is 16.1GB.
 * CACSL2BoogieTranslator took 405.90ms. Allocated memory is still 184.5MB. Free memory was 151.5MB in the beginning and 144.5MB in the end (delta: 7.0MB). Peak memory consumption was 12.6MB. Max. memory is 16.1GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator:
  - ExceptionOrErrorResult: UnsupportedOperationException: createNanOrInfinity is unsupported in non-bitprecise translation
    de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: UnsupportedOperationException: createNanOrInfinity is unsupported in non-bitprecise translation: de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.IntegerTranslation.createNanOrInfinity(IntegerTranslation.java:795)
RESULT: Ultimate could not prove your program: Toolchain returned no result.
Received shutdown request...
--- End real Ultimate output ---

Execution finished normally
Using bit-precise analysis
Retrying with bit-precise analysis

### Bit-precise run ###
Calling Ultimate with: /usr/lib/jvm/java-11-openjdk-amd64/bin/java -Dosgi.configuration.area=/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data -tc /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/AutomizerReach.xml -i /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c -s /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-64bit-Automizer_Bitvector.epf --cacsl2boogietranslator.entry.function main --witnessprinter.witness.directory /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux --witnessprinter.witness.filename witness.graphml --witnessprinter.write.witness.besides.input.file false --witnessprinter.graph.data.specification CHECK( init(main()), LTL(G ! data-race) )

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 64bit --witnessprinter.graph.data.programhash 763c6e5a3782c55a2e41fc4f81c1466e8bf5aee1c5345c80fb3017b494ccd6c9
--- Real Ultimate output ---
This is Ultimate 0.2.2-dev-2329fc7
[2023-11-13 05:24:30,734 INFO  L177        SettingsManager]: Resetting all preferences to default values...
[2023-11-13 05:24:30,735 INFO  L181        SettingsManager]: Resetting UltimateCore preferences to default values
[2023-11-13 05:24:30,772 INFO  L184        SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2023-11-13 05:24:30,772 INFO  L181        SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2023-11-13 05:24:30,773 INFO  L181        SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2023-11-13 05:24:30,775 INFO  L181        SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2023-11-13 05:24:30,776 INFO  L181        SettingsManager]: Resetting LassoRanker preferences to default values
[2023-11-13 05:24:30,778 INFO  L181        SettingsManager]: Resetting Reaching Definitions preferences to default values
[2023-11-13 05:24:30,779 INFO  L181        SettingsManager]: Resetting SyntaxChecker preferences to default values
[2023-11-13 05:24:30,780 INFO  L181        SettingsManager]: Resetting Sifa preferences to default values
[2023-11-13 05:24:30,781 INFO  L184        SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2023-11-13 05:24:30,781 INFO  L181        SettingsManager]: Resetting LTL2Aut preferences to default values
[2023-11-13 05:24:30,782 INFO  L181        SettingsManager]: Resetting PEA to Boogie preferences to default values
[2023-11-13 05:24:30,783 INFO  L181        SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2023-11-13 05:24:30,784 INFO  L181        SettingsManager]: Resetting ChcToBoogie preferences to default values
[2023-11-13 05:24:30,785 INFO  L181        SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2023-11-13 05:24:30,786 INFO  L181        SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2023-11-13 05:24:30,788 INFO  L181        SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2023-11-13 05:24:30,789 INFO  L181        SettingsManager]: Resetting CodeCheck preferences to default values
[2023-11-13 05:24:30,791 INFO  L181        SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2023-11-13 05:24:30,792 INFO  L181        SettingsManager]: Resetting RCFGBuilder preferences to default values
[2023-11-13 05:24:30,793 INFO  L181        SettingsManager]: Resetting Referee preferences to default values
[2023-11-13 05:24:30,794 INFO  L181        SettingsManager]: Resetting TraceAbstraction preferences to default values
[2023-11-13 05:24:30,797 INFO  L184        SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2023-11-13 05:24:30,798 INFO  L184        SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2023-11-13 05:24:30,798 INFO  L181        SettingsManager]: Resetting TreeAutomizer preferences to default values
[2023-11-13 05:24:30,799 INFO  L181        SettingsManager]: Resetting IcfgToChc preferences to default values
[2023-11-13 05:24:30,799 INFO  L181        SettingsManager]: Resetting IcfgTransformer preferences to default values
[2023-11-13 05:24:30,800 INFO  L184        SettingsManager]: ReqToTest provides no preferences, ignoring...
[2023-11-13 05:24:30,800 INFO  L181        SettingsManager]: Resetting Boogie Printer preferences to default values
[2023-11-13 05:24:30,801 INFO  L181        SettingsManager]: Resetting ChcSmtPrinter preferences to default values
[2023-11-13 05:24:30,802 INFO  L181        SettingsManager]: Resetting ReqPrinter preferences to default values
[2023-11-13 05:24:30,803 INFO  L181        SettingsManager]: Resetting Witness Printer preferences to default values
[2023-11-13 05:24:30,803 INFO  L184        SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2023-11-13 05:24:30,804 INFO  L181        SettingsManager]: Resetting CDTParser preferences to default values
[2023-11-13 05:24:30,804 INFO  L184        SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2023-11-13 05:24:30,804 INFO  L184        SettingsManager]: ReqParser provides no preferences, ignoring...
[2023-11-13 05:24:30,805 INFO  L181        SettingsManager]: Resetting SmtParser preferences to default values
[2023-11-13 05:24:30,805 INFO  L181        SettingsManager]: Resetting Witness Parser preferences to default values
[2023-11-13 05:24:30,806 INFO  L188        SettingsManager]: Finished resetting all preferences to default values...
[2023-11-13 05:24:30,807 INFO  L101        SettingsManager]: Beginning loading settings from /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/config/svcomp-DataRace-64bit-Automizer_Bitvector.epf
[2023-11-13 05:24:30,830 INFO  L113        SettingsManager]: Loading preferences was successful
[2023-11-13 05:24:30,830 INFO  L115        SettingsManager]: Preferences different from defaults after loading the file:
[2023-11-13 05:24:30,830 INFO  L136        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2023-11-13 05:24:30,830 INFO  L138        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2023-11-13 05:24:30,831 INFO  L136        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2023-11-13 05:24:30,831 INFO  L138        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2023-11-13 05:24:30,832 INFO  L136        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2023-11-13 05:24:30,832 INFO  L138        SettingsManager]:  * Create parallel compositions if possible=false
[2023-11-13 05:24:30,832 INFO  L138        SettingsManager]:  * Use SBE=true
[2023-11-13 05:24:30,832 INFO  L136        SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2023-11-13 05:24:30,832 INFO  L138        SettingsManager]:  * Check unreachability of error function in SV-COMP mode=false
[2023-11-13 05:24:30,832 INFO  L138        SettingsManager]:  * Check division by zero=IGNORE
[2023-11-13 05:24:30,833 INFO  L138        SettingsManager]:  * Pointer to allocated memory at dereference=IGNORE
[2023-11-13 05:24:30,833 INFO  L138        SettingsManager]:  * If two pointers are subtracted or compared they have the same base address=IGNORE
[2023-11-13 05:24:30,833 INFO  L138        SettingsManager]:  * Check array bounds for arrays that are off heap=IGNORE
[2023-11-13 05:24:30,833 INFO  L138        SettingsManager]:  * Check absence of data races in concurrent programs=true
[2023-11-13 05:24:30,833 INFO  L138        SettingsManager]:  * Use bitvectors instead of ints=true
[2023-11-13 05:24:30,833 INFO  L138        SettingsManager]:  * Memory model=HoenickeLindenmann_4ByteResolution
[2023-11-13 05:24:30,834 INFO  L138        SettingsManager]:  * Check if freed pointer was valid=false
[2023-11-13 05:24:30,834 INFO  L138        SettingsManager]:  * Use constant arrays=true
[2023-11-13 05:24:30,834 INFO  L138        SettingsManager]:  * Pointer base address is valid at dereference=IGNORE
[2023-11-13 05:24:30,834 INFO  L136        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2023-11-13 05:24:30,834 INFO  L138        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2023-11-13 05:24:30,834 INFO  L138        SettingsManager]:  * SMT solver=External_DefaultMode
[2023-11-13 05:24:30,834 INFO  L138        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-11-13 05:24:30,835 INFO  L136        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2023-11-13 05:24:30,835 INFO  L138        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2023-11-13 05:24:30,835 INFO  L138        SettingsManager]:  * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2023-11-13 05:24:30,835 INFO  L138        SettingsManager]:  * Trace refinement strategy=WOLF
[2023-11-13 05:24:30,835 INFO  L138        SettingsManager]:  * Command for external solver=cvc4 --incremental --print-success --lang smt 
[2023-11-13 05:24:30,835 INFO  L138        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2023-11-13 05:24:30,835 INFO  L138        SettingsManager]:  * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2023-11-13 05:24:30,836 INFO  L138        SettingsManager]:  * Order on configurations for Petri net unfoldings=DBO
[2023-11-13 05:24:30,836 INFO  L138        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2023-11-13 05:24:30,836 INFO  L138        SettingsManager]:  * Logic for external solver=AUFBV
[2023-11-13 05:24:30,836 INFO  L138        SettingsManager]:  * Independence relation used for large block encoding in concurrent analysis=SYNTACTIC
[2023-11-13 05:24:30,836 INFO  L138        SettingsManager]:  * Looper check in Petri net analysis=SEMANTIC
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1 (file:/mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/plugins/com.sun.xml.bind_2.2.0.v201505121915.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int)
WARNING: Please consider reporting this to the maintainers of com.sun.xml.bind.v2.runtime.reflect.opt.Injector$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
Applying setting for plugin de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: Entry function -> main
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness directory -> /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Witness filename -> witness.graphml
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Write witness besides input file -> false
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data specification -> CHECK( init(main()), LTL(G ! data-race) )


Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data producer -> Automizer
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data architecture -> 64bit
Applying setting for plugin de.uni_freiburg.informatik.ultimate.witnessprinter: Graph data programhash -> 763c6e5a3782c55a2e41fc4f81c1466e8bf5aee1c5345c80fb3017b494ccd6c9
[2023-11-13 05:24:31,078 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2023-11-13 05:24:31,096 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2023-11-13 05:24:31,098 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2023-11-13 05:24:31,098 INFO  L271        PluginConnector]: Initializing CDTParser...
[2023-11-13 05:24:31,099 INFO  L275        PluginConnector]: CDTParser initialized
[2023-11-13 05:24:31,100 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c
[2023-11-13 05:24:32,122 INFO  L500              CDTParser]: Created temporary CDT project at NULL
[2023-11-13 05:24:32,426 INFO  L351              CDTParser]: Found 1 translation units.
[2023-11-13 05:24:32,427 INFO  L172              CDTParser]: Scanning /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c
[2023-11-13 05:24:32,440 INFO  L394              CDTParser]: About to delete temporary CDT project at /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/7c9c7d7d4/99f1d804291643aea5183c1cd791bce5/FLAG609edd781
[2023-11-13 05:24:32,678 INFO  L402              CDTParser]: Successfully deleted /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/data/7c9c7d7d4/99f1d804291643aea5183c1cd791bce5
[2023-11-13 05:24:32,680 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2023-11-13 05:24:32,681 INFO  L131        ToolchainWalker]: Walking toolchain with 6 elements.
[2023-11-13 05:24:32,681 INFO  L113        PluginConnector]: ------------------------CACSL2BoogieTranslator----------------------------
[2023-11-13 05:24:32,682 INFO  L271        PluginConnector]: Initializing CACSL2BoogieTranslator...
[2023-11-13 05:24:32,685 INFO  L275        PluginConnector]: CACSL2BoogieTranslator initialized
[2023-11-13 05:24:32,685 INFO  L185        PluginConnector]: Executing the observer ACSLObjectContainerObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 13.11 05:24:32" (1/1) ...
[2023-11-13 05:24:32,686 INFO  L205        PluginConnector]: Invalid model from CACSL2BoogieTranslator for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.ACSLObjectContainerObserver@68d693cd and model type de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:32, skipping insertion in model container
[2023-11-13 05:24:32,686 INFO  L185        PluginConnector]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 13.11 05:24:32" (1/1) ...
[2023-11-13 05:24:32,691 INFO  L145         MainTranslator]: Starting translation in SV-COMP mode 
[2023-11-13 05:24:32,738 INFO  L178         MainTranslator]: Built tables and reachable declarations
[2023-11-13 05:24:32,898 WARN  L623        FunctionHandler]: Unknown extern function vfprintf
[2023-11-13 05:24:32,908 WARN  L623        FunctionHandler]: Unknown extern function getc
[2023-11-13 05:24:32,918 WARN  L623        FunctionHandler]: Unknown extern function __uflow
[2023-11-13 05:24:32,931 WARN  L623        FunctionHandler]: Unknown extern function __uflow
[2023-11-13 05:24:32,938 WARN  L623        FunctionHandler]: Unknown extern function putc
[2023-11-13 05:24:32,942 WARN  L623        FunctionHandler]: Unknown extern function __overflow
[2023-11-13 05:24:32,950 WARN  L623        FunctionHandler]: Unknown extern function __overflow
[2023-11-13 05:24:32,955 WARN  L623        FunctionHandler]: Unknown extern function __getdelim
[2023-11-13 05:24:32,964 WARN  L623        FunctionHandler]: Unknown extern function strtol
[2023-11-13 05:24:32,966 WARN  L623        FunctionHandler]: Unknown extern function strtol
[2023-11-13 05:24:32,967 WARN  L623        FunctionHandler]: Unknown extern function strtoll
[2023-11-13 05:24:32,980 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:32,983 WARN  L623        FunctionHandler]: Unknown extern function __ctype_toupper_loc
[2023-11-13 05:24:32,996 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,003 WARN  L623        FunctionHandler]: Unknown extern function isatty
[2023-11-13 05:24:33,004 WARN  L623        FunctionHandler]: Unknown extern function isatty
[2023-11-13 05:24:33,024 WARN  L623        FunctionHandler]: Unknown extern function toupper
[2023-11-13 05:24:33,024 WARN  L623        FunctionHandler]: Unknown extern function __ctype_toupper_loc
[2023-11-13 05:24:33,027 WARN  L623        FunctionHandler]: Unknown extern function strpbrk
[2023-11-13 05:24:33,037 WARN  L623        FunctionHandler]: Unknown extern function tolower
[2023-11-13 05:24:33,038 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:33,040 WARN  L623        FunctionHandler]: Unknown extern function tolower
[2023-11-13 05:24:33,041 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:33,122 WARN  L623        FunctionHandler]: Unknown extern function tcsetattr
[2023-11-13 05:24:33,124 WARN  L623        FunctionHandler]: Unknown extern function fclose
[2023-11-13 05:24:33,124 WARN  L623        FunctionHandler]: Unknown extern function close
[2023-11-13 05:24:33,126 WARN  L623        FunctionHandler]: Unknown extern function open
[2023-11-13 05:24:33,127 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,127 WARN  L623        FunctionHandler]: Unknown extern function fopen
[2023-11-13 05:24:33,129 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,129 WARN  L623        FunctionHandler]: Unknown extern function setvbuf
[2023-11-13 05:24:33,130 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,131 WARN  L623        FunctionHandler]: Unknown extern function tcgetattr
[2023-11-13 05:24:33,132 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,136 WARN  L623        FunctionHandler]: Unknown extern function tcsetattr
[2023-11-13 05:24:33,137 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,138 WARN  L623        FunctionHandler]: Unknown extern function signal
[2023-11-13 05:24:33,139 WARN  L623        FunctionHandler]: Unknown extern function fileno
[2023-11-13 05:24:33,139 WARN  L623        FunctionHandler]: Unknown extern function ioctl
[2023-11-13 05:24:33,142 WARN  L623        FunctionHandler]: Unknown extern function read
[2023-11-13 05:24:33,143 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,145 WARN  L623        FunctionHandler]: Unknown extern function sigemptyset
[2023-11-13 05:24:33,145 WARN  L623        FunctionHandler]: Unknown extern function sigaddset
[2023-11-13 05:24:33,146 WARN  L623        FunctionHandler]: Unknown extern function pselect
[2023-11-13 05:24:33,147 WARN  L623        FunctionHandler]: Unknown extern function __errno_location
[2023-11-13 05:24:33,147 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,156 WARN  L623        FunctionHandler]: Unknown extern function vfprintf
[2023-11-13 05:24:33,157 WARN  L623        FunctionHandler]: Unknown extern function fputc
[2023-11-13 05:24:33,158 WARN  L623        FunctionHandler]: Unknown extern function fflush
[2023-11-13 05:24:33,177 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,182 WARN  L623        FunctionHandler]: Unknown extern function fread
[2023-11-13 05:24:33,196 WARN  L623        FunctionHandler]: Unknown extern function sysconf
[2023-11-13 05:24:33,210 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,223 WARN  L623        FunctionHandler]: Unknown extern function __errno_location
[2023-11-13 05:24:33,225 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,229 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,232 WARN  L623        FunctionHandler]: Unknown extern function __errno_location
[2023-11-13 05:24:33,234 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,235 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,244 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,250 WARN  L623        FunctionHandler]: Unknown extern function getopt_long
[2023-11-13 05:24:33,255 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,256 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,257 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,257 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,264 WARN  L623        FunctionHandler]: Unknown extern function __ctype_b_loc
[2023-11-13 05:24:33,280 WARN  L623        FunctionHandler]: Unknown extern function fputs
[2023-11-13 05:24:33,281 WARN  L623        FunctionHandler]: Unknown extern function fputc
[2023-11-13 05:24:33,305 WARN  L623        FunctionHandler]: Unknown extern function __ctype_b_loc
[2023-11-13 05:24:33,306 WARN  L623        FunctionHandler]: Unknown extern function __ctype_b_loc
[2023-11-13 05:24:33,324 WARN  L623        FunctionHandler]: Unknown extern function strncpy
[2023-11-13 05:24:33,330 WARN  L623        FunctionHandler]: Unknown extern function strncpy
[2023-11-13 05:24:33,339 WARN  L623        FunctionHandler]: Unknown extern function strcat
[2023-11-13 05:24:33,340 WARN  L623        FunctionHandler]: Unknown extern function strncmp
[2023-11-13 05:24:33,347 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-11-13 05:24:33,379 INFO  L203         MainTranslator]: Completed pre-run
[2023-11-13 05:24:33,391 WARN  L623        FunctionHandler]: Unknown extern function vfprintf
[2023-11-13 05:24:33,392 WARN  L623        FunctionHandler]: Unknown extern function getc
[2023-11-13 05:24:33,393 WARN  L623        FunctionHandler]: Unknown extern function __uflow
[2023-11-13 05:24:33,395 WARN  L623        FunctionHandler]: Unknown extern function __uflow
[2023-11-13 05:24:33,396 WARN  L623        FunctionHandler]: Unknown extern function putc
[2023-11-13 05:24:33,397 WARN  L623        FunctionHandler]: Unknown extern function __overflow
[2023-11-13 05:24:33,399 WARN  L623        FunctionHandler]: Unknown extern function __overflow
[2023-11-13 05:24:33,400 WARN  L623        FunctionHandler]: Unknown extern function __getdelim
[2023-11-13 05:24:33,401 WARN  L623        FunctionHandler]: Unknown extern function strtol
[2023-11-13 05:24:33,402 WARN  L623        FunctionHandler]: Unknown extern function strtol
[2023-11-13 05:24:33,402 WARN  L623        FunctionHandler]: Unknown extern function strtoll
[2023-11-13 05:24:33,404 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:33,405 WARN  L623        FunctionHandler]: Unknown extern function __ctype_toupper_loc
[2023-11-13 05:24:33,408 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,411 WARN  L623        FunctionHandler]: Unknown extern function isatty
[2023-11-13 05:24:33,411 WARN  L623        FunctionHandler]: Unknown extern function isatty
[2023-11-13 05:24:33,417 WARN  L623        FunctionHandler]: Unknown extern function toupper
[2023-11-13 05:24:33,418 WARN  L623        FunctionHandler]: Unknown extern function __ctype_toupper_loc
[2023-11-13 05:24:33,419 WARN  L623        FunctionHandler]: Unknown extern function strpbrk
[2023-11-13 05:24:33,422 WARN  L623        FunctionHandler]: Unknown extern function tolower
[2023-11-13 05:24:33,423 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:33,424 WARN  L623        FunctionHandler]: Unknown extern function tolower
[2023-11-13 05:24:33,424 WARN  L623        FunctionHandler]: Unknown extern function __ctype_tolower_loc
[2023-11-13 05:24:33,472 WARN  L623        FunctionHandler]: Unknown extern function tcsetattr
[2023-11-13 05:24:33,474 WARN  L623        FunctionHandler]: Unknown extern function fclose
[2023-11-13 05:24:33,475 WARN  L623        FunctionHandler]: Unknown extern function close
[2023-11-13 05:24:33,475 WARN  L623        FunctionHandler]: Unknown extern function open
[2023-11-13 05:24:33,476 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,476 WARN  L623        FunctionHandler]: Unknown extern function fopen
[2023-11-13 05:24:33,477 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,477 WARN  L623        FunctionHandler]: Unknown extern function setvbuf
[2023-11-13 05:24:33,478 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,479 WARN  L623        FunctionHandler]: Unknown extern function tcgetattr
[2023-11-13 05:24:33,479 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,483 WARN  L623        FunctionHandler]: Unknown extern function tcsetattr
[2023-11-13 05:24:33,484 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,484 WARN  L623        FunctionHandler]: Unknown extern function signal
[2023-11-13 05:24:33,485 WARN  L623        FunctionHandler]: Unknown extern function fileno
[2023-11-13 05:24:33,486 WARN  L623        FunctionHandler]: Unknown extern function ioctl
[2023-11-13 05:24:33,487 WARN  L623        FunctionHandler]: Unknown extern function read
[2023-11-13 05:24:33,488 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,490 WARN  L623        FunctionHandler]: Unknown extern function sigemptyset
[2023-11-13 05:24:33,490 WARN  L623        FunctionHandler]: Unknown extern function sigaddset
[2023-11-13 05:24:33,491 WARN  L623        FunctionHandler]: Unknown extern function pselect
[2023-11-13 05:24:33,491 WARN  L623        FunctionHandler]: Unknown extern function __errno_location
[2023-11-13 05:24:33,492 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,497 WARN  L623        FunctionHandler]: Unknown extern function vfprintf
[2023-11-13 05:24:33,498 WARN  L623        FunctionHandler]: Unknown extern function fputc
[2023-11-13 05:24:33,499 WARN  L623        FunctionHandler]: Unknown extern function fflush
[2023-11-13 05:24:33,502 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,504 WARN  L623        FunctionHandler]: Unknown extern function fread
[2023-11-13 05:24:33,513 WARN  L623        FunctionHandler]: Unknown extern function sysconf
[2023-11-13 05:24:33,523 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,535 WARN  L623        FunctionHandler]: Unknown extern function __errno_location
[2023-11-13 05:24:33,537 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,540 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,543 WARN  L623        FunctionHandler]: Unknown extern function __errno_location
[2023-11-13 05:24:33,543 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,544 WARN  L623        FunctionHandler]: Unknown extern function perror
[2023-11-13 05:24:33,550 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,555 WARN  L623        FunctionHandler]: Unknown extern function getopt_long
[2023-11-13 05:24:33,558 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,559 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,560 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,560 WARN  L623        FunctionHandler]: Unknown extern function fprintf
[2023-11-13 05:24:33,563 WARN  L623        FunctionHandler]: Unknown extern function __ctype_b_loc
[2023-11-13 05:24:33,574 WARN  L623        FunctionHandler]: Unknown extern function fputs
[2023-11-13 05:24:33,575 WARN  L623        FunctionHandler]: Unknown extern function fputc
[2023-11-13 05:24:33,581 WARN  L623        FunctionHandler]: Unknown extern function __ctype_b_loc
[2023-11-13 05:24:33,582 WARN  L623        FunctionHandler]: Unknown extern function __ctype_b_loc
[2023-11-13 05:24:33,594 WARN  L623        FunctionHandler]: Unknown extern function strncpy
[2023-11-13 05:24:33,619 WARN  L623        FunctionHandler]: Unknown extern function strncpy
[2023-11-13 05:24:33,624 WARN  L623        FunctionHandler]: Unknown extern function strcat
[2023-11-13 05:24:33,625 WARN  L623        FunctionHandler]: Unknown extern function strncmp
[2023-11-13 05:24:33,631 INFO  L210          PostProcessor]: Analyzing one entry point: main
[2023-11-13 05:24:33,678 INFO  L208         MainTranslator]: Completed translation
[2023-11-13 05:24:33,679 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33 WrapperNode
[2023-11-13 05:24:33,679 INFO  L132        PluginConnector]: ------------------------ END CACSL2BoogieTranslator----------------------------
[2023-11-13 05:24:33,680 INFO  L113        PluginConnector]: ------------------------Boogie Procedure Inliner----------------------------
[2023-11-13 05:24:33,680 INFO  L271        PluginConnector]: Initializing Boogie Procedure Inliner...
[2023-11-13 05:24:33,680 INFO  L275        PluginConnector]: Boogie Procedure Inliner initialized
[2023-11-13 05:24:33,685 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:33,753 INFO  L185        PluginConnector]: Executing the observer Inliner from plugin Boogie Procedure Inliner for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:35,579 INFO  L138                Inliner]: procedures = 198, calls = 1765, calls flagged for inlining = 161, calls inlined = 1797, statements flattened = 70167
[2023-11-13 05:24:35,580 INFO  L132        PluginConnector]: ------------------------ END Boogie Procedure Inliner----------------------------
[2023-11-13 05:24:35,581 INFO  L113        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2023-11-13 05:24:35,581 INFO  L271        PluginConnector]: Initializing Boogie Preprocessor...
[2023-11-13 05:24:35,581 INFO  L275        PluginConnector]: Boogie Preprocessor initialized
[2023-11-13 05:24:35,590 INFO  L185        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:35,631 INFO  L185        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:36,046 INFO  L185        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:36,047 INFO  L185        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:37,282 INFO  L185        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:37,435 INFO  L185        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:37,609 INFO  L185        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:37,712 INFO  L185        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:38,032 INFO  L132        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2023-11-13 05:24:38,033 INFO  L113        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2023-11-13 05:24:38,033 INFO  L271        PluginConnector]: Initializing RCFGBuilder...
[2023-11-13 05:24:38,033 INFO  L275        PluginConnector]: RCFGBuilder initialized
[2023-11-13 05:24:38,034 INFO  L185        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (1/1) ...
[2023-11-13 05:24:38,068 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2023-11-13 05:24:38,079 INFO  L189       MonitoredProcess]: No working directory specified, using /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3
[2023-11-13 05:24:38,096 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2023-11-13 05:24:38,101 INFO  L327       MonitoredProcess]: [MP /mnt/goblint-svcomp/benchexec/tools-pldi/UAutomizer-linux/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2023-11-13 05:24:38,172 INFO  L130     BoogieDeclarations]: Found specification of procedure read~intINTTYPE1
[2023-11-13 05:24:38,172 INFO  L130     BoogieDeclarations]: Found specification of procedure strncmp
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure read~intINTTYPE8
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure read~intINTTYPE4
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure read~unchecked~$Pointer$
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure read~intINTTYPE2
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure write~unchecked~$Pointer$
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure fileno
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure sigemptyset
[2023-11-13 05:24:38,173 INFO  L130     BoogieDeclarations]: Found specification of procedure read~intFLOATTYPE8
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure write~intFLOATTYPE8
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure __ctype_toupper_loc
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure tcgetattr
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure close
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure fopen
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure strpbrk
[2023-11-13 05:24:38,174 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnStack
[2023-11-13 05:24:38,175 INFO  L130     BoogieDeclarations]: Found specification of procedure signal
[2023-11-13 05:24:38,175 INFO  L130     BoogieDeclarations]: Found specification of procedure read~$Pointer$
[2023-11-13 05:24:38,175 INFO  L130     BoogieDeclarations]: Found specification of procedure __ctype_tolower_loc
[2023-11-13 05:24:38,176 INFO  L130     BoogieDeclarations]: Found specification of procedure write~intINTTYPE8
[2023-11-13 05:24:38,178 INFO  L130     BoogieDeclarations]: Found specification of procedure write~intINTTYPE1
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.dealloc
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure write~intINTTYPE4
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~$Pointer$
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~intINTTYPE1
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure write~init~intINTTYPE4
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure strcat
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure fclose
[2023-11-13 05:24:38,179 INFO  L130     BoogieDeclarations]: Found specification of procedure read~unchecked~intFLOATTYPE8
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure write~unchecked~intFLOATTYPE8
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure vfprintf
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure sysconf
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure fread
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure fputc
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure write~unchecked~intINTTYPE4
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure write~unchecked~intINTTYPE2
[2023-11-13 05:24:38,180 INFO  L130     BoogieDeclarations]: Found specification of procedure write~unchecked~intINTTYPE1
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure write~unchecked~intINTTYPE8
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure getopt_long
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure #PthreadsMutexLock
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure tcsetattr
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocOnHeap
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure fputs
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure perror
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure fflush
[2023-11-13 05:24:38,181 INFO  L130     BoogieDeclarations]: Found specification of procedure #Ultimate.allocInit
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure isatty
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure write~$Pointer$
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure read~unchecked~intINTTYPE8
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure read~unchecked~intINTTYPE2
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure read~unchecked~intINTTYPE4
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure __errno_location
[2023-11-13 05:24:38,182 INFO  L130     BoogieDeclarations]: Found specification of procedure choices_search_worker
[2023-11-13 05:24:38,183 INFO  L138     BoogieDeclarations]: Found implementation of procedure choices_search_worker
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure read
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure setvbuf
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure __ctype_b_loc
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure sigaddset
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure pselect
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure read~unchecked~intINTTYPE1
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure strncpy
[2023-11-13 05:24:38,183 INFO  L130     BoogieDeclarations]: Found specification of procedure ULTIMATE.start
[2023-11-13 05:24:38,184 INFO  L138     BoogieDeclarations]: Found implementation of procedure ULTIMATE.start
[2023-11-13 05:24:38,236 WARN  L209             CfgBuilder]: User set CodeBlockSize to SequenceOfStatements but program contains fork statements. Overwriting the user preferences and setting CodeBlockSize to SingleStatement
[2023-11-13 05:24:38,742 INFO  L235             CfgBuilder]: Building ICFG
[2023-11-13 05:24:38,745 INFO  L261             CfgBuilder]: Building CFG for each procedure with an implementation
[2023-11-13 05:32:21,518 INFO  L276             CfgBuilder]: Performing block encoding
[2023-11-13 05:32:21,636 INFO  L295             CfgBuilder]: Using the 1 location(s) as analysis (start of procedure ULTIMATE.start)
[2023-11-13 05:32:21,636 INFO  L300             CfgBuilder]: Removed 473 assume(true) statements.
[2023-11-13 05:32:21,680 INFO  L202        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 13.11 05:32:21 BoogieIcfgContainer
[2023-11-13 05:32:21,680 INFO  L132        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2023-11-13 05:32:21,682 INFO  L113        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2023-11-13 05:32:21,682 INFO  L271        PluginConnector]: Initializing TraceAbstraction...
[2023-11-13 05:32:21,685 INFO  L275        PluginConnector]: TraceAbstraction initialized
[2023-11-13 05:32:21,685 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "CDTParser AST 13.11 05:24:32" (1/3) ...
[2023-11-13 05:32:21,686 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6dd5e6c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 13.11 05:32:21, skipping insertion in model container
[2023-11-13 05:32:21,686 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 13.11 05:24:33" (2/3) ...
[2023-11-13 05:32:21,687 INFO  L205        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6dd5e6c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 13.11 05:32:21, skipping insertion in model container
[2023-11-13 05:32:21,687 INFO  L185        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 13.11 05:32:21" (3/3) ...
[2023-11-13 05:32:21,688 INFO  L112   eAbstractionObserver]: Analyzing ICFG main.c
[2023-11-13 05:32:21,694 WARN  L145   ceAbstractionStarter]: Switching off computation of Hoare annotation because input is a concurrent program
[2023-11-13 05:32:21,703 INFO  L203   ceAbstractionStarter]: Automizer settings: Hoare:false NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2023-11-13 05:32:21,704 INFO  L162   ceAbstractionStarter]: Applying trace abstraction to program that has 4721 error locations.
[2023-11-13 05:32:21,704 INFO  L515   ceAbstractionStarter]: Constructing petrified ICFG for 1 thread instances.
[2023-11-13 05:32:33,969 INFO  L144    ThreadInstanceAdder]: Constructed 1596 joinOtherThreadTransitions.
[2023-11-13 05:32:34,864 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 135433 places, 141213 transitions, 287354 flow
[2023-11-13 05:35:29,865 INFO  L130       PetriNetUnfolder]: 3890/118648 cut-off events.
[2023-11-13 05:35:29,865 INFO  L131       PetriNetUnfolder]: For 28/28 co-relation queries the response was YES.
[2023-11-13 05:35:31,019 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 118789 conditions, 118648 events. 3890/118648 cut-off events. For 28/28 co-relation queries the response was YES. Maximal size of possible extension queue 308. Compared 1401048 event pairs, 0 based on Foata normal form. 0/107292 useless extension candidates. Maximal degree in co-relation 117204. Up to 15 conditions per place. 
[2023-11-13 05:35:31,020 INFO  L82        GeneralOperation]: Start removeDead. Operand has 135433 places, 141213 transitions, 287354 flow
[2023-11-13 05:35:31,989 INFO  L88        GeneralOperation]: Finished RemoveDead, result has has 112504 places, 116309 transitions, 232842 flow
[2023-11-13 05:35:31,992 INFO  L124   etLargeBlockEncoding]: Petri net LBE is using variable-based independence relation.
[2023-11-13 05:35:31,999 INFO  L131   etLargeBlockEncoding]: Starting large block encoding on Petri net that has 112504 places, 116309 transitions, 232842 flow
[2023-11-13 05:35:32,002 INFO  L113        LiptonReduction]: Starting Lipton reduction on Petri net that has 112504 places, 116309 transitions, 232842 flow
[2023-11-13 05:35:32,002 INFO  L73            FinitePrefix]: Start finitePrefix. Operand has 112504 places, 116309 transitions, 232842 flow
[2023-11-13 05:38:11,527 INFO  L130       PetriNetUnfolder]: 3890/118633 cut-off events.
[2023-11-13 05:38:11,528 INFO  L131       PetriNetUnfolder]: For 28/28 co-relation queries the response was YES.
[2023-11-13 05:38:12,720 INFO  L83            FinitePrefix]: Finished finitePrefix Result has 118774 conditions, 118633 events. 3890/118633 cut-off events. For 28/28 co-relation queries the response was YES. Maximal size of possible extension queue 308. Compared 1400798 event pairs, 0 based on Foata normal form. 0/107278 useless extension candidates. Maximal degree in co-relation 117189. Up to 15 conditions per place. 
[2023-11-13 05:38:15,372 INFO  L119        LiptonReduction]: Number of co-enabled transitions 7982912
[2023-11-13 05:39:16,880 WARN  L233               SmtUtils]: Spent 21.91s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:39:29,264 WARN  L233               SmtUtils]: Spent 12.38s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:40:07,529 WARN  L233               SmtUtils]: Spent 38.26s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:40:47,457 WARN  L233               SmtUtils]: Spent 39.93s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:42:56,314 WARN  L233               SmtUtils]: Spent 5.49s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:43:02,328 WARN  L233               SmtUtils]: Spent 6.01s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:43:12,397 WARN  L233               SmtUtils]: Spent 5.84s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:43:17,984 WARN  L233               SmtUtils]: Spent 5.59s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:43:30,331 WARN  L233               SmtUtils]: Spent 5.03s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:43:43,319 WARN  L233               SmtUtils]: Spent 8.23s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:43:50,910 WARN  L233               SmtUtils]: Spent 7.59s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:45:18,226 WARN  L233               SmtUtils]: Spent 22.57s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:45:54,240 WARN  L233               SmtUtils]: Spent 36.01s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:46:33,587 WARN  L233               SmtUtils]: Spent 39.35s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:47:01,983 WARN  L233               SmtUtils]: Spent 28.39s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:47:59,973 WARN  L233               SmtUtils]: Spent 27.08s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:48:26,353 WARN  L233               SmtUtils]: Spent 26.38s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:48:50,519 WARN  L233               SmtUtils]: Spent 24.16s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:49:29,382 WARN  L233               SmtUtils]: Spent 38.86s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:50:29,480 WARN  L233               SmtUtils]: Spent 34.35s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:51:06,621 WARN  L233               SmtUtils]: Spent 37.14s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:51:25,445 WARN  L233               SmtUtils]: Spent 18.82s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:51:34,491 WARN  L233               SmtUtils]: Spent 9.05s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:53:45,589 WARN  L233               SmtUtils]: Spent 6.12s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:53:52,220 WARN  L233               SmtUtils]: Spent 6.63s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:54:00,725 WARN  L233               SmtUtils]: Spent 8.50s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:54:08,762 WARN  L233               SmtUtils]: Spent 8.04s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:54:15,714 WARN  L233               SmtUtils]: Spent 6.95s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:54:22,069 WARN  L233               SmtUtils]: Spent 6.35s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:54:27,165 WARN  L233               SmtUtils]: Spent 5.10s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:58:44,872 WARN  L233               SmtUtils]: Spent 41.14s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 05:59:25,054 WARN  L233               SmtUtils]: Spent 40.18s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:00:01,610 WARN  L233               SmtUtils]: Spent 36.55s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:00:37,730 WARN  L233               SmtUtils]: Spent 36.12s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:01:41,733 WARN  L233               SmtUtils]: Spent 5.17s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:01:49,568 WARN  L233               SmtUtils]: Spent 7.83s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:01:58,150 WARN  L233               SmtUtils]: Spent 8.58s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:02:03,627 WARN  L233               SmtUtils]: Spent 5.48s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:02:09,593 WARN  L233               SmtUtils]: Spent 5.97s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:02:14,818 WARN  L233               SmtUtils]: Spent 5.22s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:02:20,059 WARN  L233               SmtUtils]: Spent 5.24s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:03:34,148 WARN  L233               SmtUtils]: Spent 7.11s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:03:42,124 WARN  L233               SmtUtils]: Spent 7.98s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:03:48,213 WARN  L233               SmtUtils]: Spent 6.09s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:03:53,685 WARN  L233               SmtUtils]: Spent 5.47s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:04:03,922 WARN  L233               SmtUtils]: Spent 5.55s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:09:26,556 WARN  L233               SmtUtils]: Spent 7.32s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:09:35,753 WARN  L233               SmtUtils]: Spent 9.20s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:09:41,825 WARN  L233               SmtUtils]: Spent 6.07s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:09:48,956 WARN  L233               SmtUtils]: Spent 7.13s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:09:54,546 WARN  L233               SmtUtils]: Spent 5.59s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:10:00,667 WARN  L233               SmtUtils]: Spent 6.12s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:10:06,417 WARN  L233               SmtUtils]: Spent 5.75s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:10:12,932 WARN  L233               SmtUtils]: Spent 6.51s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:15:31,031 WARN  L233               SmtUtils]: Spent 8.01s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:15:38,977 WARN  L233               SmtUtils]: Spent 7.95s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:15:45,764 WARN  L233               SmtUtils]: Spent 6.79s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:15:51,097 WARN  L233               SmtUtils]: Spent 5.33s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:15:56,267 WARN  L233               SmtUtils]: Spent 5.17s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:16:05,717 WARN  L233               SmtUtils]: Spent 5.11s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:22:13,524 WARN  L233               SmtUtils]: Spent 6.04s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:22:20,076 WARN  L233               SmtUtils]: Spent 6.55s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:22:27,683 WARN  L233               SmtUtils]: Spent 7.61s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:22:36,190 WARN  L233               SmtUtils]: Spent 8.51s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:22:44,755 WARN  L233               SmtUtils]: Spent 8.56s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:22:53,612 WARN  L233               SmtUtils]: Spent 8.86s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:23:01,817 WARN  L233               SmtUtils]: Spent 8.20s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:23:10,390 WARN  L233               SmtUtils]: Spent 8.57s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:23:54,563 WARN  L233               SmtUtils]: Spent 39.69s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:24:14,909 WARN  L233               SmtUtils]: Spent 20.34s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:24:51,643 WARN  L233               SmtUtils]: Spent 36.73s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:25:31,453 WARN  L233               SmtUtils]: Spent 39.81s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:27:23,101 WARN  L233               SmtUtils]: Spent 10.75s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:27:43,953 WARN  L233               SmtUtils]: Spent 20.85s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:28:18,538 WARN  L233               SmtUtils]: Spent 34.58s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:28:58,633 WARN  L233               SmtUtils]: Spent 40.09s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:29:53,650 WARN  L233               SmtUtils]: Spent 35.53s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:30:21,754 WARN  L233               SmtUtils]: Spent 28.10s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:30:51,648 WARN  L233               SmtUtils]: Spent 29.89s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:31:21,817 WARN  L233               SmtUtils]: Spent 30.17s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:36:50,318 WARN  L233               SmtUtils]: Spent 7.43s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:36:58,933 WARN  L233               SmtUtils]: Spent 8.61s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:37:04,153 WARN  L233               SmtUtils]: Spent 5.22s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:37:10,811 WARN  L233               SmtUtils]: Spent 6.66s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:37:18,142 WARN  L233               SmtUtils]: Spent 7.33s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:37:26,179 WARN  L233               SmtUtils]: Spent 8.04s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:39:32,117 WARN  L233               SmtUtils]: Spent 39.63s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:40:03,626 WARN  L233               SmtUtils]: Spent 31.51s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:40:20,418 WARN  L233               SmtUtils]: Spent 16.79s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:40:53,977 WARN  L233               SmtUtils]: Spent 33.56s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:41:21,169 WARN  L233               SmtUtils]: Spent 8.69s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:41:30,244 WARN  L233               SmtUtils]: Spent 9.07s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:41:35,249 WARN  L233               SmtUtils]: Spent 5.00s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:41:40,600 WARN  L233               SmtUtils]: Spent 5.35s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:41:49,032 WARN  L233               SmtUtils]: Spent 8.43s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:41:58,334 WARN  L233               SmtUtils]: Spent 9.30s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:42:05,121 WARN  L233               SmtUtils]: Spent 6.79s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:42:12,549 WARN  L233               SmtUtils]: Spent 7.43s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:43:36,068 WARN  L233               SmtUtils]: Spent 38.79s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:44:14,754 WARN  L233               SmtUtils]: Spent 38.68s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:44:50,488 WARN  L233               SmtUtils]: Spent 35.73s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:45:19,247 WARN  L233               SmtUtils]: Spent 28.76s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:48:28,938 WARN  L233               SmtUtils]: Spent 5.82s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:48:37,041 WARN  L233               SmtUtils]: Spent 8.10s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:48:43,618 WARN  L233               SmtUtils]: Spent 6.58s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:48:49,662 WARN  L233               SmtUtils]: Spent 6.04s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:48:59,594 WARN  L233               SmtUtils]: Spent 5.19s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:49:07,219 WARN  L233               SmtUtils]: Spent 7.62s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:49:14,616 WARN  L233               SmtUtils]: Spent 7.40s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:50:18,270 WARN  L233               SmtUtils]: Spent 34.04s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:50:40,987 WARN  L233               SmtUtils]: Spent 22.72s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:51:17,033 WARN  L233               SmtUtils]: Spent 36.04s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:51:56,674 WARN  L233               SmtUtils]: Spent 39.64s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:53:00,512 WARN  L233               SmtUtils]: Spent 39.64s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:53:34,584 WARN  L233               SmtUtils]: Spent 34.07s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:54:12,552 WARN  L233               SmtUtils]: Spent 37.97s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:54:51,442 WARN  L233               SmtUtils]: Spent 38.89s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:58:19,737 WARN  L233               SmtUtils]: Spent 25.05s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:58:49,658 WARN  L233               SmtUtils]: Spent 29.92s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:59:14,651 WARN  L233               SmtUtils]: Spent 24.99s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 06:59:42,344 WARN  L233               SmtUtils]: Spent 27.69s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:01:29,592 WARN  L233               SmtUtils]: Spent 34.39s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:02:02,156 WARN  L233               SmtUtils]: Spent 32.56s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:02:15,733 WARN  L233               SmtUtils]: Spent 13.58s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:02:54,431 WARN  L233               SmtUtils]: Spent 38.70s on a formula simplification that was a NOOP. DAG size: 51 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:14:06,359 WARN  L233               SmtUtils]: Spent 9.56s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:14:13,872 WARN  L233               SmtUtils]: Spent 7.51s on a formula simplification that was a NOOP. DAG size: 52 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:14:31,657 WARN  L233               SmtUtils]: Spent 8.61s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:14:40,244 WARN  L233               SmtUtils]: Spent 8.59s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:14:47,810 WARN  L233               SmtUtils]: Spent 7.56s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 278] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
[2023-11-13 07:14:55,214 WARN  L233               SmtUtils]: Spent 7.40s on a formula simplification that was a NOOP. DAG size: 53 (called from [L 301] de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaUtils.sequentialComposition)
Killed by 15
