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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:10,558 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:10,638 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_15e04e0f-bd91-45b9-b96d-320bd30c13d5/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:10,642 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:10,642 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:10,668 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:10,670 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:10,670 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:10,671 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:10,672 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:10,672 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:10,672 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:10,672 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:10,672 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:10,673 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:10,673 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:10,674 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:10,674 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:10,674 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:10,674 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:10,675 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:10,675 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:10,675 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:10,675 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:10,675 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:10,676 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:10,676 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:11,019 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:11,027 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:11,031 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:11,034 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:11,034 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:11,036 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_15e04e0f-bd91-45b9-b96d-320bd30c13d5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-299.smt2
[2025-04-28 21:21:11,037 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:11,042 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:11,798 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_15e04e0f-bd91-45b9-b96d-320bd30c13d5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-299.smt2
[2025-04-28 21:21:11,802 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:11,804 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:11,805 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:11,805 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:11,805 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:11,809 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,881 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11 Unit
[2025-04-28 21:21:11,881 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:11,882 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:11,882 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:11,882 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:11,897 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,897 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,939 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,940 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,959 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,962 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,966 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,981 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,988 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,031 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,032 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:12,032 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:12,032 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:12,033 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,035 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:12,054 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:12,070 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:12,073 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:12,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:12,092 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:12,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:12,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:12,092 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:12,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:12,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH2.CLN Main.java, line 36 given in one single declaration
[2025-04-28 21:21:12,092 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH2.CLN Main.java, line 36
[2025-04-28 21:21:12,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH2.CLN Main.java, line 36
[2025-04-28 21:21:12,092 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:12,092 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_19
[2025-04-28 21:21:12,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_19
[2025-04-28 21:21:12,093 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:12,093 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_18
[2025-04-28 21:21:12,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_18
[2025-04-28 21:21:12,093 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:12,093 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_17
[2025-04-28 21:21:12,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_17
[2025-04-28 21:21:12,093 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:12,093 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16
[2025-04-28 21:21:12,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16
[2025-04-28 21:21:12,093 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:12,093 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15
[2025-04-28 21:21:12,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15
[2025-04-28 21:21:12,093 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:12,094 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14
[2025-04-28 21:21:12,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14
[2025-04-28 21:21:12,094 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:12,094 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13
[2025-04-28 21:21:12,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13
[2025-04-28 21:21:12,094 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:12,094 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12
[2025-04-28 21:21:12,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12
[2025-04-28 21:21:12,094 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:12,094 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11
[2025-04-28 21:21:12,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11
[2025-04-28 21:21:12,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_.DLRStaticFields_Main_3 given in one single declaration
[2025-04-28 21:21:12,094 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_.DLRStaticFields_Main_3
[2025-04-28 21:21:12,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_.DLRStaticFields_Main_3
[2025-04-28 21:21:12,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,095 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:12,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:12,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,095 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:12,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:12,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1 given in one single declaration
[2025-04-28 21:21:12,095 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1
[2025-04-28 21:21:12,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1
[2025-04-28 21:21:12,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_pre given in one single declaration
[2025-04-28 21:21:12,095 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_pre
[2025-04-28 21:21:12,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_pre
[2025-04-28 21:21:12,095 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:12,095 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3
[2025-04-28 21:21:12,096 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3
[2025-04-28 21:21:12,096 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:12,096 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2
[2025-04-28 21:21:12,096 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2
[2025-04-28 21:21:12,096 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:12,096 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1
[2025-04-28 21:21:12,096 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1
[2025-04-28 21:21:12,096 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:12,096 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1
[2025-04-28 21:21:12,096 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1
[2025-04-28 21:21:12,096 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:12,096 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:12,097 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:12,097 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:12,097 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10
[2025-04-28 21:21:12,097 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10
[2025-04-28 21:21:12,099 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:12,100 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9
[2025-04-28 21:21:12,100 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9
[2025-04-28 21:21:12,100 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_post given in one single declaration
[2025-04-28 21:21:12,100 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_post
[2025-04-28 21:21:12,100 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_post
[2025-04-28 21:21:12,100 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block0 given in one single declaration
[2025-04-28 21:21:12,100 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block0
[2025-04-28 21:21:12,101 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block0
[2025-04-28 21:21:12,101 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_6 given in one single declaration
[2025-04-28 21:21:12,101 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1_6
[2025-04-28 21:21:12,101 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_6
[2025-04-28 21:21:12,101 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_5 given in one single declaration
[2025-04-28 21:21:12,101 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1_5
[2025-04-28 21:21:12,102 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_5
[2025-04-28 21:21:12,102 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_4 given in one single declaration
[2025-04-28 21:21:12,102 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1_4
[2025-04-28 21:21:12,102 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_4
[2025-04-28 21:21:12,102 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_3 given in one single declaration
[2025-04-28 21:21:12,102 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1_3
[2025-04-28 21:21:12,102 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_3
[2025-04-28 21:21:12,102 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,102 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1_2
[2025-04-28 21:21:12,103 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_2
[2025-04-28 21:21:12,103 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,103 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1_1
[2025-04-28 21:21:12,103 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1_1
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1 given in one single declaration
[2025-04-28 21:21:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_Block1
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_Block1
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void <init>(int)>_pre given in one single declaration
[2025-04-28 21:21:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void <init>(int)>_pre
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void <init>(int)>_pre
[2025-04-28 21:21:12,104 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:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8
[2025-04-28 21:21:12,104 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:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7
[2025-04-28 21:21:12,105 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:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6
[2025-04-28 21:21:12,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6
[2025-04-28 21:21:12,105 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:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5
[2025-04-28 21:21:12,106 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5
[2025-04-28 21:21:12,106 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_post given in one single declaration
[2025-04-28 21:21:12,106 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_post
[2025-04-28 21:21:12,106 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_post
[2025-04-28 21:21:12,106 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block0 given in one single declaration
[2025-04-28 21:21:12,106 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block0
[2025-04-28 21:21:12,106 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block0
[2025-04-28 21:21:12,106 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,106 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:12,106 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:12,106 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,107 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:12,107 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:12,107 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1 given in one single declaration
[2025-04-28 21:21:12,107 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1
[2025-04-28 21:21:12,107 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1
[2025-04-28 21:21:12,109 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_pre given in one single declaration
[2025-04-28 21:21:12,109 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_pre
[2025-04-28 21:21:12,109 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_pre
[2025-04-28 21:21:12,109 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:12,109 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4
[2025-04-28 21:21:12,109 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4
[2025-04-28 21:21:12,109 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_post given in one single declaration
[2025-04-28 21:21:12,109 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_post
[2025-04-28 21:21:12,109 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_post
[2025-04-28 21:21:12,109 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block0 given in one single declaration
[2025-04-28 21:21:12,109 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block0
[2025-04-28 21:21:12,110 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block0
[2025-04-28 21:21:12,110 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_3 given in one single declaration
[2025-04-28 21:21:12,110 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_3
[2025-04-28 21:21:12,110 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_3
[2025-04-28 21:21:12,110 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:12,110 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_post
[2025-04-28 21:21:12,110 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_post
[2025-04-28 21:21:12,110 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:12,110 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,110 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,110 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:12,110 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block0
[2025-04-28 21:21:12,111 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block0
[2025-04-28 21:21:12,111 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block2 given in one single declaration
[2025-04-28 21:21:12,111 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block2
[2025-04-28 21:21:12,111 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block2
[2025-04-28 21:21:12,111 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,111 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block1_2
[2025-04-28 21:21:12,111 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block1_2
[2025-04-28 21:21:12,111 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,111 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block1_1
[2025-04-28 21:21:12,111 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block1_1
[2025-04-28 21:21:12,111 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block1 given in one single declaration
[2025-04-28 21:21:12,111 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block1
[2025-04-28 21:21:12,112 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block1
[2025-04-28 21:21:12,112 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:12,112 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_pre
[2025-04-28 21:21:12,113 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_pre
[2025-04-28 21:21:12,113 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Object.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:12,113 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Object.CLN void <init>()>_post
[2025-04-28 21:21:12,113 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Object.CLN void <init>()>_post
[2025-04-28 21:21:12,113 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Object.CLN void <init>()>_Block0_3 given in one single declaration
[2025-04-28 21:21:12,114 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Object.CLN void <init>()>_Block0_3
[2025-04-28 21:21:12,114 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Object.CLN void <init>()>_Block0_3
[2025-04-28 21:21:12,114 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Object.CLN void <init>()>_Block0_2 given in one single declaration
[2025-04-28 21:21:12,114 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Object.CLN void <init>()>_Block0_2
[2025-04-28 21:21:12,114 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Object.CLN void <init>()>_Block0_2
[2025-04-28 21:21:12,114 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Object.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:12,114 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Object.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,114 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Object.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,114 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Object.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:12,114 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Object.CLN void <init>()>_Block0
[2025-04-28 21:21:12,114 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Object.CLN void <init>()>_Block0
[2025-04-28 21:21:12,114 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.Object.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:12,115 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.Object.CLN void <init>()>_pre
[2025-04-28 21:21:12,115 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.Object.CLN void <init>()>_pre
[2025-04-28 21:21:12,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <init>()>_Block3 given in one single declaration
[2025-04-28 21:21:12,115 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <init>()>_Block3
[2025-04-28 21:21:12,115 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <init>()>_Block3
[2025-04-28 21:21:12,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_post given in one single declaration
[2025-04-28 21:21:12,115 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_post
[2025-04-28 21:21:12,115 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_post
[2025-04-28 21:21:12,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block0 given in one single declaration
[2025-04-28 21:21:12,115 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block0
[2025-04-28 21:21:12,118 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block0
[2025-04-28 21:21:12,118 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block17 given in one single declaration
[2025-04-28 21:21:12,118 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block17
[2025-04-28 21:21:12,118 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block17
[2025-04-28 21:21:12,118 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block16_1 given in one single declaration
[2025-04-28 21:21:12,118 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block16_1
[2025-04-28 21:21:12,118 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block16_1
[2025-04-28 21:21:12,118 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block16 given in one single declaration
[2025-04-28 21:21:12,118 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block16
[2025-04-28 21:21:12,118 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block16
[2025-04-28 21:21:12,118 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block10 given in one single declaration
[2025-04-28 21:21:12,118 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block10
[2025-04-28 21:21:12,118 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block10
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block9_5 given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block9_5
[2025-04-28 21:21:12,119 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block9_5
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block9_4 given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block9_4
[2025-04-28 21:21:12,119 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block9_4
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_.DLRStaticFields_java.lang.System_115 given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_.DLRStaticFields_java.lang.System_115
[2025-04-28 21:21:12,119 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_.DLRStaticFields_java.lang.System_115
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block9_2 given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block9_2
[2025-04-28 21:21:12,119 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block9_2
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block9_1 given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block9_1
[2025-04-28 21:21:12,119 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block9_1
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_post given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_post
[2025-04-28 21:21:12,119 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_post
[2025-04-28 21:21:12,119 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_Block0 given in one single declaration
[2025-04-28 21:21:12,119 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_Block0
[2025-04-28 21:21:12,120 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_Block0
[2025-04-28 21:21:12,120 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_Block1_4 given in one single declaration
[2025-04-28 21:21:12,120 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_Block1_4
[2025-04-28 21:21:12,120 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_Block1_4
[2025-04-28 21:21:12,120 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_Block1_3 given in one single declaration
[2025-04-28 21:21:12,120 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_Block1_3
[2025-04-28 21:21:12,120 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_Block1_3
[2025-04-28 21:21:12,120 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,120 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_Block1_2
[2025-04-28 21:21:12,120 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_Block1_2
[2025-04-28 21:21:12,120 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_JayArray_int_16 given in one single declaration
[2025-04-28 21:21:12,120 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_JayArray_int_16
[2025-04-28 21:21:12,120 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_JayArray_int_16
[2025-04-28 21:21:12,120 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_JayArray_int_15 given in one single declaration
[2025-04-28 21:21:12,120 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_JayArray_int_15
[2025-04-28 21:21:12,120 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_JayArray_int_15
[2025-04-28 21:21:12,120 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_Block0 given in one single declaration
[2025-04-28 21:21:12,120 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_Block0
[2025-04-28 21:21:12,121 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_Block0
[2025-04-28 21:21:12,121 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1_3 given in one single declaration
[2025-04-28 21:21:12,121 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_Block1_3
[2025-04-28 21:21:12,121 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1_3
[2025-04-28 21:21:12,121 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,121 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_Block1_2
[2025-04-28 21:21:12,121 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1_2
[2025-04-28 21:21:12,121 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,121 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_Block1_1
[2025-04-28 21:21:12,122 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1_1
[2025-04-28 21:21:12,122 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1 given in one single declaration
[2025-04-28 21:21:12,122 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_Block1
[2025-04-28 21:21:12,122 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_Block1
[2025-04-28 21:21:12,122 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_pre given in one single declaration
[2025-04-28 21:21:12,123 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_pre
[2025-04-28 21:21:12,123 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_pre
[2025-04-28 21:21:12,123 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block6 given in one single declaration
[2025-04-28 21:21:12,123 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block6
[2025-04-28 21:21:12,123 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block6
[2025-04-28 21:21:12,123 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block5 given in one single declaration
[2025-04-28 21:21:12,123 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block5
[2025-04-28 21:21:12,123 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block5
[2025-04-28 21:21:12,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block3_1 given in one single declaration
[2025-04-28 21:21:12,124 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block3_1
[2025-04-28 21:21:12,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block3_1
[2025-04-28 21:21:12,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block3 given in one single declaration
[2025-04-28 21:21:12,124 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block3
[2025-04-28 21:21:12,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block3
[2025-04-28 21:21:12,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block1_2 given in one single declaration
[2025-04-28 21:21:12,124 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block1_2
[2025-04-28 21:21:12,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block1_2
[2025-04-28 21:21:12,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,127 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block1_1
[2025-04-28 21:21:12,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block1_1
[2025-04-28 21:21:12,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block1 given in one single declaration
[2025-04-28 21:21:12,127 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block1
[2025-04-28 21:21:12,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block1
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_pre given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_pre
[2025-04-28 21:21:12,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_pre
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_.DLRStaticFields_Main_2 given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_.DLRStaticFields_Main_2
[2025-04-28 21:21:12,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_.DLRStaticFields_Main_2
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_Block1_1 given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_Block1_1
[2025-04-28 21:21:12,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_Block1_1
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_Block1 given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_Block1
[2025-04-28 21:21:12,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_Block1
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN int get(int)>_pre given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN int get(int)>_pre
[2025-04-28 21:21:12,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN int get(int)>_pre
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block9 given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block9
[2025-04-28 21:21:12,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block9
[2025-04-28 21:21:12,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block8 given in one single declaration
[2025-04-28 21:21:12,128 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block8
[2025-04-28 21:21:12,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block8
[2025-04-28 21:21:12,129 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block7_1 given in one single declaration
[2025-04-28 21:21:12,129 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block7_1
[2025-04-28 21:21:12,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block7_1
[2025-04-28 21:21:12,129 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block7 given in one single declaration
[2025-04-28 21:21:12,129 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block7
[2025-04-28 21:21:12,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block7
[2025-04-28 21:21:12,129 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block6_2 given in one single declaration
[2025-04-28 21:21:12,129 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block6_2
[2025-04-28 21:21:12,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block6_2
[2025-04-28 21:21:12,129 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block6_1 given in one single declaration
[2025-04-28 21:21:12,129 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block6_1
[2025-04-28 21:21:12,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block6_1
[2025-04-28 21:21:12,129 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_post given in one single declaration
[2025-04-28 21:21:12,129 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_post
[2025-04-28 21:21:12,129 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_post
[2025-04-28 21:21:12,130 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_int.CLN void set(int,int)>_Block0_1 given in one single declaration
[2025-04-28 21:21:12,130 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_int.CLN void set(int,int)>_Block0_1
[2025-04-28 21:21:12,130 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_int.CLN void set(int,int)>_Block0_1
[2025-04-28 21:21:12,130 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block9_3 given in one single declaration
[2025-04-28 21:21:12,130 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block9_3
[2025-04-28 21:21:12,130 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block9_3
[2025-04-28 21:21:12,130 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_post given in one single declaration
[2025-04-28 21:21:12,130 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_post
[2025-04-28 21:21:12,130 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_post
[2025-04-28 21:21:12,130 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0_2 given in one single declaration
[2025-04-28 21:21:12,130 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0_2
[2025-04-28 21:21:12,130 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0_2
[2025-04-28 21:21:12,130 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0_1 given in one single declaration
[2025-04-28 21:21:12,131 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0_1
[2025-04-28 21:21:12,131 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0_1
[2025-04-28 21:21:12,131 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0 given in one single declaration
[2025-04-28 21:21:12,131 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0
[2025-04-28 21:21:12,131 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_Block0
[2025-04-28 21:21:12,131 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_pre given in one single declaration
[2025-04-28 21:21:12,131 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_pre
[2025-04-28 21:21:12,131 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.io.PrintStream.CLN void println(java.lang.String)>_pre
[2025-04-28 21:21:12,131 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block12 given in one single declaration
[2025-04-28 21:21:12,131 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block12
[2025-04-28 21:21:12,131 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block12
[2025-04-28 21:21:12,131 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block11_1 given in one single declaration
[2025-04-28 21:21:12,131 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block11_1
[2025-04-28 21:21:12,131 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block11_1
[2025-04-28 21:21:12,131 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block11 given in one single declaration
[2025-04-28 21:21:12,132 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block11
[2025-04-28 21:21:12,132 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block11
[2025-04-28 21:21:12,132 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block4_4 given in one single declaration
[2025-04-28 21:21:12,132 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block4_4
[2025-04-28 21:21:12,132 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block4_4
[2025-04-28 21:21:12,132 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block4_3 given in one single declaration
[2025-04-28 21:21:12,132 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block4_3
[2025-04-28 21:21:12,132 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block4_3
[2025-04-28 21:21:12,132 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:12,132 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_post
[2025-04-28 21:21:12,132 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_post
[2025-04-28 21:21:12,132 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_8 given in one single declaration
[2025-04-28 21:21:12,132 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_8
[2025-04-28 21:21:12,132 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_8
[2025-04-28 21:21:12,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_7 given in one single declaration
[2025-04-28 21:21:12,133 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_7
[2025-04-28 21:21:12,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_7
[2025-04-28 21:21:12,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_6 given in one single declaration
[2025-04-28 21:21:12,133 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_6
[2025-04-28 21:21:12,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_6
[2025-04-28 21:21:12,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_5 given in one single declaration
[2025-04-28 21:21:12,133 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_5
[2025-04-28 21:21:12,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_5
[2025-04-28 21:21:12,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_4 given in one single declaration
[2025-04-28 21:21:12,133 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_4
[2025-04-28 21:21:12,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_4
[2025-04-28 21:21:12,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_3 given in one single declaration
[2025-04-28 21:21:12,134 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_3
[2025-04-28 21:21:12,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_3
[2025-04-28 21:21:12,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_2 given in one single declaration
[2025-04-28 21:21:12,134 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_2
[2025-04-28 21:21:12,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_2
[2025-04-28 21:21:12,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:12,134 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:12,134 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0
[2025-04-28 21:21:12,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_Block0
[2025-04-28 21:21:12,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:12,134 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_pre
[2025-04-28 21:21:12,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.ArrayIndexOutOfBoundsException.CLN void <init>()>_pre
[2025-04-28 21:21:12,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block4_2 given in one single declaration
[2025-04-28 21:21:12,135 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block4_2
[2025-04-28 21:21:12,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block4_2
[2025-04-28 21:21:12,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block4_1 given in one single declaration
[2025-04-28 21:21:12,135 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block4_1
[2025-04-28 21:21:12,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block4_1
[2025-04-28 21:21:12,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block4 given in one single declaration
[2025-04-28 21:21:12,135 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block4
[2025-04-28 21:21:12,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block4
[2025-04-28 21:21:12,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block13 given in one single declaration
[2025-04-28 21:21:12,135 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block13
[2025-04-28 21:21:12,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block13
[2025-04-28 21:21:12,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block12_1 given in one single declaration
[2025-04-28 21:21:12,136 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block12_1
[2025-04-28 21:21:12,136 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block12_1
[2025-04-28 21:21:12,136 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block15 given in one single declaration
[2025-04-28 21:21:12,136 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block15
[2025-04-28 21:21:12,136 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block15
[2025-04-28 21:21:12,136 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block14 given in one single declaration
[2025-04-28 21:21:12,136 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block14
[2025-04-28 21:21:12,136 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block14
[2025-04-28 21:21:12,136 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block2_4 given in one single declaration
[2025-04-28 21:21:12,136 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block2_4
[2025-04-28 21:21:12,136 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block2_4
[2025-04-28 21:21:12,136 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block2_3 given in one single declaration
[2025-04-28 21:21:12,136 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block2_3
[2025-04-28 21:21:12,136 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block2_3
[2025-04-28 21:21:12,136 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block2_2 given in one single declaration
[2025-04-28 21:21:12,136 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block2_2
[2025-04-28 21:21:12,137 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block2_2
[2025-04-28 21:21:12,137 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block2_1 given in one single declaration
[2025-04-28 21:21:12,137 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block2_1
[2025-04-28 21:21:12,137 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block2_1
[2025-04-28 21:21:12,137 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void test(int)>_Block2 given in one single declaration
[2025-04-28 21:21:12,137 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void test(int)>_Block2
[2025-04-28 21:21:12,137 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void test(int)>_Block2
[2025-04-28 21:21:12,137 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:12,137 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_post
[2025-04-28 21:21:12,137 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_post
[2025-04-28 21:21:12,137 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_8 given in one single declaration
[2025-04-28 21:21:12,137 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_8
[2025-04-28 21:21:12,137 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_8
[2025-04-28 21:21:12,137 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_7 given in one single declaration
[2025-04-28 21:21:12,137 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_7
[2025-04-28 21:21:12,138 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_7
[2025-04-28 21:21:12,138 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_6 given in one single declaration
[2025-04-28 21:21:12,138 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_6
[2025-04-28 21:21:12,138 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_6
[2025-04-28 21:21:12,138 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_5 given in one single declaration
[2025-04-28 21:21:12,138 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_5
[2025-04-28 21:21:12,138 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_5
[2025-04-28 21:21:12,138 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_4 given in one single declaration
[2025-04-28 21:21:12,138 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_4
[2025-04-28 21:21:12,138 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_4
[2025-04-28 21:21:12,138 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_3 given in one single declaration
[2025-04-28 21:21:12,138 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_3
[2025-04-28 21:21:12,138 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_3
[2025-04-28 21:21:12,138 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_2 given in one single declaration
[2025-04-28 21:21:12,139 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_2
[2025-04-28 21:21:12,139 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_2
[2025-04-28 21:21:12,139 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:12,139 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,139 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0_1
[2025-04-28 21:21:12,139 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:12,139 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0
[2025-04-28 21:21:12,139 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_Block0
[2025-04-28 21:21:12,139 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:12,139 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NullPointerException.CLN void <init>()>_pre
[2025-04-28 21:21:12,139 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NullPointerException.CLN void <init>()>_pre
[2025-04-28 21:21:12,140 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH1.CLN Main.java, line 34 given in one single declaration
[2025-04-28 21:21:12,140 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH1.CLN Main.java, line 34
[2025-04-28 21:21:12,140 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH1.CLN Main.java, line 34
[2025-04-28 21:21:12,140 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH3.CLN Main.java, line 42 given in one single declaration
[2025-04-28 21:21:12,140 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH3.CLN Main.java, line 42
[2025-04-28 21:21:12,140 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH3.CLN Main.java, line 42
[2025-04-28 21:21:12,140 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:12,140 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:12,140 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:12,954 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:12,958 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:14,055 INFO  L?                        ?]: Removed 111 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:14,056 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:14,095 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:14,095 INFO  L312             CfgBuilder]: Removed 48 assume(true) statements.
[2025-04-28 21:21:14,096 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14 BoogieIcfgContainer
[2025-04-28 21:21:14,096 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:14,098 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:14,098 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:14,106 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:14,106 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:11" (1/3) ...
[2025-04-28 21:21:14,107 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@10f22a0c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,111 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (2/3) ...
[2025-04-28 21:21:14,111 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@10f22a0c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,111 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14" (3/3) ...
[2025-04-28 21:21:14,113 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:14,125 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:14,127 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 155 procedures, 607 locations, 846 edges, 155 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:14,179 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:14,200 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;@227322f1, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:14,200 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:14,211 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 607 states, 269 states have (on average 1.037174721189591) internal successors, (279), 279 states have internal predecessors, (279), 183 states have call successors, (189), 154 states have call predecessors, (189), 154 states have return successors, (189), 173 states have call predecessors, (189), 183 states have call successors, (189)
[2025-04-28 21:21:14,327 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 1370
[2025-04-28 21:21:14,328 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,329 INFO  L218           NwaCegarLoop]: trace histogram [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 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, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:14,330 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,337 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,338 INFO  L85        PathProgramCache]: Analyzing trace with hash 161219995, now seen corresponding path program 1 times
[2025-04-28 21:21:14,346 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,347 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1798313727]
[2025-04-28 21:21:14,348 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,349 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,872 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 1369 statements into 1 equivalence classes.
[2025-04-28 21:21:15,644 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 1369 of 1369 statements.
[2025-04-28 21:21:15,645 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,645 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,152 INFO  L134       CoverageAnalysis]: Checked inductivity of 9503 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9503 trivial. 0 not checked.
[2025-04-28 21:21:19,154 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,154 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1798313727]
[2025-04-28 21:21:19,155 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1798313727] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,155 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,159 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:19,161 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1442646553]
[2025-04-28 21:21:19,162 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,190 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:19,191 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,263 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:19,265 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:19,269 INFO  L87              Difference]: Start difference. First operand  has 607 states, 269 states have (on average 1.037174721189591) internal successors, (279), 279 states have internal predecessors, (279), 183 states have call successors, (189), 154 states have call predecessors, (189), 154 states have return successors, (189), 173 states have call predecessors, (189), 183 states have call successors, (189) Second operand  has 4 states, 3 states have (on average 33.0) internal successors, (99), 4 states have internal predecessors, (99), 3 states have call successors, (65), 1 states have call predecessors, (65), 3 states have return successors, (65), 3 states have call predecessors, (65), 3 states have call successors, (65)
[2025-04-28 21:21:19,509 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,509 INFO  L93              Difference]: Finished difference Result 607 states and 657 transitions.
[2025-04-28 21:21:19,512 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:19,514 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 33.0) internal successors, (99), 4 states have internal predecessors, (99), 3 states have call successors, (65), 1 states have call predecessors, (65), 3 states have return successors, (65), 3 states have call predecessors, (65), 3 states have call successors, (65) Word has length 1369
[2025-04-28 21:21:19,522 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,547 INFO  L225             Difference]: With dead ends: 607
[2025-04-28 21:21:19,548 INFO  L226             Difference]: Without dead ends: 607
[2025-04-28 21:21:19,550 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:19,554 INFO  L437           NwaCegarLoop]: 654 mSDtfsCounter, 1 mSDsluCounter, 1300 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1954 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,555 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1954 Invalid, 6 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:19,583 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 607 states.
[2025-04-28 21:21:19,670 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 607 to 607.
[2025-04-28 21:21:19,672 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 607 states, 269 states have (on average 1.033457249070632) internal successors, (278), 278 states have internal predecessors, (278), 183 states have call successors, (189), 154 states have call predecessors, (189), 155 states have return successors, (190), 174 states have call predecessors, (190), 183 states have call successors, (190)
[2025-04-28 21:21:19,684 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 607 states to 607 states and 657 transitions.
[2025-04-28 21:21:19,685 INFO  L79                 Accepts]: Start accepts. Automaton has 607 states and 657 transitions. Word has length 1369
[2025-04-28 21:21:19,692 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,693 INFO  L485      AbstractCegarLoop]: Abstraction has 607 states and 657 transitions.
[2025-04-28 21:21:19,693 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 33.0) internal successors, (99), 4 states have internal predecessors, (99), 3 states have call successors, (65), 1 states have call predecessors, (65), 3 states have return successors, (65), 3 states have call predecessors, (65), 3 states have call successors, (65)
[2025-04-28 21:21:19,693 INFO  L278                IsEmpty]: Start isEmpty. Operand 607 states and 657 transitions.
[2025-04-28 21:21:19,814 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 1370
[2025-04-28 21:21:19,814 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,814 INFO  L218           NwaCegarLoop]: trace histogram [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 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, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:19,815 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:19,816 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,816 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,817 INFO  L85        PathProgramCache]: Analyzing trace with hash 386545105, now seen corresponding path program 1 times
[2025-04-28 21:21:19,817 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,817 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [426663144]
[2025-04-28 21:21:19,817 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,817 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,137 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 1369 statements into 1 equivalence classes.
[2025-04-28 21:21:20,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 1369 of 1369 statements.
[2025-04-28 21:21:20,407 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,407 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,394 INFO  L134       CoverageAnalysis]: Checked inductivity of 9503 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9503 trivial. 0 not checked.
[2025-04-28 21:21:24,394 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,395 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [426663144]
[2025-04-28 21:21:24,395 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [426663144] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:24,395 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:24,395 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:24,395 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1412000014]
[2025-04-28 21:21:24,395 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,400 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:24,400 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,403 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:24,403 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:24,404 INFO  L87              Difference]: Start difference. First operand 607 states and 657 transitions. Second operand  has 8 states, 7 states have (on average 14.142857142857142) internal successors, (99), 8 states have internal predecessors, (99), 4 states have call successors, (65), 1 states have call predecessors, (65), 7 states have return successors, (65), 7 states have call predecessors, (65), 4 states have call successors, (65)
[2025-04-28 21:21:24,575 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,575 INFO  L93              Difference]: Finished difference Result 616 states and 667 transitions.
[2025-04-28 21:21:24,576 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:24,576 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 14.142857142857142) internal successors, (99), 8 states have internal predecessors, (99), 4 states have call successors, (65), 1 states have call predecessors, (65), 7 states have return successors, (65), 7 states have call predecessors, (65), 4 states have call successors, (65) Word has length 1369
[2025-04-28 21:21:24,585 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,591 INFO  L225             Difference]: With dead ends: 616
[2025-04-28 21:21:24,595 INFO  L226             Difference]: Without dead ends: 616
[2025-04-28 21:21:24,595 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:24,596 INFO  L437           NwaCegarLoop]: 652 mSDtfsCounter, 1 mSDsluCounter, 3902 mSDsCounter, 0 mSdLazyCounter, 38 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 4554 SdHoareTripleChecker+Invalid, 38 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 38 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,598 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 4554 Invalid, 38 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 38 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:24,601 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 616 states.
[2025-04-28 21:21:24,651 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 616 to 616.
[2025-04-28 21:21:24,654 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 616 states, 273 states have (on average 1.032967032967033) internal successors, (282), 282 states have internal predecessors, (282), 184 states have call successors, (190), 154 states have call predecessors, (190), 159 states have return successors, (195), 179 states have call predecessors, (195), 184 states have call successors, (195)
[2025-04-28 21:21:24,666 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 616 states to 616 states and 667 transitions.
[2025-04-28 21:21:24,670 INFO  L79                 Accepts]: Start accepts. Automaton has 616 states and 667 transitions. Word has length 1369
[2025-04-28 21:21:24,673 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,673 INFO  L485      AbstractCegarLoop]: Abstraction has 616 states and 667 transitions.
[2025-04-28 21:21:24,673 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 14.142857142857142) internal successors, (99), 8 states have internal predecessors, (99), 4 states have call successors, (65), 1 states have call predecessors, (65), 7 states have return successors, (65), 7 states have call predecessors, (65), 4 states have call successors, (65)
[2025-04-28 21:21:24,677 INFO  L278                IsEmpty]: Start isEmpty. Operand 616 states and 667 transitions.
[2025-04-28 21:21:24,712 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 1370
[2025-04-28 21:21:24,713 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,713 INFO  L218           NwaCegarLoop]: trace histogram [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 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, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:24,714 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:24,714 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,714 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,715 INFO  L85        PathProgramCache]: Analyzing trace with hash 1129010808, now seen corresponding path program 1 times
[2025-04-28 21:21:24,715 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,715 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1961848168]
[2025-04-28 21:21:24,715 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,715 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,012 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 1369 statements into 1 equivalence classes.
[2025-04-28 21:21:25,172 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 1369 of 1369 statements.
[2025-04-28 21:21:25,173 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,173 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,412 INFO  L134       CoverageAnalysis]: Checked inductivity of 9503 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9503 trivial. 0 not checked.
[2025-04-28 21:21:27,412 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,412 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1961848168]
[2025-04-28 21:21:27,413 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1961848168] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,413 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,413 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:27,413 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1250466682]
[2025-04-28 21:21:27,413 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,414 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:27,415 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,416 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:27,416 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:27,416 INFO  L87              Difference]: Start difference. First operand 616 states and 667 transitions. Second operand  has 7 states, 6 states have (on average 16.5) internal successors, (99), 7 states have internal predecessors, (99), 5 states have call successors, (65), 1 states have call predecessors, (65), 6 states have return successors, (65), 6 states have call predecessors, (65), 5 states have call successors, (65)
[2025-04-28 21:21:27,528 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,528 INFO  L93              Difference]: Finished difference Result 601 states and 648 transitions.
[2025-04-28 21:21:27,530 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:27,531 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 16.5) internal successors, (99), 7 states have internal predecessors, (99), 5 states have call successors, (65), 1 states have call predecessors, (65), 6 states have return successors, (65), 6 states have call predecessors, (65), 5 states have call successors, (65) Word has length 1369
[2025-04-28 21:21:27,533 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,537 INFO  L225             Difference]: With dead ends: 601
[2025-04-28 21:21:27,540 INFO  L226             Difference]: Without dead ends: 595
[2025-04-28 21:21:27,540 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:27,545 INFO  L437           NwaCegarLoop]: 644 mSDtfsCounter, 0 mSDsluCounter, 3206 mSDsCounter, 0 mSdLazyCounter, 27 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 3850 SdHoareTripleChecker+Invalid, 27 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 27 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,545 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 3850 Invalid, 27 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 27 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:27,547 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 595 states.
[2025-04-28 21:21:27,566 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 595 to 595.
[2025-04-28 21:21:27,568 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 595 states, 264 states have (on average 1.0265151515151516) internal successors, (271), 271 states have internal predecessors, (271), 179 states have call successors, (184), 152 states have call predecessors, (184), 152 states have return successors, (184), 171 states have call predecessors, (184), 179 states have call successors, (184)
[2025-04-28 21:21:27,572 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 595 states to 595 states and 639 transitions.
[2025-04-28 21:21:27,573 INFO  L79                 Accepts]: Start accepts. Automaton has 595 states and 639 transitions. Word has length 1369
[2025-04-28 21:21:27,573 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,573 INFO  L485      AbstractCegarLoop]: Abstraction has 595 states and 639 transitions.
[2025-04-28 21:21:27,573 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 16.5) internal successors, (99), 7 states have internal predecessors, (99), 5 states have call successors, (65), 1 states have call predecessors, (65), 6 states have return successors, (65), 6 states have call predecessors, (65), 5 states have call successors, (65)
[2025-04-28 21:21:27,574 INFO  L278                IsEmpty]: Start isEmpty. Operand 595 states and 639 transitions.
[2025-04-28 21:21:27,756 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 5057
[2025-04-28 21:21:27,756 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,758 INFO  L218           NwaCegarLoop]: trace histogram [99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 55, 55, 55, 55, 55, 55, 55, 55, 55, 55, 55, 55, 55, 55, 55, 44, 44, 44, 44, 44, 44, 44, 44, 44, 44, 44, 44, 44, 44, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27,758 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:27,758 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,760 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,760 INFO  L85        PathProgramCache]: Analyzing trace with hash 1125513121, now seen corresponding path program 1 times
[2025-04-28 21:21:27,760 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,762 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [276995791]
[2025-04-28 21:21:27,763 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,763 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,825 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5056 statements into 1 equivalence classes.
[2025-04-28 21:21:29,519 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5056 of 5056 statements.
[2025-04-28 21:21:29,519 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,519 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
