./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/types_struct/struct_recursive_3.sol_9_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:05,611 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:05,660 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dc5c9929-5f5f-4820-95cf-e6aafcdf0b81/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:05,664 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:05,664 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:05,682 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:05,682 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:05,683 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:05,683 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:05,683 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:05,683 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:05,683 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:05,683 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:05,684 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:05,684 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:05,684 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:05,684 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:05,685 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:05,685 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:05,685 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:05,685 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:05,884 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:05,892 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:05,894 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:05,895 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:05,895 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:05,896 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dc5c9929-5f5f-4820-95cf-e6aafcdf0b81/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/types_struct/struct_recursive_3.sol_9_no_adts_000.smt2
[2025-05-07 17:27:05,897 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:05,901 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:06,358 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dc5c9929-5f5f-4820-95cf-e6aafcdf0b81/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/types_struct/struct_recursive_3.sol_9_no_adts_000.smt2
[2025-05-07 17:27:06,361 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:06,362 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:06,362 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:06,362 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:06,362 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:06,364 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,427 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06 Unit
[2025-05-07 17:27:06,427 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:06,428 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:06,428 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:06,428 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:06,439 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,439 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,479 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,479 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,493 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,495 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,497 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,501 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,504 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,523 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:06,523 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:06,523 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:06,523 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:06,524 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,526 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:06,535 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:06,544 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-05-07 17:27:06,546 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:27:06,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:06,554 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:06,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:06,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_31_0 given in one single declaration
[2025-05-07 17:27:06,554 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_31_0
[2025-05-07 17:27:06,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_31_0
[2025-05-07 17:27:06,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,554 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__123_214_0
[2025-05-07 17:27:06,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__123_214_0
[2025-05-07 17:27:06,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,554 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_function_f__123_214_0
[2025-05-07 17:27:06,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_function_f__123_214_0
[2025-05-07 17:27:06,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,554 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__123_214_0
[2025-05-07 17:27:06,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_122_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_122_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_122_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_function_f__123_214_0
[2025-05-07 17:27:06,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__123_214_0
[2025-05-07 17:27:06,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__123_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__123_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_41_C_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_41_C_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_41_C_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_38_C_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_38_C_214_0
[2025-05-07 17:27:06,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_38_C_214_0
[2025-05-07 17:27:06,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_40_C_214_0 given in one single declaration
[2025-05-07 17:27:06,557 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_40_C_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_40_C_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_39_C_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_39_C_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_39_C_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_28_return_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure block_28_return_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_28_return_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_27_g_212_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure block_27_g_212_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_27_g_212_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,558 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_function_g__213_214_0
[2025-05-07 17:27:06,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_33_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_33_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_33_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_29_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_29_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_29_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_34_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_34_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_34_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_31_function_g__213_214_0 given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure block_31_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_31_function_g__213_214_0
[2025-05-07 17:27:06,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:06,559 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:06,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:06,883 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:06,885 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:07,539 INFO  L?                        ?]: Removed 1573 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:07,540 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:07,554 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:07,555 INFO  L312             CfgBuilder]: Removed 32 assume(true) statements.
[2025-05-07 17:27:07,555 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:07 BoogieIcfgContainer
[2025-05-07 17:27:07,555 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:07,558 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:07,558 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:07,562 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:07,563 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:06" (1/3) ...
[2025-05-07 17:27:07,563 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@265126d1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:07, skipping insertion in model container
[2025-05-07 17:27:07,563 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (2/3) ...
[2025-05-07 17:27:07,564 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@265126d1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:07, skipping insertion in model container
[2025-05-07 17:27:07,564 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:07" (3/3) ...
[2025-05-07 17:27:07,565 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:07,580 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:07,583 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 44 procedures, 172 locations, 296 edges, 44 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:07,630 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:07,643 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;@25c36633, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:07,643 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:07,647 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 172 states, 79 states have (on average 1.0506329113924051) internal successors, (83), 83 states have internal predecessors, (83), 48 states have call successors, (71), 43 states have call predecessors, (71), 43 states have return successors, (71), 45 states have call predecessors, (71), 48 states have call successors, (71)
[2025-05-07 17:27:07,661 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:07,661 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:07,662 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:07,662 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:07,667 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:07,667 INFO  L85        PathProgramCache]: Analyzing trace with hash 1586834530, now seen corresponding path program 1 times
[2025-05-07 17:27:07,675 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:07,675 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [846335352]
[2025-05-07 17:27:07,676 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:07,676 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:07,740 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:07,831 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:07,832 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:07,832 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,106 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:08,107 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,107 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [846335352]
[2025-05-07 17:27:08,108 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [846335352] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,108 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,110 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:08,111 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1803720994]
[2025-05-07 17:27:08,111 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,114 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:08,114 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,140 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:08,141 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:08,143 INFO  L87              Difference]: Start difference. First operand  has 172 states, 79 states have (on average 1.0506329113924051) internal successors, (83), 83 states have internal predecessors, (83), 48 states have call successors, (71), 43 states have call predecessors, (71), 43 states have return successors, (71), 45 states have call predecessors, (71), 48 states have call successors, (71) Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:08,213 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,214 INFO  L93              Difference]: Finished difference Result 175 states and 229 transitions.
[2025-05-07 17:27:08,215 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:08,216 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:08,216 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,223 INFO  L225             Difference]: With dead ends: 175
[2025-05-07 17:27:08,223 INFO  L226             Difference]: Without dead ends: 175
[2025-05-07 17:27:08,224 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-05-07 17:27:08,226 INFO  L437           NwaCegarLoop]: 225 mSDtfsCounter, 1 mSDsluCounter, 886 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1111 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:08,227 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1111 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:08,243 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 175 states.
[2025-05-07 17:27:08,266 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 175 to 175.
[2025-05-07 17:27:08,267 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 175 states, 80 states have (on average 1.0375) internal successors, (83), 83 states have internal predecessors, (83), 49 states have call successors, (72), 43 states have call predecessors, (72), 45 states have return successors, (74), 48 states have call predecessors, (74), 49 states have call successors, (74)
[2025-05-07 17:27:08,270 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 175 states to 175 states and 229 transitions.
[2025-05-07 17:27:08,271 INFO  L79                 Accepts]: Start accepts. Automaton has 175 states and 229 transitions. Word has length 51
[2025-05-07 17:27:08,272 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,272 INFO  L485      AbstractCegarLoop]: Abstraction has 175 states and 229 transitions.
[2025-05-07 17:27:08,272 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:08,272 INFO  L278                IsEmpty]: Start isEmpty. Operand 175 states and 229 transitions.
[2025-05-07 17:27:08,274 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:08,274 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,274 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:08,274 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:08,275 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,275 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,275 INFO  L85        PathProgramCache]: Analyzing trace with hash -294029994, now seen corresponding path program 1 times
[2025-05-07 17:27:08,275 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,275 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [871688815]
[2025-05-07 17:27:08,275 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,275 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,301 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:08,304 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:08,304 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,304 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,369 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:08,369 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,369 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [871688815]
[2025-05-07 17:27:08,369 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [871688815] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,369 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,369 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:08,369 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [251959781]
[2025-05-07 17:27:08,369 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,370 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:08,371 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:08,371 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:08,372 INFO  L87              Difference]: Start difference. First operand 175 states and 229 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:08,386 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,386 INFO  L93              Difference]: Finished difference Result 179 states and 234 transitions.
[2025-05-07 17:27:08,387 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:08,387 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:08,387 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,388 INFO  L225             Difference]: With dead ends: 179
[2025-05-07 17:27:08,388 INFO  L226             Difference]: Without dead ends: 175
[2025-05-07 17:27:08,388 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:08,389 INFO  L437           NwaCegarLoop]: 224 mSDtfsCounter, 1 mSDsluCounter, 440 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 664 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:08,389 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 664 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:08,390 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 175 states.
[2025-05-07 17:27:08,407 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 175 to 173.
[2025-05-07 17:27:08,408 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:08,410 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:08,411 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:08,411 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,411 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:08,411 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:08,411 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:08,414 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:08,414 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,414 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:08,415 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:08,415 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,415 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,415 INFO  L85        PathProgramCache]: Analyzing trace with hash -793007964, now seen corresponding path program 1 times
[2025-05-07 17:27:08,415 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,415 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [951637488]
[2025-05-07 17:27:08,416 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,416 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,441 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:08,454 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:08,454 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,455 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,759 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:08,759 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,759 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [951637488]
[2025-05-07 17:27:08,759 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [951637488] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,759 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,759 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:27:08,760 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [186665955]
[2025-05-07 17:27:08,760 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,760 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:27:08,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,761 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:27:08,761 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:27:08,761 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 5 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 5 states have call successors, (14)
[2025-05-07 17:27:08,944 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,944 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:08,945 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:27:08,945 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 5 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 5 states have call successors, (14) Word has length 51
[2025-05-07 17:27:08,945 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,946 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:08,946 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:08,946 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:27:08,947 INFO  L437           NwaCegarLoop]: 203 mSDtfsCounter, 1 mSDsluCounter, 1185 mSDsCounter, 0 mSdLazyCounter, 151 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1388 SdHoareTripleChecker+Invalid, 151 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 151 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:08,947 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1388 Invalid, 151 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 151 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:27:08,948 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:08,954 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:08,954 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:08,955 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:08,955 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:08,956 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,956 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:08,956 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 5 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 5 states have call successors, (14)
[2025-05-07 17:27:08,956 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:08,957 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:08,957 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,957 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:08,957 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:08,957 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,957 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,957 INFO  L85        PathProgramCache]: Analyzing trace with hash 1211323738, now seen corresponding path program 1 times
[2025-05-07 17:27:08,957 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,957 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1054468972]
[2025-05-07 17:27:08,957 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,957 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,975 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:08,985 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:08,985 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,985 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,050 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:09,051 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,051 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1054468972]
[2025-05-07 17:27:09,051 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1054468972] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,051 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,051 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:09,051 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [179025392]
[2025-05-07 17:27:09,051 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,051 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:09,051 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,052 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:09,052 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:09,052 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,083 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,083 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:09,083 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:09,083 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:09,083 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,085 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:09,085 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:09,085 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-05-07 17:27:09,086 INFO  L437           NwaCegarLoop]: 221 mSDtfsCounter, 1 mSDsluCounter, 870 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1091 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,086 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1091 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,087 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:09,097 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:09,098 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:09,099 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:09,100 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:09,100 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,100 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:09,100 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,100 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:09,101 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:09,101 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,102 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,102 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:09,102 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,102 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,102 INFO  L85        PathProgramCache]: Analyzing trace with hash -748138396, now seen corresponding path program 1 times
[2025-05-07 17:27:09,102 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,102 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1768037397]
[2025-05-07 17:27:09,102 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,103 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,119 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,143 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,143 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,143 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,210 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:09,210 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,210 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1768037397]
[2025-05-07 17:27:09,210 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1768037397] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,210 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,210 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:09,210 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [417553972]
[2025-05-07 17:27:09,210 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,211 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:09,211 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,211 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:09,211 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:09,211 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,241 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,241 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:09,241 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:09,242 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:09,242 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,243 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:09,243 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:09,243 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-05-07 17:27:09,244 INFO  L437           NwaCegarLoop]: 221 mSDtfsCounter, 1 mSDsluCounter, 870 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1091 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,244 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1091 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,245 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:09,252 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:09,253 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:09,254 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:09,255 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:09,255 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,255 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:09,255 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,255 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:09,256 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:09,256 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,257 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,257 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:09,257 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,257 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,257 INFO  L85        PathProgramCache]: Analyzing trace with hash -1722939476, now seen corresponding path program 1 times
[2025-05-07 17:27:09,257 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,257 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1059284479]
[2025-05-07 17:27:09,257 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,257 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,281 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,292 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,292 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,292 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,364 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:09,364 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,365 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1059284479]
[2025-05-07 17:27:09,365 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1059284479] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,365 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,365 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:09,365 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [689384127]
[2025-05-07 17:27:09,365 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,365 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:09,365 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,366 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:09,366 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:09,366 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,393 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,393 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:09,393 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:09,394 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:09,394 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,395 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:09,395 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:09,395 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-05-07 17:27:09,395 INFO  L437           NwaCegarLoop]: 221 mSDtfsCounter, 1 mSDsluCounter, 870 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1091 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,395 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1091 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,396 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:09,400 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:09,400 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:09,401 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:09,401 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:09,401 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,401 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:09,401 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,401 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:09,402 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:09,402 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,402 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,402 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:09,402 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,402 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,403 INFO  L85        PathProgramCache]: Analyzing trace with hash -2058035412, now seen corresponding path program 1 times
[2025-05-07 17:27:09,403 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,403 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1514266985]
[2025-05-07 17:27:09,403 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,403 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,419 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,425 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,425 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,425 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,474 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:09,474 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,474 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1514266985]
[2025-05-07 17:27:09,474 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1514266985] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,474 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,474 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:09,474 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1136956117]
[2025-05-07 17:27:09,474 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,475 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:09,475 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,475 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:09,475 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:09,475 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,510 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,511 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:09,511 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:09,511 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:09,511 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,512 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:09,513 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:09,513 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-05-07 17:27:09,513 INFO  L437           NwaCegarLoop]: 221 mSDtfsCounter, 1 mSDsluCounter, 870 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1091 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,514 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1091 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,514 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:09,521 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:09,521 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:09,522 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:09,523 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:09,523 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,523 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:09,523 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,523 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:09,524 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:09,524 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,524 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,524 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:09,525 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,525 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,525 INFO  L85        PathProgramCache]: Analyzing trace with hash -1135731798, now seen corresponding path program 1 times
[2025-05-07 17:27:09,525 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,525 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [186793766]
[2025-05-07 17:27:09,525 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,525 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,549 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,560 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,561 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,561 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,645 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:09,646 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,646 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [186793766]
[2025-05-07 17:27:09,646 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [186793766] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,646 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,646 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:09,646 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [100555418]
[2025-05-07 17:27:09,646 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,646 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:09,646 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,647 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:09,647 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:09,647 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,680 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,680 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:09,680 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:09,680 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:09,681 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,681 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:09,681 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:09,682 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-05-07 17:27:09,682 INFO  L437           NwaCegarLoop]: 219 mSDtfsCounter, 1 mSDsluCounter, 864 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1083 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,682 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1083 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,682 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:09,686 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:09,686 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:09,687 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:09,687 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:09,687 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,688 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:09,688 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,688 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:09,688 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:09,688 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,689 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,689 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:09,689 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,689 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,689 INFO  L85        PathProgramCache]: Analyzing trace with hash 924281800, now seen corresponding path program 1 times
[2025-05-07 17:27:09,689 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,689 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1922546999]
[2025-05-07 17:27:09,689 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,689 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,708 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,714 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,715 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,715 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,770 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:09,770 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,770 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1922546999]
[2025-05-07 17:27:09,770 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1922546999] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,770 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,770 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:09,770 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [313159822]
[2025-05-07 17:27:09,770 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,771 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:09,771 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,771 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:09,772 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:09,772 INFO  L87              Difference]: Start difference. First operand 173 states and 224 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,805 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,806 INFO  L93              Difference]: Finished difference Result 178 states and 230 transitions.
[2025-05-07 17:27:09,806 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:09,806 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:27:09,806 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,807 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:09,807 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:09,808 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-05-07 17:27:09,808 INFO  L437           NwaCegarLoop]: 221 mSDtfsCounter, 1 mSDsluCounter, 870 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1091 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,808 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1091 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,809 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:09,814 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 173.
[2025-05-07 17:27:09,815 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 80 states have (on average 1.025) internal successors, (82), 82 states have internal predecessors, (82), 47 states have call successors, (70), 43 states have call predecessors, (70), 45 states have return successors, (72), 47 states have call predecessors, (72), 47 states have call successors, (72)
[2025-05-07 17:27:09,816 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 224 transitions.
[2025-05-07 17:27:09,816 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 224 transitions. Word has length 51
[2025-05-07 17:27:09,817 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,817 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 224 transitions.
[2025-05-07 17:27:09,817 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:27:09,817 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 224 transitions.
[2025-05-07 17:27:09,818 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:09,818 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,818 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,818 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:09,818 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,819 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,819 INFO  L85        PathProgramCache]: Analyzing trace with hash 1659438550, now seen corresponding path program 1 times
[2025-05-07 17:27:09,819 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,819 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [115266708]
[2025-05-07 17:27:09,819 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,819 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,841 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,850 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,850 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,850 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-05-07 17:27:09,850 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-05-07 17:27:09,855 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:09,873 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:09,873 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-05-07 17:27:09,904 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-05-07 17:27:09,904 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-05-07 17:27:09,905 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:09,907 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:09,909 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:09,925 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:09,927 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:09 BoogieIcfgContainer
[2025-05-07 17:27:09,927 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:09,928 INFO  L158              Benchmark]: Toolchain (without parser) took 3566.30ms. Allocated memory is still 234.9MB. Free memory was 157.2MB in the beginning and 182.5MB in the end (delta: -25.4MB). Peak memory consumption was 92.4MB. Max. memory is 33.6GB.
[2025-05-07 17:27:09,928 INFO  L158              Benchmark]: SmtParser took 0.30ms. Allocated memory is still 234.9MB. Free memory is still 173.9MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:09,928 INFO  L158              Benchmark]: ChcToBoogie took 65.08ms. Allocated memory is still 234.9MB. Free memory was 157.2MB in the beginning and 146.7MB in the end (delta: 10.4MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:09,928 INFO  L158              Benchmark]: Boogie Preprocessor took 95.19ms. Allocated memory is still 234.9MB. Free memory was 146.7MB in the beginning and 140.2MB in the end (delta: 6.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:09,928 INFO  L158              Benchmark]: RCFGBuilder took 1032.03ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 140.2MB in the beginning and 175.4MB in the end (delta: -35.2MB). Peak memory consumption was 42.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:09,929 INFO  L158              Benchmark]: TraceAbstraction took 2369.09ms. Allocated memory was 318.8MB in the beginning and 234.9MB in the end (delta: -83.9MB). Free memory was 174.5MB in the beginning and 182.5MB in the end (delta: -8.1MB). Peak memory consumption was 32.9MB. Max. memory is 33.6GB.
[2025-05-07 17:27:09,930 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.30ms. Allocated memory is still 234.9MB. Free memory is still 173.9MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 65.08ms. Allocated memory is still 234.9MB. Free memory was 157.2MB in the beginning and 146.7MB in the end (delta: 10.4MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 95.19ms. Allocated memory is still 234.9MB. Free memory was 146.7MB in the beginning and 140.2MB in the end (delta: 6.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 1032.03ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 140.2MB in the beginning and 175.4MB in the end (delta: -35.2MB). Peak memory consumption was 42.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2369.09ms. Allocated memory was 318.8MB in the beginning and 234.9MB in the end (delta: -83.9MB). Free memory was 174.5MB in the beginning and 182.5MB in the end (delta: -8.1MB). Peak memory consumption was 32.9MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - CounterExampleResult [Unknown line] : the set of constraint Horn clauses is unsatisfiable
    the set of constraint Horn clauses is unsatisfiable
We found a FailurePath: 
[L0]  CALL  call False();
[L0]  CALL  call error_target_31_0();
[L0]        assume 6 == hbv_error_target_31_0_E_1;
      VAL   [hbv_error_target_31_0_E_1=6]
[L0]  CALL  call interface_0_C_214_0(hbv_error_target_31_0_L_2, hbv_error_target_31_0_A_3, hbv_error_target_31_0_B_4, hbv_error_target_31_0_C_5, hbv_error_target_31_0_D_6, hbv_error_target_31_0_J_7, hbv_error_target_31_0_F_8, hbv_error_target_31_0_H_9);
      VAL   [hhv_interface_0_C_214_0_G_6=0, hhv_interface_0_C_214_0_I_7=0, hhv_interface_0_C_214_0_L_0=638722033]
[L0]        assume ((((((((((((((((((((((!(hbv_interface_0_C_214_0_R_10 < 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_Q_9)) && !(1461501637330902918203684832716283019655932542975 < hbv_interface_0_C_214_0_R_10)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_P_8)) && !(hbv_interface_0_C_214_0_P_8 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_M_5)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_O_7)) && hbv_interface_0_C_214_0_M_5 == 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_N_6)) && !(hbv_interface_0_C_214_0_W_12 < 0)) && !(hbv_interface_0_C_214_0_S_11 < 0)) && !(hbv_interface_0_C_214_0_N_6 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_E_1)) && !(1461501637330902918203684832716283019655932542975 < hbv_interface_0_C_214_0_W_12)) && !(hbv_interface_0_C_214_0_E_1 < 0)) && !(hbv_interface_0_C_214_0_M_5 < 0)) && !(1461501637330902918203684832716283019655932542975 < hbv_interface_0_C_214_0_H_4)) && !(hbv_interface_0_C_214_0_O_7 < 0)) && !(hbv_interface_0_C_214_0_F_3 < 0)) && hbv_interface_0_C_214_0_M_2 == 0) && !(hbv_interface_0_C_214_0_Q_9 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_S_11)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_214_0_F_3)) && !(hbv_interface_0_C_214_0_H_4 < 0);
      VAL   [hbv_interface_0_C_214_0_E_1=0, hbv_interface_0_C_214_0_F_3=0, hbv_interface_0_C_214_0_H_4=0, hbv_interface_0_C_214_0_M_2=0, hbv_interface_0_C_214_0_M_5=0, hbv_interface_0_C_214_0_N_6=0, hbv_interface_0_C_214_0_O_7=0, hbv_interface_0_C_214_0_P_8=0, hbv_interface_0_C_214_0_Q_9=0, hbv_interface_0_C_214_0_R_10=0, hbv_interface_0_C_214_0_S_11=0, hbv_interface_0_C_214_0_W_12=0, hhv_interface_0_C_214_0_G_6=0, hhv_interface_0_C_214_0_I_7=0, hhv_interface_0_C_214_0_L_0=638722033]
[L0]  CALL  call summary_constructor_2_C_214_0(hbv_interface_0_C_214_0_M_2, hhv_interface_0_C_214_0_L_0, hhv_interface_0_C_214_0_A_1, hhv_interface_0_C_214_0_B_2, hhv_interface_0_C_214_0_C_3, hhv_interface_0_C_214_0_D_4, hbv_interface_0_C_214_0_Q_9, hbv_interface_0_C_214_0_P_8, hbv_interface_0_C_214_0_W_12, hbv_interface_0_C_214_0_S_11, hbv_interface_0_C_214_0_O_7, hbv_interface_0_C_214_0_E_1, hbv_interface_0_C_214_0_F_3, hbv_interface_0_C_214_0_U_13, hbv_interface_0_C_214_0_U_14, hbv_interface_0_C_214_0_W_15, hbv_interface_0_C_214_0_H_4, hbv_interface_0_C_214_0_X_16, hbv_interface_0_C_214_0_M_5, hbv_interface_0_C_214_0_N_6, hbv_interface_0_C_214_0_R_10, hbv_interface_0_C_214_0_J_17, hhv_interface_0_C_214_0_K_5, hbv_interface_0_C_214_0_Z_18, hbv_interface_0_C_214_0_A1_19, hhv_interface_0_C_214_0_G_6, hhv_interface_0_C_214_0_I_7);
      VAL   [hhv_summary_constructor_2_C_214_0_A1_16=0, hhv_summary_constructor_2_C_214_0_B1_17=638722040, hhv_summary_constructor_2_C_214_0_C1_18=0, hhv_summary_constructor_2_C_214_0_D1_19=0, hhv_summary_constructor_2_C_214_0_E1_20=0, hhv_summary_constructor_2_C_214_0_F_0=0, hhv_summary_constructor_2_C_214_0_G_23=0, hhv_summary_constructor_2_C_214_0_I_25=0, hhv_summary_constructor_2_C_214_0_J_24=0, hhv_summary_constructor_2_C_214_0_L_26=0, hhv_summary_constructor_2_C_214_0_P_1=638722033, hhv_summary_constructor_2_C_214_0_Q_6=0, hhv_summary_constructor_2_C_214_0_R_7=0, hhv_summary_constructor_2_C_214_0_S_8=0, hhv_summary_constructor_2_C_214_0_T_9=0, hhv_summary_constructor_2_C_214_0_U_10=0, hhv_summary_constructor_2_C_214_0_V_11=0, hhv_summary_constructor_2_C_214_0_W_12=0, hhv_summary_constructor_2_C_214_0_Z_15=638722035]
[L0]        assume hhv_summary_constructor_2_C_214_0_F_0 == 0;
      VAL   [hhv_summary_constructor_2_C_214_0_A1_16=0, hhv_summary_constructor_2_C_214_0_B1_17=638722040, hhv_summary_constructor_2_C_214_0_C1_18=0, hhv_summary_constructor_2_C_214_0_D1_19=0, hhv_summary_constructor_2_C_214_0_E1_20=0, hhv_summary_constructor_2_C_214_0_F_0=0, hhv_summary_constructor_2_C_214_0_G_23=0, hhv_summary_constructor_2_C_214_0_I_25=0, hhv_summary_constructor_2_C_214_0_J_24=0, hhv_summary_constructor_2_C_214_0_L_26=0, hhv_summary_constructor_2_C_214_0_P_1=638722033, hhv_summary_constructor_2_C_214_0_Q_6=0, hhv_summary_constructor_2_C_214_0_R_7=0, hhv_summary_constructor_2_C_214_0_S_8=0, hhv_summary_constructor_2_C_214_0_T_9=0, hhv_summary_constructor_2_C_214_0_U_10=0, hhv_summary_constructor_2_C_214_0_V_11=0, hhv_summary_constructor_2_C_214_0_W_12=0, hhv_summary_constructor_2_C_214_0_Z_15=638722035]
[L0]  CALL  call contract_initializer_38_C_214_0(hhv_summary_constructor_2_C_214_0_F_0, hhv_summary_constructor_2_C_214_0_P_1, hhv_summary_constructor_2_C_214_0_A_2, hhv_summary_constructor_2_C_214_0_B_3, hhv_summary_constructor_2_C_214_0_C_4, hhv_summary_constructor_2_C_214_0_D_5, hhv_summary_constructor_2_C_214_0_Q_6, hhv_summary_constructor_2_C_214_0_R_7, hhv_summary_constructor_2_C_214_0_S_8, hhv_summary_constructor_2_C_214_0_T_9, hhv_summary_constructor_2_C_214_0_U_10, hhv_summary_constructor_2_C_214_0_V_11, hhv_summary_constructor_2_C_214_0_W_12, hhv_summary_constructor_2_C_214_0_X_13, hhv_summary_constructor_2_C_214_0_Y_14, hhv_summary_constructor_2_C_214_0_Z_15, hhv_summary_constructor_2_C_214_0_A1_16, hhv_summary_constructor_2_C_214_0_B1_17, hhv_summary_constructor_2_C_214_0_C1_18, hhv_summary_constructor_2_C_214_0_D1_19, hhv_summary_constructor_2_C_214_0_E1_20, hbv_summary_constructor_2_C_214_0_N_1, hhv_summary_constructor_2_C_214_0_O_22, hbv_summary_constructor_2_C_214_0_H_2, hbv_summary_constructor_2_C_214_0_K_3, hhv_summary_constructor_2_C_214_0_I_25, hhv_summary_constructor_2_C_214_0_L_26);
      VAL   [hhv_contract_initializer_38_C_214_0_A1_20=0, hhv_contract_initializer_38_C_214_0_E_0=0, hhv_contract_initializer_38_C_214_0_F_23=0, hhv_contract_initializer_38_C_214_0_G_25=0, hhv_contract_initializer_38_C_214_0_H_24=0, hhv_contract_initializer_38_C_214_0_I_26=0, hhv_contract_initializer_38_C_214_0_L_1=638722033, hhv_contract_initializer_38_C_214_0_M_6=0, hhv_contract_initializer_38_C_214_0_N_7=0, hhv_contract_initializer_38_C_214_0_O_8=0, hhv_contract_initializer_38_C_214_0_P_9=0, hhv_contract_initializer_38_C_214_0_Q_10=0, hhv_contract_initializer_38_C_214_0_R_11=0, hhv_contract_initializer_38_C_214_0_S_12=0, hhv_contract_initializer_38_C_214_0_V_15=638722035, hhv_contract_initializer_38_C_214_0_W_16=0, hhv_contract_initializer_38_C_214_0_X_17=638722040, hhv_contract_initializer_38_C_214_0_Y_18=0, hhv_contract_initializer_38_C_214_0_Z_19=0]
[L0]  CALL  call contract_initializer_after_init_40_C_214_0(hhv_contract_initializer_38_C_214_0_E_0, hhv_contract_initializer_38_C_214_0_L_1, hhv_contract_initializer_38_C_214_0_A_2, hhv_contract_initializer_38_C_214_0_B_3, hhv_contract_initializer_38_C_214_0_C_4, hhv_contract_initializer_38_C_214_0_D_5, hhv_contract_initializer_38_C_214_0_M_6, hhv_contract_initializer_38_C_214_0_N_7, hhv_contract_initializer_38_C_214_0_O_8, hhv_contract_initializer_38_C_214_0_P_9, hhv_contract_initializer_38_C_214_0_Q_10, hhv_contract_initializer_38_C_214_0_R_11, hhv_contract_initializer_38_C_214_0_S_12, hhv_contract_initializer_38_C_214_0_T_13, hhv_contract_initializer_38_C_214_0_U_14, hhv_contract_initializer_38_C_214_0_V_15, hhv_contract_initializer_38_C_214_0_W_16, hhv_contract_initializer_38_C_214_0_X_17, hhv_contract_initializer_38_C_214_0_Y_18, hhv_contract_initializer_38_C_214_0_Z_19, hhv_contract_initializer_38_C_214_0_A1_20, hhv_contract_initializer_38_C_214_0_J_21, hhv_contract_initializer_38_C_214_0_K_22, hhv_contract_initializer_38_C_214_0_F_23, hhv_contract_initializer_38_C_214_0_H_24, hhv_contract_initializer_38_C_214_0_G_25, hhv_contract_initializer_38_C_214_0_I_26);
      VAL   [hhv_contract_initializer_after_init_40_C_214_0_A1_20=0, hhv_contract_initializer_after_init_40_C_214_0_E_0=0, hhv_contract_initializer_after_init_40_C_214_0_F_23=0, hhv_contract_initializer_after_init_40_C_214_0_G_25=0, hhv_contract_initializer_after_init_40_C_214_0_H_24=0, hhv_contract_initializer_after_init_40_C_214_0_I_26=0, hhv_contract_initializer_after_init_40_C_214_0_L_1=638722033, hhv_contract_initializer_after_init_40_C_214_0_M_6=0, hhv_contract_initializer_after_init_40_C_214_0_N_7=0, hhv_contract_initializer_after_init_40_C_214_0_O_8=0, hhv_contract_initializer_after_init_40_C_214_0_P_9=0, hhv_contract_initializer_after_init_40_C_214_0_Q_10=0, hhv_contract_initializer_after_init_40_C_214_0_R_11=0, hhv_contract_initializer_after_init_40_C_214_0_S_12=0, hhv_contract_initializer_after_init_40_C_214_0_V_15=638722035, hhv_contract_initializer_after_init_40_C_214_0_W_16=0, hhv_contract_initializer_after_init_40_C_214_0_X_17=638722040, hhv_contract_initializer_after_init_40_C_214_0_Y_18=0, hhv_contract_initializer_after_init_40_C_214_0_Z_19=0]
[L0]  CALL  call contract_initializer_entry_39_C_214_0(hhv_contract_initializer_after_init_40_C_214_0_E_0, hhv_contract_initializer_after_init_40_C_214_0_L_1, hhv_contract_initializer_after_init_40_C_214_0_A_2, hhv_contract_initializer_after_init_40_C_214_0_B_3, hhv_contract_initializer_after_init_40_C_214_0_C_4, hhv_contract_initializer_after_init_40_C_214_0_D_5, hhv_contract_initializer_after_init_40_C_214_0_M_6, hhv_contract_initializer_after_init_40_C_214_0_N_7, hhv_contract_initializer_after_init_40_C_214_0_O_8, hhv_contract_initializer_after_init_40_C_214_0_P_9, hhv_contract_initializer_after_init_40_C_214_0_Q_10, hhv_contract_initializer_after_init_40_C_214_0_R_11, hhv_contract_initializer_after_init_40_C_214_0_S_12, hhv_contract_initializer_after_init_40_C_214_0_T_13, hhv_contract_initializer_after_init_40_C_214_0_U_14, hhv_contract_initializer_after_init_40_C_214_0_V_15, hhv_contract_initializer_after_init_40_C_214_0_W_16, hhv_contract_initializer_after_init_40_C_214_0_X_17, hhv_contract_initializer_after_init_40_C_214_0_Y_18, hhv_contract_initializer_after_init_40_C_214_0_Z_19, hhv_contract_initializer_after_init_40_C_214_0_A1_20, hhv_contract_initializer_after_init_40_C_214_0_J_21, hhv_contract_initializer_after_init_40_C_214_0_K_22, hhv_contract_initializer_after_init_40_C_214_0_F_23, hhv_contract_initializer_after_init_40_C_214_0_H_24, hhv_contract_initializer_after_init_40_C_214_0_G_25, hhv_contract_initializer_after_init_40_C_214_0_I_26);
      VAL   [hhv_contract_initializer_entry_39_C_214_0_E_0=0, hhv_contract_initializer_entry_39_C_214_0_F_23=0, hhv_contract_initializer_entry_39_C_214_0_G_25=0, hhv_contract_initializer_entry_39_C_214_0_H_24=0, hhv_contract_initializer_entry_39_C_214_0_I_26=0]
[L0]        assume ((hhv_contract_initializer_entry_39_C_214_0_E_0 == 0 && hhv_contract_initializer_entry_39_C_214_0_G_25 == hhv_contract_initializer_entry_39_C_214_0_F_23) && hhv_contract_initializer_entry_39_C_214_0_I_26 == hhv_contract_initializer_entry_39_C_214_0_H_24) && hhv_contract_initializer_entry_39_C_214_0_J_21 == hhv_contract_initializer_entry_39_C_214_0_K_22;
      VAL   [hhv_contract_initializer_entry_39_C_214_0_E_0=0, hhv_contract_initializer_entry_39_C_214_0_F_23=0, hhv_contract_initializer_entry_39_C_214_0_G_25=0, hhv_contract_initializer_entry_39_C_214_0_H_24=0, hhv_contract_initializer_entry_39_C_214_0_I_26=0]
[L0]  RET   call contract_initializer_entry_39_C_214_0(hhv_contract_initializer_after_init_40_C_214_0_E_0, hhv_contract_initializer_after_init_40_C_214_0_L_1, hhv_contract_initializer_after_init_40_C_214_0_A_2, hhv_contract_initializer_after_init_40_C_214_0_B_3, hhv_contract_initializer_after_init_40_C_214_0_C_4, hhv_contract_initializer_after_init_40_C_214_0_D_5, hhv_contract_initializer_after_init_40_C_214_0_M_6, hhv_contract_initializer_after_init_40_C_214_0_N_7, hhv_contract_initializer_after_init_40_C_214_0_O_8, hhv_contract_initializer_after_init_40_C_214_0_P_9, hhv_contract_initializer_after_init_40_C_214_0_Q_10, hhv_contract_initializer_after_init_40_C_214_0_R_11, hhv_contract_initializer_after_init_40_C_214_0_S_12, hhv_contract_initializer_after_init_40_C_214_0_T_13, hhv_contract_initializer_after_init_40_C_214_0_U_14, hhv_contract_initializer_after_init_40_C_214_0_V_15, hhv_contract_initializer_after_init_40_C_214_0_W_16, hhv_contract_initializer_after_init_40_C_214_0_X_17, hhv_contract_initializer_after_init_40_C_214_0_Y_18, hhv_contract_initializer_after_init_40_C_214_0_Z_19, hhv_contract_initializer_after_init_40_C_214_0_A1_20, hhv_contract_initializer_after_init_40_C_214_0_J_21, hhv_contract_initializer_after_init_40_C_214_0_K_22, hhv_contract_initializer_after_init_40_C_214_0_F_23, hhv_contract_initializer_after_init_40_C_214_0_H_24, hhv_contract_initializer_after_init_40_C_214_0_G_25, hhv_contract_initializer_after_init_40_C_214_0_I_26);
      VAL   [hhv_contract_initializer_after_init_40_C_214_0_A1_20=0, hhv_contract_initializer_after_init_40_C_214_0_E_0=0, hhv_contract_initializer_after_init_40_C_214_0_F_23=0, hhv_contract_initializer_after_init_40_C_214_0_G_25=0, hhv_contract_initializer_after_init_40_C_214_0_H_24=0, hhv_contract_initializer_after_init_40_C_214_0_I_26=0, hhv_contract_initializer_after_init_40_C_214_0_L_1=638722033, hhv_contract_initializer_after_init_40_C_214_0_M_6=0, hhv_contract_initializer_after_init_40_C_214_0_N_7=0, hhv_contract_initializer_after_init_40_C_214_0_O_8=0, hhv_contract_initializer_after_init_40_C_214_0_P_9=0, hhv_contract_initializer_after_init_40_C_214_0_Q_10=0, hhv_contract_initializer_after_init_40_C_214_0_R_11=0, hhv_contract_initializer_after_init_40_C_214_0_S_12=0, hhv_contract_initializer_after_init_40_C_214_0_V_15=638722035, hhv_contract_initializer_after_init_40_C_214_0_W_16=0, hhv_contract_initializer_after_init_40_C_214_0_X_17=638722040, hhv_contract_initializer_after_init_40_C_214_0_Y_18=0, hhv_contract_initializer_after_init_40_C_214_0_Z_19=0]
[L0]  RET   call contract_initializer_after_init_40_C_214_0(hhv_contract_initializer_38_C_214_0_E_0, hhv_contract_initializer_38_C_214_0_L_1, hhv_contract_initializer_38_C_214_0_A_2, hhv_contract_initializer_38_C_214_0_B_3, hhv_contract_initializer_38_C_214_0_C_4, hhv_contract_initializer_38_C_214_0_D_5, hhv_contract_initializer_38_C_214_0_M_6, hhv_contract_initializer_38_C_214_0_N_7, hhv_contract_initializer_38_C_214_0_O_8, hhv_contract_initializer_38_C_214_0_P_9, hhv_contract_initializer_38_C_214_0_Q_10, hhv_contract_initializer_38_C_214_0_R_11, hhv_contract_initializer_38_C_214_0_S_12, hhv_contract_initializer_38_C_214_0_T_13, hhv_contract_initializer_38_C_214_0_U_14, hhv_contract_initializer_38_C_214_0_V_15, hhv_contract_initializer_38_C_214_0_W_16, hhv_contract_initializer_38_C_214_0_X_17, hhv_contract_initializer_38_C_214_0_Y_18, hhv_contract_initializer_38_C_214_0_Z_19, hhv_contract_initializer_38_C_214_0_A1_20, hhv_contract_initializer_38_C_214_0_J_21, hhv_contract_initializer_38_C_214_0_K_22, hhv_contract_initializer_38_C_214_0_F_23, hhv_contract_initializer_38_C_214_0_H_24, hhv_contract_initializer_38_C_214_0_G_25, hhv_contract_initializer_38_C_214_0_I_26);
      VAL   [hhv_contract_initializer_38_C_214_0_A1_20=0, hhv_contract_initializer_38_C_214_0_E_0=0, hhv_contract_initializer_38_C_214_0_F_23=0, hhv_contract_initializer_38_C_214_0_G_25=0, hhv_contract_initializer_38_C_214_0_H_24=0, hhv_contract_initializer_38_C_214_0_I_26=0, hhv_contract_initializer_38_C_214_0_L_1=638722033, hhv_contract_initializer_38_C_214_0_M_6=0, hhv_contract_initializer_38_C_214_0_N_7=0, hhv_contract_initializer_38_C_214_0_O_8=0, hhv_contract_initializer_38_C_214_0_P_9=0, hhv_contract_initializer_38_C_214_0_Q_10=0, hhv_contract_initializer_38_C_214_0_R_11=0, hhv_contract_initializer_38_C_214_0_S_12=0, hhv_contract_initializer_38_C_214_0_V_15=638722035, hhv_contract_initializer_38_C_214_0_W_16=0, hhv_contract_initializer_38_C_214_0_X_17=638722040, hhv_contract_initializer_38_C_214_0_Y_18=0, hhv_contract_initializer_38_C_214_0_Z_19=0]
[L0]  RET   call contract_initializer_38_C_214_0(hhv_summary_constructor_2_C_214_0_F_0, hhv_summary_constructor_2_C_214_0_P_1, hhv_summary_constructor_2_C_214_0_A_2, hhv_summary_constructor_2_C_214_0_B_3, hhv_summary_constructor_2_C_214_0_C_4, hhv_summary_constructor_2_C_214_0_D_5, hhv_summary_constructor_2_C_214_0_Q_6, hhv_summary_constructor_2_C_214_0_R_7, hhv_summary_constructor_2_C_214_0_S_8, hhv_summary_constructor_2_C_214_0_T_9, hhv_summary_constructor_2_C_214_0_U_10, hhv_summary_constructor_2_C_214_0_V_11, hhv_summary_constructor_2_C_214_0_W_12, hhv_summary_constructor_2_C_214_0_X_13, hhv_summary_constructor_2_C_214_0_Y_14, hhv_summary_constructor_2_C_214_0_Z_15, hhv_summary_constructor_2_C_214_0_A1_16, hhv_summary_constructor_2_C_214_0_B1_17, hhv_summary_constructor_2_C_214_0_C1_18, hhv_summary_constructor_2_C_214_0_D1_19, hhv_summary_constructor_2_C_214_0_E1_20, hbv_summary_constructor_2_C_214_0_N_1, hhv_summary_constructor_2_C_214_0_O_22, hbv_summary_constructor_2_C_214_0_H_2, hbv_summary_constructor_2_C_214_0_K_3, hhv_summary_constructor_2_C_214_0_I_25, hhv_summary_constructor_2_C_214_0_L_26);
      VAL   [hbv_summary_constructor_2_C_214_0_H_2=0, hbv_summary_constructor_2_C_214_0_K_3=0, hhv_summary_constructor_2_C_214_0_A1_16=0, hhv_summary_constructor_2_C_214_0_B1_17=638722040, hhv_summary_constructor_2_C_214_0_C1_18=0, hhv_summary_constructor_2_C_214_0_D1_19=0, hhv_summary_constructor_2_C_214_0_E1_20=0, hhv_summary_constructor_2_C_214_0_F_0=0, hhv_summary_constructor_2_C_214_0_G_23=0, hhv_summary_constructor_2_C_214_0_I_25=0, hhv_summary_constructor_2_C_214_0_J_24=0, hhv_summary_constructor_2_C_214_0_L_26=0, hhv_summary_constructor_2_C_214_0_P_1=638722033, hhv_summary_constructor_2_C_214_0_Q_6=0, hhv_summary_constructor_2_C_214_0_R_7=0, hhv_summary_constructor_2_C_214_0_S_8=0, hhv_summary_constructor_2_C_214_0_T_9=0, hhv_summary_constructor_2_C_214_0_U_10=0, hhv_summary_constructor_2_C_214_0_V_11=0, hhv_summary_constructor_2_C_214_0_W_12=0, hhv_summary_constructor_2_C_214_0_Z_15=638722035]
[L0]  CALL  call implicit_constructor_entry_41_C_214_0(hbv_summary_constructor_2_C_214_0_E_4, hhv_summary_constructor_2_C_214_0_P_1, hhv_summary_constructor_2_C_214_0_A_2, hhv_summary_constructor_2_C_214_0_B_3, hhv_summary_constructor_2_C_214_0_C_4, hhv_summary_constructor_2_C_214_0_D_5, hhv_summary_constructor_2_C_214_0_Q_6, hhv_summary_constructor_2_C_214_0_R_7, hhv_summary_constructor_2_C_214_0_S_8, hhv_summary_constructor_2_C_214_0_T_9, hhv_summary_constructor_2_C_214_0_U_10, hhv_summary_constructor_2_C_214_0_V_11, hhv_summary_constructor_2_C_214_0_W_12, hhv_summary_constructor_2_C_214_0_X_13, hhv_summary_constructor_2_C_214_0_Y_14, hhv_summary_constructor_2_C_214_0_Z_15, hhv_summary_constructor_2_C_214_0_A1_16, hhv_summary_constructor_2_C_214_0_B1_17, hhv_summary_constructor_2_C_214_0_C1_18, hhv_summary_constructor_2_C_214_0_D1_19, hhv_summary_constructor_2_C_214_0_E1_20, hhv_summary_constructor_2_C_214_0_M_21, hbv_summary_constructor_2_C_214_0_N_1, hhv_summary_constructor_2_C_214_0_G_23, hhv_summary_constructor_2_C_214_0_J_24, hbv_summary_constructor_2_C_214_0_H_2, hbv_summary_constructor_2_C_214_0_K_3);
      VAL   [hhv_implicit_constructor_entry_41_C_214_0_E_0=0, hhv_implicit_constructor_entry_41_C_214_0_F_23=0, hhv_implicit_constructor_entry_41_C_214_0_G_25=0, hhv_implicit_constructor_entry_41_C_214_0_H_24=0, hhv_implicit_constructor_entry_41_C_214_0_I_26=0, hhv_implicit_constructor_entry_41_C_214_0_L_1=638722033, hhv_implicit_constructor_entry_41_C_214_0_Y_18=0]
[L0]        assume (((((hhv_implicit_constructor_entry_41_C_214_0_I_26 == hhv_implicit_constructor_entry_41_C_214_0_H_24 && !(hhv_implicit_constructor_entry_41_C_214_0_K_22[hhv_implicit_constructor_entry_41_C_214_0_L_1] < hhv_implicit_constructor_entry_41_C_214_0_Y_18)) && hhv_implicit_constructor_entry_41_C_214_0_J_21 == hhv_implicit_constructor_entry_41_C_214_0_K_22) && hhv_implicit_constructor_entry_41_C_214_0_G_25 == 0) && hhv_implicit_constructor_entry_41_C_214_0_E_0 == 0) && hhv_implicit_constructor_entry_41_C_214_0_G_25 == hhv_implicit_constructor_entry_41_C_214_0_F_23) && hhv_implicit_constructor_entry_41_C_214_0_I_26 == 0;
      VAL   [hhv_implicit_constructor_entry_41_C_214_0_E_0=0, hhv_implicit_constructor_entry_41_C_214_0_F_23=0, hhv_implicit_constructor_entry_41_C_214_0_G_25=0, hhv_implicit_constructor_entry_41_C_214_0_H_24=0, hhv_implicit_constructor_entry_41_C_214_0_I_26=0, hhv_implicit_constructor_entry_41_C_214_0_L_1=638722033, hhv_implicit_constructor_entry_41_C_214_0_Y_18=0]
[L0]  RET   call implicit_constructor_entry_41_C_214_0(hbv_summary_constructor_2_C_214_0_E_4, hhv_summary_constructor_2_C_214_0_P_1, hhv_summary_constructor_2_C_214_0_A_2, hhv_summary_constructor_2_C_214_0_B_3, hhv_summary_constructor_2_C_214_0_C_4, hhv_summary_constructor_2_C_214_0_D_5, hhv_summary_constructor_2_C_214_0_Q_6, hhv_summary_constructor_2_C_214_0_R_7, hhv_summary_constructor_2_C_214_0_S_8, hhv_summary_constructor_2_C_214_0_T_9, hhv_summary_constructor_2_C_214_0_U_10, hhv_summary_constructor_2_C_214_0_V_11, hhv_summary_constructor_2_C_214_0_W_12, hhv_summary_constructor_2_C_214_0_X_13, hhv_summary_constructor_2_C_214_0_Y_14, hhv_summary_constructor_2_C_214_0_Z_15, hhv_summary_constructor_2_C_214_0_A1_16, hhv_summary_constructor_2_C_214_0_B1_17, hhv_summary_constructor_2_C_214_0_C1_18, hhv_summary_constructor_2_C_214_0_D1_19, hhv_summary_constructor_2_C_214_0_E1_20, hhv_summary_constructor_2_C_214_0_M_21, hbv_summary_constructor_2_C_214_0_N_1, hhv_summary_constructor_2_C_214_0_G_23, hhv_summary_constructor_2_C_214_0_J_24, hbv_summary_constructor_2_C_214_0_H_2, hbv_summary_constructor_2_C_214_0_K_3);
      VAL   [hbv_summary_constructor_2_C_214_0_E_4=0, hbv_summary_constructor_2_C_214_0_H_2=0, hbv_summary_constructor_2_C_214_0_K_3=0, hhv_summary_constructor_2_C_214_0_A1_16=0, hhv_summary_constructor_2_C_214_0_B1_17=638722040, hhv_summary_constructor_2_C_214_0_C1_18=0, hhv_summary_constructor_2_C_214_0_D1_19=0, hhv_summary_constructor_2_C_214_0_E1_20=0, hhv_summary_constructor_2_C_214_0_F_0=0, hhv_summary_constructor_2_C_214_0_G_23=0, hhv_summary_constructor_2_C_214_0_I_25=0, hhv_summary_constructor_2_C_214_0_J_24=0, hhv_summary_constructor_2_C_214_0_L_26=0, hhv_summary_constructor_2_C_214_0_P_1=638722033, hhv_summary_constructor_2_C_214_0_Q_6=0, hhv_summary_constructor_2_C_214_0_R_7=0, hhv_summary_constructor_2_C_214_0_S_8=0, hhv_summary_constructor_2_C_214_0_T_9=0, hhv_summary_constructor_2_C_214_0_U_10=0, hhv_summary_constructor_2_C_214_0_V_11=0, hhv_summary_constructor_2_C_214_0_W_12=0, hhv_summary_constructor_2_C_214_0_Z_15=638722035]
[L0]  RET   call summary_constructor_2_C_214_0(hbv_interface_0_C_214_0_M_2, hhv_interface_0_C_214_0_L_0, hhv_interface_0_C_214_0_A_1, hhv_interface_0_C_214_0_B_2, hhv_interface_0_C_214_0_C_3, hhv_interface_0_C_214_0_D_4, hbv_interface_0_C_214_0_Q_9, hbv_interface_0_C_214_0_P_8, hbv_interface_0_C_214_0_W_12, hbv_interface_0_C_214_0_S_11, hbv_interface_0_C_214_0_O_7, hbv_interface_0_C_214_0_E_1, hbv_interface_0_C_214_0_F_3, hbv_interface_0_C_214_0_U_13, hbv_interface_0_C_214_0_U_14, hbv_interface_0_C_214_0_W_15, hbv_interface_0_C_214_0_H_4, hbv_interface_0_C_214_0_X_16, hbv_interface_0_C_214_0_M_5, hbv_interface_0_C_214_0_N_6, hbv_interface_0_C_214_0_R_10, hbv_interface_0_C_214_0_J_17, hhv_interface_0_C_214_0_K_5, hbv_interface_0_C_214_0_Z_18, hbv_interface_0_C_214_0_A1_19, hhv_interface_0_C_214_0_G_6, hhv_interface_0_C_214_0_I_7);
      VAL   [hbv_interface_0_C_214_0_A1_19=0, hbv_interface_0_C_214_0_E_1=0, hbv_interface_0_C_214_0_F_3=0, hbv_interface_0_C_214_0_H_4=0, hbv_interface_0_C_214_0_M_2=0, hbv_interface_0_C_214_0_M_5=0, hbv_interface_0_C_214_0_N_6=0, hbv_interface_0_C_214_0_O_7=0, hbv_interface_0_C_214_0_P_8=0, hbv_interface_0_C_214_0_Q_9=0, hbv_interface_0_C_214_0_R_10=0, hbv_interface_0_C_214_0_S_11=0, hbv_interface_0_C_214_0_W_12=0, hbv_interface_0_C_214_0_W_15=638722035, hbv_interface_0_C_214_0_X_16=638722040, hbv_interface_0_C_214_0_Z_18=0, hhv_interface_0_C_214_0_G_6=0, hhv_interface_0_C_214_0_I_7=0, hhv_interface_0_C_214_0_L_0=638722033]
[L0]  RET   call interface_0_C_214_0(hbv_error_target_31_0_L_2, hbv_error_target_31_0_A_3, hbv_error_target_31_0_B_4, hbv_error_target_31_0_C_5, hbv_error_target_31_0_D_6, hbv_error_target_31_0_J_7, hbv_error_target_31_0_F_8, hbv_error_target_31_0_H_9);
      VAL   [hbv_error_target_31_0_E_1=6, hbv_error_target_31_0_F_8=0, hbv_error_target_31_0_H_9=0, hbv_error_target_31_0_L_2=638722033]
[L0]  CALL  call summary_4_function_f__123_214_0(hbv_error_target_31_0_E_1, hbv_error_target_31_0_L_2, hbv_error_target_31_0_A_3, hbv_error_target_31_0_B_4, hbv_error_target_31_0_C_5, hbv_error_target_31_0_D_6, hbv_error_target_31_0_M_10, hbv_error_target_31_0_N_11, hbv_error_target_31_0_O_12, hbv_error_target_31_0_P_13, hbv_error_target_31_0_Q_14, hbv_error_target_31_0_R_15, hbv_error_target_31_0_S_16, hbv_error_target_31_0_T_17, hbv_error_target_31_0_U_18, hbv_error_target_31_0_V_19, hbv_error_target_31_0_W_20, hbv_error_target_31_0_X_21, hbv_error_target_31_0_Y_22, hbv_error_target_31_0_Z_23, hbv_error_target_31_0_A1_24, hbv_error_target_31_0_J_7, hbv_error_target_31_0_F_8, hbv_error_target_31_0_H_9, hbv_error_target_31_0_K_25, hbv_error_target_31_0_G_26, hbv_error_target_31_0_I_27);
      VAL   [hhv_summary_4_function_f__123_214_0_B1_15=4, hhv_summary_4_function_f__123_214_0_C1_16=10, hhv_summary_4_function_f__123_214_0_D1_17=638722032, hhv_summary_4_function_f__123_214_0_E1_18=0, hhv_summary_4_function_f__123_214_0_F1_19=6, hhv_summary_4_function_f__123_214_0_F_0=6, hhv_summary_4_function_f__123_214_0_G1_20=7, hhv_summary_4_function_f__123_214_0_H_22=0, hhv_summary_4_function_f__123_214_0_J_25=0, hhv_summary_4_function_f__123_214_0_K_23=0, hhv_summary_4_function_f__123_214_0_M_26=0, hhv_summary_4_function_f__123_214_0_R_1=638722033, hhv_summary_4_function_f__123_214_0_S_6=9, hhv_summary_4_function_f__123_214_0_T_7=5, hhv_summary_4_function_f__123_214_0_U_8=14, hhv_summary_4_function_f__123_214_0_V_9=12, hhv_summary_4_function_f__123_214_0_W_10=15, hhv_summary_4_function_f__123_214_0_X_11=11, hhv_summary_4_function_f__123_214_0_Y_12=13]
[L0]        assume (((((((((((((((((((((((((((((((((((!(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_V_9) && !(hbv_summary_4_function_f__123_214_0_G_4 < hhv_summary_4_function_f__123_214_0_E1_18)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_E1_18)) && 31 == hhv_summary_4_function_f__123_214_0_A1_14[2]) && !(hhv_summary_4_function_f__123_214_0_V_9 < 0)) && !(1461501637330902918203684832716283019655932542975 < hhv_summary_4_function_f__123_214_0_U_8)) && !(hhv_summary_4_function_f__123_214_0_G1_20 < 0)) && !(hbv_summary_4_function_f__123_214_0_G_4 + hbv_summary_4_function_f__123_214_0_O_3[hhv_summary_4_function_f__123_214_0_R_1] < 0)) && hbv_summary_4_function_f__123_214_0_E_1 == 0) && !(1461501637330902918203684832716283019655932542975 < hhv_summary_4_function_f__123_214_0_C1_16)) && !(hhv_summary_4_function_f__123_214_0_Y_12 < 0)) && 638722032 == hhv_summary_4_function_f__123_214_0_D1_17) && hbv_summary_4_function_f__123_214_0_I_5 == hhv_summary_4_function_f__123_214_0_H_22) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_S_6)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_summary_4_function_f__123_214_0_G_4 + hbv_summary_4_function_f__123_214_0_O_3[hhv_summary_4_function_f__123_214_0_R_1])) && !(1461501637330902918203684832716283019655932542975 < hhv_summary_4_function_f__123_214_0_G1_20)) && !(hhv_summary_4_function_f__123_214_0_W_10 < 0)) && !(hhv_summary_4_function_f__123_214_0_S_6 < 0)) && hbv_summary_4_function_f__123_214_0_O_3[hhv_summary_4_function_f__123_214_0_R_1 := hbv_summary_4_function_f__123_214_0_G_4 + hbv_summary_4_function_f__123_214_0_O_3[hhv_summary_4_function_f__123_214_0_R_1]] == hbv_summary_4_function_f__123_214_0_P_6) && !(hhv_summary_4_function_f__123_214_0_F1_19 < 0)) && 18 == hhv_summary_4_function_f__123_214_0_A1_14[1]) && !(hhv_summary_4_function_f__123_214_0_C1_16 < 0)) && hhv_summary_4_function_f__123_214_0_A1_14[3] == 240) && hhv_summary_4_function_f__123_214_0_A1_14[0] == 38) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_W_10)) && hbv_summary_4_function_f__123_214_0_L_2 == hhv_summary_4_function_f__123_214_0_K_23) && !(hhv_summary_4_function_f__123_214_0_E1_18 < 0)) && !(hhv_summary_4_function_f__123_214_0_U_8 < 0)) && hhv_summary_4_function_f__123_214_0_N_21 == hbv_summary_4_function_f__123_214_0_O_3) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_F1_19)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_T_7)) && hhv_summary_4_function_f__123_214_0_E1_18 == 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_Y_12)) && !(hhv_summary_4_function_f__123_214_0_T_7 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__123_214_0_X_11)) && !(hhv_summary_4_function_f__123_214_0_B1_15 < 4)) && !(hhv_summary_4_function_f__123_214_0_X_11 < 0);
      VAL   [hbv_summary_4_function_f__123_214_0_E_1=0, hbv_summary_4_function_f__123_214_0_I_5=0, hbv_summary_4_function_f__123_214_0_L_2=0, hhv_summary_4_function_f__123_214_0_B1_15=4, hhv_summary_4_function_f__123_214_0_C1_16=10, hhv_summary_4_function_f__123_214_0_D1_17=638722032, hhv_summary_4_function_f__123_214_0_E1_18=0, hhv_summary_4_function_f__123_214_0_F1_19=6, hhv_summary_4_function_f__123_214_0_F_0=6, hhv_summary_4_function_f__123_214_0_G1_20=7, hhv_summary_4_function_f__123_214_0_H_22=0, hhv_summary_4_function_f__123_214_0_J_25=0, hhv_summary_4_function_f__123_214_0_K_23=0, hhv_summary_4_function_f__123_214_0_M_26=0, hhv_summary_4_function_f__123_214_0_R_1=638722033, hhv_summary_4_function_f__123_214_0_S_6=9, hhv_summary_4_function_f__123_214_0_T_7=5, hhv_summary_4_function_f__123_214_0_U_8=14, hhv_summary_4_function_f__123_214_0_V_9=12, hhv_summary_4_function_f__123_214_0_W_10=15, hhv_summary_4_function_f__123_214_0_X_11=11, hhv_summary_4_function_f__123_214_0_Y_12=13]
[L0]  CALL  call summary_3_function_f__123_214_0(hhv_summary_4_function_f__123_214_0_F_0, hhv_summary_4_function_f__123_214_0_R_1, hhv_summary_4_function_f__123_214_0_A_2, hhv_summary_4_function_f__123_214_0_B_3, hhv_summary_4_function_f__123_214_0_C_4, hhv_summary_4_function_f__123_214_0_D_5, hhv_summary_4_function_f__123_214_0_S_6, hhv_summary_4_function_f__123_214_0_T_7, hhv_summary_4_function_f__123_214_0_U_8, hhv_summary_4_function_f__123_214_0_V_9, hhv_summary_4_function_f__123_214_0_W_10, hhv_summary_4_function_f__123_214_0_X_11, hhv_summary_4_function_f__123_214_0_Y_12, hhv_summary_4_function_f__123_214_0_Z_13, hhv_summary_4_function_f__123_214_0_A1_14, hhv_summary_4_function_f__123_214_0_B1_15, hhv_summary_4_function_f__123_214_0_C1_16, hhv_summary_4_function_f__123_214_0_D1_17, hhv_summary_4_function_f__123_214_0_E1_18, hhv_summary_4_function_f__123_214_0_F1_19, hhv_summary_4_function_f__123_214_0_G1_20, hbv_summary_4_function_f__123_214_0_P_6, hbv_summary_4_function_f__123_214_0_I_5, hbv_summary_4_function_f__123_214_0_L_2, hhv_summary_4_function_f__123_214_0_Q_24, hhv_summary_4_function_f__123_214_0_J_25, hhv_summary_4_function_f__123_214_0_M_26);
      VAL   [hhv_summary_3_function_f__123_214_0_A1_20=7, hhv_summary_3_function_f__123_214_0_E_0=6, hhv_summary_3_function_f__123_214_0_F_22=0, hhv_summary_3_function_f__123_214_0_G_25=0, hhv_summary_3_function_f__123_214_0_H_23=0, hhv_summary_3_function_f__123_214_0_I_26=0, hhv_summary_3_function_f__123_214_0_L_1=638722033, hhv_summary_3_function_f__123_214_0_M_6=9, hhv_summary_3_function_f__123_214_0_N_7=5, hhv_summary_3_function_f__123_214_0_O_8=14, hhv_summary_3_function_f__123_214_0_P_9=12, hhv_summary_3_function_f__123_214_0_Q_10=15, hhv_summary_3_function_f__123_214_0_R_11=11, hhv_summary_3_function_f__123_214_0_S_12=13, hhv_summary_3_function_f__123_214_0_V_15=4, hhv_summary_3_function_f__123_214_0_W_16=10, hhv_summary_3_function_f__123_214_0_X_17=638722032, hhv_summary_3_function_f__123_214_0_Y_18=0, hhv_summary_3_function_f__123_214_0_Z_19=6]
[L0]  CALL  call block_15_function_f__123_214_0(hhv_summary_3_function_f__123_214_0_E_0, hhv_summary_3_function_f__123_214_0_L_1, hhv_summary_3_function_f__123_214_0_A_2, hhv_summary_3_function_f__123_214_0_B_3, hhv_summary_3_function_f__123_214_0_C_4, hhv_summary_3_function_f__123_214_0_D_5, hhv_summary_3_function_f__123_214_0_M_6, hhv_summary_3_function_f__123_214_0_N_7, hhv_summary_3_function_f__123_214_0_O_8, hhv_summary_3_function_f__123_214_0_P_9, hhv_summary_3_function_f__123_214_0_Q_10, hhv_summary_3_function_f__123_214_0_R_11, hhv_summary_3_function_f__123_214_0_S_12, hhv_summary_3_function_f__123_214_0_T_13, hhv_summary_3_function_f__123_214_0_U_14, hhv_summary_3_function_f__123_214_0_V_15, hhv_summary_3_function_f__123_214_0_W_16, hhv_summary_3_function_f__123_214_0_X_17, hhv_summary_3_function_f__123_214_0_Y_18, hhv_summary_3_function_f__123_214_0_Z_19, hhv_summary_3_function_f__123_214_0_A1_20, hhv_summary_3_function_f__123_214_0_J_21, hhv_summary_3_function_f__123_214_0_F_22, hhv_summary_3_function_f__123_214_0_H_23, hhv_summary_3_function_f__123_214_0_K_24, hhv_summary_3_function_f__123_214_0_G_25, hhv_summary_3_function_f__123_214_0_I_26);
      VAL   [hhv_block_15_function_f__123_214_0_B2_1=638722033, hhv_block_15_function_f__123_214_0_C2_6=9, hhv_block_15_function_f__123_214_0_D2_7=5, hhv_block_15_function_f__123_214_0_E2_8=14, hhv_block_15_function_f__123_214_0_F2_9=12, hhv_block_15_function_f__123_214_0_G2_10=15, hhv_block_15_function_f__123_214_0_H2_11=11, hhv_block_15_function_f__123_214_0_I2_12=13, hhv_block_15_function_f__123_214_0_K_0=6, hhv_block_15_function_f__123_214_0_L2_15=4, hhv_block_15_function_f__123_214_0_M2_16=10, hhv_block_15_function_f__123_214_0_N2_17=638722032, hhv_block_15_function_f__123_214_0_O2_18=0, hhv_block_15_function_f__123_214_0_P2_19=6, hhv_block_15_function_f__123_214_0_Q2_20=7, hhv_block_15_function_f__123_214_0_V1_22=0, hhv_block_15_function_f__123_214_0_W1_25=0, hhv_block_15_function_f__123_214_0_X1_23=0, hhv_block_15_function_f__123_214_0_Y1_26=0]
[L0]        assume ((((((((((((((((((((((((((((((((((((((((((!!hbv_block_15_function_f__123_214_0_G1_19 && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_block_15_function_f__123_214_0_Z_8)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_block_15_function_f__123_214_0_E1_1)) && hhv_block_15_function_f__123_214_0_W1_25 == hbv_block_15_function_f__123_214_0_Q_23) && hbv_block_15_function_f__123_214_0_U1_26 == 0) && !(0 <= hbv_block_15_function_f__123_214_0_U1_26 && hbv_block_15_function_f__123_214_0_U1_26 < hbv_block_15_function_f__123_214_0_T1_29)) && hbv_block_15_function_f__123_214_0_V_2 == hbv_block_15_function_f__123_214_0_U_40) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_block_15_function_f__123_214_0_S_7)) && hbv_block_15_function_f__123_214_0_H_32 == hbv_block_15_function_f__123_214_0_G_20) && 6 == hhv_block_15_function_f__123_214_0_K_0) && !((!hbv_block_15_function_f__123_214_0_W_36 || hbv_block_15_function_f__123_214_0_V_2 != hbv_block_15_function_f__123_214_0_S_7) && (hbv_block_15_function_f__123_214_0_W_36 || hbv_block_15_function_f__123_214_0_V_2 == hbv_block_15_function_f__123_214_0_S_7))) && !(hbv_block_15_function_f__123_214_0_Z_8 < 0)) && hhv_block_15_function_f__123_214_0_Y1_26 == hbv_block_15_function_f__123_214_0_T_33) && hbv_block_15_function_f__123_214_0_Z_8 == hbv_block_15_function_f__123_214_0_Y_41) && hbv_block_15_function_f__123_214_0_S_7 == hbv_block_15_function_f__123_214_0_R_25) && !((!hbv_block_15_function_f__123_214_0_P_17 || hbv_block_15_function_f__123_214_0_O_15 != hbv_block_15_function_f__123_214_0_M_16) && (hbv_block_15_function_f__123_214_0_P_17 || hbv_block_15_function_f__123_214_0_O_15 == hbv_block_15_function_f__123_214_0_M_16))) && !(hbv_block_15_function_f__123_214_0_Z_8 <= hbv_block_15_function_f__123_214_0_A1_27 && hbv_block_15_function_f__123_214_0_B1_28)) && hhv_block_15_function_f__123_214_0_Y1_26 == hbv_block_15_function_f__123_214_0_N_37) && hbv_block_15_function_f__123_214_0_O1_14 == 0) && !((hbv_block_15_function_f__123_214_0_R1_5 || hbv_block_15_function_f__123_214_0_Q1_3 == hbv_block_15_function_f__123_214_0_L1_4) && (!hbv_block_15_function_f__123_214_0_R1_5 || hbv_block_15_function_f__123_214_0_Q1_3 != hbv_block_15_function_f__123_214_0_L1_4))) && hhv_block_15_function_f__123_214_0_W1_25 == hbv_block_15_function_f__123_214_0_X_38) && hbv_block_15_function_f__123_214_0_A1_27 == 0) && !!hbv_block_15_function_f__123_214_0_B1_28) && hbv_block_15_function_f__123_214_0_J_39 == hbv_block_15_function_f__123_214_0_I_34) && hbv_block_15_function_f__123_214_0_P1_31 == hbv_block_15_function_f__123_214_0_N1_30[hbv_block_15_function_f__123_214_0_O1_14]) && hbv_block_15_function_f__123_214_0_G_20 == hbv_block_15_function_f__123_214_0_F_21) && !(hbv_block_15_function_f__123_214_0_E1_1 <= hbv_block_15_function_f__123_214_0_F1_18 && hbv_block_15_function_f__123_214_0_G1_19)) && !(hbv_block_15_function_f__123_214_0_E1_1 < 0)) && !(hbv_block_15_function_f__123_214_0_V_2 < 0)) && hhv_block_15_function_f__123_214_0_Y1_26 == hbv_block_15_function_f__123_214_0_C1_42) && hbv_block_15_function_f__123_214_0_E1_1 == hbv_block_15_function_f__123_214_0_D1_9) && hhv_block_15_function_f__123_214_0_W1_25 == hbv_block_15_function_f__123_214_0_L_22) && hhv_block_15_function_f__123_214_0_W1_25 == hbv_block_15_function_f__123_214_0_H1_35) && hbv_block_15_function_f__123_214_0_I_34 == hbv_block_15_function_f__123_214_0_H_32) && hbv_block_15_function_f__123_214_0_F_21 == hbv_block_15_function_f__123_214_0_E_24) && !(!hbv_block_15_function_f__123_214_0_B1_28 && hbv_block_15_function_f__123_214_0_A1_27 < hbv_block_15_function_f__123_214_0_Z_8)) && !(!hbv_block_15_function_f__123_214_0_G1_19 && hbv_block_15_function_f__123_214_0_F1_18 < hbv_block_15_function_f__123_214_0_E1_1)) && !(hbv_block_15_function_f__123_214_0_S_7 < 0)) && hhv_block_15_function_f__123_214_0_Y1_26 == hbv_block_15_function_f__123_214_0_M1_6) && hbv_block_15_function_f__123_214_0_K1_13 == hbv_block_15_function_f__123_214_0_I1_11[hbv_block_15_function_f__123_214_0_J1_12]) && hhv_block_15_function_f__123_214_0_W1_25 == hbv_block_15_function_f__123_214_0_S1_10) && hbv_block_15_function_f__123_214_0_F1_18 == 0) && hbv_block_15_function_f__123_214_0_J1_12 == 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_block_15_function_f__123_214_0_V_2);
      VAL   [hbv_block_15_function_f__123_214_0_E_24=0, hhv_block_15_function_f__123_214_0_B2_1=638722033, hhv_block_15_function_f__123_214_0_C2_6=9, hhv_block_15_function_f__123_214_0_D2_7=5, hhv_block_15_function_f__123_214_0_E2_8=14, hhv_block_15_function_f__123_214_0_F2_9=12, hhv_block_15_function_f__123_214_0_G2_10=15, hhv_block_15_function_f__123_214_0_H2_11=11, hhv_block_15_function_f__123_214_0_I2_12=13, hhv_block_15_function_f__123_214_0_K_0=6, hhv_block_15_function_f__123_214_0_L2_15=4, hhv_block_15_function_f__123_214_0_M2_16=10, hhv_block_15_function_f__123_214_0_N2_17=638722032, hhv_block_15_function_f__123_214_0_O2_18=0, hhv_block_15_function_f__123_214_0_P2_19=6, hhv_block_15_function_f__123_214_0_Q2_20=7, hhv_block_15_function_f__123_214_0_V1_22=0, hhv_block_15_function_f__123_214_0_W1_25=0, hhv_block_15_function_f__123_214_0_X1_23=0, hhv_block_15_function_f__123_214_0_Y1_26=0]
[L0]  CALL  call block_8_f_122_214_0(hbv_block_15_function_f__123_214_0_E_24, hhv_block_15_function_f__123_214_0_B2_1, hhv_block_15_function_f__123_214_0_A_2, hhv_block_15_function_f__123_214_0_B_3, hhv_block_15_function_f__123_214_0_C_4, hhv_block_15_function_f__123_214_0_D_5, hhv_block_15_function_f__123_214_0_C2_6, hhv_block_15_function_f__123_214_0_D2_7, hhv_block_15_function_f__123_214_0_E2_8, hhv_block_15_function_f__123_214_0_F2_9, hhv_block_15_function_f__123_214_0_G2_10, hhv_block_15_function_f__123_214_0_H2_11, hhv_block_15_function_f__123_214_0_I2_12, hhv_block_15_function_f__123_214_0_J2_13, hhv_block_15_function_f__123_214_0_K2_14, hhv_block_15_function_f__123_214_0_L2_15, hhv_block_15_function_f__123_214_0_M2_16, hhv_block_15_function_f__123_214_0_N2_17, hhv_block_15_function_f__123_214_0_O2_18, hhv_block_15_function_f__123_214_0_P2_19, hhv_block_15_function_f__123_214_0_Q2_20, hhv_block_15_function_f__123_214_0_Z1_21, hhv_block_15_function_f__123_214_0_V1_22, hhv_block_15_function_f__123_214_0_X1_23, hhv_block_15_function_f__123_214_0_A2_24, hhv_block_15_function_f__123_214_0_W1_25, hhv_block_15_function_f__123_214_0_Y1_26);
      VAL   [hhv_block_8_f_122_214_0_A1_20=7, hhv_block_8_f_122_214_0_E_0=0, hhv_block_8_f_122_214_0_F_22=0, hhv_block_8_f_122_214_0_G_25=0, hhv_block_8_f_122_214_0_H_23=0, hhv_block_8_f_122_214_0_I_26=0, hhv_block_8_f_122_214_0_L_1=638722033, hhv_block_8_f_122_214_0_M_6=9, hhv_block_8_f_122_214_0_N_7=5, hhv_block_8_f_122_214_0_O_8=14, hhv_block_8_f_122_214_0_P_9=12, hhv_block_8_f_122_214_0_Q_10=15, hhv_block_8_f_122_214_0_R_11=11, hhv_block_8_f_122_214_0_S_12=13, hhv_block_8_f_122_214_0_V_15=4, hhv_block_8_f_122_214_0_W_16=10, hhv_block_8_f_122_214_0_X_17=638722032, hhv_block_8_f_122_214_0_Y_18=0, hhv_block_8_f_122_214_0_Z_19=6]
[L0]        assume ((hhv_block_8_f_122_214_0_I_26 == hhv_block_8_f_122_214_0_H_23 && hhv_block_8_f_122_214_0_G_25 == hhv_block_8_f_122_214_0_F_22) && hhv_block_8_f_122_214_0_J_21 == hhv_block_8_f_122_214_0_K_24) && hhv_block_8_f_122_214_0_E_0 == 0;
      VAL   [hhv_block_8_f_122_214_0_A1_20=7, hhv_block_8_f_122_214_0_E_0=0, hhv_block_8_f_122_214_0_F_22=0, hhv_block_8_f_122_214_0_G_25=0, hhv_block_8_f_122_214_0_H_23=0, hhv_block_8_f_122_214_0_I_26=0, hhv_block_8_f_122_214_0_L_1=638722033, hhv_block_8_f_122_214_0_M_6=9, hhv_block_8_f_122_214_0_N_7=5, hhv_block_8_f_122_214_0_O_8=14, hhv_block_8_f_122_214_0_P_9=12, hhv_block_8_f_122_214_0_Q_10=15, hhv_block_8_f_122_214_0_R_11=11, hhv_block_8_f_122_214_0_S_12=13, hhv_block_8_f_122_214_0_V_15=4, hhv_block_8_f_122_214_0_W_16=10, hhv_block_8_f_122_214_0_X_17=638722032, hhv_block_8_f_122_214_0_Y_18=0, hhv_block_8_f_122_214_0_Z_19=6]
[L0]  CALL  call block_7_function_f__123_214_0(hhv_block_8_f_122_214_0_E_0, hhv_block_8_f_122_214_0_L_1, hhv_block_8_f_122_214_0_A_2, hhv_block_8_f_122_214_0_B_3, hhv_block_8_f_122_214_0_C_4, hhv_block_8_f_122_214_0_D_5, hhv_block_8_f_122_214_0_M_6, hhv_block_8_f_122_214_0_N_7, hhv_block_8_f_122_214_0_O_8, hhv_block_8_f_122_214_0_P_9, hhv_block_8_f_122_214_0_Q_10, hhv_block_8_f_122_214_0_R_11, hhv_block_8_f_122_214_0_S_12, hhv_block_8_f_122_214_0_T_13, hhv_block_8_f_122_214_0_U_14, hhv_block_8_f_122_214_0_V_15, hhv_block_8_f_122_214_0_W_16, hhv_block_8_f_122_214_0_X_17, hhv_block_8_f_122_214_0_Y_18, hhv_block_8_f_122_214_0_Z_19, hhv_block_8_f_122_214_0_A1_20, hhv_block_8_f_122_214_0_J_21, hhv_block_8_f_122_214_0_F_22, hhv_block_8_f_122_214_0_H_23, hhv_block_8_f_122_214_0_K_24, hhv_block_8_f_122_214_0_G_25, hhv_block_8_f_122_214_0_I_26);
[L0]  RET   call block_7_function_f__123_214_0(hhv_block_8_f_122_214_0_E_0, hhv_block_8_f_122_214_0_L_1, hhv_block_8_f_122_214_0_A_2, hhv_block_8_f_122_214_0_B_3, hhv_block_8_f_122_214_0_C_4, hhv_block_8_f_122_214_0_D_5, hhv_block_8_f_122_214_0_M_6, hhv_block_8_f_122_214_0_N_7, hhv_block_8_f_122_214_0_O_8, hhv_block_8_f_122_214_0_P_9, hhv_block_8_f_122_214_0_Q_10, hhv_block_8_f_122_214_0_R_11, hhv_block_8_f_122_214_0_S_12, hhv_block_8_f_122_214_0_T_13, hhv_block_8_f_122_214_0_U_14, hhv_block_8_f_122_214_0_V_15, hhv_block_8_f_122_214_0_W_16, hhv_block_8_f_122_214_0_X_17, hhv_block_8_f_122_214_0_Y_18, hhv_block_8_f_122_214_0_Z_19, hhv_block_8_f_122_214_0_A1_20, hhv_block_8_f_122_214_0_J_21, hhv_block_8_f_122_214_0_F_22, hhv_block_8_f_122_214_0_H_23, hhv_block_8_f_122_214_0_K_24, hhv_block_8_f_122_214_0_G_25, hhv_block_8_f_122_214_0_I_26);
      VAL   [hhv_block_8_f_122_214_0_A1_20=7, hhv_block_8_f_122_214_0_E_0=0, hhv_block_8_f_122_214_0_F_22=0, hhv_block_8_f_122_214_0_G_25=0, hhv_block_8_f_122_214_0_H_23=0, hhv_block_8_f_122_214_0_I_26=0, hhv_block_8_f_122_214_0_L_1=638722033, hhv_block_8_f_122_214_0_M_6=9, hhv_block_8_f_122_214_0_N_7=5, hhv_block_8_f_122_214_0_O_8=14, hhv_block_8_f_122_214_0_P_9=12, hhv_block_8_f_122_214_0_Q_10=15, hhv_block_8_f_122_214_0_R_11=11, hhv_block_8_f_122_214_0_S_12=13, hhv_block_8_f_122_214_0_V_15=4, hhv_block_8_f_122_214_0_W_16=10, hhv_block_8_f_122_214_0_X_17=638722032, hhv_block_8_f_122_214_0_Y_18=0, hhv_block_8_f_122_214_0_Z_19=6]
[L0]  RET   call block_8_f_122_214_0(hbv_block_15_function_f__123_214_0_E_24, hhv_block_15_function_f__123_214_0_B2_1, hhv_block_15_function_f__123_214_0_A_2, hhv_block_15_function_f__123_214_0_B_3, hhv_block_15_function_f__123_214_0_C_4, hhv_block_15_function_f__123_214_0_D_5, hhv_block_15_function_f__123_214_0_C2_6, hhv_block_15_function_f__123_214_0_D2_7, hhv_block_15_function_f__123_214_0_E2_8, hhv_block_15_function_f__123_214_0_F2_9, hhv_block_15_function_f__123_214_0_G2_10, hhv_block_15_function_f__123_214_0_H2_11, hhv_block_15_function_f__123_214_0_I2_12, hhv_block_15_function_f__123_214_0_J2_13, hhv_block_15_function_f__123_214_0_K2_14, hhv_block_15_function_f__123_214_0_L2_15, hhv_block_15_function_f__123_214_0_M2_16, hhv_block_15_function_f__123_214_0_N2_17, hhv_block_15_function_f__123_214_0_O2_18, hhv_block_15_function_f__123_214_0_P2_19, hhv_block_15_function_f__123_214_0_Q2_20, hhv_block_15_function_f__123_214_0_Z1_21, hhv_block_15_function_f__123_214_0_V1_22, hhv_block_15_function_f__123_214_0_X1_23, hhv_block_15_function_f__123_214_0_A2_24, hhv_block_15_function_f__123_214_0_W1_25, hhv_block_15_function_f__123_214_0_Y1_26);
      VAL   [hbv_block_15_function_f__123_214_0_E_24=0, hhv_block_15_function_f__123_214_0_B2_1=638722033, hhv_block_15_function_f__123_214_0_C2_6=9, hhv_block_15_function_f__123_214_0_D2_7=5, hhv_block_15_function_f__123_214_0_E2_8=14, hhv_block_15_function_f__123_214_0_F2_9=12, hhv_block_15_function_f__123_214_0_G2_10=15, hhv_block_15_function_f__123_214_0_H2_11=11, hhv_block_15_function_f__123_214_0_I2_12=13, hhv_block_15_function_f__123_214_0_K_0=6, hhv_block_15_function_f__123_214_0_L2_15=4, hhv_block_15_function_f__123_214_0_M2_16=10, hhv_block_15_function_f__123_214_0_N2_17=638722032, hhv_block_15_function_f__123_214_0_O2_18=0, hhv_block_15_function_f__123_214_0_P2_19=6, hhv_block_15_function_f__123_214_0_Q2_20=7, hhv_block_15_function_f__123_214_0_V1_22=0, hhv_block_15_function_f__123_214_0_W1_25=0, hhv_block_15_function_f__123_214_0_X1_23=0, hhv_block_15_function_f__123_214_0_Y1_26=0]
[L0]  RET   call block_15_function_f__123_214_0(hhv_summary_3_function_f__123_214_0_E_0, hhv_summary_3_function_f__123_214_0_L_1, hhv_summary_3_function_f__123_214_0_A_2, hhv_summary_3_function_f__123_214_0_B_3, hhv_summary_3_function_f__123_214_0_C_4, hhv_summary_3_function_f__123_214_0_D_5, hhv_summary_3_function_f__123_214_0_M_6, hhv_summary_3_function_f__123_214_0_N_7, hhv_summary_3_function_f__123_214_0_O_8, hhv_summary_3_function_f__123_214_0_P_9, hhv_summary_3_function_f__123_214_0_Q_10, hhv_summary_3_function_f__123_214_0_R_11, hhv_summary_3_function_f__123_214_0_S_12, hhv_summary_3_function_f__123_214_0_T_13, hhv_summary_3_function_f__123_214_0_U_14, hhv_summary_3_function_f__123_214_0_V_15, hhv_summary_3_function_f__123_214_0_W_16, hhv_summary_3_function_f__123_214_0_X_17, hhv_summary_3_function_f__123_214_0_Y_18, hhv_summary_3_function_f__123_214_0_Z_19, hhv_summary_3_function_f__123_214_0_A1_20, hhv_summary_3_function_f__123_214_0_J_21, hhv_summary_3_function_f__123_214_0_F_22, hhv_summary_3_function_f__123_214_0_H_23, hhv_summary_3_function_f__123_214_0_K_24, hhv_summary_3_function_f__123_214_0_G_25, hhv_summary_3_function_f__123_214_0_I_26);
      VAL   [hhv_summary_3_function_f__123_214_0_A1_20=7, hhv_summary_3_function_f__123_214_0_E_0=6, hhv_summary_3_function_f__123_214_0_F_22=0, hhv_summary_3_function_f__123_214_0_G_25=0, hhv_summary_3_function_f__123_214_0_H_23=0, hhv_summary_3_function_f__123_214_0_I_26=0, hhv_summary_3_function_f__123_214_0_L_1=638722033, hhv_summary_3_function_f__123_214_0_M_6=9, hhv_summary_3_function_f__123_214_0_N_7=5, hhv_summary_3_function_f__123_214_0_O_8=14, hhv_summary_3_function_f__123_214_0_P_9=12, hhv_summary_3_function_f__123_214_0_Q_10=15, hhv_summary_3_function_f__123_214_0_R_11=11, hhv_summary_3_function_f__123_214_0_S_12=13, hhv_summary_3_function_f__123_214_0_V_15=4, hhv_summary_3_function_f__123_214_0_W_16=10, hhv_summary_3_function_f__123_214_0_X_17=638722032, hhv_summary_3_function_f__123_214_0_Y_18=0, hhv_summary_3_function_f__123_214_0_Z_19=6]
[L0]  RET   call summary_3_function_f__123_214_0(hhv_summary_4_function_f__123_214_0_F_0, hhv_summary_4_function_f__123_214_0_R_1, hhv_summary_4_function_f__123_214_0_A_2, hhv_summary_4_function_f__123_214_0_B_3, hhv_summary_4_function_f__123_214_0_C_4, hhv_summary_4_function_f__123_214_0_D_5, hhv_summary_4_function_f__123_214_0_S_6, hhv_summary_4_function_f__123_214_0_T_7, hhv_summary_4_function_f__123_214_0_U_8, hhv_summary_4_function_f__123_214_0_V_9, hhv_summary_4_function_f__123_214_0_W_10, hhv_summary_4_function_f__123_214_0_X_11, hhv_summary_4_function_f__123_214_0_Y_12, hhv_summary_4_function_f__123_214_0_Z_13, hhv_summary_4_function_f__123_214_0_A1_14, hhv_summary_4_function_f__123_214_0_B1_15, hhv_summary_4_function_f__123_214_0_C1_16, hhv_summary_4_function_f__123_214_0_D1_17, hhv_summary_4_function_f__123_214_0_E1_18, hhv_summary_4_function_f__123_214_0_F1_19, hhv_summary_4_function_f__123_214_0_G1_20, hbv_summary_4_function_f__123_214_0_P_6, hbv_summary_4_function_f__123_214_0_I_5, hbv_summary_4_function_f__123_214_0_L_2, hhv_summary_4_function_f__123_214_0_Q_24, hhv_summary_4_function_f__123_214_0_J_25, hhv_summary_4_function_f__123_214_0_M_26);
      VAL   [hbv_summary_4_function_f__123_214_0_E_1=0, hbv_summary_4_function_f__123_214_0_I_5=0, hbv_summary_4_function_f__123_214_0_L_2=0, hhv_summary_4_function_f__123_214_0_B1_15=4, hhv_summary_4_function_f__123_214_0_C1_16=10, hhv_summary_4_function_f__123_214_0_D1_17=638722032, hhv_summary_4_function_f__123_214_0_E1_18=0, hhv_summary_4_function_f__123_214_0_F1_19=6, hhv_summary_4_function_f__123_214_0_F_0=6, hhv_summary_4_function_f__123_214_0_G1_20=7, hhv_summary_4_function_f__123_214_0_H_22=0, hhv_summary_4_function_f__123_214_0_J_25=0, hhv_summary_4_function_f__123_214_0_K_23=0, hhv_summary_4_function_f__123_214_0_M_26=0, hhv_summary_4_function_f__123_214_0_R_1=638722033, hhv_summary_4_function_f__123_214_0_S_6=9, hhv_summary_4_function_f__123_214_0_T_7=5, hhv_summary_4_function_f__123_214_0_U_8=14, hhv_summary_4_function_f__123_214_0_V_9=12, hhv_summary_4_function_f__123_214_0_W_10=15, hhv_summary_4_function_f__123_214_0_X_11=11, hhv_summary_4_function_f__123_214_0_Y_12=13]
[L0]  CALL  call block_25_function_f__123_214_0(hbv_summary_4_function_f__123_214_0_E_1, hhv_summary_4_function_f__123_214_0_R_1, hhv_summary_4_function_f__123_214_0_A_2, hhv_summary_4_function_f__123_214_0_B_3, hhv_summary_4_function_f__123_214_0_C_4, hhv_summary_4_function_f__123_214_0_D_5, hhv_summary_4_function_f__123_214_0_S_6, hhv_summary_4_function_f__123_214_0_T_7, hhv_summary_4_function_f__123_214_0_U_8, hhv_summary_4_function_f__123_214_0_V_9, hhv_summary_4_function_f__123_214_0_W_10, hhv_summary_4_function_f__123_214_0_X_11, hhv_summary_4_function_f__123_214_0_Y_12, hhv_summary_4_function_f__123_214_0_Z_13, hhv_summary_4_function_f__123_214_0_A1_14, hhv_summary_4_function_f__123_214_0_B1_15, hhv_summary_4_function_f__123_214_0_C1_16, hhv_summary_4_function_f__123_214_0_D1_17, hhv_summary_4_function_f__123_214_0_E1_18, hhv_summary_4_function_f__123_214_0_F1_19, hhv_summary_4_function_f__123_214_0_G1_20, hhv_summary_4_function_f__123_214_0_N_21, hhv_summary_4_function_f__123_214_0_H_22, hhv_summary_4_function_f__123_214_0_K_23, hbv_summary_4_function_f__123_214_0_O_3, hbv_summary_4_function_f__123_214_0_I_5, hbv_summary_4_function_f__123_214_0_L_2);
[L0]  RET   call block_25_function_f__123_214_0(hbv_summary_4_function_f__123_214_0_E_1, hhv_summary_4_function_f__123_214_0_R_1, hhv_summary_4_function_f__123_214_0_A_2, hhv_summary_4_function_f__123_214_0_B_3, hhv_summary_4_function_f__123_214_0_C_4, hhv_summary_4_function_f__123_214_0_D_5, hhv_summary_4_function_f__123_214_0_S_6, hhv_summary_4_function_f__123_214_0_T_7, hhv_summary_4_function_f__123_214_0_U_8, hhv_summary_4_function_f__123_214_0_V_9, hhv_summary_4_function_f__123_214_0_W_10, hhv_summary_4_function_f__123_214_0_X_11, hhv_summary_4_function_f__123_214_0_Y_12, hhv_summary_4_function_f__123_214_0_Z_13, hhv_summary_4_function_f__123_214_0_A1_14, hhv_summary_4_function_f__123_214_0_B1_15, hhv_summary_4_function_f__123_214_0_C1_16, hhv_summary_4_function_f__123_214_0_D1_17, hhv_summary_4_function_f__123_214_0_E1_18, hhv_summary_4_function_f__123_214_0_F1_19, hhv_summary_4_function_f__123_214_0_G1_20, hhv_summary_4_function_f__123_214_0_N_21, hhv_summary_4_function_f__123_214_0_H_22, hhv_summary_4_function_f__123_214_0_K_23, hbv_summary_4_function_f__123_214_0_O_3, hbv_summary_4_function_f__123_214_0_I_5, hbv_summary_4_function_f__123_214_0_L_2);
      VAL   [hbv_summary_4_function_f__123_214_0_E_1=0, hbv_summary_4_function_f__123_214_0_I_5=0, hbv_summary_4_function_f__123_214_0_L_2=0, hhv_summary_4_function_f__123_214_0_B1_15=4, hhv_summary_4_function_f__123_214_0_C1_16=10, hhv_summary_4_function_f__123_214_0_D1_17=638722032, hhv_summary_4_function_f__123_214_0_E1_18=0, hhv_summary_4_function_f__123_214_0_F1_19=6, hhv_summary_4_function_f__123_214_0_F_0=6, hhv_summary_4_function_f__123_214_0_G1_20=7, hhv_summary_4_function_f__123_214_0_H_22=0, hhv_summary_4_function_f__123_214_0_J_25=0, hhv_summary_4_function_f__123_214_0_K_23=0, hhv_summary_4_function_f__123_214_0_M_26=0, hhv_summary_4_function_f__123_214_0_R_1=638722033, hhv_summary_4_function_f__123_214_0_S_6=9, hhv_summary_4_function_f__123_214_0_T_7=5, hhv_summary_4_function_f__123_214_0_U_8=14, hhv_summary_4_function_f__123_214_0_V_9=12, hhv_summary_4_function_f__123_214_0_W_10=15, hhv_summary_4_function_f__123_214_0_X_11=11, hhv_summary_4_function_f__123_214_0_Y_12=13]
[L0]  RET   call summary_4_function_f__123_214_0(hbv_error_target_31_0_E_1, hbv_error_target_31_0_L_2, hbv_error_target_31_0_A_3, hbv_error_target_31_0_B_4, hbv_error_target_31_0_C_5, hbv_error_target_31_0_D_6, hbv_error_target_31_0_M_10, hbv_error_target_31_0_N_11, hbv_error_target_31_0_O_12, hbv_error_target_31_0_P_13, hbv_error_target_31_0_Q_14, hbv_error_target_31_0_R_15, hbv_error_target_31_0_S_16, hbv_error_target_31_0_T_17, hbv_error_target_31_0_U_18, hbv_error_target_31_0_V_19, hbv_error_target_31_0_W_20, hbv_error_target_31_0_X_21, hbv_error_target_31_0_Y_22, hbv_error_target_31_0_Z_23, hbv_error_target_31_0_A1_24, hbv_error_target_31_0_J_7, hbv_error_target_31_0_F_8, hbv_error_target_31_0_H_9, hbv_error_target_31_0_K_25, hbv_error_target_31_0_G_26, hbv_error_target_31_0_I_27);
      VAL   [hbv_error_target_31_0_A1_24=7, hbv_error_target_31_0_E_1=6, hbv_error_target_31_0_F_8=0, hbv_error_target_31_0_G_26=0, hbv_error_target_31_0_H_9=0, hbv_error_target_31_0_I_27=0, hbv_error_target_31_0_L_2=638722033, hbv_error_target_31_0_M_10=9, hbv_error_target_31_0_N_11=5, hbv_error_target_31_0_O_12=14, hbv_error_target_31_0_P_13=12, hbv_error_target_31_0_Q_14=15, hbv_error_target_31_0_R_15=11, hbv_error_target_31_0_S_16=13, hbv_error_target_31_0_V_19=4, hbv_error_target_31_0_W_20=10, hbv_error_target_31_0_X_21=638722032, hbv_error_target_31_0_Y_22=0, hbv_error_target_31_0_Z_23=6]
[L0]  RET   call error_target_31_0();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 44 procedures, 172 locations, 296 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.3s, OverallIterations: 10, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 18 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 9 mSDsluCounter, 9701 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 7725 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 272 IncrementalHoareTripleChecker+Invalid, 272 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 1976 mSDtfsCounter, 272 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 54 GetRequests, 18 SyntacticMatches, 0 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=175occurred in iteration=1, InterpolantAutomatonStates: 54, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 9 MinimizatonAttempts, 37 StatesRemovedByMinimization, 8 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.0s InterpolantComputationTime, 510 NumberOfCodeBlocks, 510 NumberOfCodeBlocksAsserted, 10 NumberOfCheckSat, 450 ConstructedInterpolants, 0 QuantifiedInterpolants, 631 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 9 InterpolantComputations, 9 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2025-05-07 17:27:09,941 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
unsat
