./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_9.sol_3_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:40,431 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:40,481 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_930f9843-b5c3-42fa-b45e-4de90dd0dce7/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:40,485 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:40,485 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:40,502 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:40,503 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:40,503 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:40,503 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:40,503 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:40,503 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:40,503 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:40,504 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:40,504 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:40,504 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:40,504 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:40,504 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:40,504 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:40,504 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:40,504 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:40,504 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:40,505 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:40,505 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:40,505 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:40,505 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:40,505 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:40,506 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:40,709 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:40,717 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:40,719 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:40,720 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:40,720 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:40,721 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_930f9843-b5c3-42fa-b45e-4de90dd0dce7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_9.sol_3_no_adts_000.smt2
[2025-05-07 17:26:40,722 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:40,724 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:41,092 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_930f9843-b5c3-42fa-b45e-4de90dd0dce7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_9.sol_3_no_adts_000.smt2
[2025-05-07 17:26:41,094 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:41,095 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:41,096 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:41,096 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:41,096 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:41,098 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,136 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41 Unit
[2025-05-07 17:26:41,137 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:41,137 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:41,137 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:41,137 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:41,148 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,148 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,180 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,180 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,190 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,192 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,194 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,198 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,201 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,217 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:41,218 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:41,218 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:41,218 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:41,218 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (1/1) ...
[2025-05-07 17:26:41,220 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:41,229 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:41,239 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:26:41,241 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:26:41,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:41,252 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:41,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:41,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_11_0 given in one single declaration
[2025-05-07 17:26:41,252 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_11_0
[2025-05-07 17:26:41,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_11_0
[2025-05-07 17:26:41,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_A_30_0 given in one single declaration
[2025-05-07 17:26:41,252 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_A_30_0
[2025-05-07 17:26:41,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_A_30_0
[2025-05-07 17:26:41,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_A_30_0 given in one single declaration
[2025-05-07 17:26:41,252 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_A_30_0
[2025-05-07 17:26:41,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_A_30_0
[2025-05-07 17:26:41,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_36_A_30_0 given in one single declaration
[2025-05-07 17:26:41,253 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_36_A_30_0
[2025-05-07 17:26:41,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_36_A_30_0
[2025-05-07 17:26:41,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_33_A_30_0 given in one single declaration
[2025-05-07 17:26:41,253 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_33_A_30_0
[2025-05-07 17:26:41,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_33_A_30_0
[2025-05-07 17:26:41,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_35_A_30_0 given in one single declaration
[2025-05-07 17:26:41,253 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_35_A_30_0
[2025-05-07 17:26:41,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_35_A_30_0
[2025-05-07 17:26:41,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_34_A_30_0 given in one single declaration
[2025-05-07 17:26:41,253 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_34_A_30_0
[2025-05-07 17:26:41,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_34_A_30_0
[2025-05-07 17:26:41,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_29_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_29_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_29_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_return_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_return_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_return_function_f__21_30_0
[2025-05-07 17:26:41,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_26_function_v__29_30_0 given in one single declaration
[2025-05-07 17:26:41,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_26_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_26_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_v__29_30_0 given in one single declaration
[2025-05-07 17:26:41,255 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_return_function_v__29_30_0 given in one single declaration
[2025-05-07 17:26:41,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_return_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_return_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_31_v_28_30_0 given in one single declaration
[2025-05-07 17:26:41,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_31_v_28_30_0
[2025-05-07 17:26:41,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_31_v_28_30_0
[2025-05-07 17:26:41,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_v__29_30_0 given in one single declaration
[2025-05-07 17:26:41,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_v__29_30_0
[2025-05-07 17:26:41,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_f_20_30_0 given in one single declaration
[2025-05-07 17:26:41,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_f_20_30_0
[2025-05-07 17:26:41,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_f_20_30_0
[2025-05-07 17:26:41,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,256 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_function_f__21_30_0
[2025-05-07 17:26:41,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_function_f__21_30_0
[2025-05-07 17:26:41,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_27_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,256 INFO  L130     BoogieDeclarations]: Found specification of procedure block_27_function_f__21_30_0
[2025-05-07 17:26:41,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_27_function_f__21_30_0
[2025-05-07 17:26:41,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_28_function_f__21_30_0 given in one single declaration
[2025-05-07 17:26:41,256 INFO  L130     BoogieDeclarations]: Found specification of procedure block_28_function_f__21_30_0
[2025-05-07 17:26:41,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_28_function_f__21_30_0
[2025-05-07 17:26:41,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_12_function_f__42_43_0 given in one single declaration
[2025-05-07 17:26:41,256 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_12_function_f__42_43_0
[2025-05-07 17:26:41,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_12_function_f__42_43_0
[2025-05-07 17:26:41,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_f__42_43_0 given in one single declaration
[2025-05-07 17:26:41,256 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_f__42_43_0
[2025-05-07 17:26:41,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_f__42_43_0
[2025-05-07 17:26:41,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_return_function_f__42_43_0 given in one single declaration
[2025-05-07 17:26:41,257 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_return_function_f__42_43_0
[2025-05-07 17:26:41,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_return_function_f__42_43_0
[2025-05-07 17:26:41,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_49_function_f__21_43_0 given in one single declaration
[2025-05-07 17:26:41,257 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_49_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_49_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_f__21_43_0 given in one single declaration
[2025-05-07 17:26:41,257 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_function_f__21_43_0 given in one single declaration
[2025-05-07 17:26:41,257 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_return_function_f__21_43_0 given in one single declaration
[2025-05-07 17:26:41,257 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_return_function_f__21_43_0
[2025-05-07 17:26:41,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_return_function_f__21_43_0
[2025-05-07 17:26:41,258 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_40_function_v__29_43_0 given in one single declaration
[2025-05-07 17:26:41,258 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_40_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_40_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_v__29_43_0 given in one single declaration
[2025-05-07 17:26:41,258 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_return_function_v__29_43_0 given in one single declaration
[2025-05-07 17:26:41,258 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_return_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_return_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_v_28_43_0 given in one single declaration
[2025-05-07 17:26:41,258 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_v_28_43_0
[2025-05-07 17:26:41,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_v_28_43_0
[2025-05-07 17:26:41,258 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_function_v__29_43_0 given in one single declaration
[2025-05-07 17:26:41,258 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_function_v__29_43_0
[2025-05-07 17:26:41,258 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_f_20_43_0 given in one single declaration
[2025-05-07 17:26:41,258 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_f_20_43_0
[2025-05-07 17:26:41,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_f_20_43_0
[2025-05-07 17:26:41,259 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_function_f__21_43_0 given in one single declaration
[2025-05-07 17:26:41,259 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_function_f__21_43_0
[2025-05-07 17:26:41,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_function_f__21_43_0
[2025-05-07 17:26:41,259 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_function_f__21_43_0 given in one single declaration
[2025-05-07 17:26:41,259 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_function_f__21_43_0
[2025-05-07 17:26:41,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_function_f__21_43_0
[2025-05-07 17:26:41,259 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_f_41_43_0 given in one single declaration
[2025-05-07 17:26:41,259 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_f_41_43_0
[2025-05-07 17:26:41,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_f_41_43_0
[2025-05-07 17:26:41,259 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_function_f__42_43_0 given in one single declaration
[2025-05-07 17:26:41,259 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_function_f__42_43_0
[2025-05-07 17:26:41,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_function_f__42_43_0
[2025-05-07 17:26:41,259 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_function_f__42_43_0 given in one single declaration
[2025-05-07 17:26:41,259 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_function_f__42_43_0
[2025-05-07 17:26:41,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_function_f__42_43_0
[2025-05-07 17:26:41,259 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_6_B_43_0 given in one single declaration
[2025-05-07 17:26:41,260 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_6_B_43_0
[2025-05-07 17:26:41,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_6_B_43_0
[2025-05-07 17:26:41,260 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_8_B_43_0 given in one single declaration
[2025-05-07 17:26:41,260 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_8_B_43_0
[2025-05-07 17:26:41,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_8_B_43_0
[2025-05-07 17:26:41,260 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_51_B_43_0 given in one single declaration
[2025-05-07 17:26:41,260 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_51_B_43_0
[2025-05-07 17:26:41,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_51_B_43_0
[2025-05-07 17:26:41,260 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_53_B_43_0 given in one single declaration
[2025-05-07 17:26:41,260 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_53_B_43_0
[2025-05-07 17:26:41,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_53_B_43_0
[2025-05-07 17:26:41,260 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_52_B_43_0 given in one single declaration
[2025-05-07 17:26:41,260 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_52_B_43_0
[2025-05-07 17:26:41,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_52_B_43_0
[2025-05-07 17:26:41,260 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_57_B_43_0 given in one single declaration
[2025-05-07 17:26:41,260 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_57_B_43_0
[2025-05-07 17:26:41,261 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_57_B_43_0
[2025-05-07 17:26:41,261 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_54_A_30_0 given in one single declaration
[2025-05-07 17:26:41,261 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_54_A_30_0
[2025-05-07 17:26:41,261 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_54_A_30_0
[2025-05-07 17:26:41,261 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_56_A_30_0 given in one single declaration
[2025-05-07 17:26:41,261 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_56_A_30_0
[2025-05-07 17:26:41,261 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_56_A_30_0
[2025-05-07 17:26:41,261 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_55_A_30_0 given in one single declaration
[2025-05-07 17:26:41,261 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_55_A_30_0
[2025-05-07 17:26:41,261 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_55_A_30_0
[2025-05-07 17:26:41,261 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_f__42_66_0 given in one single declaration
[2025-05-07 17:26:41,261 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_f__42_66_0
[2025-05-07 17:26:41,261 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_f__42_66_0
[2025-05-07 17:26:41,261 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_71_function_f__42_66_0 given in one single declaration
[2025-05-07 17:26:41,261 INFO  L130     BoogieDeclarations]: Found specification of procedure block_71_function_f__42_66_0
[2025-05-07 17:26:41,261 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_71_function_f__42_66_0
[2025-05-07 17:26:41,261 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_f__42_66_0 given in one single declaration
[2025-05-07 17:26:41,262 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_f__42_66_0
[2025-05-07 17:26:41,262 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_f__42_66_0
[2025-05-07 17:26:41,262 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_f_41_66_0 given in one single declaration
[2025-05-07 17:26:41,262 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_f_41_66_0
[2025-05-07 17:26:41,262 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_f_41_66_0
[2025-05-07 17:26:41,262 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_function_f__42_66_0 given in one single declaration
[2025-05-07 17:26:41,262 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_function_f__42_66_0
[2025-05-07 17:26:41,262 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_function_f__42_66_0
[2025-05-07 17:26:41,262 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_70_function_f__21_66_0 given in one single declaration
[2025-05-07 17:26:41,262 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_70_function_f__21_66_0
[2025-05-07 17:26:41,262 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_70_function_f__21_66_0
[2025-05-07 17:26:41,262 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_16_function_f__21_66_0 given in one single declaration
[2025-05-07 17:26:41,262 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_16_function_f__21_66_0
[2025-05-07 17:26:41,262 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_16_function_f__21_66_0
[2025-05-07 17:26:41,262 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_63_function_f__21_66_0 given in one single declaration
[2025-05-07 17:26:41,262 INFO  L130     BoogieDeclarations]: Found specification of procedure block_63_function_f__21_66_0
[2025-05-07 17:26:41,262 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_63_function_f__21_66_0
[2025-05-07 17:26:41,262 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_61_function_v__65_66_0 given in one single declaration
[2025-05-07 17:26:41,263 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_61_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_61_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_function_v__65_66_0 given in one single declaration
[2025-05-07 17:26:41,263 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_79_return_function_v__65_66_0 given in one single declaration
[2025-05-07 17:26:41,263 INFO  L130     BoogieDeclarations]: Found specification of procedure block_79_return_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_79_return_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_78_v_64_66_0 given in one single declaration
[2025-05-07 17:26:41,263 INFO  L130     BoogieDeclarations]: Found specification of procedure block_78_v_64_66_0
[2025-05-07 17:26:41,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_78_v_64_66_0
[2025-05-07 17:26:41,263 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_77_function_v__65_66_0 given in one single declaration
[2025-05-07 17:26:41,263 INFO  L130     BoogieDeclarations]: Found specification of procedure block_77_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_77_function_v__65_66_0
[2025-05-07 17:26:41,263 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_59_f_20_66_0 given in one single declaration
[2025-05-07 17:26:41,263 INFO  L130     BoogieDeclarations]: Found specification of procedure block_59_f_20_66_0
[2025-05-07 17:26:41,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_59_f_20_66_0
[2025-05-07 17:26:41,263 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_58_function_f__21_66_0 given in one single declaration
[2025-05-07 17:26:41,264 INFO  L130     BoogieDeclarations]: Found specification of procedure block_58_function_f__21_66_0
[2025-05-07 17:26:41,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_58_function_f__21_66_0
[2025-05-07 17:26:41,264 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_62_function_f__21_66_0 given in one single declaration
[2025-05-07 17:26:41,264 INFO  L130     BoogieDeclarations]: Found specification of procedure block_62_function_f__21_66_0
[2025-05-07 17:26:41,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_62_function_f__21_66_0
[2025-05-07 17:26:41,264 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_60_return_function_f__21_66_0 given in one single declaration
[2025-05-07 17:26:41,264 INFO  L130     BoogieDeclarations]: Found specification of procedure block_60_return_function_f__21_66_0
[2025-05-07 17:26:41,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_60_return_function_f__21_66_0
[2025-05-07 17:26:41,264 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_return_function_f__42_66_0 given in one single declaration
[2025-05-07 17:26:41,264 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_return_function_f__42_66_0
[2025-05-07 17:26:41,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_return_function_f__42_66_0
[2025-05-07 17:26:41,264 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_13_C_66_0 given in one single declaration
[2025-05-07 17:26:41,264 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_13_C_66_0
[2025-05-07 17:26:41,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_13_C_66_0
[2025-05-07 17:26:41,264 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_15_C_66_0 given in one single declaration
[2025-05-07 17:26:41,264 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_15_C_66_0
[2025-05-07 17:26:41,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_15_C_66_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_83_B_43_0 given in one single declaration
[2025-05-07 17:26:41,265 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_83_B_43_0
[2025-05-07 17:26:41,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_83_B_43_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_85_B_43_0 given in one single declaration
[2025-05-07 17:26:41,265 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_85_B_43_0
[2025-05-07 17:26:41,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_85_B_43_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_84_B_43_0 given in one single declaration
[2025-05-07 17:26:41,265 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_84_B_43_0
[2025-05-07 17:26:41,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_84_B_43_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_80_C_66_0 given in one single declaration
[2025-05-07 17:26:41,265 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_80_C_66_0
[2025-05-07 17:26:41,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_80_C_66_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_82_C_66_0 given in one single declaration
[2025-05-07 17:26:41,265 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_82_C_66_0
[2025-05-07 17:26:41,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_82_C_66_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_81_C_66_0 given in one single declaration
[2025-05-07 17:26:41,265 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_81_C_66_0
[2025-05-07 17:26:41,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_81_C_66_0
[2025-05-07 17:26:41,265 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_86_A_30_0 given in one single declaration
[2025-05-07 17:26:41,266 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_86_A_30_0
[2025-05-07 17:26:41,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_86_A_30_0
[2025-05-07 17:26:41,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_88_A_30_0 given in one single declaration
[2025-05-07 17:26:41,266 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_88_A_30_0
[2025-05-07 17:26:41,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_88_A_30_0
[2025-05-07 17:26:41,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_87_A_30_0 given in one single declaration
[2025-05-07 17:26:41,266 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_87_A_30_0
[2025-05-07 17:26:41,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_87_A_30_0
[2025-05-07 17:26:41,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_89_C_66_0 given in one single declaration
[2025-05-07 17:26:41,266 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_89_C_66_0
[2025-05-07 17:26:41,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_89_C_66_0
[2025-05-07 17:26:41,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_function_g__56_66_0 given in one single declaration
[2025-05-07 17:26:41,266 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_function_g__56_66_0
[2025-05-07 17:26:41,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_function_g__56_66_0
[2025-05-07 17:26:41,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_g__56_66_0 given in one single declaration
[2025-05-07 17:26:41,266 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_g__56_66_0
[2025-05-07 17:26:41,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_g__56_66_0
[2025-05-07 17:26:41,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_74_return_function_g__56_66_0 given in one single declaration
[2025-05-07 17:26:41,267 INFO  L130     BoogieDeclarations]: Found specification of procedure block_74_return_function_g__56_66_0
[2025-05-07 17:26:41,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_74_return_function_g__56_66_0
[2025-05-07 17:26:41,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_75_function_f__42_66_0 given in one single declaration
[2025-05-07 17:26:41,267 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_75_function_f__42_66_0
[2025-05-07 17:26:41,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_75_function_f__42_66_0
[2025-05-07 17:26:41,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_73_g_55_66_0 given in one single declaration
[2025-05-07 17:26:41,267 INFO  L130     BoogieDeclarations]: Found specification of procedure block_73_g_55_66_0
[2025-05-07 17:26:41,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_73_g_55_66_0
[2025-05-07 17:26:41,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_72_function_g__56_66_0 given in one single declaration
[2025-05-07 17:26:41,267 INFO  L130     BoogieDeclarations]: Found specification of procedure block_72_function_g__56_66_0
[2025-05-07 17:26:41,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_72_function_g__56_66_0
[2025-05-07 17:26:41,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_76_function_g__56_66_0 given in one single declaration
[2025-05-07 17:26:41,267 INFO  L130     BoogieDeclarations]: Found specification of procedure block_76_function_g__56_66_0
[2025-05-07 17:26:41,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_76_function_g__56_66_0
[2025-05-07 17:26:41,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:41,267 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:41,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:26:41,590 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:26:41,592 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:26:42,106 INFO  L?                        ?]: Removed 677 outVars from TransFormulas that were not future-live.
[2025-05-07 17:26:42,106 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:26:42,118 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:26:42,118 INFO  L312             CfgBuilder]: Removed 47 assume(true) statements.
[2025-05-07 17:26:42,119 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:42 BoogieIcfgContainer
[2025-05-07 17:26:42,119 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:26:42,120 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:26:42,120 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:26:42,123 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:26:42,123 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:41" (1/3) ...
[2025-05-07 17:26:42,123 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7deebcb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:26:42, skipping insertion in model container
[2025-05-07 17:26:42,123 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:41" (2/3) ...
[2025-05-07 17:26:42,123 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7deebcb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:26:42, skipping insertion in model container
[2025-05-07 17:26:42,123 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:42" (3/3) ...
[2025-05-07 17:26:42,124 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:26:42,134 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:26:42,136 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 86 procedures, 347 locations, 556 edges, 86 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:26:42,167 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:26:42,175 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;@7dba9573, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:26:42,175 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:26:42,178 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 347 states, 137 states have (on average 1.102189781021898) internal successors, (151), 151 states have internal predecessors, (151), 129 states have call successors, (135), 85 states have call predecessors, (135), 85 states have return successors, (135), 110 states have call predecessors, (135), 129 states have call successors, (135)
[2025-05-07 17:26:42,189 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 80
[2025-05-07 17:26:42,190 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:42,190 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, 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:26:42,190 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:42,194 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:42,194 INFO  L85        PathProgramCache]: Analyzing trace with hash 525012972, now seen corresponding path program 1 times
[2025-05-07 17:26:42,199 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:42,199 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1788955337]
[2025-05-07 17:26:42,199 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:42,199 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:42,249 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 79 statements into 1 equivalence classes.
[2025-05-07 17:26:42,267 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 79 of 79 statements.
[2025-05-07 17:26:42,267 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:42,268 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:42,478 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:26:42,479 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:42,479 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1788955337]
[2025-05-07 17:26:42,479 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1788955337] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:42,479 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:42,481 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:42,482 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1715386327]
[2025-05-07 17:26:42,483 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:42,485 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:42,486 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:42,519 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:42,520 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:42,523 INFO  L87              Difference]: Start difference. First operand  has 347 states, 137 states have (on average 1.102189781021898) internal successors, (151), 151 states have internal predecessors, (151), 129 states have call successors, (135), 85 states have call predecessors, (135), 85 states have return successors, (135), 110 states have call predecessors, (135), 129 states have call successors, (135) Second operand  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:26:42,586 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:42,586 INFO  L93              Difference]: Finished difference Result 349 states and 423 transitions.
[2025-05-07 17:26:42,587 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:42,589 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22) Word has length 79
[2025-05-07 17:26:42,589 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:42,597 INFO  L225             Difference]: With dead ends: 349
[2025-05-07 17:26:42,597 INFO  L226             Difference]: Without dead ends: 342
[2025-05-07 17:26:42,599 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:26:42,601 INFO  L437           NwaCegarLoop]: 419 mSDtfsCounter, 1 mSDsluCounter, 827 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1246 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:42,601 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1246 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:42,611 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 342 states.
[2025-05-07 17:26:42,638 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 342 to 340.
[2025-05-07 17:26:42,639 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 340 states, 136 states have (on average 1.0808823529411764) internal successors, (147), 147 states have internal predecessors, (147), 124 states have call successors, (130), 85 states have call predecessors, (130), 85 states have return successors, (130), 107 states have call predecessors, (130), 124 states have call successors, (130)
[2025-05-07 17:26:42,645 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 340 states to 340 states and 407 transitions.
[2025-05-07 17:26:42,646 INFO  L79                 Accepts]: Start accepts. Automaton has 340 states and 407 transitions. Word has length 79
[2025-05-07 17:26:42,646 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:42,646 INFO  L485      AbstractCegarLoop]: Abstraction has 340 states and 407 transitions.
[2025-05-07 17:26:42,647 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:26:42,647 INFO  L278                IsEmpty]: Start isEmpty. Operand 340 states and 407 transitions.
[2025-05-07 17:26:42,649 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:26:42,649 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:42,649 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:42,650 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:26:42,650 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:42,650 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:42,650 INFO  L85        PathProgramCache]: Analyzing trace with hash -1761368969, now seen corresponding path program 1 times
[2025-05-07 17:26:42,650 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:42,650 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [157838074]
[2025-05-07 17:26:42,650 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:42,650 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:42,682 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:26:42,707 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:26:42,707 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:42,707 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:42,849 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:26:42,849 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:42,849 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [157838074]
[2025-05-07 17:26:42,849 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [157838074] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:42,849 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:42,849 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:26:42,849 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1014149207]
[2025-05-07 17:26:42,850 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:42,850 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:26:42,851 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:42,851 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:26:42,851 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:42,851 INFO  L87              Difference]: Start difference. First operand 340 states and 407 transitions. Second operand  has 7 states, 6 states have (on average 4.833333333333333) internal successors, (29), 7 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 7 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:26:42,940 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:42,940 INFO  L93              Difference]: Finished difference Result 340 states and 406 transitions.
[2025-05-07 17:26:42,940 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:26:42,940 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 4.833333333333333) internal successors, (29), 7 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 7 states have call predecessors, (18), 4 states have call successors, (18) Word has length 65
[2025-05-07 17:26:42,940 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:42,942 INFO  L225             Difference]: With dead ends: 340
[2025-05-07 17:26:42,942 INFO  L226             Difference]: Without dead ends: 338
[2025-05-07 17:26:42,942 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:42,943 INFO  L437           NwaCegarLoop]: 400 mSDtfsCounter, 0 mSDsluCounter, 1984 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2384 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:42,943 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2384 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:42,944 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 338 states.
[2025-05-07 17:26:42,956 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 338 to 338.
[2025-05-07 17:26:42,956 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 338 states, 135 states have (on average 1.0814814814814815) internal successors, (146), 146 states have internal predecessors, (146), 122 states have call successors, (128), 85 states have call predecessors, (128), 85 states have return successors, (128), 106 states have call predecessors, (128), 122 states have call successors, (128)
[2025-05-07 17:26:42,958 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 338 states to 338 states and 402 transitions.
[2025-05-07 17:26:42,958 INFO  L79                 Accepts]: Start accepts. Automaton has 338 states and 402 transitions. Word has length 65
[2025-05-07 17:26:42,958 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:42,958 INFO  L485      AbstractCegarLoop]: Abstraction has 338 states and 402 transitions.
[2025-05-07 17:26:42,958 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 4.833333333333333) internal successors, (29), 7 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 7 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:26:42,958 INFO  L278                IsEmpty]: Start isEmpty. Operand 338 states and 402 transitions.
[2025-05-07 17:26:42,960 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 80
[2025-05-07 17:26:42,960 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:42,960 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, 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:26:42,961 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:26:42,961 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:42,961 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:42,961 INFO  L85        PathProgramCache]: Analyzing trace with hash -120766197, now seen corresponding path program 1 times
[2025-05-07 17:26:42,961 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:42,961 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [631679859]
[2025-05-07 17:26:42,961 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:42,961 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:42,995 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 79 statements into 1 equivalence classes.
[2025-05-07 17:26:43,012 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 79 of 79 statements.
[2025-05-07 17:26:43,012 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:43,012 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:43,108 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:26:43,108 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:43,109 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [631679859]
[2025-05-07 17:26:43,109 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [631679859] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:43,109 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:43,109 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:43,109 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1329328287]
[2025-05-07 17:26:43,109 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:43,109 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:43,109 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:43,110 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:43,110 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:43,110 INFO  L87              Difference]: Start difference. First operand 338 states and 402 transitions. Second operand  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 3 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 3 states have call successors, (22)
[2025-05-07 17:26:43,126 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:43,126 INFO  L93              Difference]: Finished difference Result 342 states and 408 transitions.
[2025-05-07 17:26:43,127 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:43,127 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 3 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 3 states have call successors, (22) Word has length 79
[2025-05-07 17:26:43,127 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:43,128 INFO  L225             Difference]: With dead ends: 342
[2025-05-07 17:26:43,128 INFO  L226             Difference]: Without dead ends: 331
[2025-05-07 17:26:43,129 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:26:43,129 INFO  L437           NwaCegarLoop]: 402 mSDtfsCounter, 1 mSDsluCounter, 788 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1190 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:26:43,129 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1190 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:43,130 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 331 states.
[2025-05-07 17:26:43,138 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 331 to 329.
[2025-05-07 17:26:43,139 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 329 states, 135 states have (on average 1.0592592592592593) internal successors, (143), 143 states have internal predecessors, (143), 113 states have call successors, (119), 85 states have call predecessors, (119), 85 states have return successors, (119), 100 states have call predecessors, (119), 113 states have call successors, (119)
[2025-05-07 17:26:43,140 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 329 states to 329 states and 381 transitions.
[2025-05-07 17:26:43,140 INFO  L79                 Accepts]: Start accepts. Automaton has 329 states and 381 transitions. Word has length 79
[2025-05-07 17:26:43,140 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:43,140 INFO  L485      AbstractCegarLoop]: Abstraction has 329 states and 381 transitions.
[2025-05-07 17:26:43,141 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 3 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 3 states have call successors, (22)
[2025-05-07 17:26:43,141 INFO  L278                IsEmpty]: Start isEmpty. Operand 329 states and 381 transitions.
[2025-05-07 17:26:43,142 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:26:43,142 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:43,142 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:43,142 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:26:43,142 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:43,142 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:43,143 INFO  L85        PathProgramCache]: Analyzing trace with hash 922846356, now seen corresponding path program 1 times
[2025-05-07 17:26:43,143 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:43,143 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [61016312]
[2025-05-07 17:26:43,143 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:43,143 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:43,179 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:26:43,185 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:26:43,185 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:43,185 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:43,346 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:26:43,346 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:43,347 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [61016312]
[2025-05-07 17:26:43,347 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [61016312] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:43,347 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:43,347 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:43,347 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1302596063]
[2025-05-07 17:26:43,347 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:43,347 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:43,347 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:43,348 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:43,348 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:43,348 INFO  L87              Difference]: Start difference. First operand 329 states and 381 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:26:43,394 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:43,394 INFO  L93              Difference]: Finished difference Result 326 states and 376 transitions.
[2025-05-07 17:26:43,394 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:43,394 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 4 states have call successors, (19) Word has length 68
[2025-05-07 17:26:43,395 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:43,396 INFO  L225             Difference]: With dead ends: 326
[2025-05-07 17:26:43,396 INFO  L226             Difference]: Without dead ends: 324
[2025-05-07 17:26:43,396 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:26:43,396 INFO  L437           NwaCegarLoop]: 372 mSDtfsCounter, 0 mSDsluCounter, 1476 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1848 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:43,397 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1848 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:43,397 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 324 states.
[2025-05-07 17:26:43,404 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 324 to 324.
[2025-05-07 17:26:43,404 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 324 states, 133 states have (on average 1.0601503759398496) internal successors, (141), 141 states have internal predecessors, (141), 111 states have call successors, (116), 84 states have call predecessors, (116), 84 states have return successors, (116), 98 states have call predecessors, (116), 111 states have call successors, (116)
[2025-05-07 17:26:43,406 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 324 states to 324 states and 373 transitions.
[2025-05-07 17:26:43,406 INFO  L79                 Accepts]: Start accepts. Automaton has 324 states and 373 transitions. Word has length 68
[2025-05-07 17:26:43,406 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:43,407 INFO  L485      AbstractCegarLoop]: Abstraction has 324 states and 373 transitions.
[2025-05-07 17:26:43,407 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:26:43,407 INFO  L278                IsEmpty]: Start isEmpty. Operand 324 states and 373 transitions.
[2025-05-07 17:26:43,408 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:26:43,408 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:43,408 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:43,408 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:26:43,408 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:43,408 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:43,409 INFO  L85        PathProgramCache]: Analyzing trace with hash -1146107272, now seen corresponding path program 1 times
[2025-05-07 17:26:43,409 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:43,409 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [952332950]
[2025-05-07 17:26:43,409 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:43,409 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:43,432 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:26:43,442 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:26:43,442 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:43,442 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:43,561 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:26:43,561 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:43,561 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [952332950]
[2025-05-07 17:26:43,561 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [952332950] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:43,561 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:43,561 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:43,561 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1471532106]
[2025-05-07 17:26:43,561 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:43,562 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:43,562 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:43,562 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:43,563 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:43,563 INFO  L87              Difference]: Start difference. First operand 324 states and 373 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 5 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 5 states have call successors, (19)
[2025-05-07 17:26:43,601 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:43,601 INFO  L93              Difference]: Finished difference Result 329 states and 379 transitions.
[2025-05-07 17:26:43,601 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:43,602 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 5 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 5 states have call successors, (19) Word has length 68
[2025-05-07 17:26:43,602 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:43,603 INFO  L225             Difference]: With dead ends: 329
[2025-05-07 17:26:43,603 INFO  L226             Difference]: Without dead ends: 329
[2025-05-07 17:26:43,603 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:26:43,604 INFO  L437           NwaCegarLoop]: 370 mSDtfsCounter, 1 mSDsluCounter, 1460 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1830 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:43,604 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1830 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:43,604 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 329 states.
[2025-05-07 17:26:43,611 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 329 to 329.
[2025-05-07 17:26:43,611 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 329 states, 135 states have (on average 1.0592592592592593) internal successors, (143), 143 states have internal predecessors, (143), 112 states have call successors, (117), 84 states have call predecessors, (117), 86 states have return successors, (119), 101 states have call predecessors, (119), 112 states have call successors, (119)
[2025-05-07 17:26:43,612 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 329 states to 329 states and 379 transitions.
[2025-05-07 17:26:43,613 INFO  L79                 Accepts]: Start accepts. Automaton has 329 states and 379 transitions. Word has length 68
[2025-05-07 17:26:43,613 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:43,613 INFO  L485      AbstractCegarLoop]: Abstraction has 329 states and 379 transitions.
[2025-05-07 17:26:43,613 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 5 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 5 states have call successors, (19)
[2025-05-07 17:26:43,613 INFO  L278                IsEmpty]: Start isEmpty. Operand 329 states and 379 transitions.
[2025-05-07 17:26:43,614 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:26:43,614 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:43,614 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:43,614 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:26:43,614 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:43,615 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:43,615 INFO  L85        PathProgramCache]: Analyzing trace with hash 104309720, now seen corresponding path program 1 times
[2025-05-07 17:26:43,615 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:43,615 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [206419158]
[2025-05-07 17:26:43,615 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:43,615 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:43,639 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:26:43,649 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:26:43,649 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:43,649 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:43,726 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:26:43,726 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:43,726 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [206419158]
[2025-05-07 17:26:43,726 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [206419158] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:43,726 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:43,727 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:43,727 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [404785195]
[2025-05-07 17:26:43,727 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:43,727 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:43,727 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:43,728 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:43,728 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:43,728 INFO  L87              Difference]: Start difference. First operand 329 states and 379 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 5 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 5 states have call successors, (19)
[2025-05-07 17:26:43,756 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:43,756 INFO  L93              Difference]: Finished difference Result 303 states and 345 transitions.
[2025-05-07 17:26:43,757 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:43,757 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 5 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 5 states have call successors, (19) Word has length 68
[2025-05-07 17:26:43,757 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:43,758 INFO  L225             Difference]: With dead ends: 303
[2025-05-07 17:26:43,758 INFO  L226             Difference]: Without dead ends: 255
[2025-05-07 17:26:43,758 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:26:43,758 INFO  L437           NwaCegarLoop]: 340 mSDtfsCounter, 1 mSDsluCounter, 1341 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1681 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:43,759 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1681 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:43,759 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 255 states.
[2025-05-07 17:26:43,763 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 255 to 255.
[2025-05-07 17:26:43,764 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 255 states, 105 states have (on average 1.0476190476190477) internal successors, (110), 110 states have internal predecessors, (110), 88 states have call successors, (92), 66 states have call predecessors, (92), 66 states have return successors, (92), 78 states have call predecessors, (92), 88 states have call successors, (92)
[2025-05-07 17:26:43,765 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 255 states to 255 states and 294 transitions.
[2025-05-07 17:26:43,765 INFO  L79                 Accepts]: Start accepts. Automaton has 255 states and 294 transitions. Word has length 68
[2025-05-07 17:26:43,765 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:43,765 INFO  L485      AbstractCegarLoop]: Abstraction has 255 states and 294 transitions.
[2025-05-07 17:26:43,765 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 5 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 5 states have call successors, (19)
[2025-05-07 17:26:43,765 INFO  L278                IsEmpty]: Start isEmpty. Operand 255 states and 294 transitions.
[2025-05-07 17:26:43,766 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 90
[2025-05-07 17:26:43,766 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:43,766 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:43,766 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:26:43,766 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:43,766 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:43,767 INFO  L85        PathProgramCache]: Analyzing trace with hash -406380672, now seen corresponding path program 1 times
[2025-05-07 17:26:43,767 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:43,767 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1524822069]
[2025-05-07 17:26:43,767 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:43,767 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:43,795 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 89 statements into 1 equivalence classes.
[2025-05-07 17:26:43,806 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 89 of 89 statements.
[2025-05-07 17:26:43,806 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:43,806 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:43,895 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:26:43,895 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:43,895 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1524822069]
[2025-05-07 17:26:43,895 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1524822069] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:43,895 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:43,895 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:26:43,895 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1477957017]
[2025-05-07 17:26:43,895 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:43,896 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:26:43,896 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:43,896 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:26:43,896 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:43,897 INFO  L87              Difference]: Start difference. First operand 255 states and 294 transitions. Second operand  has 7 states, 6 states have (on average 6.5) internal successors, (39), 7 states have internal predecessors, (39), 3 states have call successors, (25), 1 states have call predecessors, (25), 6 states have return successors, (25), 7 states have call predecessors, (25), 3 states have call successors, (25)
[2025-05-07 17:26:43,953 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:43,953 INFO  L93              Difference]: Finished difference Result 255 states and 293 transitions.
[2025-05-07 17:26:43,954 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:26:43,954 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 6.5) internal successors, (39), 7 states have internal predecessors, (39), 3 states have call successors, (25), 1 states have call predecessors, (25), 6 states have return successors, (25), 7 states have call predecessors, (25), 3 states have call successors, (25) Word has length 89
[2025-05-07 17:26:43,954 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:43,956 INFO  L225             Difference]: With dead ends: 255
[2025-05-07 17:26:43,956 INFO  L226             Difference]: Without dead ends: 253
[2025-05-07 17:26:43,956 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:43,956 INFO  L437           NwaCegarLoop]: 287 mSDtfsCounter, 0 mSDsluCounter, 1419 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1706 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:43,956 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1706 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:43,957 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 253 states.
[2025-05-07 17:26:43,961 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 253 to 253.
[2025-05-07 17:26:43,961 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 253 states, 104 states have (on average 1.0480769230769231) internal successors, (109), 109 states have internal predecessors, (109), 86 states have call successors, (90), 66 states have call predecessors, (90), 66 states have return successors, (90), 77 states have call predecessors, (90), 86 states have call successors, (90)
[2025-05-07 17:26:43,963 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 253 states to 253 states and 289 transitions.
[2025-05-07 17:26:43,963 INFO  L79                 Accepts]: Start accepts. Automaton has 253 states and 289 transitions. Word has length 89
[2025-05-07 17:26:43,963 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:43,963 INFO  L485      AbstractCegarLoop]: Abstraction has 253 states and 289 transitions.
[2025-05-07 17:26:43,963 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 6.5) internal successors, (39), 7 states have internal predecessors, (39), 3 states have call successors, (25), 1 states have call predecessors, (25), 6 states have return successors, (25), 7 states have call predecessors, (25), 3 states have call successors, (25)
[2025-05-07 17:26:43,963 INFO  L278                IsEmpty]: Start isEmpty. Operand 253 states and 289 transitions.
[2025-05-07 17:26:43,964 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-05-07 17:26:43,964 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:43,964 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:43,964 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:26:43,964 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:43,964 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:43,964 INFO  L85        PathProgramCache]: Analyzing trace with hash -1373913699, now seen corresponding path program 1 times
[2025-05-07 17:26:43,965 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:43,965 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [668087837]
[2025-05-07 17:26:43,965 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:43,965 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:44,000 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-05-07 17:26:44,012 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-05-07 17:26:44,012 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:44,012 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:44,146 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:26:44,146 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:44,146 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [668087837]
[2025-05-07 17:26:44,146 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [668087837] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:44,146 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:44,146 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:26:44,146 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [648831121]
[2025-05-07 17:26:44,146 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:44,146 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:26:44,146 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:44,147 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:26:44,147 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:44,147 INFO  L87              Difference]: Start difference. First operand 253 states and 289 transitions. Second operand  has 8 states, 7 states have (on average 5.714285714285714) internal successors, (40), 8 states have internal predecessors, (40), 3 states have call successors, (26), 1 states have call predecessors, (26), 7 states have return successors, (26), 8 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:26:44,214 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:44,214 INFO  L93              Difference]: Finished difference Result 261 states and 298 transitions.
[2025-05-07 17:26:44,214 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:26:44,214 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 5.714285714285714) internal successors, (40), 8 states have internal predecessors, (40), 3 states have call successors, (26), 1 states have call predecessors, (26), 7 states have return successors, (26), 8 states have call predecessors, (26), 3 states have call successors, (26) Word has length 92
[2025-05-07 17:26:44,215 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:44,216 INFO  L225             Difference]: With dead ends: 261
[2025-05-07 17:26:44,216 INFO  L226             Difference]: Without dead ends: 261
[2025-05-07 17:26:44,216 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:44,217 INFO  L437           NwaCegarLoop]: 292 mSDtfsCounter, 1 mSDsluCounter, 1726 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 2018 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:44,217 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 2018 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:44,218 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 261 states.
[2025-05-07 17:26:44,224 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 261 to 261.
[2025-05-07 17:26:44,224 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 261 states, 108 states have (on average 1.0462962962962963) internal successors, (113), 113 states have internal predecessors, (113), 86 states have call successors, (90), 66 states have call predecessors, (90), 70 states have return successors, (95), 81 states have call predecessors, (95), 86 states have call successors, (95)
[2025-05-07 17:26:44,225 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 261 states to 261 states and 298 transitions.
[2025-05-07 17:26:44,226 INFO  L79                 Accepts]: Start accepts. Automaton has 261 states and 298 transitions. Word has length 92
[2025-05-07 17:26:44,226 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:44,226 INFO  L485      AbstractCegarLoop]: Abstraction has 261 states and 298 transitions.
[2025-05-07 17:26:44,226 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 5.714285714285714) internal successors, (40), 8 states have internal predecessors, (40), 3 states have call successors, (26), 1 states have call predecessors, (26), 7 states have return successors, (26), 8 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:26:44,226 INFO  L278                IsEmpty]: Start isEmpty. Operand 261 states and 298 transitions.
[2025-05-07 17:26:44,227 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-05-07 17:26:44,227 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:44,227 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:44,227 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:26:44,228 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:44,228 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:44,228 INFO  L85        PathProgramCache]: Analyzing trace with hash -1062308579, now seen corresponding path program 1 times
[2025-05-07 17:26:44,228 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:44,228 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1239278678]
[2025-05-07 17:26:44,228 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:44,228 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:44,267 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-05-07 17:26:44,281 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-05-07 17:26:44,281 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:44,281 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:44,380 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:26:44,380 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:44,380 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1239278678]
[2025-05-07 17:26:44,380 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1239278678] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:44,380 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:44,380 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:44,380 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [26809550]
[2025-05-07 17:26:44,380 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:44,381 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:44,381 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:44,381 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:44,381 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:44,382 INFO  L87              Difference]: Start difference. First operand 261 states and 298 transitions. Second operand  has 6 states, 5 states have (on average 8.0) internal successors, (40), 6 states have internal predecessors, (40), 3 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 6 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:26:44,419 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:44,419 INFO  L93              Difference]: Finished difference Result 267 states and 304 transitions.
[2025-05-07 17:26:44,419 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:44,419 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.0) internal successors, (40), 6 states have internal predecessors, (40), 3 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 6 states have call predecessors, (26), 3 states have call successors, (26) Word has length 92
[2025-05-07 17:26:44,420 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:44,421 INFO  L225             Difference]: With dead ends: 267
[2025-05-07 17:26:44,421 INFO  L226             Difference]: Without dead ends: 267
[2025-05-07 17:26:44,421 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:26:44,421 INFO  L437           NwaCegarLoop]: 289 mSDtfsCounter, 1 mSDsluCounter, 1142 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1431 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:44,421 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1431 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:44,422 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 267 states.
[2025-05-07 17:26:44,427 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 267 to 265.
[2025-05-07 17:26:44,428 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 265 states, 110 states have (on average 1.0454545454545454) internal successors, (115), 115 states have internal predecessors, (115), 86 states have call successors, (90), 66 states have call predecessors, (90), 72 states have return successors, (97), 83 states have call predecessors, (97), 86 states have call successors, (97)
[2025-05-07 17:26:44,429 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 265 states to 265 states and 302 transitions.
[2025-05-07 17:26:44,429 INFO  L79                 Accepts]: Start accepts. Automaton has 265 states and 302 transitions. Word has length 92
[2025-05-07 17:26:44,429 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:44,429 INFO  L485      AbstractCegarLoop]: Abstraction has 265 states and 302 transitions.
[2025-05-07 17:26:44,429 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.0) internal successors, (40), 6 states have internal predecessors, (40), 3 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 6 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:26:44,429 INFO  L278                IsEmpty]: Start isEmpty. Operand 265 states and 302 transitions.
[2025-05-07 17:26:44,430 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 96
[2025-05-07 17:26:44,430 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:44,430 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:44,430 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:26:44,430 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:44,430 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:44,431 INFO  L85        PathProgramCache]: Analyzing trace with hash -1313547981, now seen corresponding path program 1 times
[2025-05-07 17:26:44,431 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:44,431 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1215693742]
[2025-05-07 17:26:44,431 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:44,431 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:44,460 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 95 statements into 1 equivalence classes.
[2025-05-07 17:26:44,470 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 95 of 95 statements.
[2025-05-07 17:26:44,470 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:44,470 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:44,545 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:26:44,545 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:44,545 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1215693742]
[2025-05-07 17:26:44,545 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1215693742] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:44,545 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:44,545 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:44,545 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [590685154]
[2025-05-07 17:26:44,545 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:44,546 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:44,546 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:44,546 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:44,546 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:44,547 INFO  L87              Difference]: Start difference. First operand 265 states and 302 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 3 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 3 states have call successors, (27)
[2025-05-07 17:26:44,579 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:44,579 INFO  L93              Difference]: Finished difference Result 269 states and 306 transitions.
[2025-05-07 17:26:44,579 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:44,580 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 3 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 3 states have call successors, (27) Word has length 95
[2025-05-07 17:26:44,580 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:44,581 INFO  L225             Difference]: With dead ends: 269
[2025-05-07 17:26:44,581 INFO  L226             Difference]: Without dead ends: 269
[2025-05-07 17:26:44,581 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:26:44,581 INFO  L437           NwaCegarLoop]: 290 mSDtfsCounter, 1 mSDsluCounter, 1139 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1429 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:44,582 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1429 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:44,582 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 269 states.
[2025-05-07 17:26:44,586 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 269 to 265.
[2025-05-07 17:26:44,587 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 265 states, 110 states have (on average 1.0454545454545454) internal successors, (115), 115 states have internal predecessors, (115), 86 states have call successors, (90), 66 states have call predecessors, (90), 72 states have return successors, (97), 83 states have call predecessors, (97), 86 states have call successors, (97)
[2025-05-07 17:26:44,588 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 265 states to 265 states and 302 transitions.
[2025-05-07 17:26:44,588 INFO  L79                 Accepts]: Start accepts. Automaton has 265 states and 302 transitions. Word has length 95
[2025-05-07 17:26:44,588 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:44,588 INFO  L485      AbstractCegarLoop]: Abstraction has 265 states and 302 transitions.
[2025-05-07 17:26:44,588 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 3 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 3 states have call successors, (27)
[2025-05-07 17:26:44,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 265 states and 302 transitions.
[2025-05-07 17:26:44,589 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-05-07 17:26:44,589 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:44,590 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:44,590 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:26:44,590 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:44,590 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:44,590 INFO  L85        PathProgramCache]: Analyzing trace with hash 1937526683, now seen corresponding path program 1 times
[2025-05-07 17:26:44,590 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:44,590 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1689987250]
[2025-05-07 17:26:44,590 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:44,590 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:44,620 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-05-07 17:26:44,628 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-05-07 17:26:44,629 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:44,629 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:44,743 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:26:44,743 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:44,743 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1689987250]
[2025-05-07 17:26:44,744 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1689987250] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:44,744 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:44,744 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:44,744 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [589885347]
[2025-05-07 17:26:44,744 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:44,744 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:44,744 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:44,745 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:44,745 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:44,745 INFO  L87              Difference]: Start difference. First operand 265 states and 302 transitions. Second operand  has 6 states, 5 states have (on average 8.0) internal successors, (40), 6 states have internal predecessors, (40), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26)
[2025-05-07 17:26:44,783 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:44,783 INFO  L93              Difference]: Finished difference Result 254 states and 287 transitions.
[2025-05-07 17:26:44,783 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:44,783 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.0) internal successors, (40), 6 states have internal predecessors, (40), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26) Word has length 92
[2025-05-07 17:26:44,783 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:44,784 INFO  L225             Difference]: With dead ends: 254
[2025-05-07 17:26:44,784 INFO  L226             Difference]: Without dead ends: 152
[2025-05-07 17:26:44,784 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:26:44,784 INFO  L437           NwaCegarLoop]: 279 mSDtfsCounter, 0 mSDsluCounter, 1104 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1383 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:44,785 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1383 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:44,785 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 152 states.
[2025-05-07 17:26:44,787 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 152 to 152.
[2025-05-07 17:26:44,788 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 152 states, 62 states have (on average 1.0483870967741935) internal successors, (65), 65 states have internal predecessors, (65), 53 states have call successors, (55), 39 states have call predecessors, (55), 39 states have return successors, (55), 47 states have call predecessors, (55), 53 states have call successors, (55)
[2025-05-07 17:26:44,788 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 152 states to 152 states and 175 transitions.
[2025-05-07 17:26:44,788 INFO  L79                 Accepts]: Start accepts. Automaton has 152 states and 175 transitions. Word has length 92
[2025-05-07 17:26:44,789 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:44,789 INFO  L485      AbstractCegarLoop]: Abstraction has 152 states and 175 transitions.
[2025-05-07 17:26:44,789 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.0) internal successors, (40), 6 states have internal predecessors, (40), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26)
[2025-05-07 17:26:44,789 INFO  L278                IsEmpty]: Start isEmpty. Operand 152 states and 175 transitions.
[2025-05-07 17:26:44,789 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 100
[2025-05-07 17:26:44,790 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:44,790 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:44,790 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:26:44,790 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:44,790 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:44,790 INFO  L85        PathProgramCache]: Analyzing trace with hash 1018013365, now seen corresponding path program 1 times
[2025-05-07 17:26:44,790 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:44,790 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1565300049]
[2025-05-07 17:26:44,790 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:44,790 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:44,821 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 99 statements into 1 equivalence classes.
[2025-05-07 17:26:44,831 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 99 of 99 statements.
[2025-05-07 17:26:44,831 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:44,831 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:44,917 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:26:44,917 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:44,917 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1565300049]
[2025-05-07 17:26:44,917 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1565300049] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:44,917 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:44,917 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:26:44,917 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1822402583]
[2025-05-07 17:26:44,917 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:44,917 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:26:44,918 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:44,918 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:26:44,918 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:44,918 INFO  L87              Difference]: Start difference. First operand 152 states and 175 transitions. Second operand  has 7 states, 6 states have (on average 7.166666666666667) internal successors, (43), 7 states have internal predecessors, (43), 4 states have call successors, (28), 1 states have call predecessors, (28), 6 states have return successors, (28), 7 states have call predecessors, (28), 4 states have call successors, (28)
[2025-05-07 17:26:44,972 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:44,972 INFO  L93              Difference]: Finished difference Result 152 states and 174 transitions.
[2025-05-07 17:26:44,973 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:26:44,973 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 7.166666666666667) internal successors, (43), 7 states have internal predecessors, (43), 4 states have call successors, (28), 1 states have call predecessors, (28), 6 states have return successors, (28), 7 states have call predecessors, (28), 4 states have call successors, (28) Word has length 99
[2025-05-07 17:26:44,973 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:44,974 INFO  L225             Difference]: With dead ends: 152
[2025-05-07 17:26:44,974 INFO  L226             Difference]: Without dead ends: 150
[2025-05-07 17:26:44,974 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:44,975 INFO  L437           NwaCegarLoop]: 168 mSDtfsCounter, 0 mSDsluCounter, 824 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 992 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:44,975 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 992 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:44,975 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 150 states.
[2025-05-07 17:26:44,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 150 to 150.
[2025-05-07 17:26:44,980 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 150 states, 61 states have (on average 1.0491803278688525) internal successors, (64), 64 states have internal predecessors, (64), 51 states have call successors, (53), 39 states have call predecessors, (53), 39 states have return successors, (53), 46 states have call predecessors, (53), 51 states have call successors, (53)
[2025-05-07 17:26:44,981 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 150 states to 150 states and 170 transitions.
[2025-05-07 17:26:44,981 INFO  L79                 Accepts]: Start accepts. Automaton has 150 states and 170 transitions. Word has length 99
[2025-05-07 17:26:44,981 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:44,981 INFO  L485      AbstractCegarLoop]: Abstraction has 150 states and 170 transitions.
[2025-05-07 17:26:44,981 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 7.166666666666667) internal successors, (43), 7 states have internal predecessors, (43), 4 states have call successors, (28), 1 states have call predecessors, (28), 6 states have return successors, (28), 7 states have call predecessors, (28), 4 states have call successors, (28)
[2025-05-07 17:26:44,981 INFO  L278                IsEmpty]: Start isEmpty. Operand 150 states and 170 transitions.
[2025-05-07 17:26:44,983 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:26:44,983 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:44,983 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:44,983 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:26:44,983 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:44,983 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:44,983 INFO  L85        PathProgramCache]: Analyzing trace with hash -1663766508, now seen corresponding path program 1 times
[2025-05-07 17:26:44,984 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:44,984 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [984568798]
[2025-05-07 17:26:44,984 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:44,984 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:45,012 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:26:45,024 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:26:45,024 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:45,024 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:45,125 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:26:45,125 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:45,125 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [984568798]
[2025-05-07 17:26:45,125 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [984568798] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:45,125 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:45,125 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:45,125 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1387875265]
[2025-05-07 17:26:45,125 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:45,125 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:45,126 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:45,126 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:45,126 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:45,126 INFO  L87              Difference]: Start difference. First operand 150 states and 170 transitions. Second operand  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:45,165 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:45,165 INFO  L93              Difference]: Finished difference Result 156 states and 177 transitions.
[2025-05-07 17:26:45,166 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:45,166 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33) Word has length 116
[2025-05-07 17:26:45,166 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:45,167 INFO  L225             Difference]: With dead ends: 156
[2025-05-07 17:26:45,167 INFO  L226             Difference]: Without dead ends: 156
[2025-05-07 17:26:45,167 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:26:45,167 INFO  L437           NwaCegarLoop]: 166 mSDtfsCounter, 1 mSDsluCounter, 652 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 818 SdHoareTripleChecker+Invalid, 29 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:45,167 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 818 Invalid, 29 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:45,168 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 156 states.
[2025-05-07 17:26:45,170 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 156 to 154.
[2025-05-07 17:26:45,170 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 154 states, 63 states have (on average 1.0476190476190477) internal successors, (66), 66 states have internal predecessors, (66), 51 states have call successors, (53), 39 states have call predecessors, (53), 41 states have return successors, (55), 48 states have call predecessors, (55), 51 states have call successors, (55)
[2025-05-07 17:26:45,171 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 174 transitions.
[2025-05-07 17:26:45,171 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 174 transitions. Word has length 116
[2025-05-07 17:26:45,171 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:45,171 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 174 transitions.
[2025-05-07 17:26:45,171 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:45,171 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 174 transitions.
[2025-05-07 17:26:45,172 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:26:45,172 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:45,172 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:45,172 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:26:45,172 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:45,172 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:45,172 INFO  L85        PathProgramCache]: Analyzing trace with hash -1031370636, now seen corresponding path program 1 times
[2025-05-07 17:26:45,173 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:45,173 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [102793302]
[2025-05-07 17:26:45,173 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:45,173 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:45,207 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:26:45,214 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:26:45,214 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:45,214 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:45,345 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:26:45,345 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:45,345 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [102793302]
[2025-05-07 17:26:45,345 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [102793302] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:45,345 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:45,346 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:45,346 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [841566525]
[2025-05-07 17:26:45,346 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:45,346 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:45,346 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:45,347 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:45,347 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:45,347 INFO  L87              Difference]: Start difference. First operand 154 states and 174 transitions. Second operand  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:45,381 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:45,381 INFO  L93              Difference]: Finished difference Result 152 states and 171 transitions.
[2025-05-07 17:26:45,381 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:45,382 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33) Word has length 116
[2025-05-07 17:26:45,382 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:45,382 INFO  L225             Difference]: With dead ends: 152
[2025-05-07 17:26:45,382 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:26:45,382 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:26:45,383 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 0 mSDsluCounter, 639 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 802 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:45,383 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 802 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:45,383 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:26:45,386 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 149.
[2025-05-07 17:26:45,386 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 61 states have (on average 1.0491803278688525) internal successors, (64), 64 states have internal predecessors, (64), 49 states have call successors, (50), 38 states have call predecessors, (50), 40 states have return successors, (52), 46 states have call predecessors, (52), 49 states have call successors, (52)
[2025-05-07 17:26:45,387 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 166 transitions.
[2025-05-07 17:26:45,387 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 166 transitions. Word has length 116
[2025-05-07 17:26:45,387 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:45,387 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 166 transitions.
[2025-05-07 17:26:45,387 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:45,387 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 166 transitions.
[2025-05-07 17:26:45,388 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 106
[2025-05-07 17:26:45,388 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:45,388 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:45,388 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:26:45,388 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:45,388 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:45,388 INFO  L85        PathProgramCache]: Analyzing trace with hash 666706882, now seen corresponding path program 1 times
[2025-05-07 17:26:45,388 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:45,388 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [202237955]
[2025-05-07 17:26:45,389 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:45,389 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:45,418 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 105 statements into 1 equivalence classes.
[2025-05-07 17:26:45,428 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 105 of 105 statements.
[2025-05-07 17:26:45,428 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:45,428 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:45,495 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:26:45,495 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:45,495 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [202237955]
[2025-05-07 17:26:45,495 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [202237955] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:45,495 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:45,495 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:45,495 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [57970905]
[2025-05-07 17:26:45,495 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:45,496 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:45,496 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:45,496 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:45,496 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:45,496 INFO  L87              Difference]: Start difference. First operand 149 states and 166 transitions. Second operand  has 6 states, 5 states have (on average 9.0) internal successors, (45), 6 states have internal predecessors, (45), 5 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 5 states have call predecessors, (30), 5 states have call successors, (30)
[2025-05-07 17:26:45,529 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:45,529 INFO  L93              Difference]: Finished difference Result 154 states and 173 transitions.
[2025-05-07 17:26:45,529 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:45,530 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.0) internal successors, (45), 6 states have internal predecessors, (45), 5 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 5 states have call predecessors, (30), 5 states have call successors, (30) Word has length 105
[2025-05-07 17:26:45,530 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:45,530 INFO  L225             Difference]: With dead ends: 154
[2025-05-07 17:26:45,530 INFO  L226             Difference]: Without dead ends: 154
[2025-05-07 17:26:45,530 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:26:45,531 INFO  L437           NwaCegarLoop]: 158 mSDtfsCounter, 1 mSDsluCounter, 616 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 774 SdHoareTripleChecker+Invalid, 25 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:45,531 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 774 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:45,531 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 154 states.
[2025-05-07 17:26:45,534 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 154 to 154.
[2025-05-07 17:26:45,534 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 154 states, 63 states have (on average 1.0476190476190477) internal successors, (66), 66 states have internal predecessors, (66), 50 states have call successors, (51), 38 states have call predecessors, (51), 42 states have return successors, (56), 49 states have call predecessors, (56), 50 states have call successors, (56)
[2025-05-07 17:26:45,535 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 173 transitions.
[2025-05-07 17:26:45,535 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 173 transitions. Word has length 105
[2025-05-07 17:26:45,535 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:45,535 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 173 transitions.
[2025-05-07 17:26:45,535 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.0) internal successors, (45), 6 states have internal predecessors, (45), 5 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 5 states have call predecessors, (30), 5 states have call successors, (30)
[2025-05-07 17:26:45,535 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 173 transitions.
[2025-05-07 17:26:45,536 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 103
[2025-05-07 17:26:45,536 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:45,536 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:45,536 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:26:45,536 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:45,536 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:45,536 INFO  L85        PathProgramCache]: Analyzing trace with hash 2005120914, now seen corresponding path program 1 times
[2025-05-07 17:26:45,536 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:45,536 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1137219017]
[2025-05-07 17:26:45,536 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:45,536 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:45,566 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 102 statements into 1 equivalence classes.
[2025-05-07 17:26:45,575 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 102 of 102 statements.
[2025-05-07 17:26:45,575 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:45,575 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:45,673 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:26:45,673 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:45,673 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1137219017]
[2025-05-07 17:26:45,673 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1137219017] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:45,674 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:45,674 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:26:45,674 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2050861803]
[2025-05-07 17:26:45,674 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:45,674 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:26:45,674 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:45,675 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:26:45,675 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:45,675 INFO  L87              Difference]: Start difference. First operand 154 states and 173 transitions. Second operand  has 8 states, 7 states have (on average 6.285714285714286) internal successors, (44), 8 states have internal predecessors, (44), 6 states have call successors, (29), 1 states have call predecessors, (29), 7 states have return successors, (29), 7 states have call predecessors, (29), 6 states have call successors, (29)
[2025-05-07 17:26:45,737 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:45,737 INFO  L93              Difference]: Finished difference Result 153 states and 170 transitions.
[2025-05-07 17:26:45,737 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:26:45,738 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 6.285714285714286) internal successors, (44), 8 states have internal predecessors, (44), 6 states have call successors, (29), 1 states have call predecessors, (29), 7 states have return successors, (29), 7 states have call predecessors, (29), 6 states have call successors, (29) Word has length 102
[2025-05-07 17:26:45,738 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:45,738 INFO  L225             Difference]: With dead ends: 153
[2025-05-07 17:26:45,739 INFO  L226             Difference]: Without dead ends: 152
[2025-05-07 17:26:45,739 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:45,739 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 1 mSDsluCounter, 954 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1117 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:45,739 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1117 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:45,740 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 152 states.
[2025-05-07 17:26:45,743 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 152 to 147.
[2025-05-07 17:26:45,743 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 147 states, 61 states have (on average 1.0327868852459017) internal successors, (63), 63 states have internal predecessors, (63), 47 states have call successors, (48), 38 states have call predecessors, (48), 40 states have return successors, (50), 45 states have call predecessors, (50), 47 states have call successors, (50)
[2025-05-07 17:26:45,744 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 147 states to 147 states and 161 transitions.
[2025-05-07 17:26:45,744 INFO  L79                 Accepts]: Start accepts. Automaton has 147 states and 161 transitions. Word has length 102
[2025-05-07 17:26:45,744 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:45,744 INFO  L485      AbstractCegarLoop]: Abstraction has 147 states and 161 transitions.
[2025-05-07 17:26:45,744 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 6.285714285714286) internal successors, (44), 8 states have internal predecessors, (44), 6 states have call successors, (29), 1 states have call predecessors, (29), 7 states have return successors, (29), 7 states have call predecessors, (29), 6 states have call successors, (29)
[2025-05-07 17:26:45,744 INFO  L278                IsEmpty]: Start isEmpty. Operand 147 states and 161 transitions.
[2025-05-07 17:26:45,745 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 120
[2025-05-07 17:26:45,745 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:45,745 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:45,745 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:26:45,745 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:45,746 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:45,746 INFO  L85        PathProgramCache]: Analyzing trace with hash -81498710, now seen corresponding path program 1 times
[2025-05-07 17:26:45,746 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:45,746 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1815073413]
[2025-05-07 17:26:45,746 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:45,746 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:45,777 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:26:45,789 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:26:45,789 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:45,789 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:45,891 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:26:45,891 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:45,891 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1815073413]
[2025-05-07 17:26:45,891 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1815073413] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:45,891 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:45,891 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:45,891 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1982004225]
[2025-05-07 17:26:45,891 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:45,892 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:45,892 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:45,892 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:45,892 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:45,892 INFO  L87              Difference]: Start difference. First operand 147 states and 161 transitions. Second operand  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:26:45,934 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:45,934 INFO  L93              Difference]: Finished difference Result 153 states and 168 transitions.
[2025-05-07 17:26:45,935 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:45,935 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34) Word has length 119
[2025-05-07 17:26:45,935 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:45,936 INFO  L225             Difference]: With dead ends: 153
[2025-05-07 17:26:45,936 INFO  L226             Difference]: Without dead ends: 153
[2025-05-07 17:26:45,936 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:26:45,936 INFO  L437           NwaCegarLoop]: 154 mSDtfsCounter, 1 mSDsluCounter, 602 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 756 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:45,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 756 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:45,937 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-05-07 17:26:45,940 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 151.
[2025-05-07 17:26:45,940 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 151 states, 63 states have (on average 1.0317460317460319) internal successors, (65), 65 states have internal predecessors, (65), 47 states have call successors, (48), 38 states have call predecessors, (48), 42 states have return successors, (53), 47 states have call predecessors, (53), 47 states have call successors, (53)
[2025-05-07 17:26:45,941 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 151 states to 151 states and 166 transitions.
[2025-05-07 17:26:45,941 INFO  L79                 Accepts]: Start accepts. Automaton has 151 states and 166 transitions. Word has length 119
[2025-05-07 17:26:45,941 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:45,941 INFO  L485      AbstractCegarLoop]: Abstraction has 151 states and 166 transitions.
[2025-05-07 17:26:45,941 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:26:45,941 INFO  L278                IsEmpty]: Start isEmpty. Operand 151 states and 166 transitions.
[2025-05-07 17:26:45,942 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:26:45,942 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:45,942 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:45,942 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:26:45,942 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:45,943 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:45,943 INFO  L85        PathProgramCache]: Analyzing trace with hash 707070954, now seen corresponding path program 1 times
[2025-05-07 17:26:45,943 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:45,943 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [387093081]
[2025-05-07 17:26:45,943 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:45,943 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:45,981 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:26:45,991 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:26:45,991 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:45,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:46,114 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:26:46,114 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:46,114 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [387093081]
[2025-05-07 17:26:46,114 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [387093081] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:46,114 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:46,114 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:26:46,115 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2147201568]
[2025-05-07 17:26:46,115 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:46,115 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:26:46,115 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:46,116 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:26:46,116 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:26:46,116 INFO  L87              Difference]: Start difference. First operand 151 states and 166 transitions. Second operand  has 10 states, 9 states have (on average 5.555555555555555) internal successors, (50), 10 states have internal predecessors, (50), 5 states have call successors, (33), 1 states have call predecessors, (33), 9 states have return successors, (33), 9 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:26:46,214 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:46,214 INFO  L93              Difference]: Finished difference Result 155 states and 170 transitions.
[2025-05-07 17:26:46,214 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:26:46,215 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 5.555555555555555) internal successors, (50), 10 states have internal predecessors, (50), 5 states have call successors, (33), 1 states have call predecessors, (33), 9 states have return successors, (33), 9 states have call predecessors, (33), 5 states have call successors, (33) Word has length 116
[2025-05-07 17:26:46,215 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:46,215 INFO  L225             Difference]: With dead ends: 155
[2025-05-07 17:26:46,215 INFO  L226             Difference]: Without dead ends: 155
[2025-05-07 17:26:46,216 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:26:46,216 INFO  L437           NwaCegarLoop]: 160 mSDtfsCounter, 1 mSDsluCounter, 1252 mSDsCounter, 0 mSdLazyCounter, 97 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1412 SdHoareTripleChecker+Invalid, 97 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 97 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:46,216 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1412 Invalid, 97 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 97 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:46,216 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 155 states.
[2025-05-07 17:26:46,219 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 155 to 155.
[2025-05-07 17:26:46,219 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 155 states, 65 states have (on average 1.0307692307692307) internal successors, (67), 67 states have internal predecessors, (67), 47 states have call successors, (48), 38 states have call predecessors, (48), 44 states have return successors, (55), 49 states have call predecessors, (55), 47 states have call successors, (55)
[2025-05-07 17:26:46,219 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 155 states to 155 states and 170 transitions.
[2025-05-07 17:26:46,220 INFO  L79                 Accepts]: Start accepts. Automaton has 155 states and 170 transitions. Word has length 116
[2025-05-07 17:26:46,220 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:46,220 INFO  L485      AbstractCegarLoop]: Abstraction has 155 states and 170 transitions.
[2025-05-07 17:26:46,220 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 5.555555555555555) internal successors, (50), 10 states have internal predecessors, (50), 5 states have call successors, (33), 1 states have call predecessors, (33), 9 states have return successors, (33), 9 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:26:46,220 INFO  L278                IsEmpty]: Start isEmpty. Operand 155 states and 170 transitions.
[2025-05-07 17:26:46,221 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:26:46,221 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:46,221 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:46,221 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:26:46,221 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:46,221 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:46,221 INFO  L85        PathProgramCache]: Analyzing trace with hash 1615024318, now seen corresponding path program 1 times
[2025-05-07 17:26:46,221 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:46,221 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [271465889]
[2025-05-07 17:26:46,221 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:46,221 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:46,264 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:26:46,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:26:46,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:46,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:46,347 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:26:46,348 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:46,348 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [271465889]
[2025-05-07 17:26:46,348 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [271465889] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:46,348 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:46,348 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:46,348 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [166310620]
[2025-05-07 17:26:46,348 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:46,348 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:46,348 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:46,349 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:46,349 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:46,349 INFO  L87              Difference]: Start difference. First operand 155 states and 170 transitions. Second operand  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 4 states have call successors, (35)
[2025-05-07 17:26:46,370 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:46,370 INFO  L93              Difference]: Finished difference Result 96 states and 103 transitions.
[2025-05-07 17:26:46,370 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:46,370 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 4 states have call successors, (35) Word has length 122
[2025-05-07 17:26:46,370 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:46,371 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:26:46,371 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:26:46,371 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:26:46,371 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 0 mSDsluCounter, 352 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 442 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:46,371 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 442 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:46,371 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:26:46,371 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:26:46,372 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:26:46,372 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:26:46,372 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 122
[2025-05-07 17:26:46,372 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:46,372 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:26:46,372 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 4 states have call successors, (35)
[2025-05-07 17:26:46,372 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:26:46,372 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:26:46,374 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:26:46,374 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:26:46,376 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:46,378 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:26:46,380 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:26:46 BoogieIcfgContainer
[2025-05-07 17:26:46,380 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:26:46,381 INFO  L158              Benchmark]: Toolchain (without parser) took 5285.73ms. Allocated memory was 302.0MB in the beginning and 436.2MB in the end (delta: 134.2MB). Free memory was 253.5MB in the beginning and 314.1MB in the end (delta: -60.6MB). Peak memory consumption was 69.9MB. Max. memory is 33.6GB.
[2025-05-07 17:26:46,381 INFO  L158              Benchmark]: SmtParser took 0.23ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:46,381 INFO  L158              Benchmark]: ChcToBoogie took 41.18ms. Allocated memory is still 302.0MB. Free memory was 253.5MB in the beginning and 246.4MB in the end (delta: 7.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:26:46,381 INFO  L158              Benchmark]: Boogie Preprocessor took 80.02ms. Allocated memory is still 302.0MB. Free memory was 246.4MB in the beginning and 240.1MB in the end (delta: 6.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:46,381 INFO  L158              Benchmark]: RCFGBuilder took 901.14ms. Allocated memory is still 302.0MB. Free memory was 240.1MB in the beginning and 222.8MB in the end (delta: 17.3MB). Peak memory consumption was 95.5MB. Max. memory is 33.6GB.
[2025-05-07 17:26:46,382 INFO  L158              Benchmark]: TraceAbstraction took 4260.38ms. Allocated memory was 302.0MB in the beginning and 436.2MB in the end (delta: 134.2MB). Free memory was 221.7MB in the beginning and 314.1MB in the end (delta: -92.4MB). Peak memory consumption was 41.5MB. Max. memory is 33.6GB.
[2025-05-07 17:26:46,382 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.23ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 41.18ms. Allocated memory is still 302.0MB. Free memory was 253.5MB in the beginning and 246.4MB in the end (delta: 7.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 80.02ms. Allocated memory is still 302.0MB. Free memory was 246.4MB in the beginning and 240.1MB in the end (delta: 6.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 901.14ms. Allocated memory is still 302.0MB. Free memory was 240.1MB in the beginning and 222.8MB in the end (delta: 17.3MB). Peak memory consumption was 95.5MB. Max. memory is 33.6GB.
 * TraceAbstraction took 4260.38ms. Allocated memory was 302.0MB in the beginning and 436.2MB in the end (delta: 134.2MB). Free memory was 221.7MB in the beginning and 314.1MB in the end (delta: -92.4MB). Peak memory consumption was 41.5MB. 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
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 86 procedures, 347 locations, 556 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 4.2s, OverallIterations: 19, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 60 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 12 mSDsluCounter, 25259 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 20297 mSDsCounter, 15 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 560 IncrementalHoareTripleChecker+Invalid, 575 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 15 mSolverCounterUnsat, 4962 mSDtfsCounter, 560 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 121 GetRequests, 38 SyntacticMatches, 0 SemanticMatches, 83 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=347occurred in iteration=0, InterpolantAutomatonStates: 121, 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, 19 MinimizatonAttempts, 19 StatesRemovedByMinimization, 7 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 2.1s InterpolantComputationTime, 1782 NumberOfCodeBlocks, 1782 NumberOfCodeBlocksAsserted, 19 NumberOfCheckSat, 1763 ConstructedInterpolants, 0 QuantifiedInterpolants, 2157 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 19 InterpolantComputations, 19 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:26:46,395 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...
sat
