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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:41,345 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:41,433 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fdc1a649-ad5b-4558-842d-b8c0f50b0c70/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:41,437 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:41,438 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:41,476 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:41,477 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:41,477 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:41,478 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:41,479 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:41,480 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:41,480 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:41,480 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:41,480 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:41,480 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:41,480 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:41,480 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,481 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:41,481 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:41,482 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:41,482 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:41,817 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:41,829 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:41,832 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:41,835 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:41,836 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:41,837 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fdc1a649-ad5b-4558-842d-b8c0f50b0c70/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-235.smt2
[2025-04-28 21:21:41,838 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:41,843 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:44,194 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fdc1a649-ad5b-4558-842d-b8c0f50b0c70/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-235.smt2
[2025-04-28 21:21:44,198 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:44,200 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:44,202 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:44,202 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:44,202 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:44,209 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,498 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44 Unit
[2025-04-28 21:21:44,499 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:44,500 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:44,500 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:44,500 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:44,517 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,517 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,668 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,668 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,738 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,746 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,749 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,769 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,784 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,889 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:44,890 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:44,890 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:44,890 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:44,891 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,894 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:44,909 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,924 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:44,931 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:44,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:44,949 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:44,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:44,950 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:44,950 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:44,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:44,951 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_1 given in one single declaration
[2025-04-28 21:21:44,951 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_1
[2025-04-28 21:21:44,951 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_1
[2025-04-28 21:21:44,951 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25 given in one single declaration
[2025-04-28 21:21:44,951 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25
[2025-04-28 21:21:44,951 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25
[2025-04-28 21:21:44,951 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block24 given in one single declaration
[2025-04-28 21:21:44,951 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block24
[2025-04-28 21:21:44,952 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block24
[2025-04-28 21:21:44,952 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block22_1 given in one single declaration
[2025-04-28 21:21:44,952 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block22_1
[2025-04-28 21:21:44,952 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block22_1
[2025-04-28 21:21:44,954 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block22 given in one single declaration
[2025-04-28 21:21:44,954 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block22
[2025-04-28 21:21:44,954 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block22
[2025-04-28 21:21:44,954 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block21_1 given in one single declaration
[2025-04-28 21:21:44,954 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block21_1
[2025-04-28 21:21:44,954 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block21_1
[2025-04-28 21:21:44,954 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block21 given in one single declaration
[2025-04-28 21:21:44,954 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block21
[2025-04-28 21:21:44,955 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block21
[2025-04-28 21:21:44,955 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19 given in one single declaration
[2025-04-28 21:21:44,955 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19
[2025-04-28 21:21:44,955 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19
[2025-04-28 21:21:44,955 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17_1 given in one single declaration
[2025-04-28 21:21:44,955 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17_1
[2025-04-28 21:21:44,955 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17_1
[2025-04-28 21:21:44,955 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN int nextInt()>_post given in one single declaration
[2025-04-28 21:21:44,955 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN int nextInt()>_post
[2025-04-28 21:21:44,955 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN int nextInt()>_post
[2025-04-28 21:21:44,955 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN int nextInt()>_Block0_2 given in one single declaration
[2025-04-28 21:21:44,955 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN int nextInt()>_Block0_2
[2025-04-28 21:21:44,955 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN int nextInt()>_Block0_2
[2025-04-28 21:21:44,955 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN int nextInt()>_Block0_1 given in one single declaration
[2025-04-28 21:21:44,955 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN int nextInt()>_Block0_1
[2025-04-28 21:21:44,956 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN int nextInt()>_Block0_1
[2025-04-28 21:21:44,956 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN int nextInt()>_Block0 given in one single declaration
[2025-04-28 21:21:44,956 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN int nextInt()>_Block0
[2025-04-28 21:21:44,956 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN int nextInt()>_Block0
[2025-04-28 21:21:44,956 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN int nextInt()>_pre given in one single declaration
[2025-04-28 21:21:44,956 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN int nextInt()>_pre
[2025-04-28 21:21:44,956 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN int nextInt()>_pre
[2025-04-28 21:21:44,956 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17 given in one single declaration
[2025-04-28 21:21:44,956 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17
[2025-04-28 21:21:44,956 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17
[2025-04-28 21:21:44,956 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_8 given in one single declaration
[2025-04-28 21:21:44,957 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_8
[2025-04-28 21:21:44,957 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_8
[2025-04-28 21:21:44,957 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_7 given in one single declaration
[2025-04-28 21:21:44,957 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_7
[2025-04-28 21:21:44,958 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_7
[2025-04-28 21:21:44,958 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:44,958 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_post
[2025-04-28 21:21:44,958 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_post
[2025-04-28 21:21:44,958 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0_6 given in one single declaration
[2025-04-28 21:21:44,958 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0_6
[2025-04-28 21:21:44,959 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0_6
[2025-04-28 21:21:44,959 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0_5 given in one single declaration
[2025-04-28 21:21:44,959 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0_5
[2025-04-28 21:21:44,959 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0_5
[2025-04-28 21:21:44,959 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0_4 given in one single declaration
[2025-04-28 21:21:44,959 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0_4
[2025-04-28 21:21:44,960 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0_4
[2025-04-28 21:21:44,960 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0_3 given in one single declaration
[2025-04-28 21:21:44,960 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0_3
[2025-04-28 21:21:44,960 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0_3
[2025-04-28 21:21:44,960 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0_2 given in one single declaration
[2025-04-28 21:21:44,960 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0_2
[2025-04-28 21:21:44,960 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0_2
[2025-04-28 21:21:44,960 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:44,960 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0_1
[2025-04-28 21:21:44,960 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0_1
[2025-04-28 21:21:44,960 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:44,960 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_Block0
[2025-04-28 21:21:44,960 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_Block0
[2025-04-28 21:21:44,960 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:44,960 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void <init>()>_pre
[2025-04-28 21:21:44,960 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void <init>()>_pre
[2025-04-28 21:21:44,960 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_1 given in one single declaration
[2025-04-28 21:21:44,961 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_1
[2025-04-28 21:21:44,961 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_1
[2025-04-28 21:21:44,961 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20 given in one single declaration
[2025-04-28 21:21:44,961 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20
[2025-04-28 21:21:44,961 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20
[2025-04-28 21:21:44,962 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_1 given in one single declaration
[2025-04-28 21:21:44,962 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_1
[2025-04-28 21:21:44,962 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_1
[2025-04-28 21:21:44,962 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26 given in one single declaration
[2025-04-28 21:21:44,962 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26
[2025-04-28 21:21:44,962 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26
[2025-04-28 21:21:44,962 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_1 given in one single declaration
[2025-04-28 21:21:44,962 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_1
[2025-04-28 21:21:44,963 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_1
[2025-04-28 21:21:44,963 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28 given in one single declaration
[2025-04-28 21:21:44,963 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28
[2025-04-28 21:21:44,963 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28
[2025-04-28 21:21:44,963 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_5 given in one single declaration
[2025-04-28 21:21:44,963 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_5
[2025-04-28 21:21:44,963 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_5
[2025-04-28 21:21:44,963 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_4 given in one single declaration
[2025-04-28 21:21:44,963 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_4
[2025-04-28 21:21:44,964 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_4
[2025-04-28 21:21:44,964 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_3 given in one single declaration
[2025-04-28 21:21:44,964 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_3
[2025-04-28 21:21:44,964 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_3
[2025-04-28 21:21:44,964 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_post given in one single declaration
[2025-04-28 21:21:44,964 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_post
[2025-04-28 21:21:44,964 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_post
[2025-04-28 21:21:44,964 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block0 given in one single declaration
[2025-04-28 21:21:44,965 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block0
[2025-04-28 21:21:44,965 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block0
[2025-04-28 21:21:44,965 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_6 given in one single declaration
[2025-04-28 21:21:44,965 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1_6
[2025-04-28 21:21:44,965 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_6
[2025-04-28 21:21:44,965 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_5 given in one single declaration
[2025-04-28 21:21:44,965 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1_5
[2025-04-28 21:21:44,965 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_5
[2025-04-28 21:21:44,965 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_4 given in one single declaration
[2025-04-28 21:21:44,965 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1_4
[2025-04-28 21:21:44,965 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_4
[2025-04-28 21:21:44,965 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_3 given in one single declaration
[2025-04-28 21:21:44,967 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1_3
[2025-04-28 21:21:44,968 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_3
[2025-04-28 21:21:44,968 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_2 given in one single declaration
[2025-04-28 21:21:44,968 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1_2
[2025-04-28 21:21:44,968 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_2
[2025-04-28 21:21:44,968 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_1 given in one single declaration
[2025-04-28 21:21:44,968 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1_1
[2025-04-28 21:21:44,968 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1_1
[2025-04-28 21:21:44,968 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1 given in one single declaration
[2025-04-28 21:21:44,968 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_Block1
[2025-04-28 21:21:44,968 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_Block1
[2025-04-28 21:21:44,968 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayArray_byte.CLN void <init>(int)>_pre given in one single declaration
[2025-04-28 21:21:44,968 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayArray_byte.CLN void <init>(int)>_pre
[2025-04-28 21:21:44,968 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayArray_byte.CLN void <init>(int)>_pre
[2025-04-28 21:21:44,968 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_2 given in one single declaration
[2025-04-28 21:21:44,968 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_2
[2025-04-28 21:21:44,968 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block26_2
[2025-04-28 21:21:44,969 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_post given in one single declaration
[2025-04-28 21:21:44,969 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_post
[2025-04-28 21:21:44,969 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_post
[2025-04-28 21:21:44,969 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0_2 given in one single declaration
[2025-04-28 21:21:44,969 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0_2
[2025-04-28 21:21:44,969 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0_2
[2025-04-28 21:21:44,969 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0_1 given in one single declaration
[2025-04-28 21:21:44,969 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0_1
[2025-04-28 21:21:44,969 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0_1
[2025-04-28 21:21:44,969 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0 given in one single declaration
[2025-04-28 21:21:44,969 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0
[2025-04-28 21:21:44,969 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_Block0
[2025-04-28 21:21:44,969 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_pre given in one single declaration
[2025-04-28 21:21:44,969 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_pre
[2025-04-28 21:21:44,969 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.util.Random.CLN void nextBytes(JayArray_byte)>_pre
[2025-04-28 21:21:44,969 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_6 given in one single declaration
[2025-04-28 21:21:44,969 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_6
[2025-04-28 21:21:44,969 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_6
[2025-04-28 21:21:44,970 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_5 given in one single declaration
[2025-04-28 21:21:44,970 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_5
[2025-04-28 21:21:44,970 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_5
[2025-04-28 21:21:44,970 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_4 given in one single declaration
[2025-04-28 21:21:44,970 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_4
[2025-04-28 21:21:44,970 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_4
[2025-04-28 21:21:44,970 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_3 given in one single declaration
[2025-04-28 21:21:44,970 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_3
[2025-04-28 21:21:44,970 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_3
[2025-04-28 21:21:44,970 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_2 given in one single declaration
[2025-04-28 21:21:44,970 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_2
[2025-04-28 21:21:44,970 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_2
[2025-04-28 21:21:44,970 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_1 given in one single declaration
[2025-04-28 21:21:44,970 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_1
[2025-04-28 21:21:44,970 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8_1
[2025-04-28 21:21:44,970 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8 given in one single declaration
[2025-04-28 21:21:44,970 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8
[2025-04-28 21:21:44,970 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block8
[2025-04-28 21:21:44,971 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:44,971 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:44,971 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:44,971 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block2_1 given in one single declaration
[2025-04-28 21:21:44,971 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block2_1
[2025-04-28 21:21:44,971 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block2_1
[2025-04-28 21:21:44,971 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block2 given in one single declaration
[2025-04-28 21:21:44,971 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block2
[2025-04-28 21:21:44,971 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block2
[2025-04-28 21:21:44,971 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0_2 given in one single declaration
[2025-04-28 21:21:44,971 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0_2
[2025-04-28 21:21:44,971 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0_2
[2025-04-28 21:21:44,971 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0_1 given in one single declaration
[2025-04-28 21:21:44,971 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0_1
[2025-04-28 21:21:44,971 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0_1
[2025-04-28 21:21:44,971 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0 given in one single declaration
[2025-04-28 21:21:44,971 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0
[2025-04-28 21:21:44,972 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_Block0
[2025-04-28 21:21:44,972 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_pre given in one single declaration
[2025-04-28 21:21:44,972 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_pre
[2025-04-28 21:21:44,972 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN java.lang.String substring(int,int)>_pre
[2025-04-28 21:21:44,972 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_4 given in one single declaration
[2025-04-28 21:21:44,974 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_4
[2025-04-28 21:21:44,975 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_4
[2025-04-28 21:21:44,975 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_3 given in one single declaration
[2025-04-28 21:21:44,975 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_3
[2025-04-28 21:21:44,975 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_3
[2025-04-28 21:21:44,976 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_2 given in one single declaration
[2025-04-28 21:21:44,976 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_2
[2025-04-28 21:21:44,976 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_2
[2025-04-28 21:21:44,976 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1 given in one single declaration
[2025-04-28 21:21:44,976 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1
[2025-04-28 21:21:44,976 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1
[2025-04-28 21:21:44,976 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14 given in one single declaration
[2025-04-28 21:21:44,976 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14
[2025-04-28 21:21:44,976 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14
[2025-04-28 21:21:44,976 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block30_1 given in one single declaration
[2025-04-28 21:21:44,976 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block30_1
[2025-04-28 21:21:44,976 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block30_1
[2025-04-28 21:21:44,976 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block30 given in one single declaration
[2025-04-28 21:21:44,976 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block30
[2025-04-28 21:21:44,977 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block30
[2025-04-28 21:21:44,977 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_3 given in one single declaration
[2025-04-28 21:21:44,977 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_3
[2025-04-28 21:21:44,977 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_3
[2025-04-28 21:21:44,977 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_2 given in one single declaration
[2025-04-28 21:21:44,977 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_2
[2025-04-28 21:21:44,977 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block28_2
[2025-04-28 21:21:44,977 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_post given in one single declaration
[2025-04-28 21:21:44,977 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_post
[2025-04-28 21:21:44,977 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_post
[2025-04-28 21:21:44,977 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_5 given in one single declaration
[2025-04-28 21:21:44,977 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_5
[2025-04-28 21:21:44,977 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_5
[2025-04-28 21:21:44,977 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_4 given in one single declaration
[2025-04-28 21:21:44,978 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_4
[2025-04-28 21:21:44,978 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_4
[2025-04-28 21:21:44,978 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_3 given in one single declaration
[2025-04-28 21:21:44,978 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_3
[2025-04-28 21:21:44,978 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_3
[2025-04-28 21:21:44,978 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_2 given in one single declaration
[2025-04-28 21:21:44,978 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_2
[2025-04-28 21:21:44,978 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_2
[2025-04-28 21:21:44,978 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_1 given in one single declaration
[2025-04-28 21:21:44,978 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_1
[2025-04-28 21:21:44,978 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0_1
[2025-04-28 21:21:44,978 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0 given in one single declaration
[2025-04-28 21:21:44,978 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0
[2025-04-28 21:21:44,978 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_Block0
[2025-04-28 21:21:44,979 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_pre given in one single declaration
[2025-04-28 21:21:44,979 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_pre
[2025-04-28 21:21:44,979 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.String.CLN void <init>(JayArray_byte)>_pre
[2025-04-28 21:21:44,979 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block27_1 given in one single declaration
[2025-04-28 21:21:44,979 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block27_1
[2025-04-28 21:21:44,979 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block27_1
[2025-04-28 21:21:44,979 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block27 given in one single declaration
[2025-04-28 21:21:44,979 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block27
[2025-04-28 21:21:44,979 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block27
[2025-04-28 21:21:44,979 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block23_1 given in one single declaration
[2025-04-28 21:21:44,979 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block23_1
[2025-04-28 21:21:44,981 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block23_1
[2025-04-28 21:21:44,981 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block23 given in one single declaration
[2025-04-28 21:21:44,981 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block23
[2025-04-28 21:21:44,982 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block23
[2025-04-28 21:21:44,982 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_5 given in one single declaration
[2025-04-28 21:21:44,982 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_5
[2025-04-28 21:21:44,982 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_5
[2025-04-28 21:21:44,982 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_4 given in one single declaration
[2025-04-28 21:21:44,982 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_4
[2025-04-28 21:21:44,982 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_4
[2025-04-28 21:21:44,982 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_3 given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_3
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_3
[2025-04-28 21:21:44,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_post given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_post
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_post
[2025-04-28 21:21:44,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_8 given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_8
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_8
[2025-04-28 21:21:44,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_7 given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_7
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_7
[2025-04-28 21:21:44,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_6 given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_6
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_6
[2025-04-28 21:21:44,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_5 given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_5
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_5
[2025-04-28 21:21:44,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_4 given in one single declaration
[2025-04-28 21:21:44,983 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_4
[2025-04-28 21:21:44,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_4
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_3 given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_3
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_3
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_2 given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_2
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_2
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_1 given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_1
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0_1
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0 given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_Block0
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_pre given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_pre
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <java.lang.NegativeArraySizeException.CLN void <init>()>_pre
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_2 given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_2
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block25_2
[2025-04-28 21:21:44,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18_1 given in one single declaration
[2025-04-28 21:21:44,984 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18_1
[2025-04-28 21:21:44,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18_1
[2025-04-28 21:21:44,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18 given in one single declaration
[2025-04-28 21:21:44,985 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18
[2025-04-28 21:21:44,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18
[2025-04-28 21:21:44,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16_1 given in one single declaration
[2025-04-28 21:21:44,985 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16_1
[2025-04-28 21:21:44,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16_1
[2025-04-28 21:21:44,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16 given in one single declaration
[2025-04-28 21:21:44,986 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16
[2025-04-28 21:21:44,986 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16
[2025-04-28 21:21:44,986 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block29_1 given in one single declaration
[2025-04-28 21:21:44,986 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block29_1
[2025-04-28 21:21:44,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block29_1
[2025-04-28 21:21:44,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block29 given in one single declaration
[2025-04-28 21:21:44,987 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block29
[2025-04-28 21:21:44,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block29
[2025-04-28 21:21:44,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:44,988 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:44,988 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:48,326 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:48,331 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:51,915 INFO  L?                        ?]: Removed 171 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:51,916 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:51,945 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:51,946 INFO  L312             CfgBuilder]: Removed 35 assume(true) statements.
[2025-04-28 21:21:51,946 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:51 BoogieIcfgContainer
[2025-04-28 21:21:51,946 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:51,949 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:51,949 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:51,954 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:51,954 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:44" (1/3) ...
[2025-04-28 21:21:51,955 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@31d3974b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:51, skipping insertion in model container
[2025-04-28 21:21:51,955 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (2/3) ...
[2025-04-28 21:21:51,955 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@31d3974b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:51, skipping insertion in model container
[2025-04-28 21:21:51,955 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:51" (3/3) ...
[2025-04-28 21:21:51,957 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:51,978 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:51,981 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 110 procedures, 437 locations, 635 edges, 110 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:52,055 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:52,069 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;@107fa9fd, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:52,069 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:52,079 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 437 states, 192 states have (on average 1.1041666666666667) internal successors, (212), 212 states have internal predecessors, (212), 134 states have call successors, (141), 109 states have call predecessors, (141), 109 states have return successors, (141), 115 states have call predecessors, (141), 134 states have call successors, (141)
[2025-04-28 21:21:52,108 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:52,112 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,113 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,113 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,119 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,120 INFO  L85        PathProgramCache]: Analyzing trace with hash 1976972784, now seen corresponding path program 1 times
[2025-04-28 21:21:52,129 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,130 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1604788757]
[2025-04-28 21:21:52,130 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,130 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:52,583 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:52,583 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,583 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,505 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:53,506 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,506 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1604788757]
[2025-04-28 21:21:53,507 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1604788757] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,507 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,511 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:53,517 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [979987740]
[2025-04-28 21:21:53,521 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,530 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:53,530 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,601 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:53,605 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,609 INFO  L87              Difference]: Start difference. First operand  has 437 states, 192 states have (on average 1.1041666666666667) internal successors, (212), 212 states have internal predecessors, (212), 134 states have call successors, (141), 109 states have call predecessors, (141), 109 states have return successors, (141), 115 states have call predecessors, (141), 134 states have call successors, (141) Second operand  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:54,175 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,176 INFO  L93              Difference]: Finished difference Result 435 states and 491 transitions.
[2025-04-28 21:21:54,182 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,184 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10) Word has length 39
[2025-04-28 21:21:54,184 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,200 INFO  L225             Difference]: With dead ends: 435
[2025-04-28 21:21:54,201 INFO  L226             Difference]: Without dead ends: 434
[2025-04-28 21:21:54,203 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,206 INFO  L437           NwaCegarLoop]: 486 mSDtfsCounter, 0 mSDsluCounter, 1926 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2412 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,207 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2412 Invalid, 35 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:54,227 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 434 states.
[2025-04-28 21:21:54,300 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 434 to 434.
[2025-04-28 21:21:54,302 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 434 states, 191 states have (on average 1.094240837696335) internal successors, (209), 209 states have internal predecessors, (209), 133 states have call successors, (140), 109 states have call predecessors, (140), 109 states have return successors, (140), 115 states have call predecessors, (140), 133 states have call successors, (140)
[2025-04-28 21:21:54,312 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 434 states to 434 states and 489 transitions.
[2025-04-28 21:21:54,314 INFO  L79                 Accepts]: Start accepts. Automaton has 434 states and 489 transitions. Word has length 39
[2025-04-28 21:21:54,314 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,315 INFO  L485      AbstractCegarLoop]: Abstraction has 434 states and 489 transitions.
[2025-04-28 21:21:54,315 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:54,315 INFO  L278                IsEmpty]: Start isEmpty. Operand 434 states and 489 transitions.
[2025-04-28 21:21:54,318 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:54,321 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,322 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,322 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:54,322 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,323 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,323 INFO  L85        PathProgramCache]: Analyzing trace with hash -1719526930, now seen corresponding path program 1 times
[2025-04-28 21:21:54,323 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,323 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [18111832]
[2025-04-28 21:21:54,323 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,323 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,454 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:54,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:54,497 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,498 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,002 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:55,002 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,002 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [18111832]
[2025-04-28 21:21:55,003 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [18111832] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,003 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,003 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,003 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1786083226]
[2025-04-28 21:21:55,003 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,004 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,005 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,006 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,008 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,008 INFO  L87              Difference]: Start difference. First operand 434 states and 489 transitions. Second operand  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:55,267 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,268 INFO  L93              Difference]: Finished difference Result 434 states and 488 transitions.
[2025-04-28 21:21:55,269 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,270 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10) Word has length 39
[2025-04-28 21:21:55,270 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,277 INFO  L225             Difference]: With dead ends: 434
[2025-04-28 21:21:55,278 INFO  L226             Difference]: Without dead ends: 433
[2025-04-28 21:21:55,278 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,279 INFO  L437           NwaCegarLoop]: 484 mSDtfsCounter, 0 mSDsluCounter, 1920 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2404 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,279 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2404 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:55,281 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 433 states.
[2025-04-28 21:21:55,323 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 433 to 433.
[2025-04-28 21:21:55,324 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 433 states, 191 states have (on average 1.0890052356020943) internal successors, (208), 208 states have internal predecessors, (208), 132 states have call successors, (139), 109 states have call predecessors, (139), 109 states have return successors, (139), 115 states have call predecessors, (139), 132 states have call successors, (139)
[2025-04-28 21:21:55,329 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 433 states to 433 states and 486 transitions.
[2025-04-28 21:21:55,332 INFO  L79                 Accepts]: Start accepts. Automaton has 433 states and 486 transitions. Word has length 39
[2025-04-28 21:21:55,332 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,332 INFO  L485      AbstractCegarLoop]: Abstraction has 433 states and 486 transitions.
[2025-04-28 21:21:55,332 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:55,332 INFO  L278                IsEmpty]: Start isEmpty. Operand 433 states and 486 transitions.
[2025-04-28 21:21:55,334 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:55,336 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,336 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,336 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:55,337 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,337 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,341 INFO  L85        PathProgramCache]: Analyzing trace with hash -397358097, now seen corresponding path program 1 times
[2025-04-28 21:21:55,341 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,341 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [671013614]
[2025-04-28 21:21:55,341 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,341 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,455 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:55,503 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:55,504 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,504 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,173 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:56,173 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,173 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [671013614]
[2025-04-28 21:21:56,173 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [671013614] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,173 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,173 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:56,174 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1049244231]
[2025-04-28 21:21:56,174 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,174 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:56,174 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,175 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:56,175 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:56,175 INFO  L87              Difference]: Start difference. First operand 433 states and 486 transitions. Second operand  has 10 states, 8 states have (on average 2.375) internal successors, (19), 10 states have internal predecessors, (19), 4 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (10), 8 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:56,586 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,586 INFO  L93              Difference]: Finished difference Result 433 states and 485 transitions.
[2025-04-28 21:21:56,591 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:56,591 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 2.375) internal successors, (19), 10 states have internal predecessors, (19), 4 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (10), 8 states have call predecessors, (10), 4 states have call successors, (10) Word has length 39
[2025-04-28 21:21:56,591 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,596 INFO  L225             Difference]: With dead ends: 433
[2025-04-28 21:21:56,597 INFO  L226             Difference]: Without dead ends: 432
[2025-04-28 21:21:56,597 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:56,598 INFO  L437           NwaCegarLoop]: 478 mSDtfsCounter, 2 mSDsluCounter, 3793 mSDsCounter, 0 mSdLazyCounter, 67 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 4271 SdHoareTripleChecker+Invalid, 72 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 67 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,598 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 4271 Invalid, 72 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 67 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:56,599 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 432 states.
[2025-04-28 21:21:56,631 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 432 to 432.
[2025-04-28 21:21:56,632 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 432 states, 191 states have (on average 1.0837696335078535) internal successors, (207), 207 states have internal predecessors, (207), 131 states have call successors, (138), 109 states have call predecessors, (138), 109 states have return successors, (138), 115 states have call predecessors, (138), 131 states have call successors, (138)
[2025-04-28 21:21:56,641 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 432 states to 432 states and 483 transitions.
[2025-04-28 21:21:56,641 INFO  L79                 Accepts]: Start accepts. Automaton has 432 states and 483 transitions. Word has length 39
[2025-04-28 21:21:56,641 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,641 INFO  L485      AbstractCegarLoop]: Abstraction has 432 states and 483 transitions.
[2025-04-28 21:21:56,641 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 2.375) internal successors, (19), 10 states have internal predecessors, (19), 4 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (10), 8 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:56,642 INFO  L278                IsEmpty]: Start isEmpty. Operand 432 states and 483 transitions.
[2025-04-28 21:21:56,646 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 164
[2025-04-28 21:21:56,646 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,646 INFO  L218           NwaCegarLoop]: trace histogram [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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,647 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:56,647 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,651 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,651 INFO  L85        PathProgramCache]: Analyzing trace with hash 1982710403, now seen corresponding path program 1 times
[2025-04-28 21:21:56,651 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,651 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [44314071]
[2025-04-28 21:21:56,652 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,652 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,993 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 163 statements into 1 equivalence classes.
[2025-04-28 21:21:57,159 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 163 of 163 statements.
[2025-04-28 21:21:57,159 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,159 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,172 INFO  L134       CoverageAnalysis]: Checked inductivity of 34 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 34 trivial. 0 not checked.
[2025-04-28 21:21:59,174 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [44314071]
[2025-04-28 21:21:59,174 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [44314071] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,174 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,175 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:59,175 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1300175532]
[2025-04-28 21:21:59,175 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,175 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:59,176 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,176 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:59,178 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:59,178 INFO  L87              Difference]: Start difference. First operand 432 states and 483 transitions. Second operand  has 10 states, 9 states have (on average 6.666666666666667) internal successors, (60), 10 states have internal predecessors, (60), 4 states have call successors, (35), 1 states have call predecessors, (35), 9 states have return successors, (35), 9 states have call predecessors, (35), 4 states have call successors, (35)
[2025-04-28 21:21:59,684 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,684 INFO  L93              Difference]: Finished difference Result 428 states and 478 transitions.
[2025-04-28 21:21:59,685 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:59,685 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 6.666666666666667) internal successors, (60), 10 states have internal predecessors, (60), 4 states have call successors, (35), 1 states have call predecessors, (35), 9 states have return successors, (35), 9 states have call predecessors, (35), 4 states have call successors, (35) Word has length 163
[2025-04-28 21:21:59,686 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,690 INFO  L225             Difference]: With dead ends: 428
[2025-04-28 21:21:59,690 INFO  L226             Difference]: Without dead ends: 424
[2025-04-28 21:21:59,690 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:59,691 INFO  L437           NwaCegarLoop]: 468 mSDtfsCounter, 0 mSDsluCounter, 3721 mSDsCounter, 0 mSdLazyCounter, 93 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 4189 SdHoareTripleChecker+Invalid, 96 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 93 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,692 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 4189 Invalid, 96 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 93 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:59,693 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 424 states.
[2025-04-28 21:21:59,723 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 424 to 424.
[2025-04-28 21:21:59,724 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 424 states, 187 states have (on average 1.085561497326203) internal successors, (203), 203 states have internal predecessors, (203), 129 states have call successors, (135), 107 states have call predecessors, (135), 107 states have return successors, (135), 113 states have call predecessors, (135), 129 states have call successors, (135)
[2025-04-28 21:21:59,729 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 424 states to 424 states and 473 transitions.
[2025-04-28 21:21:59,729 INFO  L79                 Accepts]: Start accepts. Automaton has 424 states and 473 transitions. Word has length 163
[2025-04-28 21:21:59,730 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,730 INFO  L485      AbstractCegarLoop]: Abstraction has 424 states and 473 transitions.
[2025-04-28 21:21:59,730 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 6.666666666666667) internal successors, (60), 10 states have internal predecessors, (60), 4 states have call successors, (35), 1 states have call predecessors, (35), 9 states have return successors, (35), 9 states have call predecessors, (35), 4 states have call successors, (35)
[2025-04-28 21:21:59,731 INFO  L278                IsEmpty]: Start isEmpty. Operand 424 states and 473 transitions.
[2025-04-28 21:21:59,739 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 283
[2025-04-28 21:21:59,739 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,740 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 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, 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]
[2025-04-28 21:21:59,742 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:59,742 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,743 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,744 INFO  L85        PathProgramCache]: Analyzing trace with hash -828621947, now seen corresponding path program 1 times
[2025-04-28 21:21:59,744 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,744 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1368366634]
[2025-04-28 21:21:59,744 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,744 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,369 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 282 statements into 1 equivalence classes.
[2025-04-28 21:22:00,446 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 282 of 282 statements.
[2025-04-28 21:22:00,446 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,446 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,108 INFO  L134       CoverageAnalysis]: Checked inductivity of 246 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 246 trivial. 0 not checked.
[2025-04-28 21:22:03,109 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,109 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1368366634]
[2025-04-28 21:22:03,109 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1368366634] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,109 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,109 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:22:03,109 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1791202954]
[2025-04-28 21:22:03,109 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,110 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:22:03,112 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,112 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:22:03,112 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:03,113 INFO  L87              Difference]: Start difference. First operand 424 states and 473 transitions. Second operand  has 8 states, 7 states have (on average 9.142857142857142) internal successors, (64), 8 states have internal predecessors, (64), 3 states have call successors, (38), 1 states have call predecessors, (38), 7 states have return successors, (38), 7 states have call predecessors, (38), 3 states have call successors, (38)
[2025-04-28 21:22:03,439 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,439 INFO  L93              Difference]: Finished difference Result 430 states and 480 transitions.
[2025-04-28 21:22:03,440 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:03,440 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 9.142857142857142) internal successors, (64), 8 states have internal predecessors, (64), 3 states have call successors, (38), 1 states have call predecessors, (38), 7 states have return successors, (38), 7 states have call predecessors, (38), 3 states have call successors, (38) Word has length 282
[2025-04-28 21:22:03,441 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,444 INFO  L225             Difference]: With dead ends: 430
[2025-04-28 21:22:03,444 INFO  L226             Difference]: Without dead ends: 430
[2025-04-28 21:22:03,444 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:03,445 INFO  L437           NwaCegarLoop]: 473 mSDtfsCounter, 1 mSDsluCounter, 2820 mSDsCounter, 0 mSdLazyCounter, 53 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 3293 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 53 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,446 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 3293 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 53 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:03,447 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 430 states.
[2025-04-28 21:22:03,461 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 430 to 430.
[2025-04-28 21:22:03,462 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 430 states, 190 states have (on average 1.0842105263157895) internal successors, (206), 206 states have internal predecessors, (206), 129 states have call successors, (135), 107 states have call predecessors, (135), 110 states have return successors, (139), 116 states have call predecessors, (139), 129 states have call successors, (139)
[2025-04-28 21:22:03,465 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 430 states to 430 states and 480 transitions.
[2025-04-28 21:22:03,465 INFO  L79                 Accepts]: Start accepts. Automaton has 430 states and 480 transitions. Word has length 282
[2025-04-28 21:22:03,466 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,466 INFO  L485      AbstractCegarLoop]: Abstraction has 430 states and 480 transitions.
[2025-04-28 21:22:03,467 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 9.142857142857142) internal successors, (64), 8 states have internal predecessors, (64), 3 states have call successors, (38), 1 states have call predecessors, (38), 7 states have return successors, (38), 7 states have call predecessors, (38), 3 states have call successors, (38)
[2025-04-28 21:22:03,467 INFO  L278                IsEmpty]: Start isEmpty. Operand 430 states and 480 transitions.
[2025-04-28 21:22:03,475 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 283
[2025-04-28 21:22:03,475 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,475 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 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, 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]
[2025-04-28 21:22:03,479 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:22:03,479 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,480 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,480 INFO  L85        PathProgramCache]: Analyzing trace with hash -2035096768, now seen corresponding path program 1 times
[2025-04-28 21:22:03,480 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,480 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [649129994]
[2025-04-28 21:22:03,480 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,480 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,952 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 282 statements into 1 equivalence classes.
[2025-04-28 21:22:04,052 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 282 of 282 statements.
[2025-04-28 21:22:04,052 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,052 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,728 INFO  L134       CoverageAnalysis]: Checked inductivity of 246 backedges. 0 proven. 65 refuted. 0 times theorem prover too weak. 181 trivial. 0 not checked.
[2025-04-28 21:22:05,728 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:05,729 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [649129994]
[2025-04-28 21:22:05,729 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [649129994] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:05,729 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [172191991]
[2025-04-28 21:22:05,729 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,729 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,732 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:05,735 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:05,738 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
