./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/function.sol_1_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:51,546 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:51,582 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_51daaa36-a853-4dd7-b479-0b03f589cc47/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:51,585 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:51,585 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:51,598 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:51,598 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:51,598 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:51,599 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:51,599 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:51,599 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:51,599 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:51,599 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:51,599 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:51,600 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:51,600 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:51,600 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:51,600 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:51,600 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:51,600 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:51,600 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:51,788 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:51,796 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:51,798 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:51,799 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:51,799 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:51,800 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_51daaa36-a853-4dd7-b479-0b03f589cc47/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/function.sol_1_no_adts_000.smt2
[2025-05-07 17:27:51,801 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:51,803 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:52,043 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_51daaa36-a853-4dd7-b479-0b03f589cc47/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/function.sol_1_no_adts_000.smt2
[2025-05-07 17:27:52,045 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:52,046 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:52,046 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:52,047 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:52,047 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:52,048 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,077 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52 Unit
[2025-05-07 17:27:52,077 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:52,078 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:52,078 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:52,078 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:52,089 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,089 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,111 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,111 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,115 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,116 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,118 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,120 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,121 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,132 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:52,132 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:52,133 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:52,133 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:52,133 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (1/1) ...
[2025-05-07 17:27:52,136 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:52,145 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:52,153 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:52,156 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:52,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:52,166 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:52,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:52,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_6_0 given in one single declaration
[2025-05-07 17:27:52,166 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_6_0
[2025-05-07 17:27:52,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_6_0
[2025-05-07 17:27:52,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,166 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__40_49_0
[2025-05-07 17:27:52,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__40_49_0
[2025-05-07 17:27:52,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,166 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__40_49_0
[2025-05-07 17:27:52,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__40_49_0
[2025-05-07 17:27:52,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,166 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__40_49_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__40_49_0
[2025-05-07 17:27:52,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,167 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__40_49_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__40_49_0
[2025-05-07 17:27:52,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_call_13_0 given in one single declaration
[2025-05-07 17:27:52,167 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_call_13_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_call_13_0
[2025-05-07 17:27:52,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_interface_1_C_49_0 given in one single declaration
[2025-05-07 17:27:52,167 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_interface_1_C_49_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_interface_1_C_49_0
[2025-05-07 17:27:52,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_X__48_49_0 given in one single declaration
[2025-05-07 17:27:52,167 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_X__48_49_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_X__48_49_0
[2025-05-07 17:27:52,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_function_X__48_49_0 given in one single declaration
[2025-05-07 17:27:52,167 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_function_X__48_49_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_function_X__48_49_0
[2025-05-07 17:27:52,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_X__48_49_0 given in one single declaration
[2025-05-07 17:27:52,167 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_X__48_49_0
[2025-05-07 17:27:52,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_X__48_49_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_return_function_X__48_49_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_return_function_X__48_49_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_return_function_X__48_49_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_X_47_49_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_X_47_49_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_X_47_49_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_X__48_49_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_X__48_49_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_X__48_49_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_39_49_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_39_49_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_39_49_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__40_49_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__40_49_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_call_11_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_call_11_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_call_11_0
[2025-05-07 17:27:52,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_call_10_0 given in one single declaration
[2025-05-07 17:27:52,168 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_call_10_0
[2025-05-07 17:27:52,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_call_10_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__40_49_0
[2025-05-07 17:27:52,169 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__40_49_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__40_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__40_49_0
[2025-05-07 17:27:52,169 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__40_49_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_49_0
[2025-05-07 17:27:52,169 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_49_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_49_0
[2025-05-07 17:27:52,169 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_49_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_24_C_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_24_C_49_0
[2025-05-07 17:27:52,169 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_24_C_49_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_21_C_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_21_C_49_0
[2025-05-07 17:27:52,169 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_21_C_49_0
[2025-05-07 17:27:52,169 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_23_C_49_0 given in one single declaration
[2025-05-07 17:27:52,169 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_23_C_49_0
[2025-05-07 17:27:52,170 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_23_C_49_0
[2025-05-07 17:27:52,170 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_22_C_49_0 given in one single declaration
[2025-05-07 17:27:52,170 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_22_C_49_0
[2025-05-07 17:27:52,170 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_22_C_49_0
[2025-05-07 17:27:52,170 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:52,170 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:52,170 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:52,307 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:52,309 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:52,547 INFO  L?                        ?]: Removed 225 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:52,547 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:52,555 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:52,555 INFO  L312             CfgBuilder]: Removed 14 assume(true) statements.
[2025-05-07 17:27:52,555 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:52 BoogieIcfgContainer
[2025-05-07 17:27:52,556 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:52,557 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:52,557 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:52,560 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:52,560 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:52" (1/3) ...
[2025-05-07 17:27:52,560 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@58668b2d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:52, skipping insertion in model container
[2025-05-07 17:27:52,560 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:52" (2/3) ...
[2025-05-07 17:27:52,560 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@58668b2d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:52, skipping insertion in model container
[2025-05-07 17:27:52,560 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:52" (3/3) ...
[2025-05-07 17:27:52,561 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:52,571 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:52,573 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 27 procedures, 121 locations, 210 edges, 27 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:52,603 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:52,611 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;@6735985d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:52,611 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:52,614 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 121 states, 43 states have (on average 1.186046511627907) internal successors, (51), 51 states have internal predecessors, (51), 51 states have call successors, (53), 26 states have call predecessors, (53), 26 states have return successors, (53), 44 states have call predecessors, (53), 51 states have call successors, (53)
[2025-05-07 17:27:52,622 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-05-07 17:27:52,622 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:52,623 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, 1, 1, 1, 1]
[2025-05-07 17:27:52,623 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:52,626 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:52,627 INFO  L85        PathProgramCache]: Analyzing trace with hash 298854273, now seen corresponding path program 1 times
[2025-05-07 17:27:52,632 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:52,632 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1949924758]
[2025-05-07 17:27:52,632 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:52,633 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:52,680 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-05-07 17:27:52,754 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-05-07 17:27:52,754 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:52,754 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:52,906 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:52,907 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:52,907 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1949924758]
[2025-05-07 17:27:52,908 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1949924758] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:52,908 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:52,910 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:27:52,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1284779988]
[2025-05-07 17:27:52,912 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:52,916 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:27:52,916 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:52,948 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:27:52,948 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:52,950 INFO  L87              Difference]: Start difference. First operand  has 121 states, 43 states have (on average 1.186046511627907) internal successors, (51), 51 states have internal predecessors, (51), 51 states have call successors, (53), 26 states have call predecessors, (53), 26 states have return successors, (53), 44 states have call predecessors, (53), 51 states have call successors, (53) Second operand  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 2 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 2 states have call successors, (15)
[2025-05-07 17:27:53,084 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:53,084 INFO  L93              Difference]: Finished difference Result 125 states and 169 transitions.
[2025-05-07 17:27:53,086 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:53,088 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 2 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 2 states have call successors, (15) Word has length 55
[2025-05-07 17:27:53,088 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:53,096 INFO  L225             Difference]: With dead ends: 125
[2025-05-07 17:27:53,096 INFO  L226             Difference]: Without dead ends: 125
[2025-05-07 17:27:53,098 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:53,101 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 416 mSDsCounter, 0 mSdLazyCounter, 53 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 562 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 53 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:53,101 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 562 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 53 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:53,112 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-05-07 17:27:53,139 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 123.
[2025-05-07 17:27:53,141 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 123 states, 44 states have (on average 1.1590909090909092) internal successors, (51), 51 states have internal predecessors, (51), 51 states have call successors, (53), 26 states have call predecessors, (53), 28 states have return successors, (63), 45 states have call predecessors, (63), 51 states have call successors, (63)
[2025-05-07 17:27:53,146 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 123 states to 123 states and 167 transitions.
[2025-05-07 17:27:53,147 INFO  L79                 Accepts]: Start accepts. Automaton has 123 states and 167 transitions. Word has length 55
[2025-05-07 17:27:53,148 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:53,148 INFO  L485      AbstractCegarLoop]: Abstraction has 123 states and 167 transitions.
[2025-05-07 17:27:53,148 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 2 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 2 states have call successors, (15)
[2025-05-07 17:27:53,148 INFO  L278                IsEmpty]: Start isEmpty. Operand 123 states and 167 transitions.
[2025-05-07 17:27:53,152 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-05-07 17:27:53,152 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:53,152 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:53,152 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:53,153 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:53,153 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:53,153 INFO  L85        PathProgramCache]: Analyzing trace with hash -2095975575, now seen corresponding path program 1 times
[2025-05-07 17:27:53,153 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:53,153 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2056984908]
[2025-05-07 17:27:53,153 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:53,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:53,180 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-05-07 17:27:53,208 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-05-07 17:27:53,209 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:53,209 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:53,324 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:27:53,324 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:53,324 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2056984908]
[2025-05-07 17:27:53,324 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2056984908] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:53,324 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:53,324 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:27:53,324 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [996511731]
[2025-05-07 17:27:53,324 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:53,325 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:27:53,325 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:53,326 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:27:53,326 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:53,326 INFO  L87              Difference]: Start difference. First operand 123 states and 167 transitions. Second operand  has 5 states, 4 states have (on average 7.0) internal successors, (28), 5 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 4 states have return successors, (17), 4 states have call predecessors, (17), 3 states have call successors, (17)
[2025-05-07 17:27:53,404 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:53,404 INFO  L93              Difference]: Finished difference Result 127 states and 174 transitions.
[2025-05-07 17:27:53,405 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:53,405 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 7.0) internal successors, (28), 5 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 4 states have return successors, (17), 4 states have call predecessors, (17), 3 states have call successors, (17) Word has length 62
[2025-05-07 17:27:53,405 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:53,407 INFO  L225             Difference]: With dead ends: 127
[2025-05-07 17:27:53,407 INFO  L226             Difference]: Without dead ends: 127
[2025-05-07 17:27:53,407 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:53,408 INFO  L437           NwaCegarLoop]: 149 mSDtfsCounter, 1 mSDsluCounter, 424 mSDsCounter, 0 mSdLazyCounter, 49 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 573 SdHoareTripleChecker+Invalid, 51 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 49 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:53,408 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 573 Invalid, 51 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 49 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:53,409 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-05-07 17:27:53,420 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 125.
[2025-05-07 17:27:53,421 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 45 states have (on average 1.1555555555555554) internal successors, (52), 52 states have internal predecessors, (52), 51 states have call successors, (53), 26 states have call predecessors, (53), 29 states have return successors, (67), 46 states have call predecessors, (67), 51 states have call successors, (67)
[2025-05-07 17:27:53,423 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 172 transitions.
[2025-05-07 17:27:53,423 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 172 transitions. Word has length 62
[2025-05-07 17:27:53,423 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:53,423 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 172 transitions.
[2025-05-07 17:27:53,423 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 7.0) internal successors, (28), 5 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 4 states have return successors, (17), 4 states have call predecessors, (17), 3 states have call successors, (17)
[2025-05-07 17:27:53,424 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 172 transitions.
[2025-05-07 17:27:53,426 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:27:53,426 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:53,426 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:53,427 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:53,427 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:53,427 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:53,428 INFO  L85        PathProgramCache]: Analyzing trace with hash -2090005447, now seen corresponding path program 1 times
[2025-05-07 17:27:53,428 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:53,428 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1206011181]
[2025-05-07 17:27:53,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:53,428 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:53,455 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:27:53,476 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:27:53,476 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:53,476 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:53,648 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:27:53,648 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:53,649 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1206011181]
[2025-05-07 17:27:53,649 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1206011181] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:53,649 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:53,649 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:27:53,649 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1057258355]
[2025-05-07 17:27:53,649 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:53,649 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:27:53,649 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:53,650 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:27:53,650 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:53,650 INFO  L87              Difference]: Start difference. First operand 125 states and 172 transitions. Second operand  has 9 states, 8 states have (on average 4.5) internal successors, (36), 9 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 8 states have return successors, (22), 9 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:53,804 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:53,804 INFO  L93              Difference]: Finished difference Result 131 states and 186 transitions.
[2025-05-07 17:27:53,804 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:27:53,804 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 4.5) internal successors, (36), 9 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 8 states have return successors, (22), 9 states have call predecessors, (22), 4 states have call successors, (22) Word has length 80
[2025-05-07 17:27:53,805 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:53,806 INFO  L225             Difference]: With dead ends: 131
[2025-05-07 17:27:53,806 INFO  L226             Difference]: Without dead ends: 131
[2025-05-07 17:27:53,807 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:53,807 INFO  L437           NwaCegarLoop]: 141 mSDtfsCounter, 1 mSDsluCounter, 952 mSDsCounter, 0 mSdLazyCounter, 138 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 1093 SdHoareTripleChecker+Invalid, 141 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 138 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:53,808 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 1093 Invalid, 141 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 138 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:53,808 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 131 states.
[2025-05-07 17:27:53,820 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 131 to 127.
[2025-05-07 17:27:53,821 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 127 states, 46 states have (on average 1.1521739130434783) internal successors, (53), 53 states have internal predecessors, (53), 51 states have call successors, (53), 26 states have call predecessors, (53), 30 states have return successors, (72), 47 states have call predecessors, (72), 51 states have call successors, (72)
[2025-05-07 17:27:53,823 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 178 transitions.
[2025-05-07 17:27:53,823 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 178 transitions. Word has length 80
[2025-05-07 17:27:53,823 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:53,823 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 178 transitions.
[2025-05-07 17:27:53,823 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 4.5) internal successors, (36), 9 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 8 states have return successors, (22), 9 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:53,824 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 178 transitions.
[2025-05-07 17:27:53,826 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:27:53,826 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:53,826 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:53,826 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:53,826 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:53,827 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:53,827 INFO  L85        PathProgramCache]: Analyzing trace with hash -798891679, now seen corresponding path program 1 times
[2025-05-07 17:27:53,827 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:53,827 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [52667845]
[2025-05-07 17:27:53,827 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:53,827 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:53,849 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:27:53,853 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:27:53,853 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:53,853 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:53,916 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:27:53,916 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:53,916 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [52667845]
[2025-05-07 17:27:53,916 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [52667845] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:53,916 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:53,916 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:53,916 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [854541042]
[2025-05-07 17:27:53,917 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:53,917 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:53,917 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:53,918 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:53,918 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:53,918 INFO  L87              Difference]: Start difference. First operand 127 states and 178 transitions. Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:27:53,929 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:53,929 INFO  L93              Difference]: Finished difference Result 129 states and 179 transitions.
[2025-05-07 17:27:53,929 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:53,929 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 65
[2025-05-07 17:27:53,929 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:53,931 INFO  L225             Difference]: With dead ends: 129
[2025-05-07 17:27:53,931 INFO  L226             Difference]: Without dead ends: 125
[2025-05-07 17:27:53,931 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:53,931 INFO  L437           NwaCegarLoop]: 156 mSDtfsCounter, 1 mSDsluCounter, 297 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 453 SdHoareTripleChecker+Invalid, 4 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:53,932 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 453 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:53,933 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-05-07 17:27:53,942 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 125.
[2025-05-07 17:27:53,942 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 46 states have (on average 1.1304347826086956) internal successors, (52), 52 states have internal predecessors, (52), 49 states have call successors, (51), 26 states have call predecessors, (51), 30 states have return successors, (70), 46 states have call predecessors, (70), 49 states have call successors, (70)
[2025-05-07 17:27:53,944 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 173 transitions.
[2025-05-07 17:27:53,944 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 173 transitions. Word has length 65
[2025-05-07 17:27:53,944 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:53,944 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 173 transitions.
[2025-05-07 17:27:53,944 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:27:53,944 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 173 transitions.
[2025-05-07 17:27:53,945 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:27:53,945 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:53,946 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:53,946 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:53,946 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:53,946 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:53,946 INFO  L85        PathProgramCache]: Analyzing trace with hash -1765709211, now seen corresponding path program 1 times
[2025-05-07 17:27:53,946 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:53,947 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1152464181]
[2025-05-07 17:27:53,947 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:53,947 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:53,963 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:27:53,973 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:27:53,973 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:53,974 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:54,041 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:27:54,041 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:54,041 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1152464181]
[2025-05-07 17:27:54,041 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1152464181] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:54,041 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:54,041 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:54,041 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [912502381]
[2025-05-07 17:27:54,041 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:54,042 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:54,042 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:54,042 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:54,042 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:54,042 INFO  L87              Difference]: Start difference. First operand 125 states and 173 transitions. Second operand  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:27:54,084 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:54,084 INFO  L93              Difference]: Finished difference Result 129 states and 178 transitions.
[2025-05-07 17:27:54,085 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:54,085 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18) Word has length 65
[2025-05-07 17:27:54,085 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:54,087 INFO  L225             Difference]: With dead ends: 129
[2025-05-07 17:27:54,087 INFO  L226             Difference]: Without dead ends: 129
[2025-05-07 17:27:54,087 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:54,088 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 568 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 714 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:54,088 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 714 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:54,089 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-05-07 17:27:54,098 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 129.
[2025-05-07 17:27:54,098 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 129 states, 48 states have (on average 1.125) internal successors, (54), 54 states have internal predecessors, (54), 49 states have call successors, (51), 26 states have call predecessors, (51), 32 states have return successors, (73), 48 states have call predecessors, (73), 49 states have call successors, (73)
[2025-05-07 17:27:54,099 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 129 states to 129 states and 178 transitions.
[2025-05-07 17:27:54,100 INFO  L79                 Accepts]: Start accepts. Automaton has 129 states and 178 transitions. Word has length 65
[2025-05-07 17:27:54,100 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:54,101 INFO  L485      AbstractCegarLoop]: Abstraction has 129 states and 178 transitions.
[2025-05-07 17:27:54,101 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:27:54,101 INFO  L278                IsEmpty]: Start isEmpty. Operand 129 states and 178 transitions.
[2025-05-07 17:27:54,102 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-05-07 17:27:54,102 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:54,102 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:54,102 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:54,103 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:54,103 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:54,103 INFO  L85        PathProgramCache]: Analyzing trace with hash -998903859, now seen corresponding path program 1 times
[2025-05-07 17:27:54,103 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:54,103 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1719095825]
[2025-05-07 17:27:54,103 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:54,103 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:54,120 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-05-07 17:27:54,128 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-05-07 17:27:54,129 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:54,129 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:54,177 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:27:54,177 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:54,177 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1719095825]
[2025-05-07 17:27:54,177 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1719095825] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:54,177 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1092152390]
[2025-05-07 17:27:54,177 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:54,178 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:54,180 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:54,182 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:27:54,183 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:27:54,371 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-05-07 17:27:54,447 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-05-07 17:27:54,447 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:54,447 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:54,451 INFO  L256         TraceCheckSpWp]: Trace formula consists of 735 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:54,458 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:54,522 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:27:54,523 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:27:54,999 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:27:54,999 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1092152390] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:27:54,999 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:27:54,999 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 7, 7] total 9
[2025-05-07 17:27:54,999 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1512276869]
[2025-05-07 17:27:54,999 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:27:54,999 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:27:54,999 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,000 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:27:55,000 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:55,000 INFO  L87              Difference]: Start difference. First operand 129 states and 178 transitions. Second operand  has 9 states, 6 states have (on average 5.666666666666667) internal successors, (34), 9 states have internal predecessors, (34), 6 states have call successors, (27), 1 states have call predecessors, (27), 6 states have return successors, (28), 8 states have call predecessors, (28), 6 states have call successors, (28)
[2025-05-07 17:27:55,083 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,083 INFO  L93              Difference]: Finished difference Result 133 states and 183 transitions.
[2025-05-07 17:27:55,084 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:55,084 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 5.666666666666667) internal successors, (34), 9 states have internal predecessors, (34), 6 states have call successors, (27), 1 states have call predecessors, (27), 6 states have return successors, (28), 8 states have call predecessors, (28), 6 states have call successors, (28) Word has length 69
[2025-05-07 17:27:55,084 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,085 INFO  L225             Difference]: With dead ends: 133
[2025-05-07 17:27:55,085 INFO  L226             Difference]: Without dead ends: 133
[2025-05-07 17:27:55,085 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 142 GetRequests, 131 SyntacticMatches, 4 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:55,085 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 3 mSDsluCounter, 822 mSDsCounter, 0 mSdLazyCounter, 80 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 966 SdHoareTripleChecker+Invalid, 83 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 80 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:55,085 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 966 Invalid, 83 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 80 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:55,086 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-05-07 17:27:55,090 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 131.
[2025-05-07 17:27:55,091 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 131 states, 49 states have (on average 1.1224489795918366) internal successors, (55), 55 states have internal predecessors, (55), 49 states have call successors, (51), 26 states have call predecessors, (51), 33 states have return successors, (75), 49 states have call predecessors, (75), 49 states have call successors, (75)
[2025-05-07 17:27:55,091 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 131 states to 131 states and 181 transitions.
[2025-05-07 17:27:55,091 INFO  L79                 Accepts]: Start accepts. Automaton has 131 states and 181 transitions. Word has length 69
[2025-05-07 17:27:55,092 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,092 INFO  L485      AbstractCegarLoop]: Abstraction has 131 states and 181 transitions.
[2025-05-07 17:27:55,092 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 5.666666666666667) internal successors, (34), 9 states have internal predecessors, (34), 6 states have call successors, (27), 1 states have call predecessors, (27), 6 states have return successors, (28), 8 states have call predecessors, (28), 6 states have call successors, (28)
[2025-05-07 17:27:55,092 INFO  L278                IsEmpty]: Start isEmpty. Operand 131 states and 181 transitions.
[2025-05-07 17:27:55,092 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 88
[2025-05-07 17:27:55,093 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,093 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:55,099 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:27:55,293 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable6
[2025-05-07 17:27:55,294 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,295 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,295 INFO  L85        PathProgramCache]: Analyzing trace with hash -436059253, now seen corresponding path program 1 times
[2025-05-07 17:27:55,296 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,296 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1708681633]
[2025-05-07 17:27:55,296 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,296 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,393 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 87 statements into 1 equivalence classes.
[2025-05-07 17:27:55,431 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 87 of 87 statements.
[2025-05-07 17:27:55,431 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,431 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:55,563 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:27:55,563 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:55,563 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1708681633]
[2025-05-07 17:27:55,563 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1708681633] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:55,563 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:55,563 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:27:55,563 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [741403554]
[2025-05-07 17:27:55,564 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:55,564 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:27:55,564 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,564 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:27:55,564 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:55,564 INFO  L87              Difference]: Start difference. First operand 131 states and 181 transitions. Second operand  has 9 states, 8 states have (on average 4.625) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 8 states have return successors, (24), 9 states have call predecessors, (24), 5 states have call successors, (24)
[2025-05-07 17:27:55,677 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,677 INFO  L93              Difference]: Finished difference Result 135 states and 188 transitions.
[2025-05-07 17:27:55,678 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:27:55,678 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 4.625) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 8 states have return successors, (24), 9 states have call predecessors, (24), 5 states have call successors, (24) Word has length 87
[2025-05-07 17:27:55,678 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,679 INFO  L225             Difference]: With dead ends: 135
[2025-05-07 17:27:55,680 INFO  L226             Difference]: Without dead ends: 135
[2025-05-07 17:27:55,680 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:55,680 INFO  L437           NwaCegarLoop]: 139 mSDtfsCounter, 1 mSDsluCounter, 938 mSDsCounter, 0 mSdLazyCounter, 130 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1077 SdHoareTripleChecker+Invalid, 133 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 130 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:55,681 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1077 Invalid, 133 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 130 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:55,681 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 135 states.
[2025-05-07 17:27:55,689 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 135 to 131.
[2025-05-07 17:27:55,689 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 131 states, 49 states have (on average 1.1224489795918366) internal successors, (55), 55 states have internal predecessors, (55), 49 states have call successors, (51), 26 states have call predecessors, (51), 33 states have return successors, (75), 49 states have call predecessors, (75), 49 states have call successors, (75)
[2025-05-07 17:27:55,691 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 131 states to 131 states and 181 transitions.
[2025-05-07 17:27:55,691 INFO  L79                 Accepts]: Start accepts. Automaton has 131 states and 181 transitions. Word has length 87
[2025-05-07 17:27:55,691 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,691 INFO  L485      AbstractCegarLoop]: Abstraction has 131 states and 181 transitions.
[2025-05-07 17:27:55,691 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 4.625) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 8 states have return successors, (24), 9 states have call predecessors, (24), 5 states have call successors, (24)
[2025-05-07 17:27:55,691 INFO  L278                IsEmpty]: Start isEmpty. Operand 131 states and 181 transitions.
[2025-05-07 17:27:55,693 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-05-07 17:27:55,693 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,693 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:55,693 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:55,693 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,694 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,694 INFO  L85        PathProgramCache]: Analyzing trace with hash 1873504388, now seen corresponding path program 1 times
[2025-05-07 17:27:55,694 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,694 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1883904991]
[2025-05-07 17:27:55,694 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,694 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,714 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-05-07 17:27:55,722 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-05-07 17:27:55,722 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,722 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:55,783 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-05-07 17:27:55,783 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:55,783 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1883904991]
[2025-05-07 17:27:55,784 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1883904991] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:55,784 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:55,784 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:55,784 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [939036844]
[2025-05-07 17:27:55,784 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:55,784 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:55,784 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,784 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:55,784 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:55,785 INFO  L87              Difference]: Start difference. First operand 131 states and 181 transitions. Second operand  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (20), 1 states have call predecessors, (20), 5 states have return successors, (20), 6 states have call predecessors, (20), 3 states have call successors, (20)
[2025-05-07 17:27:55,824 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,824 INFO  L93              Difference]: Finished difference Result 135 states and 186 transitions.
[2025-05-07 17:27:55,824 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:55,825 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (20), 1 states have call predecessors, (20), 5 states have return successors, (20), 6 states have call predecessors, (20), 3 states have call successors, (20) Word has length 72
[2025-05-07 17:27:55,825 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,826 INFO  L225             Difference]: With dead ends: 135
[2025-05-07 17:27:55,826 INFO  L226             Difference]: Without dead ends: 135
[2025-05-07 17:27:55,826 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:55,827 INFO  L437           NwaCegarLoop]: 151 mSDtfsCounter, 1 mSDsluCounter, 584 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 735 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:55,827 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 735 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:55,827 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 135 states.
[2025-05-07 17:27:55,833 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 135 to 131.
[2025-05-07 17:27:55,834 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 131 states, 49 states have (on average 1.1224489795918366) internal successors, (55), 55 states have internal predecessors, (55), 49 states have call successors, (51), 26 states have call predecessors, (51), 33 states have return successors, (75), 49 states have call predecessors, (75), 49 states have call successors, (75)
[2025-05-07 17:27:55,835 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 131 states to 131 states and 181 transitions.
[2025-05-07 17:27:55,835 INFO  L79                 Accepts]: Start accepts. Automaton has 131 states and 181 transitions. Word has length 72
[2025-05-07 17:27:55,835 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,835 INFO  L485      AbstractCegarLoop]: Abstraction has 131 states and 181 transitions.
[2025-05-07 17:27:55,835 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (20), 1 states have call predecessors, (20), 5 states have return successors, (20), 6 states have call predecessors, (20), 3 states have call successors, (20)
[2025-05-07 17:27:55,836 INFO  L278                IsEmpty]: Start isEmpty. Operand 131 states and 181 transitions.
[2025-05-07 17:27:55,837 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-05-07 17:27:55,837 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,837 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:55,837 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:55,837 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,837 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,837 INFO  L85        PathProgramCache]: Analyzing trace with hash 390854308, now seen corresponding path program 1 times
[2025-05-07 17:27:55,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,838 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1667838207]
[2025-05-07 17:27:55,838 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,838 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,857 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-05-07 17:27:55,872 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-05-07 17:27:55,872 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,872 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-05-07 17:27:55,872 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-05-07 17:27:55,882 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-05-07 17:27:55,892 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-05-07 17:27:55,892 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,892 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-05-07 17:27:55,913 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-05-07 17:27:55,913 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-05-07 17:27:55,914 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:55,915 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:55,917 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:55,933 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:55,935 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:55 BoogieIcfgContainer
[2025-05-07 17:27:55,935 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:55,936 INFO  L158              Benchmark]: Toolchain (without parser) took 3889.83ms. Allocated memory is still 234.9MB. Free memory was 147.4MB in the beginning and 91.7MB in the end (delta: 55.7MB). Peak memory consumption was 65.4MB. Max. memory is 33.6GB.
[2025-05-07 17:27:55,936 INFO  L158              Benchmark]: SmtParser took 0.32ms. Allocated memory is still 234.9MB. Free memory is still 173.3MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:55,936 INFO  L158              Benchmark]: ChcToBoogie took 30.70ms. Allocated memory is still 234.9MB. Free memory was 147.3MB in the beginning and 144.4MB in the end (delta: 2.9MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:55,936 INFO  L158              Benchmark]: Boogie Preprocessor took 54.38ms. Allocated memory is still 234.9MB. Free memory was 144.4MB in the beginning and 141.1MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:55,936 INFO  L158              Benchmark]: RCFGBuilder took 423.16ms. Allocated memory is still 234.9MB. Free memory was 141.1MB in the beginning and 174.9MB in the end (delta: -33.9MB). Peak memory consumption was 43.0MB. Max. memory is 33.6GB.
[2025-05-07 17:27:55,936 INFO  L158              Benchmark]: TraceAbstraction took 3378.42ms. Allocated memory is still 234.9MB. Free memory was 174.4MB in the beginning and 91.7MB in the end (delta: 82.7MB). Peak memory consumption was 72.7MB. Max. memory is 33.6GB.
[2025-05-07 17:27:55,937 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.32ms. Allocated memory is still 234.9MB. Free memory is still 173.3MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 30.70ms. Allocated memory is still 234.9MB. Free memory was 147.3MB in the beginning and 144.4MB in the end (delta: 2.9MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 54.38ms. Allocated memory is still 234.9MB. Free memory was 144.4MB in the beginning and 141.1MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 423.16ms. Allocated memory is still 234.9MB. Free memory was 141.1MB in the beginning and 174.9MB in the end (delta: -33.9MB). Peak memory consumption was 43.0MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3378.42ms. Allocated memory is still 234.9MB. Free memory was 174.4MB in the beginning and 91.7MB in the end (delta: 82.7MB). Peak memory consumption was 72.7MB. 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_6_0();
[L0]        assume 2 == hbv_error_target_6_0_E_1;
      VAL   [hbv_error_target_6_0_E_1=2]
[L0]  CALL  call interface_0_C_49_0(hbv_error_target_6_0_J_2, hbv_error_target_6_0_A_3, hbv_error_target_6_0_B_4, hbv_error_target_6_0_C_5, hbv_error_target_6_0_D_6, hbv_error_target_6_0_H_7, hbv_error_target_6_0_F_8);
      VAL   [hhv_interface_0_C_49_0_G_6=0, hhv_interface_0_C_49_0_J_0=638722033]
[L0]        assume ((((((((((((((((((((((!(hbv_interface_0_C_49_0_N_7 < 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_L_5)) && !(hbv_interface_0_C_49_0_Q_10 < 0)) && !(hbv_interface_0_C_49_0_F_3 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_N_7)) && !(hbv_interface_0_C_49_0_M_6 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_K_4)) && !(hbv_interface_0_C_49_0_U_11 < 0)) && !(1461501637330902918203684832716283019655932542975 < hbv_interface_0_C_49_0_M_6)) && hbv_interface_0_C_49_0_E_1 == 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_P_9)) && !(hbv_interface_0_C_49_0_V_12 < 0)) && !(1461501637330902918203684832716283019655932542975 < hbv_interface_0_C_49_0_L_2)) && !(hbv_interface_0_C_49_0_P_9 < 0)) && !(hbv_interface_0_C_49_0_O_8 < 0)) && !(1461501637330902918203684832716283019655932542975 < hbv_interface_0_C_49_0_U_11)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_F_3)) && !(hbv_interface_0_C_49_0_K_4 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_V_12)) && !(hbv_interface_0_C_49_0_L_5 < 0)) && !(hbv_interface_0_C_49_0_L_2 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_O_8)) && hbv_interface_0_C_49_0_N_7 == 0) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_interface_0_C_49_0_Q_10);
      VAL   [hbv_interface_0_C_49_0_E_1=0, hbv_interface_0_C_49_0_F_3=0, hbv_interface_0_C_49_0_K_4=0, hbv_interface_0_C_49_0_L_2=0, hbv_interface_0_C_49_0_L_5=0, hbv_interface_0_C_49_0_M_6=0, hbv_interface_0_C_49_0_N_7=0, hbv_interface_0_C_49_0_O_8=0, hbv_interface_0_C_49_0_P_9=0, hbv_interface_0_C_49_0_Q_10=0, hbv_interface_0_C_49_0_U_11=0, hbv_interface_0_C_49_0_V_12=0, hhv_interface_0_C_49_0_G_6=0, hhv_interface_0_C_49_0_J_0=638722033]
[L0]  CALL  call summary_constructor_2_C_49_0(hbv_interface_0_C_49_0_E_1, hhv_interface_0_C_49_0_J_0, hhv_interface_0_C_49_0_A_1, hhv_interface_0_C_49_0_B_2, hhv_interface_0_C_49_0_C_3, hhv_interface_0_C_49_0_D_4, hbv_interface_0_C_49_0_V_12, hbv_interface_0_C_49_0_Q_10, hbv_interface_0_C_49_0_L_2, hbv_interface_0_C_49_0_L_5, hbv_interface_0_C_49_0_P_9, hbv_interface_0_C_49_0_O_8, hbv_interface_0_C_49_0_K_4, hbv_interface_0_C_49_0_R_13, hbv_interface_0_C_49_0_S_14, hbv_interface_0_C_49_0_V_15, hbv_interface_0_C_49_0_M_6, hbv_interface_0_C_49_0_W_16, hbv_interface_0_C_49_0_N_7, hbv_interface_0_C_49_0_F_3, hbv_interface_0_C_49_0_U_11, hbv_interface_0_C_49_0_I_17, hhv_interface_0_C_49_0_I_5, hbv_interface_0_C_49_0_Y_18, hhv_interface_0_C_49_0_G_6);
      VAL   [hhv_summary_constructor_2_C_49_0_A1_19=0, hhv_summary_constructor_2_C_49_0_B1_20=0, hhv_summary_constructor_2_C_49_0_F_0=0, hhv_summary_constructor_2_C_49_0_G_23=0, hhv_summary_constructor_2_C_49_0_I_24=0, hhv_summary_constructor_2_C_49_0_M_1=638722033, hhv_summary_constructor_2_C_49_0_N_6=0, hhv_summary_constructor_2_C_49_0_O_7=0, hhv_summary_constructor_2_C_49_0_P_8=0, hhv_summary_constructor_2_C_49_0_Q_9=0, hhv_summary_constructor_2_C_49_0_R_10=0, hhv_summary_constructor_2_C_49_0_S_11=0, hhv_summary_constructor_2_C_49_0_T_12=0, hhv_summary_constructor_2_C_49_0_W_15=638722035, hhv_summary_constructor_2_C_49_0_X_16=0, hhv_summary_constructor_2_C_49_0_Y_17=638722037, hhv_summary_constructor_2_C_49_0_Z_18=0]
[L0]        assume hhv_summary_constructor_2_C_49_0_F_0 == 0;
      VAL   [hhv_summary_constructor_2_C_49_0_A1_19=0, hhv_summary_constructor_2_C_49_0_B1_20=0, hhv_summary_constructor_2_C_49_0_F_0=0, hhv_summary_constructor_2_C_49_0_G_23=0, hhv_summary_constructor_2_C_49_0_I_24=0, hhv_summary_constructor_2_C_49_0_M_1=638722033, hhv_summary_constructor_2_C_49_0_N_6=0, hhv_summary_constructor_2_C_49_0_O_7=0, hhv_summary_constructor_2_C_49_0_P_8=0, hhv_summary_constructor_2_C_49_0_Q_9=0, hhv_summary_constructor_2_C_49_0_R_10=0, hhv_summary_constructor_2_C_49_0_S_11=0, hhv_summary_constructor_2_C_49_0_T_12=0, hhv_summary_constructor_2_C_49_0_W_15=638722035, hhv_summary_constructor_2_C_49_0_X_16=0, hhv_summary_constructor_2_C_49_0_Y_17=638722037, hhv_summary_constructor_2_C_49_0_Z_18=0]
[L0]  CALL  call contract_initializer_21_C_49_0(hhv_summary_constructor_2_C_49_0_F_0, hhv_summary_constructor_2_C_49_0_M_1, hhv_summary_constructor_2_C_49_0_A_2, hhv_summary_constructor_2_C_49_0_B_3, hhv_summary_constructor_2_C_49_0_C_4, hhv_summary_constructor_2_C_49_0_D_5, hhv_summary_constructor_2_C_49_0_N_6, hhv_summary_constructor_2_C_49_0_O_7, hhv_summary_constructor_2_C_49_0_P_8, hhv_summary_constructor_2_C_49_0_Q_9, hhv_summary_constructor_2_C_49_0_R_10, hhv_summary_constructor_2_C_49_0_S_11, hhv_summary_constructor_2_C_49_0_T_12, hhv_summary_constructor_2_C_49_0_U_13, hhv_summary_constructor_2_C_49_0_V_14, hhv_summary_constructor_2_C_49_0_W_15, hhv_summary_constructor_2_C_49_0_X_16, hhv_summary_constructor_2_C_49_0_Y_17, hhv_summary_constructor_2_C_49_0_Z_18, hhv_summary_constructor_2_C_49_0_A1_19, hhv_summary_constructor_2_C_49_0_B1_20, hbv_summary_constructor_2_C_49_0_K_1, hhv_summary_constructor_2_C_49_0_L_22, hbv_summary_constructor_2_C_49_0_H_2, hhv_summary_constructor_2_C_49_0_I_24);
      VAL   [hhv_contract_initializer_21_C_49_0_E_0=0, hhv_contract_initializer_21_C_49_0_F_23=0, hhv_contract_initializer_21_C_49_0_G_24=0, hhv_contract_initializer_21_C_49_0_J_1=638722033, hhv_contract_initializer_21_C_49_0_K_6=0, hhv_contract_initializer_21_C_49_0_L_7=0, hhv_contract_initializer_21_C_49_0_M_8=0, hhv_contract_initializer_21_C_49_0_N_9=0, hhv_contract_initializer_21_C_49_0_O_10=0, hhv_contract_initializer_21_C_49_0_P_11=0, hhv_contract_initializer_21_C_49_0_Q_12=0, hhv_contract_initializer_21_C_49_0_T_15=638722035, hhv_contract_initializer_21_C_49_0_U_16=0, hhv_contract_initializer_21_C_49_0_V_17=638722037, hhv_contract_initializer_21_C_49_0_W_18=0, hhv_contract_initializer_21_C_49_0_X_19=0, hhv_contract_initializer_21_C_49_0_Y_20=0]
[L0]  CALL  call contract_initializer_after_init_23_C_49_0(hhv_contract_initializer_21_C_49_0_E_0, hhv_contract_initializer_21_C_49_0_J_1, hhv_contract_initializer_21_C_49_0_A_2, hhv_contract_initializer_21_C_49_0_B_3, hhv_contract_initializer_21_C_49_0_C_4, hhv_contract_initializer_21_C_49_0_D_5, hhv_contract_initializer_21_C_49_0_K_6, hhv_contract_initializer_21_C_49_0_L_7, hhv_contract_initializer_21_C_49_0_M_8, hhv_contract_initializer_21_C_49_0_N_9, hhv_contract_initializer_21_C_49_0_O_10, hhv_contract_initializer_21_C_49_0_P_11, hhv_contract_initializer_21_C_49_0_Q_12, hhv_contract_initializer_21_C_49_0_R_13, hhv_contract_initializer_21_C_49_0_S_14, hhv_contract_initializer_21_C_49_0_T_15, hhv_contract_initializer_21_C_49_0_U_16, hhv_contract_initializer_21_C_49_0_V_17, hhv_contract_initializer_21_C_49_0_W_18, hhv_contract_initializer_21_C_49_0_X_19, hhv_contract_initializer_21_C_49_0_Y_20, hhv_contract_initializer_21_C_49_0_H_21, hhv_contract_initializer_21_C_49_0_I_22, hhv_contract_initializer_21_C_49_0_F_23, hhv_contract_initializer_21_C_49_0_G_24);
      VAL   [hhv_contract_initializer_after_init_23_C_49_0_E_0=0, hhv_contract_initializer_after_init_23_C_49_0_F_23=0, hhv_contract_initializer_after_init_23_C_49_0_G_24=0, hhv_contract_initializer_after_init_23_C_49_0_J_1=638722033, hhv_contract_initializer_after_init_23_C_49_0_K_6=0, hhv_contract_initializer_after_init_23_C_49_0_L_7=0, hhv_contract_initializer_after_init_23_C_49_0_M_8=0, hhv_contract_initializer_after_init_23_C_49_0_N_9=0, hhv_contract_initializer_after_init_23_C_49_0_O_10=0, hhv_contract_initializer_after_init_23_C_49_0_P_11=0, hhv_contract_initializer_after_init_23_C_49_0_Q_12=0, hhv_contract_initializer_after_init_23_C_49_0_T_15=638722035, hhv_contract_initializer_after_init_23_C_49_0_U_16=0, hhv_contract_initializer_after_init_23_C_49_0_V_17=638722037, hhv_contract_initializer_after_init_23_C_49_0_W_18=0, hhv_contract_initializer_after_init_23_C_49_0_X_19=0, hhv_contract_initializer_after_init_23_C_49_0_Y_20=0]
[L0]  CALL  call contract_initializer_entry_22_C_49_0(hhv_contract_initializer_after_init_23_C_49_0_E_0, hhv_contract_initializer_after_init_23_C_49_0_J_1, hhv_contract_initializer_after_init_23_C_49_0_A_2, hhv_contract_initializer_after_init_23_C_49_0_B_3, hhv_contract_initializer_after_init_23_C_49_0_C_4, hhv_contract_initializer_after_init_23_C_49_0_D_5, hhv_contract_initializer_after_init_23_C_49_0_K_6, hhv_contract_initializer_after_init_23_C_49_0_L_7, hhv_contract_initializer_after_init_23_C_49_0_M_8, hhv_contract_initializer_after_init_23_C_49_0_N_9, hhv_contract_initializer_after_init_23_C_49_0_O_10, hhv_contract_initializer_after_init_23_C_49_0_P_11, hhv_contract_initializer_after_init_23_C_49_0_Q_12, hhv_contract_initializer_after_init_23_C_49_0_R_13, hhv_contract_initializer_after_init_23_C_49_0_S_14, hhv_contract_initializer_after_init_23_C_49_0_T_15, hhv_contract_initializer_after_init_23_C_49_0_U_16, hhv_contract_initializer_after_init_23_C_49_0_V_17, hhv_contract_initializer_after_init_23_C_49_0_W_18, hhv_contract_initializer_after_init_23_C_49_0_X_19, hhv_contract_initializer_after_init_23_C_49_0_Y_20, hhv_contract_initializer_after_init_23_C_49_0_H_21, hhv_contract_initializer_after_init_23_C_49_0_I_22, hhv_contract_initializer_after_init_23_C_49_0_F_23, hhv_contract_initializer_after_init_23_C_49_0_G_24);
      VAL   [hhv_contract_initializer_entry_22_C_49_0_E_0=0, hhv_contract_initializer_entry_22_C_49_0_F_23=0, hhv_contract_initializer_entry_22_C_49_0_G_24=0]
[L0]        assume (hhv_contract_initializer_entry_22_C_49_0_G_24 == hhv_contract_initializer_entry_22_C_49_0_F_23 && hhv_contract_initializer_entry_22_C_49_0_E_0 == 0) && hhv_contract_initializer_entry_22_C_49_0_H_21 == hhv_contract_initializer_entry_22_C_49_0_I_22;
      VAL   [hhv_contract_initializer_entry_22_C_49_0_E_0=0, hhv_contract_initializer_entry_22_C_49_0_F_23=0, hhv_contract_initializer_entry_22_C_49_0_G_24=0]
[L0]  RET   call contract_initializer_entry_22_C_49_0(hhv_contract_initializer_after_init_23_C_49_0_E_0, hhv_contract_initializer_after_init_23_C_49_0_J_1, hhv_contract_initializer_after_init_23_C_49_0_A_2, hhv_contract_initializer_after_init_23_C_49_0_B_3, hhv_contract_initializer_after_init_23_C_49_0_C_4, hhv_contract_initializer_after_init_23_C_49_0_D_5, hhv_contract_initializer_after_init_23_C_49_0_K_6, hhv_contract_initializer_after_init_23_C_49_0_L_7, hhv_contract_initializer_after_init_23_C_49_0_M_8, hhv_contract_initializer_after_init_23_C_49_0_N_9, hhv_contract_initializer_after_init_23_C_49_0_O_10, hhv_contract_initializer_after_init_23_C_49_0_P_11, hhv_contract_initializer_after_init_23_C_49_0_Q_12, hhv_contract_initializer_after_init_23_C_49_0_R_13, hhv_contract_initializer_after_init_23_C_49_0_S_14, hhv_contract_initializer_after_init_23_C_49_0_T_15, hhv_contract_initializer_after_init_23_C_49_0_U_16, hhv_contract_initializer_after_init_23_C_49_0_V_17, hhv_contract_initializer_after_init_23_C_49_0_W_18, hhv_contract_initializer_after_init_23_C_49_0_X_19, hhv_contract_initializer_after_init_23_C_49_0_Y_20, hhv_contract_initializer_after_init_23_C_49_0_H_21, hhv_contract_initializer_after_init_23_C_49_0_I_22, hhv_contract_initializer_after_init_23_C_49_0_F_23, hhv_contract_initializer_after_init_23_C_49_0_G_24);
      VAL   [hhv_contract_initializer_after_init_23_C_49_0_E_0=0, hhv_contract_initializer_after_init_23_C_49_0_F_23=0, hhv_contract_initializer_after_init_23_C_49_0_G_24=0, hhv_contract_initializer_after_init_23_C_49_0_J_1=638722033, hhv_contract_initializer_after_init_23_C_49_0_K_6=0, hhv_contract_initializer_after_init_23_C_49_0_L_7=0, hhv_contract_initializer_after_init_23_C_49_0_M_8=0, hhv_contract_initializer_after_init_23_C_49_0_N_9=0, hhv_contract_initializer_after_init_23_C_49_0_O_10=0, hhv_contract_initializer_after_init_23_C_49_0_P_11=0, hhv_contract_initializer_after_init_23_C_49_0_Q_12=0, hhv_contract_initializer_after_init_23_C_49_0_T_15=638722035, hhv_contract_initializer_after_init_23_C_49_0_U_16=0, hhv_contract_initializer_after_init_23_C_49_0_V_17=638722037, hhv_contract_initializer_after_init_23_C_49_0_W_18=0, hhv_contract_initializer_after_init_23_C_49_0_X_19=0, hhv_contract_initializer_after_init_23_C_49_0_Y_20=0]
[L0]  RET   call contract_initializer_after_init_23_C_49_0(hhv_contract_initializer_21_C_49_0_E_0, hhv_contract_initializer_21_C_49_0_J_1, hhv_contract_initializer_21_C_49_0_A_2, hhv_contract_initializer_21_C_49_0_B_3, hhv_contract_initializer_21_C_49_0_C_4, hhv_contract_initializer_21_C_49_0_D_5, hhv_contract_initializer_21_C_49_0_K_6, hhv_contract_initializer_21_C_49_0_L_7, hhv_contract_initializer_21_C_49_0_M_8, hhv_contract_initializer_21_C_49_0_N_9, hhv_contract_initializer_21_C_49_0_O_10, hhv_contract_initializer_21_C_49_0_P_11, hhv_contract_initializer_21_C_49_0_Q_12, hhv_contract_initializer_21_C_49_0_R_13, hhv_contract_initializer_21_C_49_0_S_14, hhv_contract_initializer_21_C_49_0_T_15, hhv_contract_initializer_21_C_49_0_U_16, hhv_contract_initializer_21_C_49_0_V_17, hhv_contract_initializer_21_C_49_0_W_18, hhv_contract_initializer_21_C_49_0_X_19, hhv_contract_initializer_21_C_49_0_Y_20, hhv_contract_initializer_21_C_49_0_H_21, hhv_contract_initializer_21_C_49_0_I_22, hhv_contract_initializer_21_C_49_0_F_23, hhv_contract_initializer_21_C_49_0_G_24);
      VAL   [hhv_contract_initializer_21_C_49_0_E_0=0, hhv_contract_initializer_21_C_49_0_F_23=0, hhv_contract_initializer_21_C_49_0_G_24=0, hhv_contract_initializer_21_C_49_0_J_1=638722033, hhv_contract_initializer_21_C_49_0_K_6=0, hhv_contract_initializer_21_C_49_0_L_7=0, hhv_contract_initializer_21_C_49_0_M_8=0, hhv_contract_initializer_21_C_49_0_N_9=0, hhv_contract_initializer_21_C_49_0_O_10=0, hhv_contract_initializer_21_C_49_0_P_11=0, hhv_contract_initializer_21_C_49_0_Q_12=0, hhv_contract_initializer_21_C_49_0_T_15=638722035, hhv_contract_initializer_21_C_49_0_U_16=0, hhv_contract_initializer_21_C_49_0_V_17=638722037, hhv_contract_initializer_21_C_49_0_W_18=0, hhv_contract_initializer_21_C_49_0_X_19=0, hhv_contract_initializer_21_C_49_0_Y_20=0]
[L0]  RET   call contract_initializer_21_C_49_0(hhv_summary_constructor_2_C_49_0_F_0, hhv_summary_constructor_2_C_49_0_M_1, hhv_summary_constructor_2_C_49_0_A_2, hhv_summary_constructor_2_C_49_0_B_3, hhv_summary_constructor_2_C_49_0_C_4, hhv_summary_constructor_2_C_49_0_D_5, hhv_summary_constructor_2_C_49_0_N_6, hhv_summary_constructor_2_C_49_0_O_7, hhv_summary_constructor_2_C_49_0_P_8, hhv_summary_constructor_2_C_49_0_Q_9, hhv_summary_constructor_2_C_49_0_R_10, hhv_summary_constructor_2_C_49_0_S_11, hhv_summary_constructor_2_C_49_0_T_12, hhv_summary_constructor_2_C_49_0_U_13, hhv_summary_constructor_2_C_49_0_V_14, hhv_summary_constructor_2_C_49_0_W_15, hhv_summary_constructor_2_C_49_0_X_16, hhv_summary_constructor_2_C_49_0_Y_17, hhv_summary_constructor_2_C_49_0_Z_18, hhv_summary_constructor_2_C_49_0_A1_19, hhv_summary_constructor_2_C_49_0_B1_20, hbv_summary_constructor_2_C_49_0_K_1, hhv_summary_constructor_2_C_49_0_L_22, hbv_summary_constructor_2_C_49_0_H_2, hhv_summary_constructor_2_C_49_0_I_24);
      VAL   [hbv_summary_constructor_2_C_49_0_H_2=0, hhv_summary_constructor_2_C_49_0_A1_19=0, hhv_summary_constructor_2_C_49_0_B1_20=0, hhv_summary_constructor_2_C_49_0_F_0=0, hhv_summary_constructor_2_C_49_0_G_23=0, hhv_summary_constructor_2_C_49_0_I_24=0, hhv_summary_constructor_2_C_49_0_M_1=638722033, hhv_summary_constructor_2_C_49_0_N_6=0, hhv_summary_constructor_2_C_49_0_O_7=0, hhv_summary_constructor_2_C_49_0_P_8=0, hhv_summary_constructor_2_C_49_0_Q_9=0, hhv_summary_constructor_2_C_49_0_R_10=0, hhv_summary_constructor_2_C_49_0_S_11=0, hhv_summary_constructor_2_C_49_0_T_12=0, hhv_summary_constructor_2_C_49_0_W_15=638722035, hhv_summary_constructor_2_C_49_0_X_16=0, hhv_summary_constructor_2_C_49_0_Y_17=638722037, hhv_summary_constructor_2_C_49_0_Z_18=0]
[L0]  CALL  call implicit_constructor_entry_24_C_49_0(hbv_summary_constructor_2_C_49_0_E_3, hhv_summary_constructor_2_C_49_0_M_1, hhv_summary_constructor_2_C_49_0_A_2, hhv_summary_constructor_2_C_49_0_B_3, hhv_summary_constructor_2_C_49_0_C_4, hhv_summary_constructor_2_C_49_0_D_5, hhv_summary_constructor_2_C_49_0_N_6, hhv_summary_constructor_2_C_49_0_O_7, hhv_summary_constructor_2_C_49_0_P_8, hhv_summary_constructor_2_C_49_0_Q_9, hhv_summary_constructor_2_C_49_0_R_10, hhv_summary_constructor_2_C_49_0_S_11, hhv_summary_constructor_2_C_49_0_T_12, hhv_summary_constructor_2_C_49_0_U_13, hhv_summary_constructor_2_C_49_0_V_14, hhv_summary_constructor_2_C_49_0_W_15, hhv_summary_constructor_2_C_49_0_X_16, hhv_summary_constructor_2_C_49_0_Y_17, hhv_summary_constructor_2_C_49_0_Z_18, hhv_summary_constructor_2_C_49_0_A1_19, hhv_summary_constructor_2_C_49_0_B1_20, hhv_summary_constructor_2_C_49_0_J_21, hbv_summary_constructor_2_C_49_0_K_1, hhv_summary_constructor_2_C_49_0_G_23, hbv_summary_constructor_2_C_49_0_H_2);
      VAL   [hhv_implicit_constructor_entry_24_C_49_0_E_0=0, hhv_implicit_constructor_entry_24_C_49_0_F_23=0, hhv_implicit_constructor_entry_24_C_49_0_G_24=0, hhv_implicit_constructor_entry_24_C_49_0_J_1=638722033, hhv_implicit_constructor_entry_24_C_49_0_W_18=0]
[L0]        assume (((hhv_implicit_constructor_entry_24_C_49_0_H_21 == hhv_implicit_constructor_entry_24_C_49_0_I_22 && hhv_implicit_constructor_entry_24_C_49_0_E_0 == 0) && !(hhv_implicit_constructor_entry_24_C_49_0_I_22[hhv_implicit_constructor_entry_24_C_49_0_J_1] < hhv_implicit_constructor_entry_24_C_49_0_W_18)) && hhv_implicit_constructor_entry_24_C_49_0_G_24 == 0) && hhv_implicit_constructor_entry_24_C_49_0_G_24 == hhv_implicit_constructor_entry_24_C_49_0_F_23;
      VAL   [hhv_implicit_constructor_entry_24_C_49_0_E_0=0, hhv_implicit_constructor_entry_24_C_49_0_F_23=0, hhv_implicit_constructor_entry_24_C_49_0_G_24=0, hhv_implicit_constructor_entry_24_C_49_0_J_1=638722033, hhv_implicit_constructor_entry_24_C_49_0_W_18=0]
[L0]  RET   call implicit_constructor_entry_24_C_49_0(hbv_summary_constructor_2_C_49_0_E_3, hhv_summary_constructor_2_C_49_0_M_1, hhv_summary_constructor_2_C_49_0_A_2, hhv_summary_constructor_2_C_49_0_B_3, hhv_summary_constructor_2_C_49_0_C_4, hhv_summary_constructor_2_C_49_0_D_5, hhv_summary_constructor_2_C_49_0_N_6, hhv_summary_constructor_2_C_49_0_O_7, hhv_summary_constructor_2_C_49_0_P_8, hhv_summary_constructor_2_C_49_0_Q_9, hhv_summary_constructor_2_C_49_0_R_10, hhv_summary_constructor_2_C_49_0_S_11, hhv_summary_constructor_2_C_49_0_T_12, hhv_summary_constructor_2_C_49_0_U_13, hhv_summary_constructor_2_C_49_0_V_14, hhv_summary_constructor_2_C_49_0_W_15, hhv_summary_constructor_2_C_49_0_X_16, hhv_summary_constructor_2_C_49_0_Y_17, hhv_summary_constructor_2_C_49_0_Z_18, hhv_summary_constructor_2_C_49_0_A1_19, hhv_summary_constructor_2_C_49_0_B1_20, hhv_summary_constructor_2_C_49_0_J_21, hbv_summary_constructor_2_C_49_0_K_1, hhv_summary_constructor_2_C_49_0_G_23, hbv_summary_constructor_2_C_49_0_H_2);
      VAL   [hbv_summary_constructor_2_C_49_0_E_3=0, hbv_summary_constructor_2_C_49_0_H_2=0, hhv_summary_constructor_2_C_49_0_A1_19=0, hhv_summary_constructor_2_C_49_0_B1_20=0, hhv_summary_constructor_2_C_49_0_F_0=0, hhv_summary_constructor_2_C_49_0_G_23=0, hhv_summary_constructor_2_C_49_0_I_24=0, hhv_summary_constructor_2_C_49_0_M_1=638722033, hhv_summary_constructor_2_C_49_0_N_6=0, hhv_summary_constructor_2_C_49_0_O_7=0, hhv_summary_constructor_2_C_49_0_P_8=0, hhv_summary_constructor_2_C_49_0_Q_9=0, hhv_summary_constructor_2_C_49_0_R_10=0, hhv_summary_constructor_2_C_49_0_S_11=0, hhv_summary_constructor_2_C_49_0_T_12=0, hhv_summary_constructor_2_C_49_0_W_15=638722035, hhv_summary_constructor_2_C_49_0_X_16=0, hhv_summary_constructor_2_C_49_0_Y_17=638722037, hhv_summary_constructor_2_C_49_0_Z_18=0]
[L0]  RET   call summary_constructor_2_C_49_0(hbv_interface_0_C_49_0_E_1, hhv_interface_0_C_49_0_J_0, hhv_interface_0_C_49_0_A_1, hhv_interface_0_C_49_0_B_2, hhv_interface_0_C_49_0_C_3, hhv_interface_0_C_49_0_D_4, hbv_interface_0_C_49_0_V_12, hbv_interface_0_C_49_0_Q_10, hbv_interface_0_C_49_0_L_2, hbv_interface_0_C_49_0_L_5, hbv_interface_0_C_49_0_P_9, hbv_interface_0_C_49_0_O_8, hbv_interface_0_C_49_0_K_4, hbv_interface_0_C_49_0_R_13, hbv_interface_0_C_49_0_S_14, hbv_interface_0_C_49_0_V_15, hbv_interface_0_C_49_0_M_6, hbv_interface_0_C_49_0_W_16, hbv_interface_0_C_49_0_N_7, hbv_interface_0_C_49_0_F_3, hbv_interface_0_C_49_0_U_11, hbv_interface_0_C_49_0_I_17, hhv_interface_0_C_49_0_I_5, hbv_interface_0_C_49_0_Y_18, hhv_interface_0_C_49_0_G_6);
      VAL   [hbv_interface_0_C_49_0_E_1=0, hbv_interface_0_C_49_0_F_3=0, hbv_interface_0_C_49_0_K_4=0, hbv_interface_0_C_49_0_L_2=0, hbv_interface_0_C_49_0_L_5=0, hbv_interface_0_C_49_0_M_6=0, hbv_interface_0_C_49_0_N_7=0, hbv_interface_0_C_49_0_O_8=0, hbv_interface_0_C_49_0_P_9=0, hbv_interface_0_C_49_0_Q_10=0, hbv_interface_0_C_49_0_U_11=0, hbv_interface_0_C_49_0_V_12=0, hbv_interface_0_C_49_0_V_15=638722035, hbv_interface_0_C_49_0_W_16=638722037, hbv_interface_0_C_49_0_Y_18=0, hhv_interface_0_C_49_0_G_6=0, hhv_interface_0_C_49_0_J_0=638722033]
[L0]  RET   call interface_0_C_49_0(hbv_error_target_6_0_J_2, hbv_error_target_6_0_A_3, hbv_error_target_6_0_B_4, hbv_error_target_6_0_C_5, hbv_error_target_6_0_D_6, hbv_error_target_6_0_H_7, hbv_error_target_6_0_F_8);
      VAL   [hbv_error_target_6_0_E_1=2, hbv_error_target_6_0_F_8=0, hbv_error_target_6_0_J_2=638722033]
[L0]  CALL  call summary_4_function_f__40_49_0(hbv_error_target_6_0_E_1, hbv_error_target_6_0_J_2, hbv_error_target_6_0_A_3, hbv_error_target_6_0_B_4, hbv_error_target_6_0_C_5, hbv_error_target_6_0_D_6, hbv_error_target_6_0_K_9, hbv_error_target_6_0_L_10, hbv_error_target_6_0_M_11, hbv_error_target_6_0_N_12, hbv_error_target_6_0_O_13, hbv_error_target_6_0_P_14, hbv_error_target_6_0_Q_15, hbv_error_target_6_0_R_16, hbv_error_target_6_0_S_17, hbv_error_target_6_0_T_18, hbv_error_target_6_0_U_19, hbv_error_target_6_0_V_20, hbv_error_target_6_0_W_21, hbv_error_target_6_0_X_22, hbv_error_target_6_0_Y_23, hbv_error_target_6_0_H_7, hbv_error_target_6_0_F_8, hbv_error_target_6_0_I_24, hbv_error_target_6_0_G_25);
      VAL   [hhv_summary_4_function_f__40_49_0_A1_16=8, hhv_summary_4_function_f__40_49_0_B1_17=638722032, hhv_summary_4_function_f__40_49_0_C1_18=0, hhv_summary_4_function_f__40_49_0_D1_19=10, hhv_summary_4_function_f__40_49_0_E1_20=12, hhv_summary_4_function_f__40_49_0_G_0=2, hhv_summary_4_function_f__40_49_0_I_22=0, hhv_summary_4_function_f__40_49_0_K_24=638722038, hhv_summary_4_function_f__40_49_0_P_1=638722033, hhv_summary_4_function_f__40_49_0_Q_6=7, hhv_summary_4_function_f__40_49_0_R_7=11, hhv_summary_4_function_f__40_49_0_S_8=6, hhv_summary_4_function_f__40_49_0_T_9=15, hhv_summary_4_function_f__40_49_0_U_10=9, hhv_summary_4_function_f__40_49_0_V_11=13, hhv_summary_4_function_f__40_49_0_W_12=5, hhv_summary_4_function_f__40_49_0_Z_15=4]
[L0]        assume ((((((((((((((((((((((((((((((((((!(hhv_summary_4_function_f__40_49_0_D1_19 < 0) && !(hhv_summary_4_function_f__40_49_0_A1_16 < 0)) && hbv_summary_4_function_f__40_49_0_N_4 == hbv_summary_4_function_f__40_49_0_M_1[hhv_summary_4_function_f__40_49_0_P_1 := hbv_summary_4_function_f__40_49_0_H_2 + hbv_summary_4_function_f__40_49_0_M_1[hhv_summary_4_function_f__40_49_0_P_1]]) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_U_10)) && !(hhv_summary_4_function_f__40_49_0_T_9 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_W_12)) && !(hhv_summary_4_function_f__40_49_0_Z_15 < 4)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hbv_summary_4_function_f__40_49_0_H_2 + hbv_summary_4_function_f__40_49_0_M_1[hhv_summary_4_function_f__40_49_0_P_1])) && hbv_summary_4_function_f__40_49_0_J_5 == hhv_summary_4_function_f__40_49_0_I_22) && hhv_summary_4_function_f__40_49_0_C1_18 == 0) && hbv_summary_4_function_f__40_49_0_F_3 == 0) && !(hhv_summary_4_function_f__40_49_0_V_11 < 0)) && !(hhv_summary_4_function_f__40_49_0_S_8 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_C1_18)) && hhv_summary_4_function_f__40_49_0_Y_14[0] == 38) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_D1_19)) && 240 == hhv_summary_4_function_f__40_49_0_Y_14[3]) && !(hbv_summary_4_function_f__40_49_0_H_2 + hbv_summary_4_function_f__40_49_0_M_1[hhv_summary_4_function_f__40_49_0_P_1] < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_T_9)) && !(1461501637330902918203684832716283019655932542975 < hhv_summary_4_function_f__40_49_0_A1_16)) && !(hbv_summary_4_function_f__40_49_0_H_2 < hhv_summary_4_function_f__40_49_0_C1_18)) && !(hhv_summary_4_function_f__40_49_0_C1_18 < 0)) && hhv_summary_4_function_f__40_49_0_Y_14[2] == 31) && !(hhv_summary_4_function_f__40_49_0_E1_20 < 0)) && !(1461501637330902918203684832716283019655932542975 < hhv_summary_4_function_f__40_49_0_S_8)) && !(hhv_summary_4_function_f__40_49_0_W_12 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_Q_6)) && hhv_summary_4_function_f__40_49_0_Y_14[1] == 18) && !(hhv_summary_4_function_f__40_49_0_R_7 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_V_11)) && !(hhv_summary_4_function_f__40_49_0_Q_6 < 0)) && !(115792089237316195423570985008687907853269984665640564039457584007913129639935 < hhv_summary_4_function_f__40_49_0_R_7)) && !(1461501637330902918203684832716283019655932542975 < hhv_summary_4_function_f__40_49_0_E1_20)) && !(hhv_summary_4_function_f__40_49_0_U_10 < 0)) && hhv_summary_4_function_f__40_49_0_L_21 == hbv_summary_4_function_f__40_49_0_M_1) && 638722032 == hhv_summary_4_function_f__40_49_0_B1_17;
      VAL   [hbv_summary_4_function_f__40_49_0_F_3=0, hbv_summary_4_function_f__40_49_0_J_5=0, hhv_summary_4_function_f__40_49_0_A1_16=8, hhv_summary_4_function_f__40_49_0_B1_17=638722032, hhv_summary_4_function_f__40_49_0_C1_18=0, hhv_summary_4_function_f__40_49_0_D1_19=10, hhv_summary_4_function_f__40_49_0_E1_20=12, hhv_summary_4_function_f__40_49_0_G_0=2, hhv_summary_4_function_f__40_49_0_I_22=0, hhv_summary_4_function_f__40_49_0_K_24=638722038, hhv_summary_4_function_f__40_49_0_P_1=638722033, hhv_summary_4_function_f__40_49_0_Q_6=7, hhv_summary_4_function_f__40_49_0_R_7=11, hhv_summary_4_function_f__40_49_0_S_8=6, hhv_summary_4_function_f__40_49_0_T_9=15, hhv_summary_4_function_f__40_49_0_U_10=9, hhv_summary_4_function_f__40_49_0_V_11=13, hhv_summary_4_function_f__40_49_0_W_12=5, hhv_summary_4_function_f__40_49_0_Z_15=4]
[L0]  CALL  call block_15_function_f__40_49_0(hbv_summary_4_function_f__40_49_0_F_3, hhv_summary_4_function_f__40_49_0_P_1, hhv_summary_4_function_f__40_49_0_A_2, hhv_summary_4_function_f__40_49_0_B_3, hhv_summary_4_function_f__40_49_0_C_4, hhv_summary_4_function_f__40_49_0_D_5, hhv_summary_4_function_f__40_49_0_Q_6, hhv_summary_4_function_f__40_49_0_R_7, hhv_summary_4_function_f__40_49_0_S_8, hhv_summary_4_function_f__40_49_0_T_9, hhv_summary_4_function_f__40_49_0_U_10, hhv_summary_4_function_f__40_49_0_V_11, hhv_summary_4_function_f__40_49_0_W_12, hhv_summary_4_function_f__40_49_0_X_13, hhv_summary_4_function_f__40_49_0_Y_14, hhv_summary_4_function_f__40_49_0_Z_15, hhv_summary_4_function_f__40_49_0_A1_16, hhv_summary_4_function_f__40_49_0_B1_17, hhv_summary_4_function_f__40_49_0_C1_18, hhv_summary_4_function_f__40_49_0_D1_19, hhv_summary_4_function_f__40_49_0_E1_20, hhv_summary_4_function_f__40_49_0_L_21, hhv_summary_4_function_f__40_49_0_I_22, hbv_summary_4_function_f__40_49_0_M_1, hbv_summary_4_function_f__40_49_0_J_5, hbv_summary_4_function_f__40_49_0_E_6);
[L0]  RET   call block_15_function_f__40_49_0(hbv_summary_4_function_f__40_49_0_F_3, hhv_summary_4_function_f__40_49_0_P_1, hhv_summary_4_function_f__40_49_0_A_2, hhv_summary_4_function_f__40_49_0_B_3, hhv_summary_4_function_f__40_49_0_C_4, hhv_summary_4_function_f__40_49_0_D_5, hhv_summary_4_function_f__40_49_0_Q_6, hhv_summary_4_function_f__40_49_0_R_7, hhv_summary_4_function_f__40_49_0_S_8, hhv_summary_4_function_f__40_49_0_T_9, hhv_summary_4_function_f__40_49_0_U_10, hhv_summary_4_function_f__40_49_0_V_11, hhv_summary_4_function_f__40_49_0_W_12, hhv_summary_4_function_f__40_49_0_X_13, hhv_summary_4_function_f__40_49_0_Y_14, hhv_summary_4_function_f__40_49_0_Z_15, hhv_summary_4_function_f__40_49_0_A1_16, hhv_summary_4_function_f__40_49_0_B1_17, hhv_summary_4_function_f__40_49_0_C1_18, hhv_summary_4_function_f__40_49_0_D1_19, hhv_summary_4_function_f__40_49_0_E1_20, hhv_summary_4_function_f__40_49_0_L_21, hhv_summary_4_function_f__40_49_0_I_22, hbv_summary_4_function_f__40_49_0_M_1, hbv_summary_4_function_f__40_49_0_J_5, hbv_summary_4_function_f__40_49_0_E_6);
      VAL   [hbv_summary_4_function_f__40_49_0_E_6=638722036, hbv_summary_4_function_f__40_49_0_F_3=0, hbv_summary_4_function_f__40_49_0_J_5=0, hhv_summary_4_function_f__40_49_0_A1_16=8, hhv_summary_4_function_f__40_49_0_B1_17=638722032, hhv_summary_4_function_f__40_49_0_C1_18=0, hhv_summary_4_function_f__40_49_0_D1_19=10, hhv_summary_4_function_f__40_49_0_E1_20=12, hhv_summary_4_function_f__40_49_0_G_0=2, hhv_summary_4_function_f__40_49_0_I_22=0, hhv_summary_4_function_f__40_49_0_K_24=638722038, hhv_summary_4_function_f__40_49_0_P_1=638722033, hhv_summary_4_function_f__40_49_0_Q_6=7, hhv_summary_4_function_f__40_49_0_R_7=11, hhv_summary_4_function_f__40_49_0_S_8=6, hhv_summary_4_function_f__40_49_0_T_9=15, hhv_summary_4_function_f__40_49_0_U_10=9, hhv_summary_4_function_f__40_49_0_V_11=13, hhv_summary_4_function_f__40_49_0_W_12=5, hhv_summary_4_function_f__40_49_0_Z_15=4]
[L0]  CALL  call summary_3_function_f__40_49_0(hhv_summary_4_function_f__40_49_0_G_0, hhv_summary_4_function_f__40_49_0_P_1, hhv_summary_4_function_f__40_49_0_A_2, hhv_summary_4_function_f__40_49_0_B_3, hhv_summary_4_function_f__40_49_0_C_4, hhv_summary_4_function_f__40_49_0_D_5, hhv_summary_4_function_f__40_49_0_Q_6, hhv_summary_4_function_f__40_49_0_R_7, hhv_summary_4_function_f__40_49_0_S_8, hhv_summary_4_function_f__40_49_0_T_9, hhv_summary_4_function_f__40_49_0_U_10, hhv_summary_4_function_f__40_49_0_V_11, hhv_summary_4_function_f__40_49_0_W_12, hhv_summary_4_function_f__40_49_0_X_13, hhv_summary_4_function_f__40_49_0_Y_14, hhv_summary_4_function_f__40_49_0_Z_15, hhv_summary_4_function_f__40_49_0_A1_16, hhv_summary_4_function_f__40_49_0_B1_17, hhv_summary_4_function_f__40_49_0_C1_18, hhv_summary_4_function_f__40_49_0_D1_19, hhv_summary_4_function_f__40_49_0_E1_20, hbv_summary_4_function_f__40_49_0_N_4, hbv_summary_4_function_f__40_49_0_J_5, hhv_summary_4_function_f__40_49_0_O_23, hhv_summary_4_function_f__40_49_0_K_24);
      VAL   [hhv_summary_3_function_f__40_49_0_A1_11=13, hhv_summary_3_function_f__40_49_0_B1_12=5, hhv_summary_3_function_f__40_49_0_E1_15=4, hhv_summary_3_function_f__40_49_0_F1_16=8, hhv_summary_3_function_f__40_49_0_G1_17=638722032, hhv_summary_3_function_f__40_49_0_H1_18=0, hhv_summary_3_function_f__40_49_0_H_0=2, hhv_summary_3_function_f__40_49_0_I1_19=10, hhv_summary_3_function_f__40_49_0_J1_20=12, hhv_summary_3_function_f__40_49_0_N_22=0, hhv_summary_3_function_f__40_49_0_Q_24=638722038, hhv_summary_3_function_f__40_49_0_U_1=638722033, hhv_summary_3_function_f__40_49_0_V_6=7, hhv_summary_3_function_f__40_49_0_W_7=11, hhv_summary_3_function_f__40_49_0_X_8=6, hhv_summary_3_function_f__40_49_0_Y_9=15, hhv_summary_3_function_f__40_49_0_Z_10=9]
[L0]  CALL  call block_14_function_f__40_49_0(hhv_summary_3_function_f__40_49_0_H_0, hhv_summary_3_function_f__40_49_0_U_1, hhv_summary_3_function_f__40_49_0_A_2, hhv_summary_3_function_f__40_49_0_B_3, hhv_summary_3_function_f__40_49_0_C_4, hhv_summary_3_function_f__40_49_0_D_5, hhv_summary_3_function_f__40_49_0_V_6, hhv_summary_3_function_f__40_49_0_W_7, hhv_summary_3_function_f__40_49_0_X_8, hhv_summary_3_function_f__40_49_0_Y_9, hhv_summary_3_function_f__40_49_0_Z_10, hhv_summary_3_function_f__40_49_0_A1_11, hhv_summary_3_function_f__40_49_0_B1_12, hhv_summary_3_function_f__40_49_0_C1_13, hhv_summary_3_function_f__40_49_0_D1_14, hhv_summary_3_function_f__40_49_0_E1_15, hhv_summary_3_function_f__40_49_0_F1_16, hhv_summary_3_function_f__40_49_0_G1_17, hhv_summary_3_function_f__40_49_0_H1_18, hhv_summary_3_function_f__40_49_0_I1_19, hhv_summary_3_function_f__40_49_0_J1_20, hhv_summary_3_function_f__40_49_0_R_21, hhv_summary_3_function_f__40_49_0_N_22, hhv_summary_3_function_f__40_49_0_T_23, hhv_summary_3_function_f__40_49_0_Q_24, hbv_summary_3_function_f__40_49_0_E_1);
      VAL   [hhv_block_14_function_f__40_49_0_E1_24=638722038, hhv_block_14_function_f__40_49_0_F_25=638722038, hhv_block_14_function_f__40_49_0_K1_1=638722033, hhv_block_14_function_f__40_49_0_L1_6=7, hhv_block_14_function_f__40_49_0_L_0=2, hhv_block_14_function_f__40_49_0_M1_7=11, hhv_block_14_function_f__40_49_0_N1_8=6, hhv_block_14_function_f__40_49_0_O1_9=15, hhv_block_14_function_f__40_49_0_P1_10=9, hhv_block_14_function_f__40_49_0_Q1_11=13, hhv_block_14_function_f__40_49_0_R1_12=5, hhv_block_14_function_f__40_49_0_U1_15=4, hhv_block_14_function_f__40_49_0_V1_16=8, hhv_block_14_function_f__40_49_0_W1_17=638722032, hhv_block_14_function_f__40_49_0_X1_18=0, hhv_block_14_function_f__40_49_0_Y1_19=10, hhv_block_14_function_f__40_49_0_Z1_20=12, hhv_block_14_function_f__40_49_0_Z_22=0]
[L0]        assume ((((((((((((((((hbv_block_14_function_f__40_49_0_I_20 == 0 && hhv_block_14_function_f__40_49_0_F_25 == hbv_block_14_function_f__40_49_0_P_12) && hbv_block_14_function_f__40_49_0_A1_5 == hbv_block_14_function_f__40_49_0_Y_6) && hbv_block_14_function_f__40_49_0_O_18 == hhv_block_14_function_f__40_49_0_F_25) && !hbv_block_14_function_f__40_49_0_X_4) && hhv_block_14_function_f__40_49_0_K1_1 == hbv_block_14_function_f__40_49_0_M_21) && hbv_block_14_function_f__40_49_0_E_1 == 0) && hbv_block_14_function_f__40_49_0_J_19 == hbv_block_14_function_f__40_49_0_I_20) && !((!hbv_block_14_function_f__40_49_0_T_16 || hbv_block_14_function_f__40_49_0_S_14 != hbv_block_14_function_f__40_49_0_Q_15) && (hbv_block_14_function_f__40_49_0_S_14 == hbv_block_14_function_f__40_49_0_Q_15 || hbv_block_14_function_f__40_49_0_T_16))) && 2 == hhv_block_14_function_f__40_49_0_L_0) && hbv_block_14_function_f__40_49_0_W_2 == 1) && hbv_block_14_function_f__40_49_0_C1_8 == hbv_block_14_function_f__40_49_0_R_9) && !((hbv_block_14_function_f__40_49_0_W_2 == hbv_block_14_function_f__40_49_0_V_3 || hbv_block_14_function_f__40_49_0_X_4) && (!hbv_block_14_function_f__40_49_0_X_4 || hbv_block_14_function_f__40_49_0_W_2 != hbv_block_14_function_f__40_49_0_V_3))) && hbv_block_14_function_f__40_49_0_H_11 == 0) && hhv_block_14_function_f__40_49_0_K1_1 == hbv_block_14_function_f__40_49_0_N_13) && hbv_block_14_function_f__40_49_0_K_10 == 0) && hhv_block_14_function_f__40_49_0_F_25 == hbv_block_14_function_f__40_49_0_U_7) && hbv_block_14_function_f__40_49_0_B1_17 == hbv_block_14_function_f__40_49_0_O_18;
      VAL   [hbv_block_14_function_f__40_49_0_A1_5=0, hbv_block_14_function_f__40_49_0_B1_17=638722038, hbv_block_14_function_f__40_49_0_C1_8=638722038, hbv_block_14_function_f__40_49_0_E_1=0, hbv_block_14_function_f__40_49_0_H_11=0, hbv_block_14_function_f__40_49_0_I_20=0, hbv_block_14_function_f__40_49_0_K_10=0, hhv_block_14_function_f__40_49_0_E1_24=638722038, hhv_block_14_function_f__40_49_0_F_25=638722038, hhv_block_14_function_f__40_49_0_K1_1=638722033, hhv_block_14_function_f__40_49_0_L1_6=7, hhv_block_14_function_f__40_49_0_L_0=2, hhv_block_14_function_f__40_49_0_M1_7=11, hhv_block_14_function_f__40_49_0_N1_8=6, hhv_block_14_function_f__40_49_0_O1_9=15, hhv_block_14_function_f__40_49_0_P1_10=9, hhv_block_14_function_f__40_49_0_Q1_11=13, hhv_block_14_function_f__40_49_0_R1_12=5, hhv_block_14_function_f__40_49_0_U1_15=4, hhv_block_14_function_f__40_49_0_V1_16=8, hhv_block_14_function_f__40_49_0_W1_17=638722032, hhv_block_14_function_f__40_49_0_X1_18=0, hhv_block_14_function_f__40_49_0_Y1_19=10, hhv_block_14_function_f__40_49_0_Z1_20=12, hhv_block_14_function_f__40_49_0_Z_22=0]
[L0]  CALL  call nondet_call_13_0(hbv_block_14_function_f__40_49_0_K_10, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hbv_block_14_function_f__40_49_0_I1_22, hbv_block_14_function_f__40_49_0_D1_23, hhv_block_14_function_f__40_49_0_J1_23, hhv_block_14_function_f__40_49_0_E1_24);
      VAL   [hhv_nondet_call_13_0_E_0=0, hhv_nondet_call_13_0_F_7=638722038, hhv_nondet_call_13_0_G_9=638722038, hhv_nondet_call_13_0_J_1=638722033]
[L0]  CALL  call nondet_interface_1_C_49_0(hhv_nondet_call_13_0_E_0, hhv_nondet_call_13_0_J_1, hhv_nondet_call_13_0_A_2, hhv_nondet_call_13_0_B_3, hhv_nondet_call_13_0_C_4, hhv_nondet_call_13_0_D_5, hhv_nondet_call_13_0_H_6, hhv_nondet_call_13_0_F_7, hhv_nondet_call_13_0_I_8, hhv_nondet_call_13_0_G_9);
      VAL   [hhv_nondet_interface_1_C_49_0_E_0=0, hhv_nondet_interface_1_C_49_0_F_7=638722038, hhv_nondet_interface_1_C_49_0_H_1=638722033, hhv_nondet_interface_1_C_49_0_v_9_9=638722038]
[L0]        assume (hhv_nondet_interface_1_C_49_0_v_9_9 == hhv_nondet_interface_1_C_49_0_F_7 && hhv_nondet_interface_1_C_49_0_E_0 == 0) && hhv_nondet_interface_1_C_49_0_G_6 == hhv_nondet_interface_1_C_49_0_v_8_8;
      VAL   [hhv_nondet_interface_1_C_49_0_E_0=0, hhv_nondet_interface_1_C_49_0_F_7=638722038, hhv_nondet_interface_1_C_49_0_H_1=638722033, hhv_nondet_interface_1_C_49_0_v_9_9=638722038]
[L0]  RET   call nondet_interface_1_C_49_0(hhv_nondet_call_13_0_E_0, hhv_nondet_call_13_0_J_1, hhv_nondet_call_13_0_A_2, hhv_nondet_call_13_0_B_3, hhv_nondet_call_13_0_C_4, hhv_nondet_call_13_0_D_5, hhv_nondet_call_13_0_H_6, hhv_nondet_call_13_0_F_7, hhv_nondet_call_13_0_I_8, hhv_nondet_call_13_0_G_9);
      VAL   [hhv_nondet_call_13_0_E_0=0, hhv_nondet_call_13_0_F_7=638722038, hhv_nondet_call_13_0_G_9=638722038, hhv_nondet_call_13_0_J_1=638722033]
[L0]  RET   call nondet_call_13_0(hbv_block_14_function_f__40_49_0_K_10, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hbv_block_14_function_f__40_49_0_I1_22, hbv_block_14_function_f__40_49_0_D1_23, hhv_block_14_function_f__40_49_0_J1_23, hhv_block_14_function_f__40_49_0_E1_24);
      VAL   [hbv_block_14_function_f__40_49_0_A1_5=0, hbv_block_14_function_f__40_49_0_B1_17=638722038, hbv_block_14_function_f__40_49_0_C1_8=638722038, hbv_block_14_function_f__40_49_0_D1_23=638722038, hbv_block_14_function_f__40_49_0_E_1=0, hbv_block_14_function_f__40_49_0_H_11=0, hbv_block_14_function_f__40_49_0_I_20=0, hbv_block_14_function_f__40_49_0_K_10=0, hhv_block_14_function_f__40_49_0_E1_24=638722038, hhv_block_14_function_f__40_49_0_F_25=638722038, hhv_block_14_function_f__40_49_0_K1_1=638722033, hhv_block_14_function_f__40_49_0_L1_6=7, hhv_block_14_function_f__40_49_0_L_0=2, hhv_block_14_function_f__40_49_0_M1_7=11, hhv_block_14_function_f__40_49_0_N1_8=6, hhv_block_14_function_f__40_49_0_O1_9=15, hhv_block_14_function_f__40_49_0_P1_10=9, hhv_block_14_function_f__40_49_0_Q1_11=13, hhv_block_14_function_f__40_49_0_R1_12=5, hhv_block_14_function_f__40_49_0_U1_15=4, hhv_block_14_function_f__40_49_0_V1_16=8, hhv_block_14_function_f__40_49_0_W1_17=638722032, hhv_block_14_function_f__40_49_0_X1_18=0, hhv_block_14_function_f__40_49_0_Y1_19=10, hhv_block_14_function_f__40_49_0_Z1_20=12, hhv_block_14_function_f__40_49_0_Z_22=0]
[L0]  CALL  call block_8_f_39_49_0(hbv_block_14_function_f__40_49_0_G_24, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hhv_block_14_function_f__40_49_0_L1_6, hhv_block_14_function_f__40_49_0_M1_7, hhv_block_14_function_f__40_49_0_N1_8, hhv_block_14_function_f__40_49_0_O1_9, hhv_block_14_function_f__40_49_0_P1_10, hhv_block_14_function_f__40_49_0_Q1_11, hhv_block_14_function_f__40_49_0_R1_12, hhv_block_14_function_f__40_49_0_S1_13, hhv_block_14_function_f__40_49_0_T1_14, hhv_block_14_function_f__40_49_0_U1_15, hhv_block_14_function_f__40_49_0_V1_16, hhv_block_14_function_f__40_49_0_W1_17, hhv_block_14_function_f__40_49_0_X1_18, hhv_block_14_function_f__40_49_0_Y1_19, hhv_block_14_function_f__40_49_0_Z1_20, hhv_block_14_function_f__40_49_0_F1_21, hhv_block_14_function_f__40_49_0_Z_22, hbv_block_14_function_f__40_49_0_G1_25, hbv_block_14_function_f__40_49_0_A1_5, hbv_block_14_function_f__40_49_0_E_1);
      VAL   [hhv_block_8_f_39_49_0_E_25=0, hhv_block_8_f_39_49_0_F_0=0, hhv_block_8_f_39_49_0_G_22=0, hhv_block_8_f_39_49_0_H_24=0, hhv_block_8_f_39_49_0_K_1=638722033, hhv_block_8_f_39_49_0_L_6=7, hhv_block_8_f_39_49_0_M_7=11, hhv_block_8_f_39_49_0_N_8=6, hhv_block_8_f_39_49_0_O_9=15, hhv_block_8_f_39_49_0_P_10=9, hhv_block_8_f_39_49_0_Q_11=13, hhv_block_8_f_39_49_0_R_12=5, hhv_block_8_f_39_49_0_U_15=4, hhv_block_8_f_39_49_0_V_16=8, hhv_block_8_f_39_49_0_W_17=638722032, hhv_block_8_f_39_49_0_X_18=0, hhv_block_8_f_39_49_0_Y_19=10, hhv_block_8_f_39_49_0_Z_20=12]
[L0]        assume (hhv_block_8_f_39_49_0_H_24 == hhv_block_8_f_39_49_0_G_22 && hhv_block_8_f_39_49_0_F_0 == 0) && hhv_block_8_f_39_49_0_I_21 == hhv_block_8_f_39_49_0_J_23;
      VAL   [hhv_block_8_f_39_49_0_E_25=0, hhv_block_8_f_39_49_0_F_0=0, hhv_block_8_f_39_49_0_G_22=0, hhv_block_8_f_39_49_0_H_24=0, hhv_block_8_f_39_49_0_K_1=638722033, hhv_block_8_f_39_49_0_L_6=7, hhv_block_8_f_39_49_0_M_7=11, hhv_block_8_f_39_49_0_N_8=6, hhv_block_8_f_39_49_0_O_9=15, hhv_block_8_f_39_49_0_P_10=9, hhv_block_8_f_39_49_0_Q_11=13, hhv_block_8_f_39_49_0_R_12=5, hhv_block_8_f_39_49_0_U_15=4, hhv_block_8_f_39_49_0_V_16=8, hhv_block_8_f_39_49_0_W_17=638722032, hhv_block_8_f_39_49_0_X_18=0, hhv_block_8_f_39_49_0_Y_19=10, hhv_block_8_f_39_49_0_Z_20=12]
[L0]  CALL  call block_7_function_f__40_49_0(hhv_block_8_f_39_49_0_F_0, hhv_block_8_f_39_49_0_K_1, hhv_block_8_f_39_49_0_A_2, hhv_block_8_f_39_49_0_B_3, hhv_block_8_f_39_49_0_C_4, hhv_block_8_f_39_49_0_D_5, hhv_block_8_f_39_49_0_L_6, hhv_block_8_f_39_49_0_M_7, hhv_block_8_f_39_49_0_N_8, hhv_block_8_f_39_49_0_O_9, hhv_block_8_f_39_49_0_P_10, hhv_block_8_f_39_49_0_Q_11, hhv_block_8_f_39_49_0_R_12, hhv_block_8_f_39_49_0_S_13, hhv_block_8_f_39_49_0_T_14, hhv_block_8_f_39_49_0_U_15, hhv_block_8_f_39_49_0_V_16, hhv_block_8_f_39_49_0_W_17, hhv_block_8_f_39_49_0_X_18, hhv_block_8_f_39_49_0_Y_19, hhv_block_8_f_39_49_0_Z_20, hhv_block_8_f_39_49_0_I_21, hhv_block_8_f_39_49_0_G_22, hhv_block_8_f_39_49_0_J_23, hhv_block_8_f_39_49_0_H_24, hhv_block_8_f_39_49_0_E_25);
[L0]  RET   call block_7_function_f__40_49_0(hhv_block_8_f_39_49_0_F_0, hhv_block_8_f_39_49_0_K_1, hhv_block_8_f_39_49_0_A_2, hhv_block_8_f_39_49_0_B_3, hhv_block_8_f_39_49_0_C_4, hhv_block_8_f_39_49_0_D_5, hhv_block_8_f_39_49_0_L_6, hhv_block_8_f_39_49_0_M_7, hhv_block_8_f_39_49_0_N_8, hhv_block_8_f_39_49_0_O_9, hhv_block_8_f_39_49_0_P_10, hhv_block_8_f_39_49_0_Q_11, hhv_block_8_f_39_49_0_R_12, hhv_block_8_f_39_49_0_S_13, hhv_block_8_f_39_49_0_T_14, hhv_block_8_f_39_49_0_U_15, hhv_block_8_f_39_49_0_V_16, hhv_block_8_f_39_49_0_W_17, hhv_block_8_f_39_49_0_X_18, hhv_block_8_f_39_49_0_Y_19, hhv_block_8_f_39_49_0_Z_20, hhv_block_8_f_39_49_0_I_21, hhv_block_8_f_39_49_0_G_22, hhv_block_8_f_39_49_0_J_23, hhv_block_8_f_39_49_0_H_24, hhv_block_8_f_39_49_0_E_25);
      VAL   [hhv_block_8_f_39_49_0_E_25=0, hhv_block_8_f_39_49_0_F_0=0, hhv_block_8_f_39_49_0_G_22=0, hhv_block_8_f_39_49_0_H_24=0, hhv_block_8_f_39_49_0_K_1=638722033, hhv_block_8_f_39_49_0_L_6=7, hhv_block_8_f_39_49_0_M_7=11, hhv_block_8_f_39_49_0_N_8=6, hhv_block_8_f_39_49_0_O_9=15, hhv_block_8_f_39_49_0_P_10=9, hhv_block_8_f_39_49_0_Q_11=13, hhv_block_8_f_39_49_0_R_12=5, hhv_block_8_f_39_49_0_U_15=4, hhv_block_8_f_39_49_0_V_16=8, hhv_block_8_f_39_49_0_W_17=638722032, hhv_block_8_f_39_49_0_X_18=0, hhv_block_8_f_39_49_0_Y_19=10, hhv_block_8_f_39_49_0_Z_20=12]
[L0]  RET   call block_8_f_39_49_0(hbv_block_14_function_f__40_49_0_G_24, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hhv_block_14_function_f__40_49_0_L1_6, hhv_block_14_function_f__40_49_0_M1_7, hhv_block_14_function_f__40_49_0_N1_8, hhv_block_14_function_f__40_49_0_O1_9, hhv_block_14_function_f__40_49_0_P1_10, hhv_block_14_function_f__40_49_0_Q1_11, hhv_block_14_function_f__40_49_0_R1_12, hhv_block_14_function_f__40_49_0_S1_13, hhv_block_14_function_f__40_49_0_T1_14, hhv_block_14_function_f__40_49_0_U1_15, hhv_block_14_function_f__40_49_0_V1_16, hhv_block_14_function_f__40_49_0_W1_17, hhv_block_14_function_f__40_49_0_X1_18, hhv_block_14_function_f__40_49_0_Y1_19, hhv_block_14_function_f__40_49_0_Z1_20, hhv_block_14_function_f__40_49_0_F1_21, hhv_block_14_function_f__40_49_0_Z_22, hbv_block_14_function_f__40_49_0_G1_25, hbv_block_14_function_f__40_49_0_A1_5, hbv_block_14_function_f__40_49_0_E_1);
      VAL   [hbv_block_14_function_f__40_49_0_A1_5=0, hbv_block_14_function_f__40_49_0_B1_17=638722038, hbv_block_14_function_f__40_49_0_C1_8=638722038, hbv_block_14_function_f__40_49_0_D1_23=638722038, hbv_block_14_function_f__40_49_0_E_1=0, hbv_block_14_function_f__40_49_0_G_24=0, hbv_block_14_function_f__40_49_0_H_11=0, hbv_block_14_function_f__40_49_0_I_20=0, hbv_block_14_function_f__40_49_0_K_10=0, hhv_block_14_function_f__40_49_0_E1_24=638722038, hhv_block_14_function_f__40_49_0_F_25=638722038, hhv_block_14_function_f__40_49_0_K1_1=638722033, hhv_block_14_function_f__40_49_0_L1_6=7, hhv_block_14_function_f__40_49_0_L_0=2, hhv_block_14_function_f__40_49_0_M1_7=11, hhv_block_14_function_f__40_49_0_N1_8=6, hhv_block_14_function_f__40_49_0_O1_9=15, hhv_block_14_function_f__40_49_0_P1_10=9, hhv_block_14_function_f__40_49_0_Q1_11=13, hhv_block_14_function_f__40_49_0_R1_12=5, hhv_block_14_function_f__40_49_0_U1_15=4, hhv_block_14_function_f__40_49_0_V1_16=8, hhv_block_14_function_f__40_49_0_W1_17=638722032, hhv_block_14_function_f__40_49_0_X1_18=0, hhv_block_14_function_f__40_49_0_Y1_19=10, hhv_block_14_function_f__40_49_0_Z1_20=12, hhv_block_14_function_f__40_49_0_Z_22=0]
[L0]  CALL  call nondet_call_11_0(hbv_block_14_function_f__40_49_0_I_20, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hbv_block_14_function_f__40_49_0_H1_26, hbv_block_14_function_f__40_49_0_C1_8, hbv_block_14_function_f__40_49_0_I1_22, hbv_block_14_function_f__40_49_0_D1_23);
      VAL   [hhv_nondet_call_11_0_E_0=0, hhv_nondet_call_11_0_F_7=638722038, hhv_nondet_call_11_0_G_9=638722038, hhv_nondet_call_11_0_J_1=638722033]
[L0]  CALL  call nondet_interface_1_C_49_0(hhv_nondet_call_11_0_E_0, hhv_nondet_call_11_0_J_1, hhv_nondet_call_11_0_A_2, hhv_nondet_call_11_0_B_3, hhv_nondet_call_11_0_C_4, hhv_nondet_call_11_0_D_5, hhv_nondet_call_11_0_H_6, hhv_nondet_call_11_0_F_7, hhv_nondet_call_11_0_I_8, hhv_nondet_call_11_0_G_9);
      VAL   [hhv_nondet_interface_1_C_49_0_E_0=0, hhv_nondet_interface_1_C_49_0_F_7=638722038, hhv_nondet_interface_1_C_49_0_H_1=638722033, hhv_nondet_interface_1_C_49_0_v_9_9=638722038]
[L0]        assume (hhv_nondet_interface_1_C_49_0_v_9_9 == hhv_nondet_interface_1_C_49_0_F_7 && hhv_nondet_interface_1_C_49_0_E_0 == 0) && hhv_nondet_interface_1_C_49_0_G_6 == hhv_nondet_interface_1_C_49_0_v_8_8;
      VAL   [hhv_nondet_interface_1_C_49_0_E_0=0, hhv_nondet_interface_1_C_49_0_F_7=638722038, hhv_nondet_interface_1_C_49_0_H_1=638722033, hhv_nondet_interface_1_C_49_0_v_9_9=638722038]
[L0]  RET   call nondet_interface_1_C_49_0(hhv_nondet_call_11_0_E_0, hhv_nondet_call_11_0_J_1, hhv_nondet_call_11_0_A_2, hhv_nondet_call_11_0_B_3, hhv_nondet_call_11_0_C_4, hhv_nondet_call_11_0_D_5, hhv_nondet_call_11_0_H_6, hhv_nondet_call_11_0_F_7, hhv_nondet_call_11_0_I_8, hhv_nondet_call_11_0_G_9);
      VAL   [hhv_nondet_call_11_0_E_0=0, hhv_nondet_call_11_0_F_7=638722038, hhv_nondet_call_11_0_G_9=638722038, hhv_nondet_call_11_0_J_1=638722033]
[L0]  RET   call nondet_call_11_0(hbv_block_14_function_f__40_49_0_I_20, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hbv_block_14_function_f__40_49_0_H1_26, hbv_block_14_function_f__40_49_0_C1_8, hbv_block_14_function_f__40_49_0_I1_22, hbv_block_14_function_f__40_49_0_D1_23);
      VAL   [hbv_block_14_function_f__40_49_0_A1_5=0, hbv_block_14_function_f__40_49_0_B1_17=638722038, hbv_block_14_function_f__40_49_0_C1_8=638722038, hbv_block_14_function_f__40_49_0_D1_23=638722038, hbv_block_14_function_f__40_49_0_E_1=0, hbv_block_14_function_f__40_49_0_G_24=0, hbv_block_14_function_f__40_49_0_H_11=0, hbv_block_14_function_f__40_49_0_I_20=0, hbv_block_14_function_f__40_49_0_K_10=0, hhv_block_14_function_f__40_49_0_E1_24=638722038, hhv_block_14_function_f__40_49_0_F_25=638722038, hhv_block_14_function_f__40_49_0_K1_1=638722033, hhv_block_14_function_f__40_49_0_L1_6=7, hhv_block_14_function_f__40_49_0_L_0=2, hhv_block_14_function_f__40_49_0_M1_7=11, hhv_block_14_function_f__40_49_0_N1_8=6, hhv_block_14_function_f__40_49_0_O1_9=15, hhv_block_14_function_f__40_49_0_P1_10=9, hhv_block_14_function_f__40_49_0_Q1_11=13, hhv_block_14_function_f__40_49_0_R1_12=5, hhv_block_14_function_f__40_49_0_U1_15=4, hhv_block_14_function_f__40_49_0_V1_16=8, hhv_block_14_function_f__40_49_0_W1_17=638722032, hhv_block_14_function_f__40_49_0_X1_18=0, hhv_block_14_function_f__40_49_0_Y1_19=10, hhv_block_14_function_f__40_49_0_Z1_20=12, hhv_block_14_function_f__40_49_0_Z_22=0]
[L0]  CALL  call nondet_call_10_0(hbv_block_14_function_f__40_49_0_H_11, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hbv_block_14_function_f__40_49_0_G1_25, hbv_block_14_function_f__40_49_0_B1_17, hbv_block_14_function_f__40_49_0_H1_26, hbv_block_14_function_f__40_49_0_C1_8);
      VAL   [hhv_nondet_call_10_0_E_0=0, hhv_nondet_call_10_0_F_7=638722038, hhv_nondet_call_10_0_G_9=638722038, hhv_nondet_call_10_0_J_1=638722033]
[L0]  CALL  call nondet_interface_1_C_49_0(hhv_nondet_call_10_0_E_0, hhv_nondet_call_10_0_J_1, hhv_nondet_call_10_0_A_2, hhv_nondet_call_10_0_B_3, hhv_nondet_call_10_0_C_4, hhv_nondet_call_10_0_D_5, hhv_nondet_call_10_0_H_6, hhv_nondet_call_10_0_F_7, hhv_nondet_call_10_0_I_8, hhv_nondet_call_10_0_G_9);
      VAL   [hhv_nondet_interface_1_C_49_0_E_0=0, hhv_nondet_interface_1_C_49_0_F_7=638722038, hhv_nondet_interface_1_C_49_0_H_1=638722033, hhv_nondet_interface_1_C_49_0_v_9_9=638722038]
[L0]        assume (hhv_nondet_interface_1_C_49_0_v_9_9 == hhv_nondet_interface_1_C_49_0_F_7 && hhv_nondet_interface_1_C_49_0_E_0 == 0) && hhv_nondet_interface_1_C_49_0_G_6 == hhv_nondet_interface_1_C_49_0_v_8_8;
      VAL   [hhv_nondet_interface_1_C_49_0_E_0=0, hhv_nondet_interface_1_C_49_0_F_7=638722038, hhv_nondet_interface_1_C_49_0_H_1=638722033, hhv_nondet_interface_1_C_49_0_v_9_9=638722038]
[L0]  RET   call nondet_interface_1_C_49_0(hhv_nondet_call_10_0_E_0, hhv_nondet_call_10_0_J_1, hhv_nondet_call_10_0_A_2, hhv_nondet_call_10_0_B_3, hhv_nondet_call_10_0_C_4, hhv_nondet_call_10_0_D_5, hhv_nondet_call_10_0_H_6, hhv_nondet_call_10_0_F_7, hhv_nondet_call_10_0_I_8, hhv_nondet_call_10_0_G_9);
      VAL   [hhv_nondet_call_10_0_E_0=0, hhv_nondet_call_10_0_F_7=638722038, hhv_nondet_call_10_0_G_9=638722038, hhv_nondet_call_10_0_J_1=638722033]
[L0]  RET   call nondet_call_10_0(hbv_block_14_function_f__40_49_0_H_11, hhv_block_14_function_f__40_49_0_K1_1, hhv_block_14_function_f__40_49_0_A_2, hhv_block_14_function_f__40_49_0_B_3, hhv_block_14_function_f__40_49_0_C_4, hhv_block_14_function_f__40_49_0_D_5, hbv_block_14_function_f__40_49_0_G1_25, hbv_block_14_function_f__40_49_0_B1_17, hbv_block_14_function_f__40_49_0_H1_26, hbv_block_14_function_f__40_49_0_C1_8);
      VAL   [hbv_block_14_function_f__40_49_0_A1_5=0, hbv_block_14_function_f__40_49_0_B1_17=638722038, hbv_block_14_function_f__40_49_0_C1_8=638722038, hbv_block_14_function_f__40_49_0_D1_23=638722038, hbv_block_14_function_f__40_49_0_E_1=0, hbv_block_14_function_f__40_49_0_G_24=0, hbv_block_14_function_f__40_49_0_H_11=0, hbv_block_14_function_f__40_49_0_I_20=0, hbv_block_14_function_f__40_49_0_K_10=0, hhv_block_14_function_f__40_49_0_E1_24=638722038, hhv_block_14_function_f__40_49_0_F_25=638722038, hhv_block_14_function_f__40_49_0_K1_1=638722033, hhv_block_14_function_f__40_49_0_L1_6=7, hhv_block_14_function_f__40_49_0_L_0=2, hhv_block_14_function_f__40_49_0_M1_7=11, hhv_block_14_function_f__40_49_0_N1_8=6, hhv_block_14_function_f__40_49_0_O1_9=15, hhv_block_14_function_f__40_49_0_P1_10=9, hhv_block_14_function_f__40_49_0_Q1_11=13, hhv_block_14_function_f__40_49_0_R1_12=5, hhv_block_14_function_f__40_49_0_U1_15=4, hhv_block_14_function_f__40_49_0_V1_16=8, hhv_block_14_function_f__40_49_0_W1_17=638722032, hhv_block_14_function_f__40_49_0_X1_18=0, hhv_block_14_function_f__40_49_0_Y1_19=10, hhv_block_14_function_f__40_49_0_Z1_20=12, hhv_block_14_function_f__40_49_0_Z_22=0]
[L0]  RET   call block_14_function_f__40_49_0(hhv_summary_3_function_f__40_49_0_H_0, hhv_summary_3_function_f__40_49_0_U_1, hhv_summary_3_function_f__40_49_0_A_2, hhv_summary_3_function_f__40_49_0_B_3, hhv_summary_3_function_f__40_49_0_C_4, hhv_summary_3_function_f__40_49_0_D_5, hhv_summary_3_function_f__40_49_0_V_6, hhv_summary_3_function_f__40_49_0_W_7, hhv_summary_3_function_f__40_49_0_X_8, hhv_summary_3_function_f__40_49_0_Y_9, hhv_summary_3_function_f__40_49_0_Z_10, hhv_summary_3_function_f__40_49_0_A1_11, hhv_summary_3_function_f__40_49_0_B1_12, hhv_summary_3_function_f__40_49_0_C1_13, hhv_summary_3_function_f__40_49_0_D1_14, hhv_summary_3_function_f__40_49_0_E1_15, hhv_summary_3_function_f__40_49_0_F1_16, hhv_summary_3_function_f__40_49_0_G1_17, hhv_summary_3_function_f__40_49_0_H1_18, hhv_summary_3_function_f__40_49_0_I1_19, hhv_summary_3_function_f__40_49_0_J1_20, hhv_summary_3_function_f__40_49_0_R_21, hhv_summary_3_function_f__40_49_0_N_22, hhv_summary_3_function_f__40_49_0_T_23, hhv_summary_3_function_f__40_49_0_Q_24, hbv_summary_3_function_f__40_49_0_E_1);
      VAL   [hbv_summary_3_function_f__40_49_0_E_1=638722038, hhv_summary_3_function_f__40_49_0_A1_11=13, hhv_summary_3_function_f__40_49_0_B1_12=5, hhv_summary_3_function_f__40_49_0_E1_15=4, hhv_summary_3_function_f__40_49_0_F1_16=8, hhv_summary_3_function_f__40_49_0_G1_17=638722032, hhv_summary_3_function_f__40_49_0_H1_18=0, hhv_summary_3_function_f__40_49_0_H_0=2, hhv_summary_3_function_f__40_49_0_I1_19=10, hhv_summary_3_function_f__40_49_0_J1_20=12, hhv_summary_3_function_f__40_49_0_N_22=0, hhv_summary_3_function_f__40_49_0_Q_24=638722038, hhv_summary_3_function_f__40_49_0_U_1=638722033, hhv_summary_3_function_f__40_49_0_V_6=7, hhv_summary_3_function_f__40_49_0_W_7=11, hhv_summary_3_function_f__40_49_0_X_8=6, hhv_summary_3_function_f__40_49_0_Y_9=15, hhv_summary_3_function_f__40_49_0_Z_10=9]
[L0]  RET   call summary_3_function_f__40_49_0(hhv_summary_4_function_f__40_49_0_G_0, hhv_summary_4_function_f__40_49_0_P_1, hhv_summary_4_function_f__40_49_0_A_2, hhv_summary_4_function_f__40_49_0_B_3, hhv_summary_4_function_f__40_49_0_C_4, hhv_summary_4_function_f__40_49_0_D_5, hhv_summary_4_function_f__40_49_0_Q_6, hhv_summary_4_function_f__40_49_0_R_7, hhv_summary_4_function_f__40_49_0_S_8, hhv_summary_4_function_f__40_49_0_T_9, hhv_summary_4_function_f__40_49_0_U_10, hhv_summary_4_function_f__40_49_0_V_11, hhv_summary_4_function_f__40_49_0_W_12, hhv_summary_4_function_f__40_49_0_X_13, hhv_summary_4_function_f__40_49_0_Y_14, hhv_summary_4_function_f__40_49_0_Z_15, hhv_summary_4_function_f__40_49_0_A1_16, hhv_summary_4_function_f__40_49_0_B1_17, hhv_summary_4_function_f__40_49_0_C1_18, hhv_summary_4_function_f__40_49_0_D1_19, hhv_summary_4_function_f__40_49_0_E1_20, hbv_summary_4_function_f__40_49_0_N_4, hbv_summary_4_function_f__40_49_0_J_5, hhv_summary_4_function_f__40_49_0_O_23, hhv_summary_4_function_f__40_49_0_K_24);
      VAL   [hbv_summary_4_function_f__40_49_0_E_6=638722036, hbv_summary_4_function_f__40_49_0_F_3=0, hbv_summary_4_function_f__40_49_0_J_5=0, hhv_summary_4_function_f__40_49_0_A1_16=8, hhv_summary_4_function_f__40_49_0_B1_17=638722032, hhv_summary_4_function_f__40_49_0_C1_18=0, hhv_summary_4_function_f__40_49_0_D1_19=10, hhv_summary_4_function_f__40_49_0_E1_20=12, hhv_summary_4_function_f__40_49_0_G_0=2, hhv_summary_4_function_f__40_49_0_I_22=0, hhv_summary_4_function_f__40_49_0_K_24=638722038, hhv_summary_4_function_f__40_49_0_P_1=638722033, hhv_summary_4_function_f__40_49_0_Q_6=7, hhv_summary_4_function_f__40_49_0_R_7=11, hhv_summary_4_function_f__40_49_0_S_8=6, hhv_summary_4_function_f__40_49_0_T_9=15, hhv_summary_4_function_f__40_49_0_U_10=9, hhv_summary_4_function_f__40_49_0_V_11=13, hhv_summary_4_function_f__40_49_0_W_12=5, hhv_summary_4_function_f__40_49_0_Z_15=4]
[L0]  RET   call summary_4_function_f__40_49_0(hbv_error_target_6_0_E_1, hbv_error_target_6_0_J_2, hbv_error_target_6_0_A_3, hbv_error_target_6_0_B_4, hbv_error_target_6_0_C_5, hbv_error_target_6_0_D_6, hbv_error_target_6_0_K_9, hbv_error_target_6_0_L_10, hbv_error_target_6_0_M_11, hbv_error_target_6_0_N_12, hbv_error_target_6_0_O_13, hbv_error_target_6_0_P_14, hbv_error_target_6_0_Q_15, hbv_error_target_6_0_R_16, hbv_error_target_6_0_S_17, hbv_error_target_6_0_T_18, hbv_error_target_6_0_U_19, hbv_error_target_6_0_V_20, hbv_error_target_6_0_W_21, hbv_error_target_6_0_X_22, hbv_error_target_6_0_Y_23, hbv_error_target_6_0_H_7, hbv_error_target_6_0_F_8, hbv_error_target_6_0_I_24, hbv_error_target_6_0_G_25);
      VAL   [hbv_error_target_6_0_E_1=2, hbv_error_target_6_0_F_8=0, hbv_error_target_6_0_G_25=638722038, hbv_error_target_6_0_J_2=638722033, hbv_error_target_6_0_K_9=7, hbv_error_target_6_0_L_10=11, hbv_error_target_6_0_M_11=6, hbv_error_target_6_0_N_12=15, hbv_error_target_6_0_O_13=9, hbv_error_target_6_0_P_14=13, hbv_error_target_6_0_Q_15=5, hbv_error_target_6_0_T_18=4, hbv_error_target_6_0_U_19=8, hbv_error_target_6_0_V_20=638722032, hbv_error_target_6_0_W_21=0, hbv_error_target_6_0_X_22=10, hbv_error_target_6_0_Y_23=12]
[L0]  RET   call error_target_6_0();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 27 procedures, 121 locations, 210 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.3s, OverallIterations: 9, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.7s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 64 SdHoareTripleChecker+Valid, 0.5s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 10 mSDsluCounter, 6173 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 5001 mSDsCounter, 15 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 504 IncrementalHoareTripleChecker+Invalid, 519 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 15 mSolverCounterUnsat, 1172 mSDtfsCounter, 504 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 186 GetRequests, 145 SyntacticMatches, 4 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=131occurred in iteration=6, InterpolantAutomatonStates: 50, 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, 8 MinimizatonAttempts, 18 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 1.4s InterpolantComputationTime, 696 NumberOfCodeBlocks, 696 NumberOfCodeBlocksAsserted, 10 NumberOfCheckSat, 683 ConstructedInterpolants, 0 QuantifiedInterpolants, 887 SizeOfPredicates, 0 NumberOfNonLiveVariables, 735 ConjunctsInSsa, 6 ConjunctsInUnsatCore, 10 InterpolantComputations, 7 PerfectInterpolantSequences, 51/57 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:55,947 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
