./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_1_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:16,698 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:16,736 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a69fdce-d703-462d-8eb1-e48b5874220a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:16,739 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:16,739 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:16,752 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:16,752 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:16,752 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:16,753 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:16,753 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:16,753 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:16,753 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:16,753 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:16,754 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:16,754 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:16,754 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:16,754 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:16,755 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:16,755 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:16,755 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:16,944 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:16,950 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:16,951 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:16,952 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:16,952 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:16,953 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a69fdce-d703-462d-8eb1-e48b5874220a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_1_no_adts_000.smt2
[2025-05-07 17:27:16,954 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:16,956 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:17,203 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a69fdce-d703-462d-8eb1-e48b5874220a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_1_no_adts_000.smt2
[2025-05-07 17:27:17,205 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:17,206 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:17,206 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:17,206 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:17,207 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:17,208 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,239 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17 Unit
[2025-05-07 17:27:17,239 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:17,240 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:17,240 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:17,240 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:17,251 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,251 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,273 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,273 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,278 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,280 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,281 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,283 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,285 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,296 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:17,297 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:17,297 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:17,297 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:17,297 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (1/1) ...
[2025-05-07 17:27:17,299 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:17,308 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:17,316 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:27:17,318 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:27:17,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:17,326 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:17,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:17,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_15_0 given in one single declaration
[2025-05-07 17:27:17,326 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_15_0
[2025-05-07 17:27:17,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_15_0
[2025-05-07 17:27:17,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_g__36_37_0 given in one single declaration
[2025-05-07 17:27:17,326 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_g__36_37_0
[2025-05-07 17:27:17,326 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_g__36_37_0
[2025-05-07 17:27:17,326 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_g__36_37_0 given in one single declaration
[2025-05-07 17:27:17,326 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_g__36_37_0
[2025-05-07 17:27:17,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_g__36_37_0
[2025-05-07 17:27:17,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_34_g_35_37_0 given in one single declaration
[2025-05-07 17:27:17,327 INFO  L130     BoogieDeclarations]: Found specification of procedure block_34_g_35_37_0
[2025-05-07 17:27:17,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_34_g_35_37_0
[2025-05-07 17:27:17,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_33_function_g__36_37_0 given in one single declaration
[2025-05-07 17:27:17,327 INFO  L130     BoogieDeclarations]: Found specification of procedure block_33_function_g__36_37_0
[2025-05-07 17:27:17,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_33_function_g__36_37_0
[2025-05-07 17:27:17,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_36_function_v__23_37_0 given in one single declaration
[2025-05-07 17:27:17,327 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_36_function_v__23_37_0
[2025-05-07 17:27:17,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_36_function_v__23_37_0
[2025-05-07 17:27:17,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_v__23_37_0 given in one single declaration
[2025-05-07 17:27:17,327 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_v__23_37_0
[2025-05-07 17:27:17,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_v__23_37_0
[2025-05-07 17:27:17,327 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_return_function_v__23_37_0 given in one single declaration
[2025-05-07 17:27:17,327 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_return_function_v__23_37_0
[2025-05-07 17:27:17,327 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_return_function_v__23_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_31_v_22_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure block_31_v_22_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_31_v_22_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_v__23_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_v__23_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_v__23_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_function_g__36_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_function_g__36_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_function_g__36_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_return_function_g__36_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_return_function_g__36_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_return_function_g__36_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_function_g__36_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_function_g__36_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_function_g__36_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_A_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_A_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_A_37_0
[2025-05-07 17:27:17,328 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_A_37_0 given in one single declaration
[2025-05-07 17:27:17,328 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_A_37_0
[2025-05-07 17:27:17,328 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_A_37_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_42_A_37_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_42_A_37_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_42_A_37_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_39_A_37_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_39_A_37_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_39_A_37_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_41_A_37_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_41_A_37_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_41_A_37_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_40_A_37_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_40_A_37_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_40_A_37_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_7_B_50_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_7_B_50_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_7_B_50_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_9_B_50_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_9_B_50_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_9_B_50_0
[2025-05-07 17:27:17,329 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_61_B_50_0 given in one single declaration
[2025-05-07 17:27:17,329 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_61_B_50_0
[2025-05-07 17:27:17,329 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_61_B_50_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_63_B_50_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_63_B_50_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_63_B_50_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_62_B_50_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_62_B_50_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_62_B_50_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_64_A_37_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_64_A_37_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_64_A_37_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_66_A_37_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_66_A_37_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_66_A_37_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_65_A_37_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_65_A_37_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_65_A_37_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_67_B_50_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_67_B_50_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_67_B_50_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_g__36_50_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_g__36_50_0
[2025-05-07 17:27:17,330 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_g__36_50_0
[2025-05-07 17:27:17,330 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_12_function_g__36_50_0 given in one single declaration
[2025-05-07 17:27:17,330 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_12_function_g__36_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_12_function_g__36_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_54_function_v__23_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_54_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_54_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_v__23_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_return_function_v__23_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_return_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_return_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_v_22_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_v_22_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_v_22_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_function_v__23_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_function_v__23_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_g_35_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_g_35_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_g_35_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_function_g__36_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_function_g__36_50_0
[2025-05-07 17:27:17,331 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_function_g__36_50_0
[2025-05-07 17:27:17,331 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_function_g__36_50_0 given in one single declaration
[2025-05-07 17:27:17,331 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_function_g__36_50_0
[2025-05-07 17:27:17,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_function_g__36_50_0
[2025-05-07 17:27:17,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_return_function_g__36_50_0 given in one single declaration
[2025-05-07 17:27:17,332 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_return_function_g__36_50_0
[2025-05-07 17:27:17,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_return_function_g__36_50_0
[2025-05-07 17:27:17,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_function_g__36_50_0 given in one single declaration
[2025-05-07 17:27:17,332 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_function_g__36_50_0
[2025-05-07 17:27:17,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_function_g__36_50_0
[2025-05-07 17:27:17,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:17,332 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:17,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:17,510 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:17,512 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:17,762 INFO  L?                        ?]: Removed 320 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:17,762 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:17,775 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:17,776 INFO  L312             CfgBuilder]: Removed 21 assume(true) statements.
[2025-05-07 17:27:17,776 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:17 BoogieIcfgContainer
[2025-05-07 17:27:17,776 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:17,778 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:17,778 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:17,782 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:17,782 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:17" (1/3) ...
[2025-05-07 17:27:17,782 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2c8a734a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:17, skipping insertion in model container
[2025-05-07 17:27:17,783 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:17" (2/3) ...
[2025-05-07 17:27:17,783 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2c8a734a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:17, skipping insertion in model container
[2025-05-07 17:27:17,783 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:17" (3/3) ...
[2025-05-07 17:27:17,784 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:17,797 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:17,799 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 42 procedures, 166 locations, 254 edges, 42 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:17,832 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:17,842 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;@38fa943d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:17,842 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:17,846 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 166 states, 67 states have (on average 1.1044776119402986) internal successors, (74), 74 states have internal predecessors, (74), 58 states have call successors, (60), 41 states have call predecessors, (60), 41 states have return successors, (60), 50 states have call predecessors, (60), 58 states have call successors, (60)
[2025-05-07 17:27:17,857 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:27:17,857 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:17,858 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:27:17,858 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:17,862 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:17,863 INFO  L85        PathProgramCache]: Analyzing trace with hash 1078840766, now seen corresponding path program 1 times
[2025-05-07 17:27:17,868 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:17,868 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [46802794]
[2025-05-07 17:27:17,868 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:17,869 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:17,921 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:27:17,979 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:27:17,980 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:17,980 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:18,344 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:18,345 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:18,345 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [46802794]
[2025-05-07 17:27:18,346 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [46802794] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:18,346 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:18,348 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:18,354 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2000978022]
[2025-05-07 17:27:18,356 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:18,360 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:18,360 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:18,382 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:18,382 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:18,385 INFO  L87              Difference]: Start difference. First operand  has 166 states, 67 states have (on average 1.1044776119402986) internal successors, (74), 74 states have internal predecessors, (74), 58 states have call successors, (60), 41 states have call predecessors, (60), 41 states have return successors, (60), 50 states have call predecessors, (60), 58 states have call successors, (60) Second operand  has 4 states, 3 states have (on average 9.666666666666666) internal successors, (29), 4 states have internal predecessors, (29), 3 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:27:18,427 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:18,427 INFO  L93              Difference]: Finished difference Result 168 states and 196 transitions.
[2025-05-07 17:27:18,428 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:18,430 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.666666666666666) internal successors, (29), 4 states have internal predecessors, (29), 3 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 3 states have call successors, (18) Word has length 65
[2025-05-07 17:27:18,430 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:18,436 INFO  L225             Difference]: With dead ends: 168
[2025-05-07 17:27:18,436 INFO  L226             Difference]: Without dead ends: 161
[2025-05-07 17:27:18,437 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:18,439 INFO  L437           NwaCegarLoop]: 193 mSDtfsCounter, 1 mSDsluCounter, 374 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 567 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:27:18,440 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 567 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:18,449 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 161 states.
[2025-05-07 17:27:18,468 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 161 to 159.
[2025-05-07 17:27:18,469 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 66 states have (on average 1.0606060606060606) internal successors, (70), 70 states have internal predecessors, (70), 53 states have call successors, (55), 41 states have call predecessors, (55), 41 states have return successors, (55), 47 states have call predecessors, (55), 53 states have call successors, (55)
[2025-05-07 17:27:18,473 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 180 transitions.
[2025-05-07 17:27:18,473 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 180 transitions. Word has length 65
[2025-05-07 17:27:18,474 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:18,474 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 180 transitions.
[2025-05-07 17:27:18,474 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.666666666666666) internal successors, (29), 4 states have internal predecessors, (29), 3 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:27:18,474 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 180 transitions.
[2025-05-07 17:27:18,476 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:27:18,476 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:18,476 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:27:18,477 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:18,477 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:18,477 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:18,477 INFO  L85        PathProgramCache]: Analyzing trace with hash -1449495125, now seen corresponding path program 1 times
[2025-05-07 17:27:18,477 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:18,477 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [998434457]
[2025-05-07 17:27:18,477 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:18,477 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:18,503 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:27:18,521 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:27:18,521 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:18,522 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:18,618 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:18,618 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:18,618 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [998434457]
[2025-05-07 17:27:18,618 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [998434457] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:18,618 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:18,618 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:18,618 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [522973467]
[2025-05-07 17:27:18,619 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:18,620 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:18,620 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:18,620 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:18,620 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:18,621 INFO  L87              Difference]: Start difference. First operand 159 states and 180 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 3 states have call successors, (19)
[2025-05-07 17:27:18,670 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:18,671 INFO  L93              Difference]: Finished difference Result 163 states and 184 transitions.
[2025-05-07 17:27:18,671 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:18,671 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), 3 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 3 states have call successors, (19) Word has length 68
[2025-05-07 17:27:18,672 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:18,673 INFO  L225             Difference]: With dead ends: 163
[2025-05-07 17:27:18,673 INFO  L226             Difference]: Without dead ends: 163
[2025-05-07 17:27:18,673 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:18,674 INFO  L437           NwaCegarLoop]: 177 mSDtfsCounter, 1 mSDsluCounter, 693 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 870 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:18,674 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 870 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:18,675 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 163 states.
[2025-05-07 17:27:18,681 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 163 to 163.
[2025-05-07 17:27:18,682 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 163 states, 68 states have (on average 1.0588235294117647) internal successors, (72), 72 states have internal predecessors, (72), 53 states have call successors, (55), 41 states have call predecessors, (55), 43 states have return successors, (57), 49 states have call predecessors, (57), 53 states have call successors, (57)
[2025-05-07 17:27:18,683 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 163 states to 163 states and 184 transitions.
[2025-05-07 17:27:18,683 INFO  L79                 Accepts]: Start accepts. Automaton has 163 states and 184 transitions. Word has length 68
[2025-05-07 17:27:18,683 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:18,683 INFO  L485      AbstractCegarLoop]: Abstraction has 163 states and 184 transitions.
[2025-05-07 17:27:18,684 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), 3 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 3 states have call successors, (19)
[2025-05-07 17:27:18,684 INFO  L278                IsEmpty]: Start isEmpty. Operand 163 states and 184 transitions.
[2025-05-07 17:27:18,685 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:27:18,685 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:18,685 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:27:18,685 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:18,685 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:18,686 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:18,686 INFO  L85        PathProgramCache]: Analyzing trace with hash 961745767, now seen corresponding path program 1 times
[2025-05-07 17:27:18,686 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:18,686 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [510106767]
[2025-05-07 17:27:18,686 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:18,686 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:18,707 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:27:18,710 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:27:18,710 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:18,710 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:18,762 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:18,762 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:18,762 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [510106767]
[2025-05-07 17:27:18,762 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [510106767] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:18,762 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:18,762 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:18,762 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1870420387]
[2025-05-07 17:27:18,762 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:18,762 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:18,762 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:18,763 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:18,763 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:18,763 INFO  L87              Difference]: Start difference. First operand 163 states and 184 transitions. Second operand  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (19), 1 states have call predecessors, (19), 3 states have return successors, (19), 3 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:27:18,774 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:18,774 INFO  L93              Difference]: Finished difference Result 167 states and 188 transitions.
[2025-05-07 17:27:18,775 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:18,775 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (19), 1 states have call predecessors, (19), 3 states have return successors, (19), 3 states have call predecessors, (19), 4 states have call successors, (19) Word has length 68
[2025-05-07 17:27:18,775 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:18,776 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:27:18,776 INFO  L226             Difference]: Without dead ends: 163
[2025-05-07 17:27:18,776 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:18,777 INFO  L437           NwaCegarLoop]: 180 mSDtfsCounter, 1 mSDsluCounter, 353 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 533 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:18,777 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 533 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:18,777 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 163 states.
[2025-05-07 17:27:18,783 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 163 to 161.
[2025-05-07 17:27:18,784 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 161 states, 68 states have (on average 1.0441176470588236) internal successors, (71), 71 states have internal predecessors, (71), 51 states have call successors, (53), 41 states have call predecessors, (53), 43 states have return successors, (55), 48 states have call predecessors, (55), 51 states have call successors, (55)
[2025-05-07 17:27:18,785 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 179 transitions.
[2025-05-07 17:27:18,785 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 179 transitions. Word has length 68
[2025-05-07 17:27:18,785 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:18,785 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 179 transitions.
[2025-05-07 17:27:18,785 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (19), 1 states have call predecessors, (19), 3 states have return successors, (19), 3 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:27:18,785 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 179 transitions.
[2025-05-07 17:27:18,786 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:27:18,786 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:18,786 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:27:18,787 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:18,787 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:18,787 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:18,787 INFO  L85        PathProgramCache]: Analyzing trace with hash 1372154603, now seen corresponding path program 1 times
[2025-05-07 17:27:18,787 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:18,787 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1699982398]
[2025-05-07 17:27:18,787 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:18,787 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:18,812 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:27:18,827 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:27:18,827 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:18,827 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:18,938 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:18,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:18,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1699982398]
[2025-05-07 17:27:18,939 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1699982398] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:18,939 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:18,939 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:18,939 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [305078293]
[2025-05-07 17:27:18,939 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:18,939 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:18,939 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:18,940 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:18,940 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:18,940 INFO  L87              Difference]: Start difference. First operand 161 states and 179 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 3 states have call successors, (19)
[2025-05-07 17:27:18,981 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:18,981 INFO  L93              Difference]: Finished difference Result 165 states and 183 transitions.
[2025-05-07 17:27:18,981 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:18,982 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), 3 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 3 states have call successors, (19) Word has length 68
[2025-05-07 17:27:18,982 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:18,983 INFO  L225             Difference]: With dead ends: 165
[2025-05-07 17:27:18,983 INFO  L226             Difference]: Without dead ends: 165
[2025-05-07 17:27:18,983 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:18,984 INFO  L437           NwaCegarLoop]: 176 mSDtfsCounter, 1 mSDsluCounter, 686 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 862 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:18,984 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 862 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:18,984 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-05-07 17:27:18,989 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 161.
[2025-05-07 17:27:18,990 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 161 states, 68 states have (on average 1.0441176470588236) internal successors, (71), 71 states have internal predecessors, (71), 51 states have call successors, (53), 41 states have call predecessors, (53), 43 states have return successors, (55), 48 states have call predecessors, (55), 51 states have call successors, (55)
[2025-05-07 17:27:18,990 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 179 transitions.
[2025-05-07 17:27:18,990 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 179 transitions. Word has length 68
[2025-05-07 17:27:18,991 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:18,991 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 179 transitions.
[2025-05-07 17:27:18,991 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), 3 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 3 states have call successors, (19)
[2025-05-07 17:27:18,991 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 179 transitions.
[2025-05-07 17:27:18,992 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:27:18,992 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:18,992 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:27:18,992 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:18,992 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:18,992 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:18,992 INFO  L85        PathProgramCache]: Analyzing trace with hash 475144278, now seen corresponding path program 1 times
[2025-05-07 17:27:18,992 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:18,992 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [23079787]
[2025-05-07 17:27:18,993 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:18,993 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:19,015 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:27:19,024 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:27:19,024 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:19,024 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:19,101 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:19,101 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:19,101 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [23079787]
[2025-05-07 17:27:19,101 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [23079787] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:19,101 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:19,101 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:19,101 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1988403592]
[2025-05-07 17:27:19,102 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:19,102 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:19,102 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:19,103 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:19,103 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:19,103 INFO  L87              Difference]: Start difference. First operand 161 states and 179 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), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:27:19,155 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:19,155 INFO  L93              Difference]: Finished difference Result 156 states and 171 transitions.
[2025-05-07 17:27:19,156 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:19,156 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), 6 states have call predecessors, (18), 4 states have call successors, (18) Word has length 65
[2025-05-07 17:27:19,156 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:19,156 INFO  L225             Difference]: With dead ends: 156
[2025-05-07 17:27:19,157 INFO  L226             Difference]: Without dead ends: 88
[2025-05-07 17:27:19,157 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:27:19,157 INFO  L437           NwaCegarLoop]: 166 mSDtfsCounter, 0 mSDsluCounter, 816 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 982 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:19,157 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 982 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:19,158 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 88 states.
[2025-05-07 17:27:19,160 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 88 to 88.
[2025-05-07 17:27:19,161 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 88 states, 37 states have (on average 1.027027027027027) internal successors, (38), 38 states have internal predecessors, (38), 28 states have call successors, (29), 23 states have call predecessors, (29), 23 states have return successors, (29), 26 states have call predecessors, (29), 28 states have call successors, (29)
[2025-05-07 17:27:19,161 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 88 states to 88 states and 96 transitions.
[2025-05-07 17:27:19,161 INFO  L79                 Accepts]: Start accepts. Automaton has 88 states and 96 transitions. Word has length 65
[2025-05-07 17:27:19,161 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:19,161 INFO  L485      AbstractCegarLoop]: Abstraction has 88 states and 96 transitions.
[2025-05-07 17:27:19,161 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), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:27:19,162 INFO  L278                IsEmpty]: Start isEmpty. Operand 88 states and 96 transitions.
[2025-05-07 17:27:19,162 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:27:19,162 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:19,162 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]
[2025-05-07 17:27:19,162 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:19,162 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:19,162 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:19,163 INFO  L85        PathProgramCache]: Analyzing trace with hash 1560126571, now seen corresponding path program 1 times
[2025-05-07 17:27:19,163 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:19,163 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [440426201]
[2025-05-07 17:27:19,163 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:19,163 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:19,189 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:27:19,200 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:27:19,200 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:19,200 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:19,294 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:19,295 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:19,295 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [440426201]
[2025-05-07 17:27:19,295 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [440426201] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:19,295 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:19,295 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:19,295 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1576406239]
[2025-05-07 17:27:19,295 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:19,295 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:19,296 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:19,296 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:19,296 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:19,296 INFO  L87              Difference]: Start difference. First operand 88 states and 96 transitions. Second operand  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 7 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:27:19,347 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:19,347 INFO  L93              Difference]: Finished difference Result 88 states and 95 transitions.
[2025-05-07 17:27:19,348 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:19,348 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 7 states have call predecessors, (21), 4 states have call successors, (21) Word has length 75
[2025-05-07 17:27:19,348 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:19,349 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:27:19,349 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:27:19,349 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:27:19,350 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 0 mSDsluCounter, 435 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 525 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:19,350 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 525 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:19,351 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:27:19,353 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:27:19,353 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 36 states have (on average 1.0277777777777777) internal successors, (37), 37 states have internal predecessors, (37), 26 states have call successors, (27), 23 states have call predecessors, (27), 23 states have return successors, (27), 25 states have call predecessors, (27), 26 states have call successors, (27)
[2025-05-07 17:27:19,354 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 91 transitions.
[2025-05-07 17:27:19,354 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 91 transitions. Word has length 75
[2025-05-07 17:27:19,354 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:19,354 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 91 transitions.
[2025-05-07 17:27:19,354 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 7 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:27:19,354 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 91 transitions.
[2025-05-07 17:27:19,354 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 79
[2025-05-07 17:27:19,354 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:19,355 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]
[2025-05-07 17:27:19,355 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:19,355 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:19,355 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:19,355 INFO  L85        PathProgramCache]: Analyzing trace with hash -909717312, now seen corresponding path program 1 times
[2025-05-07 17:27:19,355 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:19,355 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1619326680]
[2025-05-07 17:27:19,355 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:19,355 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:19,383 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 78 statements into 1 equivalence classes.
[2025-05-07 17:27:19,392 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 78 of 78 statements.
[2025-05-07 17:27:19,392 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:19,392 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:19,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:19,464 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:19,464 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1619326680]
[2025-05-07 17:27:19,464 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1619326680] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:19,464 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:19,464 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:19,464 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [351089972]
[2025-05-07 17:27:19,464 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:19,465 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:19,465 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:19,466 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:19,466 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:19,466 INFO  L87              Difference]: Start difference. First operand 86 states and 91 transitions. Second operand  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:19,496 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:19,497 INFO  L93              Difference]: Finished difference Result 90 states and 95 transitions.
[2025-05-07 17:27:19,497 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:19,497 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 4 states have call successors, (22) Word has length 78
[2025-05-07 17:27:19,498 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:19,498 INFO  L225             Difference]: With dead ends: 90
[2025-05-07 17:27:19,498 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:27:19,498 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:19,499 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 1 mSDsluCounter, 345 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 434 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:19,499 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 434 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:19,499 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:27:19,502 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:27:19,502 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 38 states have (on average 1.0263157894736843) internal successors, (39), 39 states have internal predecessors, (39), 26 states have call successors, (27), 23 states have call predecessors, (27), 25 states have return successors, (29), 27 states have call predecessors, (29), 26 states have call successors, (29)
[2025-05-07 17:27:19,503 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 95 transitions.
[2025-05-07 17:27:19,503 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 95 transitions. Word has length 78
[2025-05-07 17:27:19,503 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:19,503 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 95 transitions.
[2025-05-07 17:27:19,503 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:19,503 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 95 transitions.
[2025-05-07 17:27:19,504 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 79
[2025-05-07 17:27:19,504 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:19,504 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]
[2025-05-07 17:27:19,504 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:19,504 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:19,504 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:19,504 INFO  L85        PathProgramCache]: Analyzing trace with hash 1847932352, now seen corresponding path program 1 times
[2025-05-07 17:27:19,505 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:19,505 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [812637676]
[2025-05-07 17:27:19,505 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:19,505 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:19,531 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 78 statements into 1 equivalence classes.
[2025-05-07 17:27:19,540 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 78 of 78 statements.
[2025-05-07 17:27:19,540 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:19,540 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:19,623 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:19,623 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:19,623 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [812637676]
[2025-05-07 17:27:19,623 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [812637676] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:19,623 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:19,623 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:19,623 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [332855283]
[2025-05-07 17:27:19,623 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:19,623 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:19,623 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:19,624 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:19,624 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:19,624 INFO  L87              Difference]: Start difference. First operand 90 states and 95 transitions. Second operand  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:19,641 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:19,641 INFO  L93              Difference]: Finished difference Result 50 states and 51 transitions.
[2025-05-07 17:27:19,641 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:19,641 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 4 states have call successors, (22) Word has length 78
[2025-05-07 17:27:19,642 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:19,642 INFO  L225             Difference]: With dead ends: 50
[2025-05-07 17:27:19,642 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:19,642 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:19,642 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 0 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 223 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:19,642 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 223 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:19,643 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:19,643 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:19,643 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:27:19,643 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:19,643 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 78
[2025-05-07 17:27:19,643 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:19,643 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:19,643 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:19,643 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:19,643 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:19,645 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:19,645 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:19,648 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:19,649 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:19,651 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:19 BoogieIcfgContainer
[2025-05-07 17:27:19,652 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:19,652 INFO  L158              Benchmark]: Toolchain (without parser) took 2446.15ms. Allocated memory is still 234.9MB. Free memory was 142.8MB in the beginning and 185.8MB in the end (delta: -43.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:19,652 INFO  L158              Benchmark]: SmtParser took 0.20ms. Allocated memory is still 234.9MB. Free memory is still 173.8MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:19,652 INFO  L158              Benchmark]: ChcToBoogie took 33.25ms. Allocated memory is still 234.9MB. Free memory was 142.8MB in the beginning and 139.1MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:19,652 INFO  L158              Benchmark]: Boogie Preprocessor took 56.36ms. Allocated memory is still 234.9MB. Free memory was 139.1MB in the beginning and 135.2MB in the end (delta: 3.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:19,653 INFO  L158              Benchmark]: RCFGBuilder took 479.38ms. Allocated memory is still 234.9MB. Free memory was 135.2MB in the beginning and 154.8MB in the end (delta: -19.6MB). Peak memory consumption was 26.7MB. Max. memory is 33.6GB.
[2025-05-07 17:27:19,653 INFO  L158              Benchmark]: TraceAbstraction took 1873.29ms. Allocated memory is still 234.9MB. Free memory was 154.4MB in the beginning and 185.8MB in the end (delta: -31.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:19,653 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.20ms. Allocated memory is still 234.9MB. Free memory is still 173.8MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 33.25ms. Allocated memory is still 234.9MB. Free memory was 142.8MB in the beginning and 139.1MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 56.36ms. Allocated memory is still 234.9MB. Free memory was 139.1MB in the beginning and 135.2MB in the end (delta: 3.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 479.38ms. Allocated memory is still 234.9MB. Free memory was 135.2MB in the beginning and 154.8MB in the end (delta: -19.6MB). Peak memory consumption was 26.7MB. Max. memory is 33.6GB.
 * TraceAbstraction took 1873.29ms. Allocated memory is still 234.9MB. Free memory was 154.4MB in the beginning and 185.8MB in the end (delta: -31.4MB). There was no memory consumed. 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 42 procedures, 166 locations, 254 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 1.8s, OverallIterations: 8, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.4s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 18 SdHoareTripleChecker+Valid, 0.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 5 mSDsluCounter, 4996 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 3879 mSDsCounter, 3 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 136 IncrementalHoareTripleChecker+Invalid, 139 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 3 mSolverCounterUnsat, 1117 mSDtfsCounter, 136 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 48 GetRequests, 18 SyntacticMatches, 0 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=166occurred in iteration=0, InterpolantAutomatonStates: 46, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 8 MinimizatonAttempts, 8 StatesRemovedByMinimization, 3 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.9s InterpolantComputationTime, 565 NumberOfCodeBlocks, 565 NumberOfCodeBlocksAsserted, 8 NumberOfCheckSat, 557 ConstructedInterpolants, 0 QuantifiedInterpolants, 695 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 8 InterpolantComputations, 8 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:27:19,664 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
