./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-242.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:51,278 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:51,355 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b120e747-25c6-4d3f-8b49-39e5688e2b1d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:51,360 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:51,361 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:51,402 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:51,402 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:51,402 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:51,403 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:51,403 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:51,403 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:51,403 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:51,404 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:51,404 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:51,404 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:51,404 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:51,404 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:51,404 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:51,404 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:51,405 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:51,405 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:51,405 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:51,405 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:51,405 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:51,405 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:51,406 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:51,406 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:51,742 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:51,753 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:51,757 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:51,761 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:51,761 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:51,763 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b120e747-25c6-4d3f-8b49-39e5688e2b1d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-242.smt2
[2025-04-28 21:21:51,764 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:51,770 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:53,644 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b120e747-25c6-4d3f-8b49-39e5688e2b1d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-242.smt2
[2025-04-28 21:21:53,648 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:53,651 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:53,651 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:53,652 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:53,652 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:53,657 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,855 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53 Unit
[2025-04-28 21:21:53,856 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:53,858 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:53,858 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:53,858 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:53,875 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,875 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,017 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,017 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,094 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,103 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,109 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,133 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,146 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,247 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:54,250 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:54,250 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:54,251 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:54,252 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:54,254 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:54,271 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,291 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,294 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,307 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:54,310 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:54,311 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:54,311 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:54,311 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:54,311 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:54,311 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH0.CLN Main.java, line 17 given in one single declaration
[2025-04-28 21:21:54,311 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH0.CLN Main.java, line 17
[2025-04-28 21:21:54,311 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH0.CLN Main.java, line 17
[2025-04-28 21:21:54,312 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9 given in one single declaration
[2025-04-28 21:21:54,312 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9
[2025-04-28 21:21:54,312 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9
[2025-04-28 21:21:54,312 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8 given in one single declaration
[2025-04-28 21:21:54,313 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8
[2025-04-28 21:21:54,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8
[2025-04-28 21:21:54,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7 given in one single declaration
[2025-04-28 21:21:54,313 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7
[2025-04-28 21:21:54,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7
[2025-04-28 21:21:54,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6 given in one single declaration
[2025-04-28 21:21:54,313 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6
[2025-04-28 21:21:54,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6
[2025-04-28 21:21:54,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5 given in one single declaration
[2025-04-28 21:21:54,314 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5
[2025-04-28 21:21:54,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5
[2025-04-28 21:21:54,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_post given in one single declaration
[2025-04-28 21:21:54,315 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_post
[2025-04-28 21:21:54,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_post
[2025-04-28 21:21:54,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,315 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block0
[2025-04-28 21:21:54,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block0
[2025-04-28 21:21:54,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,315 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:54,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:54,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,315 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:54,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:54,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1 given in one single declaration
[2025-04-28 21:21:54,316 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1
[2025-04-28 21:21:54,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1
[2025-04-28 21:21:54,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_pre given in one single declaration
[2025-04-28 21:21:54,316 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_pre
[2025-04-28 21:21:54,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_pre
[2025-04-28 21:21:54,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4 given in one single declaration
[2025-04-28 21:21:54,316 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4
[2025-04-28 21:21:54,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4
[2025-04-28 21:21:54,317 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_post given in one single declaration
[2025-04-28 21:21:54,317 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_post
[2025-04-28 21:21:54,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_post
[2025-04-28 21:21:54,317 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,317 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block0
[2025-04-28 21:21:54,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block0
[2025-04-28 21:21:54,317 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_3 given in one single declaration
[2025-04-28 21:21:54,317 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_3
[2025-04-28 21:21:54,318 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_3
[2025-04-28 21:21:54,318 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,318 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:54,318 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:54,318 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,318 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:54,318 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:54,318 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1 given in one single declaration
[2025-04-28 21:21:54,318 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1
[2025-04-28 21:21:54,318 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1
[2025-04-28 21:21:54,318 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_pre given in one single declaration
[2025-04-28 21:21:54,318 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_pre
[2025-04-28 21:21:54,320 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_pre
[2025-04-28 21:21:54,320 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3 given in one single declaration
[2025-04-28 21:21:54,320 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3
[2025-04-28 21:21:54,320 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3
[2025-04-28 21:21:54,320 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,321 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2
[2025-04-28 21:21:54,321 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2
[2025-04-28 21:21:54,321 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,321 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1
[2025-04-28 21:21:54,321 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1
[2025-04-28 21:21:54,321 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1 given in one single declaration
[2025-04-28 21:21:54,321 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1
[2025-04-28 21:21:54,321 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1
[2025-04-28 21:21:54,321 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre given in one single declaration
[2025-04-28 21:21:54,321 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:54,321 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:54,321 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:54,322 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_post
[2025-04-28 21:21:54,322 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_post
[2025-04-28 21:21:54,322 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,322 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block0
[2025-04-28 21:21:54,322 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block0
[2025-04-28 21:21:54,322 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block3_1 given in one single declaration
[2025-04-28 21:21:54,323 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,324 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,324 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block3 given in one single declaration
[2025-04-28 21:21:54,324 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block3
[2025-04-28 21:21:54,324 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block3
[2025-04-28 21:21:54,324 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,324 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,324 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,324 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,324 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,324 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,324 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block1 given in one single declaration
[2025-04-28 21:21:54,324 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block1
[2025-04-28 21:21:54,324 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block1
[2025-04-28 21:21:54,324 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:54,325 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_pre
[2025-04-28 21:21:54,325 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_pre
[2025-04-28 21:21:54,325 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:54,325 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_post
[2025-04-28 21:21:54,325 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_post
[2025-04-28 21:21:54,325 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,325 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block0
[2025-04-28 21:21:54,325 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block0
[2025-04-28 21:21:54,325 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block3_1 given in one single declaration
[2025-04-28 21:21:54,325 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,325 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,325 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block3 given in one single declaration
[2025-04-28 21:21:54,325 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block3
[2025-04-28 21:21:54,325 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block3
[2025-04-28 21:21:54,325 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,325 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:54,326 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_post
[2025-04-28 21:21:54,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_post
[2025-04-28 21:21:54,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,326 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block0
[2025-04-28 21:21:54,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block0
[2025-04-28 21:21:54,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block3_1 given in one single declaration
[2025-04-28 21:21:54,326 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block3 given in one single declaration
[2025-04-28 21:21:54,326 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block3
[2025-04-28 21:21:54,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block3
[2025-04-28 21:21:54,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,326 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:54,327 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_post
[2025-04-28 21:21:54,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_post
[2025-04-28 21:21:54,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,327 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block0
[2025-04-28 21:21:54,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block0
[2025-04-28 21:21:54,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block3_1 given in one single declaration
[2025-04-28 21:21:54,327 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block3_1
[2025-04-28 21:21:54,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block3 given in one single declaration
[2025-04-28 21:21:54,327 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block3
[2025-04-28 21:21:54,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block3
[2025-04-28 21:21:54,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:54,327 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block1_2
[2025-04-28 21:21:54,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,328 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block1 given in one single declaration
[2025-04-28 21:21:54,328 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block1
[2025-04-28 21:21:54,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block1
[2025-04-28 21:21:54,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:54,328 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_pre
[2025-04-28 21:21:54,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_pre
[2025-04-28 21:21:54,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_22 given in one single declaration
[2025-04-28 21:21:54,329 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_22
[2025-04-28 21:21:54,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_22
[2025-04-28 21:21:54,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_21 given in one single declaration
[2025-04-28 21:21:54,329 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_21
[2025-04-28 21:21:54,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_21
[2025-04-28 21:21:54,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_20 given in one single declaration
[2025-04-28 21:21:54,329 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_20
[2025-04-28 21:21:54,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_20
[2025-04-28 21:21:54,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_19 given in one single declaration
[2025-04-28 21:21:54,330 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_19
[2025-04-28 21:21:54,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_19
[2025-04-28 21:21:54,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_18 given in one single declaration
[2025-04-28 21:21:54,330 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_18
[2025-04-28 21:21:54,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_18
[2025-04-28 21:21:54,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_17 given in one single declaration
[2025-04-28 21:21:54,330 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_17
[2025-04-28 21:21:54,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_17
[2025-04-28 21:21:54,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16 given in one single declaration
[2025-04-28 21:21:54,330 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16
[2025-04-28 21:21:54,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16
[2025-04-28 21:21:54,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15 given in one single declaration
[2025-04-28 21:21:54,330 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15
[2025-04-28 21:21:54,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15
[2025-04-28 21:21:54,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14 given in one single declaration
[2025-04-28 21:21:54,331 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14
[2025-04-28 21:21:54,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14
[2025-04-28 21:21:54,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13 given in one single declaration
[2025-04-28 21:21:54,331 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13
[2025-04-28 21:21:54,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13
[2025-04-28 21:21:54,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12 given in one single declaration
[2025-04-28 21:21:54,331 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12
[2025-04-28 21:21:54,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12
[2025-04-28 21:21:54,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11 given in one single declaration
[2025-04-28 21:21:54,331 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11
[2025-04-28 21:21:54,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11
[2025-04-28 21:21:54,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10 given in one single declaration
[2025-04-28 21:21:54,331 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10
[2025-04-28 21:21:54,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10
[2025-04-28 21:21:54,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:54,331 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_post
[2025-04-28 21:21:54,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_post
[2025-04-28 21:21:54,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_8 given in one single declaration
[2025-04-28 21:21:54,332 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_8
[2025-04-28 21:21:54,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_8
[2025-04-28 21:21:54,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_7 given in one single declaration
[2025-04-28 21:21:54,332 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_7
[2025-04-28 21:21:54,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_7
[2025-04-28 21:21:54,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_6 given in one single declaration
[2025-04-28 21:21:54,332 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_6
[2025-04-28 21:21:54,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_6
[2025-04-28 21:21:54,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_5 given in one single declaration
[2025-04-28 21:21:54,332 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_5
[2025-04-28 21:21:54,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_5
[2025-04-28 21:21:54,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_4 given in one single declaration
[2025-04-28 21:21:54,333 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_4
[2025-04-28 21:21:54,334 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_4
[2025-04-28 21:21:54,334 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_3 given in one single declaration
[2025-04-28 21:21:54,334 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_3
[2025-04-28 21:21:54,334 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_3
[2025-04-28 21:21:54,334 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_2 given in one single declaration
[2025-04-28 21:21:54,334 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_2
[2025-04-28 21:21:54,334 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_2
[2025-04-28 21:21:54,335 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:54,335 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0_1
[2025-04-28 21:21:54,335 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0_1
[2025-04-28 21:21:54,335 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:54,335 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_Block0
[2025-04-28 21:21:54,335 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_Block0
[2025-04-28 21:21:54,335 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Throwable.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:54,335 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Throwable.CLN void <init>()>_pre
[2025-04-28 21:21:54,335 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Throwable.CLN void <init>()>_pre
[2025-04-28 21:21:54,335 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block2_1 given in one single declaration
[2025-04-28 21:21:54,335 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,335 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,335 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <A.CLN void <init>()>_Block2 given in one single declaration
[2025-04-28 21:21:54,335 INFO  L130     BoogieDeclarations]: Found specification of procedure <A.CLN void <init>()>_Block2
[2025-04-28 21:21:54,335 INFO  L138     BoogieDeclarations]: Found implementation of procedure <A.CLN void <init>()>_Block2
[2025-04-28 21:21:54,335 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,336 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,336 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block1 given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block1
[2025-04-28 21:21:54,336 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block1
[2025-04-28 21:21:54,336 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_pre
[2025-04-28 21:21:54,336 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_pre
[2025-04-28 21:21:54,336 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block2_1 given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,336 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,336 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <B.CLN void <init>()>_Block2 given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <B.CLN void <init>()>_Block2
[2025-04-28 21:21:54,336 INFO  L138     BoogieDeclarations]: Found implementation of procedure <B.CLN void <init>()>_Block2
[2025-04-28 21:21:54,336 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,336 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block1_1
[2025-04-28 21:21:54,336 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block1 given in one single declaration
[2025-04-28 21:21:54,336 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block1
[2025-04-28 21:21:54,337 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block1
[2025-04-28 21:21:54,337 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:54,337 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_pre
[2025-04-28 21:21:54,337 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_pre
[2025-04-28 21:21:54,337 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block2_1 given in one single declaration
[2025-04-28 21:21:54,337 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,337 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,337 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <C.CLN void <init>()>_Block2 given in one single declaration
[2025-04-28 21:21:54,337 INFO  L130     BoogieDeclarations]: Found specification of procedure <C.CLN void <init>()>_Block2
[2025-04-28 21:21:54,337 INFO  L138     BoogieDeclarations]: Found implementation of procedure <C.CLN void <init>()>_Block2
[2025-04-28 21:21:54,338 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block2_1 given in one single declaration
[2025-04-28 21:21:54,338 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,338 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block2_1
[2025-04-28 21:21:54,338 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <D.CLN void <init>()>_Block2 given in one single declaration
[2025-04-28 21:21:54,338 INFO  L130     BoogieDeclarations]: Found specification of procedure <D.CLN void <init>()>_Block2
[2025-04-28 21:21:54,339 INFO  L138     BoogieDeclarations]: Found implementation of procedure <D.CLN void <init>()>_Block2
[2025-04-28 21:21:54,339 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH3.CLN Main.java, line 20 given in one single declaration
[2025-04-28 21:21:54,339 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH3.CLN Main.java, line 20
[2025-04-28 21:21:54,339 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH3.CLN Main.java, line 20
[2025-04-28 21:21:54,339 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_24 given in one single declaration
[2025-04-28 21:21:54,339 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_24
[2025-04-28 21:21:54,339 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_24
[2025-04-28 21:21:54,339 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_23 given in one single declaration
[2025-04-28 21:21:54,339 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_23
[2025-04-28 21:21:54,339 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_23
[2025-04-28 21:21:54,339 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH2.CLN Main.java, line 19 given in one single declaration
[2025-04-28 21:21:54,339 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH2.CLN Main.java, line 19
[2025-04-28 21:21:54,339 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH2.CLN Main.java, line 19
[2025-04-28 21:21:54,340 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH6.CLN Main.java, line 26 given in one single declaration
[2025-04-28 21:21:54,340 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH6.CLN Main.java, line 26
[2025-04-28 21:21:54,340 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH6.CLN Main.java, line 26
[2025-04-28 21:21:54,340 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13_1 given in one single declaration
[2025-04-28 21:21:54,340 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13_1
[2025-04-28 21:21:54,340 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13_1
[2025-04-28 21:21:54,340 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13 given in one single declaration
[2025-04-28 21:21:54,340 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13
[2025-04-28 21:21:54,340 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13
[2025-04-28 21:21:54,340 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8 given in one single declaration
[2025-04-28 21:21:54,340 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8
[2025-04-28 21:21:54,340 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8
[2025-04-28 21:21:54,340 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block7_1 given in one single declaration
[2025-04-28 21:21:54,340 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block7_1
[2025-04-28 21:21:54,340 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block7_1
[2025-04-28 21:21:54,340 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block7 given in one single declaration
[2025-04-28 21:21:54,340 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block7
[2025-04-28 21:21:54,341 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block7
[2025-04-28 21:21:54,341 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5_1 given in one single declaration
[2025-04-28 21:21:54,341 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5_1
[2025-04-28 21:21:54,341 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5_1
[2025-04-28 21:21:54,341 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5 given in one single declaration
[2025-04-28 21:21:54,341 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5
[2025-04-28 21:21:54,341 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5
[2025-04-28 21:21:54,341 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3_1 given in one single declaration
[2025-04-28 21:21:54,341 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3_1
[2025-04-28 21:21:54,341 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3_1
[2025-04-28 21:21:54,341 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3 given in one single declaration
[2025-04-28 21:21:54,341 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3
[2025-04-28 21:21:54,341 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3
[2025-04-28 21:21:54,344 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_26 given in one single declaration
[2025-04-28 21:21:54,344 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_26
[2025-04-28 21:21:54,344 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_26
[2025-04-28 21:21:54,345 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_25 given in one single declaration
[2025-04-28 21:21:54,346 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_25
[2025-04-28 21:21:54,346 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_25
[2025-04-28 21:21:54,346 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH5.CLN Main.java, line 28 given in one single declaration
[2025-04-28 21:21:54,346 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH5.CLN Main.java, line 28
[2025-04-28 21:21:54,346 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH5.CLN Main.java, line 28
[2025-04-28 21:21:54,346 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1 given in one single declaration
[2025-04-28 21:21:54,346 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1
[2025-04-28 21:21:54,346 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1
[2025-04-28 21:21:54,346 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14 given in one single declaration
[2025-04-28 21:21:54,346 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14
[2025-04-28 21:21:54,346 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14
[2025-04-28 21:21:54,346 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block6 given in one single declaration
[2025-04-28 21:21:54,347 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block6
[2025-04-28 21:21:54,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block6
[2025-04-28 21:21:54,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH7.CLN Main.java, line 24 given in one single declaration
[2025-04-28 21:21:54,347 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH7.CLN Main.java, line 24
[2025-04-28 21:21:54,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH7.CLN Main.java, line 24
[2025-04-28 21:21:54,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block11_1 given in one single declaration
[2025-04-28 21:21:54,347 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block11_1
[2025-04-28 21:21:54,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block11_1
[2025-04-28 21:21:54,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block11 given in one single declaration
[2025-04-28 21:21:54,347 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block11
[2025-04-28 21:21:54,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block11
[2025-04-28 21:21:54,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block9_1 given in one single declaration
[2025-04-28 21:21:54,347 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block9_1
[2025-04-28 21:21:54,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block9_1
[2025-04-28 21:21:54,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block9 given in one single declaration
[2025-04-28 21:21:54,347 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block9
[2025-04-28 21:21:54,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block9
[2025-04-28 21:21:54,348 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10 given in one single declaration
[2025-04-28 21:21:54,348 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10
[2025-04-28 21:21:54,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10
[2025-04-28 21:21:54,348 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH4.CLN Main.java, line 30 given in one single declaration
[2025-04-28 21:21:54,348 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH4.CLN Main.java, line 30
[2025-04-28 21:21:54,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH4.CLN Main.java, line 30
[2025-04-28 21:21:54,348 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_1 given in one single declaration
[2025-04-28 21:21:54,348 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_1
[2025-04-28 21:21:54,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_1
[2025-04-28 21:21:54,348 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15 given in one single declaration
[2025-04-28 21:21:54,348 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15
[2025-04-28 21:21:54,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15
[2025-04-28 21:21:54,348 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4 given in one single declaration
[2025-04-28 21:21:54,348 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4
[2025-04-28 21:21:54,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4
[2025-04-28 21:21:54,352 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block2 given in one single declaration
[2025-04-28 21:21:54,352 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block2
[2025-04-28 21:21:54,352 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block2
[2025-04-28 21:21:54,352 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH1.CLN Main.java, line 18 given in one single declaration
[2025-04-28 21:21:54,352 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH1.CLN Main.java, line 18
[2025-04-28 21:21:54,352 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH1.CLN Main.java, line 18
[2025-04-28 21:21:54,352 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:54,352 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:54,352 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:56,933 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:56,937 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:59,562 INFO  L?                        ?]: Removed 128 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:59,563 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:59,598 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:59,599 INFO  L312             CfgBuilder]: Removed 52 assume(true) statements.
[2025-04-28 21:21:59,599 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:59 BoogieIcfgContainer
[2025-04-28 21:21:59,599 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:59,604 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:59,604 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:59,648 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:59,648 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:53" (1/3) ...
[2025-04-28 21:21:59,649 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@147a0bb6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:59, skipping insertion in model container
[2025-04-28 21:21:59,649 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (2/3) ...
[2025-04-28 21:21:59,649 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@147a0bb6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:59, skipping insertion in model container
[2025-04-28 21:21:59,650 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:59" (3/3) ...
[2025-04-28 21:21:59,651 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:59,667 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:59,671 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 124 procedures, 490 locations, 740 edges, 124 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:59,744 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:59,766 INFO  L340      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=None, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@268f9045, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:59,766 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:59,774 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 490 states, 212 states have (on average 1.099056603773585) internal successors, (233), 233 states have internal predecessors, (233), 157 states have call successors, (169), 123 states have call predecessors, (169), 123 states have return successors, (169), 133 states have call predecessors, (169), 157 states have call successors, (169)
[2025-04-28 21:21:59,880 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 1281
[2025-04-28 21:21:59,881 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,882 INFO  L218           NwaCegarLoop]: trace histogram [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,883 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,890 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,891 INFO  L85        PathProgramCache]: Analyzing trace with hash 1101163613, now seen corresponding path program 1 times
[2025-04-28 21:21:59,900 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,900 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [543659467]
[2025-04-28 21:21:59,901 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,901 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,897 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 1280 statements into 1 equivalence classes.
[2025-04-28 21:22:02,332 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 1280 of 1280 statements.
[2025-04-28 21:22:02,333 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,086 INFO  L134       CoverageAnalysis]: Checked inductivity of 7607 backedges. 0 proven. 248 refuted. 0 times theorem prover too weak. 7359 trivial. 0 not checked.
[2025-04-28 21:22:10,087 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:10,087 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [543659467]
[2025-04-28 21:22:10,088 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [543659467] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:10,089 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1376789193]
[2025-04-28 21:22:10,089 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:10,090 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:10,093 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:10,097 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:10,111 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:22:19,359 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 1280 statements into 1 equivalence classes.
