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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:12,996 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:13,032 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_accd281c-8353-4500-a530-1f347057a295/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:13,035 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:13,035 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:13,048 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:13,049 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:13,049 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:13,049 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:13,049 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:13,049 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:13,049 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:13,049 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:13,049 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:13,049 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:13,049 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:13,050 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:13,050 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:13,050 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:13,051 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:13,240 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:13,248 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:13,250 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:13,251 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:13,251 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:13,252 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_accd281c-8353-4500-a530-1f347057a295/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol_1_no_adts_000.smt2
[2025-05-07 17:28:13,253 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:13,255 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:13,525 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_accd281c-8353-4500-a530-1f347057a295/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol_1_no_adts_000.smt2
[2025-05-07 17:28:13,527 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:13,528 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:13,529 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:13,529 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:13,529 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:13,532 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,571 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13 Unit
[2025-05-07 17:28:13,572 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:13,573 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:13,573 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:13,573 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:13,585 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,585 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,616 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,616 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,624 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,626 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,628 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,631 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,632 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,645 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:13,645 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:13,645 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:13,646 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:13,646 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (1/1) ...
[2025-05-07 17:28:13,648 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:13,660 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:13,671 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:28:13,673 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:28:13,681 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:13,681 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:13,681 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:13,681 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_7_0 given in one single declaration
[2025-05-07 17:28:13,681 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_7_0
[2025-05-07 17:28:13,681 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_7_0
[2025-05-07 17:28:13,681 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_26_A_55_0 given in one single declaration
[2025-05-07 17:28:13,681 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_26_A_55_0
[2025-05-07 17:28:13,682 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_26_A_55_0
[2025-05-07 17:28:13,682 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_109_A_55_0 given in one single declaration
[2025-05-07 17:28:13,682 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_109_A_55_0
[2025-05-07 17:28:13,682 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_109_A_55_0
[2025-05-07 17:28:13,682 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_111_A_55_0 given in one single declaration
[2025-05-07 17:28:13,682 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_111_A_55_0
[2025-05-07 17:28:13,682 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_111_A_55_0
[2025-05-07 17:28:13,682 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_110_A_55_0 given in one single declaration
[2025-05-07 17:28:13,682 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_110_A_55_0
[2025-05-07 17:28:13,682 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_110_A_55_0
[2025-05-07 17:28:13,683 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_117_B_52_0 given in one single declaration
[2025-05-07 17:28:13,683 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_117_B_52_0
[2025-05-07 17:28:13,683 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_117_B_52_0
[2025-05-07 17:28:13,683 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_119_B_52_0 given in one single declaration
[2025-05-07 17:28:13,683 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_119_B_52_0
[2025-05-07 17:28:13,683 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_119_B_52_0
[2025-05-07 17:28:13,683 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_118_B_52_0 given in one single declaration
[2025-05-07 17:28:13,683 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_118_B_52_0
[2025-05-07 17:28:13,684 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_118_B_52_0
[2025-05-07 17:28:13,684 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_29_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:13,684 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_29_constructor_51_55_0
[2025-05-07 17:28:13,684 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_29_constructor_51_55_0
[2025-05-07 17:28:13,684 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_116_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:13,684 INFO  L130     BoogieDeclarations]: Found specification of procedure block_116_constructor_51_55_0
[2025-05-07 17:28:13,684 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_116_constructor_51_55_0
[2025-05-07 17:28:13,684 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_113__50_55_0 given in one single declaration
[2025-05-07 17:28:13,684 INFO  L130     BoogieDeclarations]: Found specification of procedure block_113__50_55_0
[2025-05-07 17:28:13,684 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_113__50_55_0
[2025-05-07 17:28:13,685 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_112_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:13,685 INFO  L130     BoogieDeclarations]: Found specification of procedure block_112_constructor_51_55_0
[2025-05-07 17:28:13,685 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_112_constructor_51_55_0
[2025-05-07 17:28:13,685 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_115_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:13,685 INFO  L130     BoogieDeclarations]: Found specification of procedure block_115_constructor_51_55_0
[2025-05-07 17:28:13,685 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_115_constructor_51_55_0
[2025-05-07 17:28:13,685 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_114_return_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:13,685 INFO  L130     BoogieDeclarations]: Found specification of procedure block_114_return_constructor_51_55_0
[2025-05-07 17:28:13,685 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_114_return_constructor_51_55_0
[2025-05-07 17:28:13,685 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_120_C_30_0 given in one single declaration
[2025-05-07 17:28:13,685 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_120_C_30_0
[2025-05-07 17:28:13,685 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_120_C_30_0
[2025-05-07 17:28:13,686 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_122_C_30_0 given in one single declaration
[2025-05-07 17:28:13,686 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_122_C_30_0
[2025-05-07 17:28:13,686 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_122_C_30_0
[2025-05-07 17:28:13,686 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_121_C_30_0 given in one single declaration
[2025-05-07 17:28:13,686 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_121_C_30_0
[2025-05-07 17:28:13,686 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_121_C_30_0
[2025-05-07 17:28:13,686 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_126_D_27_0 given in one single declaration
[2025-05-07 17:28:13,686 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_126_D_27_0
[2025-05-07 17:28:13,686 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_126_D_27_0
[2025-05-07 17:28:13,686 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_128_D_27_0 given in one single declaration
[2025-05-07 17:28:13,686 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_128_D_27_0
[2025-05-07 17:28:13,686 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_128_D_27_0
[2025-05-07 17:28:13,686 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_127_D_27_0 given in one single declaration
[2025-05-07 17:28:13,687 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_127_D_27_0
[2025-05-07 17:28:13,687 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_127_D_27_0
[2025-05-07 17:28:13,687 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_28_constructor_26_55_0 given in one single declaration
[2025-05-07 17:28:13,687 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_28_constructor_26_55_0
[2025-05-07 17:28:13,687 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_28_constructor_26_55_0
[2025-05-07 17:28:13,687 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_125_return_constructor_26_55_0 given in one single declaration
[2025-05-07 17:28:13,687 INFO  L130     BoogieDeclarations]: Found specification of procedure block_125_return_constructor_26_55_0
[2025-05-07 17:28:13,687 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_125_return_constructor_26_55_0
[2025-05-07 17:28:13,687 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_124__25_55_0 given in one single declaration
[2025-05-07 17:28:13,687 INFO  L130     BoogieDeclarations]: Found specification of procedure block_124__25_55_0
[2025-05-07 17:28:13,687 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_124__25_55_0
[2025-05-07 17:28:13,687 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_123_constructor_26_55_0 given in one single declaration
[2025-05-07 17:28:13,687 INFO  L130     BoogieDeclarations]: Found specification of procedure block_123_constructor_26_55_0
[2025-05-07 17:28:13,688 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_123_constructor_26_55_0
[2025-05-07 17:28:13,688 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_129_E_16_0 given in one single declaration
[2025-05-07 17:28:13,688 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_129_E_16_0
[2025-05-07 17:28:13,688 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_129_E_16_0
[2025-05-07 17:28:13,688 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_131_E_16_0 given in one single declaration
[2025-05-07 17:28:13,688 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_131_E_16_0
[2025-05-07 17:28:13,688 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_131_E_16_0
[2025-05-07 17:28:13,688 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_130_E_16_0 given in one single declaration
[2025-05-07 17:28:13,688 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_130_E_16_0
[2025-05-07 17:28:13,688 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_130_E_16_0
[2025-05-07 17:28:13,688 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_138_A_55_0 given in one single declaration
[2025-05-07 17:28:13,688 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_138_A_55_0
[2025-05-07 17:28:13,688 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_138_A_55_0
[2025-05-07 17:28:13,688 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_135_F_13_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_135_F_13_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_135_F_13_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_137_F_13_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_137_F_13_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_137_F_13_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_136_F_13_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_136_F_13_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_136_F_13_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_27_constructor_12_55_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_27_constructor_12_55_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_27_constructor_12_55_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_134_return_constructor_12_55_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure block_134_return_constructor_12_55_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_134_return_constructor_12_55_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_133__11_55_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure block_133__11_55_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_133__11_55_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_132_constructor_12_55_0 given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure block_132_constructor_12_55_0
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_132_constructor_12_55_0
[2025-05-07 17:28:13,689 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:13,689 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:13,689 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:13,864 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:13,867 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:14,151 INFO  L?                        ?]: Removed 353 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:14,151 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:14,160 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:14,160 INFO  L312             CfgBuilder]: Removed 18 assume(true) statements.
[2025-05-07 17:28:14,161 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:14 BoogieIcfgContainer
[2025-05-07 17:28:14,161 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:14,162 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:14,163 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:14,165 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:14,165 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:13" (1/3) ...
[2025-05-07 17:28:14,166 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@12b77ca4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:14, skipping insertion in model container
[2025-05-07 17:28:14,166 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:13" (2/3) ...
[2025-05-07 17:28:14,166 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@12b77ca4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:14, skipping insertion in model container
[2025-05-07 17:28:14,166 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:14" (3/3) ...
[2025-05-07 17:28:14,167 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:14,178 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:14,179 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 37 procedures, 165 locations, 281 edges, 37 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:14,209 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:14,217 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;@2986623e, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:14,217 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:14,220 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 165 states, 58 states have (on average 1.1724137931034482) internal successors, (68), 68 states have internal predecessors, (68), 69 states have call successors, (71), 36 states have call predecessors, (71), 36 states have return successors, (71), 60 states have call predecessors, (71), 69 states have call successors, (71)
[2025-05-07 17:28:14,229 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:14,229 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:14,229 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:14,230 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:14,233 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:14,233 INFO  L85        PathProgramCache]: Analyzing trace with hash 948096035, now seen corresponding path program 1 times
[2025-05-07 17:28:14,238 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:14,238 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1943849638]
[2025-05-07 17:28:14,238 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:14,239 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:14,279 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:14,336 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:14,336 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:14,336 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:14,529 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:28:14,530 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:14,530 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1943849638]
[2025-05-07 17:28:14,531 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1943849638] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:14,531 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:14,533 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:14,534 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [594684506]
[2025-05-07 17:28:14,539 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:14,542 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:14,542 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:14,564 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:14,564 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:14,566 INFO  L87              Difference]: Start difference. First operand  has 165 states, 58 states have (on average 1.1724137931034482) internal successors, (68), 68 states have internal predecessors, (68), 69 states have call successors, (71), 36 states have call predecessors, (71), 36 states have return successors, (71), 60 states have call predecessors, (71), 69 states have call successors, (71) Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:28:14,700 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:14,701 INFO  L93              Difference]: Finished difference Result 165 states and 209 transitions.
[2025-05-07 17:28:14,701 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:14,703 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 2 states have call successors, (14) Word has length 51
[2025-05-07 17:28:14,703 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:14,712 INFO  L225             Difference]: With dead ends: 165
[2025-05-07 17:28:14,712 INFO  L226             Difference]: Without dead ends: 162
[2025-05-07 17:28:14,714 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:28:14,716 INFO  L437           NwaCegarLoop]: 199 mSDtfsCounter, 1 mSDsluCounter, 754 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 953 SdHoareTripleChecker+Invalid, 49 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:14,717 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 953 Invalid, 49 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:14,732 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 162 states.
[2025-05-07 17:28:14,761 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 162 to 160.
[2025-05-07 17:28:14,763 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 160 states, 57 states have (on average 1.1403508771929824) internal successors, (65), 65 states have internal predecessors, (65), 66 states have call successors, (68), 36 states have call predecessors, (68), 36 states have return successors, (68), 58 states have call predecessors, (68), 66 states have call successors, (68)
[2025-05-07 17:28:14,768 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 160 states to 160 states and 201 transitions.
[2025-05-07 17:28:14,770 INFO  L79                 Accepts]: Start accepts. Automaton has 160 states and 201 transitions. Word has length 51
[2025-05-07 17:28:14,770 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:14,770 INFO  L485      AbstractCegarLoop]: Abstraction has 160 states and 201 transitions.
[2025-05-07 17:28:14,771 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:28:14,771 INFO  L278                IsEmpty]: Start isEmpty. Operand 160 states and 201 transitions.
[2025-05-07 17:28:14,773 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:14,773 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:14,773 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]
[2025-05-07 17:28:14,774 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:14,774 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:14,774 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:14,775 INFO  L85        PathProgramCache]: Analyzing trace with hash 1267291788, now seen corresponding path program 1 times
[2025-05-07 17:28:14,775 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:14,775 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1892749744]
[2025-05-07 17:28:14,775 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:14,775 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:14,800 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:14,817 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:14,817 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:14,818 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:14,900 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:28:14,900 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:14,901 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1892749744]
[2025-05-07 17:28:14,901 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1892749744] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:14,901 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:14,901 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:14,901 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [602738339]
[2025-05-07 17:28:14,901 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:14,902 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:14,902 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:14,903 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:14,903 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:14,903 INFO  L87              Difference]: Start difference. First operand 160 states and 201 transitions. Second operand  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:28:14,956 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:14,956 INFO  L93              Difference]: Finished difference Result 159 states and 198 transitions.
[2025-05-07 17:28:14,956 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:14,956 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:28:14,957 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:14,958 INFO  L225             Difference]: With dead ends: 159
[2025-05-07 17:28:14,958 INFO  L226             Difference]: Without dead ends: 158
[2025-05-07 17:28:14,958 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:28:14,959 INFO  L437           NwaCegarLoop]: 195 mSDtfsCounter, 0 mSDsluCounter, 763 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 958 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:14,959 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 958 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:14,959 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-05-07 17:28:14,966 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 158.
[2025-05-07 17:28:14,966 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 57 states have (on average 1.1228070175438596) internal successors, (64), 64 states have internal predecessors, (64), 64 states have call successors, (66), 36 states have call predecessors, (66), 36 states have return successors, (66), 57 states have call predecessors, (66), 64 states have call successors, (66)
[2025-05-07 17:28:14,967 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 196 transitions.
[2025-05-07 17:28:14,968 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 196 transitions. Word has length 41
[2025-05-07 17:28:14,968 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:14,968 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 196 transitions.
[2025-05-07 17:28:14,968 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:28:14,968 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 196 transitions.
[2025-05-07 17:28:14,970 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:14,970 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:14,970 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]
[2025-05-07 17:28:14,971 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:14,971 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:14,971 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:14,971 INFO  L85        PathProgramCache]: Analyzing trace with hash 1665462544, now seen corresponding path program 1 times
[2025-05-07 17:28:14,971 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:14,971 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1491454182]
[2025-05-07 17:28:14,972 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:14,972 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:14,988 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:14,991 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:14,991 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:14,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:15,031 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:28:15,031 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:15,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1491454182]
[2025-05-07 17:28:15,031 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1491454182] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:15,031 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:15,031 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:15,031 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [878331323]
[2025-05-07 17:28:15,031 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:15,032 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:15,032 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:15,032 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:15,032 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:15,032 INFO  L87              Difference]: Start difference. First operand 158 states and 196 transitions. Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:28:15,090 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:15,090 INFO  L93              Difference]: Finished difference Result 159 states and 195 transitions.
[2025-05-07 17:28:15,090 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:15,091 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:28:15,091 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:15,092 INFO  L225             Difference]: With dead ends: 159
[2025-05-07 17:28:15,092 INFO  L226             Difference]: Without dead ends: 158
[2025-05-07 17:28:15,092 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:28:15,093 INFO  L437           NwaCegarLoop]: 189 mSDtfsCounter, 1 mSDsluCounter, 342 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 531 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:15,093 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 531 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:15,093 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-05-07 17:28:15,100 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 156.
[2025-05-07 17:28:15,100 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 57 states have (on average 1.105263157894737) internal successors, (63), 63 states have internal predecessors, (63), 62 states have call successors, (64), 36 states have call predecessors, (64), 36 states have return successors, (64), 56 states have call predecessors, (64), 62 states have call successors, (64)
[2025-05-07 17:28:15,102 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 191 transitions.
[2025-05-07 17:28:15,102 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 191 transitions. Word has length 41
[2025-05-07 17:28:15,102 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:15,102 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 191 transitions.
[2025-05-07 17:28:15,102 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:28:15,102 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 191 transitions.
[2025-05-07 17:28:15,104 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:15,104 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:15,104 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]
[2025-05-07 17:28:15,104 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:15,105 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:15,105 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:15,105 INFO  L85        PathProgramCache]: Analyzing trace with hash 997412977, now seen corresponding path program 1 times
[2025-05-07 17:28:15,105 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:15,105 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [226125338]
[2025-05-07 17:28:15,105 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:15,105 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:15,135 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:15,150 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:15,150 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:15,150 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:15,236 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:28:15,237 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:15,237 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [226125338]
[2025-05-07 17:28:15,237 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [226125338] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:15,237 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:15,237 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:15,237 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [647688409]
[2025-05-07 17:28:15,237 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:15,237 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:15,238 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:15,238 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:15,238 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:15,238 INFO  L87              Difference]: Start difference. First operand 156 states and 191 transitions. Second operand  has 4 states, 3 states have (on average 11.333333333333334) internal successors, (34), 4 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 3 states have return successors, (21), 4 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:15,290 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:15,290 INFO  L93              Difference]: Finished difference Result 160 states and 198 transitions.
[2025-05-07 17:28:15,290 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:15,291 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 11.333333333333334) internal successors, (34), 4 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 3 states have return successors, (21), 4 states have call predecessors, (21), 4 states have call successors, (21) Word has length 76
[2025-05-07 17:28:15,291 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:15,293 INFO  L225             Difference]: With dead ends: 160
[2025-05-07 17:28:15,293 INFO  L226             Difference]: Without dead ends: 160
[2025-05-07 17:28:15,293 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:28:15,294 INFO  L437           NwaCegarLoop]: 188 mSDtfsCounter, 1 mSDsluCounter, 340 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 528 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:15,294 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 528 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:15,295 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 160 states.
[2025-05-07 17:28:15,306 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 160 to 158.
[2025-05-07 17:28:15,307 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 58 states have (on average 1.103448275862069) internal successors, (64), 64 states have internal predecessors, (64), 62 states have call successors, (64), 36 states have call predecessors, (64), 37 states have return successors, (68), 57 states have call predecessors, (68), 62 states have call successors, (68)
[2025-05-07 17:28:15,308 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 196 transitions.
[2025-05-07 17:28:15,309 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 196 transitions. Word has length 76
[2025-05-07 17:28:15,309 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:15,309 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 196 transitions.
[2025-05-07 17:28:15,309 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 11.333333333333334) internal successors, (34), 4 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 3 states have return successors, (21), 4 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:15,310 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 196 transitions.
[2025-05-07 17:28:15,311 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:15,312 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:15,312 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]
[2025-05-07 17:28:15,312 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:15,312 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:15,312 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:15,313 INFO  L85        PathProgramCache]: Analyzing trace with hash 558495733, now seen corresponding path program 1 times
[2025-05-07 17:28:15,313 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:15,313 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [483872174]
[2025-05-07 17:28:15,313 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:15,313 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:15,345 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:15,359 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:15,359 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:15,359 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:15,438 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:28:15,438 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:15,438 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [483872174]
[2025-05-07 17:28:15,438 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [483872174] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:15,438 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:15,438 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:15,438 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1707656395]
[2025-05-07 17:28:15,438 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:15,439 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:15,439 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:15,439 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:15,439 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:15,439 INFO  L87              Difference]: Start difference. First operand 158 states and 196 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, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:15,479 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:15,479 INFO  L93              Difference]: Finished difference Result 154 states and 185 transitions.
[2025-05-07 17:28:15,479 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:15,479 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, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 4 states have call successors, (21) Word has length 76
[2025-05-07 17:28:15,480 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:15,481 INFO  L225             Difference]: With dead ends: 154
[2025-05-07 17:28:15,481 INFO  L226             Difference]: Without dead ends: 150
[2025-05-07 17:28:15,481 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:28:15,482 INFO  L437           NwaCegarLoop]: 182 mSDtfsCounter, 0 mSDsluCounter, 712 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 894 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:15,482 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 894 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:15,482 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 150 states.
[2025-05-07 17:28:15,487 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 150 to 150.
[2025-05-07 17:28:15,487 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 150 states, 57 states have (on average 1.0701754385964912) internal successors, (61), 61 states have internal predecessors, (61), 56 states have call successors, (58), 36 states have call predecessors, (58), 36 states have return successors, (58), 52 states have call predecessors, (58), 56 states have call successors, (58)
[2025-05-07 17:28:15,488 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 150 states to 150 states and 177 transitions.
[2025-05-07 17:28:15,488 INFO  L79                 Accepts]: Start accepts. Automaton has 150 states and 177 transitions. Word has length 76
[2025-05-07 17:28:15,488 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:15,488 INFO  L485      AbstractCegarLoop]: Abstraction has 150 states and 177 transitions.
[2025-05-07 17:28:15,488 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, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:15,488 INFO  L278                IsEmpty]: Start isEmpty. Operand 150 states and 177 transitions.
[2025-05-07 17:28:15,490 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:28:15,490 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:15,490 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:15,490 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:15,490 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:15,490 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:15,490 INFO  L85        PathProgramCache]: Analyzing trace with hash 1214172540, now seen corresponding path program 1 times
[2025-05-07 17:28:15,491 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:15,491 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1151205942]
[2025-05-07 17:28:15,491 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:15,491 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:15,518 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:28:15,534 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:28:15,534 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:15,534 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:15,616 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:28:15,616 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:15,616 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1151205942]
[2025-05-07 17:28:15,616 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1151205942] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:15,616 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:15,617 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:15,617 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1362829512]
[2025-05-07 17:28:15,617 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:15,617 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:15,617 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:15,618 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:15,618 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:15,618 INFO  L87              Difference]: Start difference. First operand 150 states and 177 transitions. Second operand  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 2 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 2 states have call successors, (24)
[2025-05-07 17:28:15,672 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:15,672 INFO  L93              Difference]: Finished difference Result 152 states and 178 transitions.
[2025-05-07 17:28:15,673 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:15,673 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 2 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 2 states have call successors, (24) Word has length 86
[2025-05-07 17:28:15,673 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:15,674 INFO  L225             Difference]: With dead ends: 152
[2025-05-07 17:28:15,674 INFO  L226             Difference]: Without dead ends: 147
[2025-05-07 17:28:15,674 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:28:15,675 INFO  L437           NwaCegarLoop]: 170 mSDtfsCounter, 1 mSDsluCounter, 650 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 820 SdHoareTripleChecker+Invalid, 36 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:15,675 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 820 Invalid, 36 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:15,676 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 147 states.
[2025-05-07 17:28:15,680 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 147 to 145.
[2025-05-07 17:28:15,680 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 145 states, 57 states have (on average 1.0526315789473684) internal successors, (60), 60 states have internal predecessors, (60), 51 states have call successors, (53), 36 states have call predecessors, (53), 36 states have return successors, (53), 48 states have call predecessors, (53), 51 states have call successors, (53)
[2025-05-07 17:28:15,681 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 145 states to 145 states and 166 transitions.
[2025-05-07 17:28:15,681 INFO  L79                 Accepts]: Start accepts. Automaton has 145 states and 166 transitions. Word has length 86
[2025-05-07 17:28:15,681 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:15,681 INFO  L485      AbstractCegarLoop]: Abstraction has 145 states and 166 transitions.
[2025-05-07 17:28:15,681 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 2 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 2 states have call successors, (24)
[2025-05-07 17:28:15,681 INFO  L278                IsEmpty]: Start isEmpty. Operand 145 states and 166 transitions.
[2025-05-07 17:28:15,682 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:28:15,682 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:15,683 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:15,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:15,683 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:15,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:15,683 INFO  L85        PathProgramCache]: Analyzing trace with hash 491668030, now seen corresponding path program 1 times
[2025-05-07 17:28:15,683 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:15,683 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1094919966]
[2025-05-07 17:28:15,683 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:15,683 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:15,730 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:28:15,737 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:28:15,737 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:15,737 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:15,816 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:28:15,817 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:15,817 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1094919966]
[2025-05-07 17:28:15,817 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1094919966] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:15,817 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:15,817 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:15,817 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [37407412]
[2025-05-07 17:28:15,817 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:15,817 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:15,818 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:15,818 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:15,818 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:15,818 INFO  L87              Difference]: Start difference. First operand 145 states and 166 transitions. Second operand  has 4 states, 3 states have (on average 17.666666666666668) internal successors, (53), 4 states have internal predecessors, (53), 4 states have call successors, (34), 1 states have call predecessors, (34), 3 states have return successors, (34), 4 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:28:15,841 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:15,841 INFO  L93              Difference]: Finished difference Result 147 states and 168 transitions.
[2025-05-07 17:28:15,841 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:15,841 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 17.666666666666668) internal successors, (53), 4 states have internal predecessors, (53), 4 states have call successors, (34), 1 states have call predecessors, (34), 3 states have return successors, (34), 4 states have call predecessors, (34), 4 states have call successors, (34) Word has length 121
[2025-05-07 17:28:15,842 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:15,842 INFO  L225             Difference]: With dead ends: 147
[2025-05-07 17:28:15,842 INFO  L226             Difference]: Without dead ends: 147
[2025-05-07 17:28:15,842 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:28:15,843 INFO  L437           NwaCegarLoop]: 165 mSDtfsCounter, 1 mSDsluCounter, 300 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 465 SdHoareTripleChecker+Invalid, 9 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:15,843 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 465 Invalid, 9 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:15,843 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 147 states.
[2025-05-07 17:28:15,847 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 147 to 147.
[2025-05-07 17:28:15,847 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 147 states, 58 states have (on average 1.0517241379310345) internal successors, (61), 61 states have internal predecessors, (61), 51 states have call successors, (53), 36 states have call predecessors, (53), 37 states have return successors, (54), 49 states have call predecessors, (54), 51 states have call successors, (54)
[2025-05-07 17:28:15,848 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 147 states to 147 states and 168 transitions.
[2025-05-07 17:28:15,848 INFO  L79                 Accepts]: Start accepts. Automaton has 147 states and 168 transitions. Word has length 121
[2025-05-07 17:28:15,848 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:15,849 INFO  L485      AbstractCegarLoop]: Abstraction has 147 states and 168 transitions.
[2025-05-07 17:28:15,849 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 17.666666666666668) internal successors, (53), 4 states have internal predecessors, (53), 4 states have call successors, (34), 1 states have call predecessors, (34), 3 states have return successors, (34), 4 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:28:15,849 INFO  L278                IsEmpty]: Start isEmpty. Operand 147 states and 168 transitions.
[2025-05-07 17:28:15,850 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:28:15,850 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:15,850 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:15,850 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:15,850 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:15,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:15,850 INFO  L85        PathProgramCache]: Analyzing trace with hash -50887895, now seen corresponding path program 1 times
[2025-05-07 17:28:15,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:15,850 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1024085867]
[2025-05-07 17:28:15,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:15,850 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:15,887 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:28:15,889 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:28:15,889 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:15,889 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:15,970 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:28:15,971 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:15,971 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1024085867]
[2025-05-07 17:28:15,971 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1024085867] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:15,971 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:15,971 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:15,971 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1414517969]
[2025-05-07 17:28:15,971 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:15,971 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:15,971 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:15,972 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:15,972 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:15,972 INFO  L87              Difference]: Start difference. First operand 147 states and 168 transitions. Second operand  has 4 states, 3 states have (on average 17.666666666666668) internal successors, (53), 4 states have internal predecessors, (53), 3 states have call successors, (34), 1 states have call predecessors, (34), 3 states have return successors, (34), 3 states have call predecessors, (34), 3 states have call successors, (34)
[2025-05-07 17:28:15,982 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:15,982 INFO  L93              Difference]: Finished difference Result 149 states and 169 transitions.
[2025-05-07 17:28:15,983 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:15,983 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 17.666666666666668) internal successors, (53), 4 states have internal predecessors, (53), 3 states have call successors, (34), 1 states have call predecessors, (34), 3 states have return successors, (34), 3 states have call predecessors, (34), 3 states have call successors, (34) Word has length 121
[2025-05-07 17:28:15,984 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:15,984 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:28:15,984 INFO  L226             Difference]: Without dead ends: 140
[2025-05-07 17:28:15,985 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:28:15,985 INFO  L437           NwaCegarLoop]: 167 mSDtfsCounter, 1 mSDsluCounter, 319 mSDsCounter, 0 mSdLazyCounter, 3 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 486 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 3 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:15,985 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 486 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 3 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:15,986 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-05-07 17:28:15,991 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 140.
[2025-05-07 17:28:15,991 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 58 states have (on average 1.0344827586206897) internal successors, (60), 60 states have internal predecessors, (60), 44 states have call successors, (46), 36 states have call predecessors, (46), 37 states have return successors, (47), 43 states have call predecessors, (47), 44 states have call successors, (47)
[2025-05-07 17:28:15,992 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 153 transitions.
[2025-05-07 17:28:15,992 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 153 transitions. Word has length 121
[2025-05-07 17:28:15,992 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:15,993 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 153 transitions.
[2025-05-07 17:28:15,993 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 17.666666666666668) internal successors, (53), 4 states have internal predecessors, (53), 3 states have call successors, (34), 1 states have call predecessors, (34), 3 states have return successors, (34), 3 states have call predecessors, (34), 3 states have call successors, (34)
[2025-05-07 17:28:15,993 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 153 transitions.
[2025-05-07 17:28:15,994 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:28:15,994 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:15,994 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:15,994 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:15,994 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:15,995 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:15,995 INFO  L85        PathProgramCache]: Analyzing trace with hash -1407362886, now seen corresponding path program 1 times
[2025-05-07 17:28:15,995 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:15,995 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1052954877]
[2025-05-07 17:28:15,995 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:15,995 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:16,044 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:28:16,069 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:28:16,069 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:16,069 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:16,166 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:28:16,166 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:16,166 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1052954877]
[2025-05-07 17:28:16,166 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1052954877] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:16,166 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:16,166 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:16,166 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1483275544]
[2025-05-07 17:28:16,167 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:16,167 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:16,167 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:16,167 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:16,168 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:16,168 INFO  L87              Difference]: Start difference. First operand 140 states and 153 transitions. Second operand  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 3 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 4 states have call predecessors, (34), 3 states have call successors, (34)
[2025-05-07 17:28:16,199 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:16,199 INFO  L93              Difference]: Finished difference Result 134 states and 140 transitions.
[2025-05-07 17:28:16,199 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:16,200 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 3 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 4 states have call predecessors, (34), 3 states have call successors, (34) Word has length 121
[2025-05-07 17:28:16,200 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:16,201 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:28:16,201 INFO  L226             Difference]: Without dead ends: 124
[2025-05-07 17:28:16,201 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:28:16,201 INFO  L437           NwaCegarLoop]: 135 mSDtfsCounter, 1 mSDsluCounter, 523 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 658 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:16,202 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 658 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:16,202 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-05-07 17:28:16,206 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 122.
[2025-05-07 17:28:16,206 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 53 states have (on average 1.0188679245283019) internal successors, (54), 54 states have internal predecessors, (54), 35 states have call successors, (37), 33 states have call predecessors, (37), 33 states have return successors, (37), 34 states have call predecessors, (37), 35 states have call successors, (37)
[2025-05-07 17:28:16,207 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 128 transitions.
[2025-05-07 17:28:16,207 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 128 transitions. Word has length 121
[2025-05-07 17:28:16,207 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:16,207 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 128 transitions.
[2025-05-07 17:28:16,207 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 3 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 4 states have call predecessors, (34), 3 states have call successors, (34)
[2025-05-07 17:28:16,207 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 128 transitions.
[2025-05-07 17:28:16,208 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:16,208 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:16,209 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:16,209 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:16,209 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:16,209 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:16,209 INFO  L85        PathProgramCache]: Analyzing trace with hash -433906298, now seen corresponding path program 1 times
[2025-05-07 17:28:16,209 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:16,209 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [624531828]
[2025-05-07 17:28:16,209 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:16,209 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:16,251 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:16,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:16,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:16,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:16,356 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:28:16,357 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:16,357 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [624531828]
[2025-05-07 17:28:16,357 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [624531828] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:16,357 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:16,357 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:16,357 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1608159412]
[2025-05-07 17:28:16,357 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:16,358 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:16,358 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:16,358 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:16,358 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:16,358 INFO  L87              Difference]: Start difference. First operand 122 states and 128 transitions. Second operand  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 3 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 4 states have call predecessors, (31), 3 states have call successors, (31)
[2025-05-07 17:28:16,371 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:16,371 INFO  L93              Difference]: Finished difference Result 124 states and 129 transitions.
[2025-05-07 17:28:16,372 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:16,372 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 3 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 4 states have call predecessors, (31), 3 states have call successors, (31) Word has length 111
[2025-05-07 17:28:16,372 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:16,373 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:28:16,373 INFO  L226             Difference]: Without dead ends: 120
[2025-05-07 17:28:16,373 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:28:16,373 INFO  L437           NwaCegarLoop]: 128 mSDtfsCounter, 1 mSDsluCounter, 241 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 369 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:16,373 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 369 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:16,374 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-05-07 17:28:16,377 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 120.
[2025-05-07 17:28:16,377 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 120 states, 53 states have (on average 1.0) internal successors, (53), 53 states have internal predecessors, (53), 33 states have call successors, (35), 33 states have call predecessors, (35), 33 states have return successors, (35), 33 states have call predecessors, (35), 33 states have call successors, (35)
[2025-05-07 17:28:16,378 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 120 states to 120 states and 123 transitions.
[2025-05-07 17:28:16,378 INFO  L79                 Accepts]: Start accepts. Automaton has 120 states and 123 transitions. Word has length 111
[2025-05-07 17:28:16,378 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:16,378 INFO  L485      AbstractCegarLoop]: Abstraction has 120 states and 123 transitions.
[2025-05-07 17:28:16,378 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 3 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 4 states have call predecessors, (31), 3 states have call successors, (31)
[2025-05-07 17:28:16,378 INFO  L278                IsEmpty]: Start isEmpty. Operand 120 states and 123 transitions.
[2025-05-07 17:28:16,379 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:16,379 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:16,379 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:16,379 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:16,379 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:16,379 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:16,380 INFO  L85        PathProgramCache]: Analyzing trace with hash -172451318, now seen corresponding path program 1 times
[2025-05-07 17:28:16,380 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:16,380 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [909498108]
[2025-05-07 17:28:16,380 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:16,380 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:16,408 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:16,424 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:16,424 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:16,424 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:16,855 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:28:16,856 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:16,856 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [909498108]
[2025-05-07 17:28:16,856 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [909498108] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:16,856 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:16,856 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [] total 18
[2025-05-07 17:28:16,856 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [519199686]
[2025-05-07 17:28:16,856 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:16,856 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:28:16,857 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:16,857 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:28:16,857 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=273, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:28:16,858 INFO  L87              Difference]: Start difference. First operand 120 states and 123 transitions. Second operand  has 18 states, 14 states have (on average 3.5) internal successors, (49), 15 states have internal predecessors, (49), 8 states have call successors, (31), 1 states have call predecessors, (31), 14 states have return successors, (31), 15 states have call predecessors, (31), 8 states have call successors, (31)
[2025-05-07 17:28:17,075 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:17,076 INFO  L93              Difference]: Finished difference Result 125 states and 128 transitions.
[2025-05-07 17:28:17,076 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:28:17,076 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 14 states have (on average 3.5) internal successors, (49), 15 states have internal predecessors, (49), 8 states have call successors, (31), 1 states have call predecessors, (31), 14 states have return successors, (31), 15 states have call predecessors, (31), 8 states have call successors, (31) Word has length 111
[2025-05-07 17:28:17,076 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:17,077 INFO  L225             Difference]: With dead ends: 125
[2025-05-07 17:28:17,077 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:28:17,077 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 21 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=45, Invalid=375, Unknown=0, NotChecked=0, Total=420
[2025-05-07 17:28:17,078 INFO  L437           NwaCegarLoop]: 114 mSDtfsCounter, 4 mSDsluCounter, 1781 mSDsCounter, 0 mSdLazyCounter, 240 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1895 SdHoareTripleChecker+Invalid, 242 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 240 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:17,078 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1895 Invalid, 242 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 240 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:28:17,078 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:28:17,080 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 116.
[2025-05-07 17:28:17,080 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 116 states, 51 states have (on average 1.0) internal successors, (51), 51 states have internal predecessors, (51), 32 states have call successors, (33), 32 states have call predecessors, (33), 32 states have return successors, (33), 32 states have call predecessors, (33), 32 states have call successors, (33)
[2025-05-07 17:28:17,081 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 117 transitions.
[2025-05-07 17:28:17,081 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 117 transitions. Word has length 111
[2025-05-07 17:28:17,081 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:17,081 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 117 transitions.
[2025-05-07 17:28:17,081 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 14 states have (on average 3.5) internal successors, (49), 15 states have internal predecessors, (49), 8 states have call successors, (31), 1 states have call predecessors, (31), 14 states have return successors, (31), 15 states have call predecessors, (31), 8 states have call successors, (31)
[2025-05-07 17:28:17,081 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 117 transitions.
[2025-05-07 17:28:17,082 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:17,082 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:17,082 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:17,082 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:17,082 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:17,082 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:17,082 INFO  L85        PathProgramCache]: Analyzing trace with hash -877373546, now seen corresponding path program 1 times
[2025-05-07 17:28:17,082 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:17,082 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [640113382]
[2025-05-07 17:28:17,083 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:17,083 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:17,115 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:17,137 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:17,137 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:17,137 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:17,263 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:28:17,263 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:17,263 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [640113382]
[2025-05-07 17:28:17,264 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [640113382] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:17,264 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:17,264 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:17,264 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1146331237]
[2025-05-07 17:28:17,264 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:17,264 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:17,264 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:17,265 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:17,265 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:17,265 INFO  L87              Difference]: Start difference. First operand 116 states and 117 transitions. Second operand  has 7 states, 5 states have (on average 9.8) internal successors, (49), 7 states have internal predecessors, (49), 5 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (31), 5 states have call predecessors, (31), 5 states have call successors, (31)
[2025-05-07 17:28:17,303 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:17,303 INFO  L93              Difference]: Finished difference Result 118 states and 118 transitions.
[2025-05-07 17:28:17,303 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:17,304 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 9.8) internal successors, (49), 7 states have internal predecessors, (49), 5 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (31), 5 states have call predecessors, (31), 5 states have call successors, (31) Word has length 111
[2025-05-07 17:28:17,304 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:17,304 INFO  L225             Difference]: With dead ends: 118
[2025-05-07 17:28:17,304 INFO  L226             Difference]: Without dead ends: 112
[2025-05-07 17:28:17,305 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:17,305 INFO  L437           NwaCegarLoop]: 113 mSDtfsCounter, 2 mSDsluCounter, 548 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 661 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:17,305 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 661 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:17,306 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-05-07 17:28:17,307 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 112.
[2025-05-07 17:28:17,308 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 112 states, 49 states have (on average 1.0) internal successors, (49), 49 states have internal predecessors, (49), 31 states have call successors, (31), 31 states have call predecessors, (31), 31 states have return successors, (31), 31 states have call predecessors, (31), 31 states have call successors, (31)
[2025-05-07 17:28:17,308 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 112 states to 112 states and 111 transitions.
[2025-05-07 17:28:17,308 INFO  L79                 Accepts]: Start accepts. Automaton has 112 states and 111 transitions. Word has length 111
[2025-05-07 17:28:17,309 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:17,309 INFO  L485      AbstractCegarLoop]: Abstraction has 112 states and 111 transitions.
[2025-05-07 17:28:17,309 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 9.8) internal successors, (49), 7 states have internal predecessors, (49), 5 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (31), 5 states have call predecessors, (31), 5 states have call successors, (31)
[2025-05-07 17:28:17,309 INFO  L278                IsEmpty]: Start isEmpty. Operand 112 states and 111 transitions.
[2025-05-07 17:28:17,310 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:17,310 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:17,310 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:17,310 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:28:17,310 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:17,310 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:17,310 INFO  L85        PathProgramCache]: Analyzing trace with hash 1630210256, now seen corresponding path program 1 times
[2025-05-07 17:28:17,310 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:17,310 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1587340513]
[2025-05-07 17:28:17,310 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:17,311 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:17,345 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:17,359 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:17,359 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:17,359 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:17,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:28:17,464 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:17,464 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1587340513]
[2025-05-07 17:28:17,464 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1587340513] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:17,464 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:17,464 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:17,464 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1938684679]
[2025-05-07 17:28:17,464 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:17,464 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:17,464 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:17,465 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:17,465 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:17,465 INFO  L87              Difference]: Start difference. First operand 112 states and 111 transitions. Second operand  has 7 states, 6 states have (on average 8.166666666666666) internal successors, (49), 7 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 6 states have return successors, (31), 6 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:28:17,491 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:17,491 INFO  L93              Difference]: Finished difference Result 106 states and 105 transitions.
[2025-05-07 17:28:17,492 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:17,492 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 8.166666666666666) internal successors, (49), 7 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 6 states have return successors, (31), 6 states have call predecessors, (31), 4 states have call successors, (31) Word has length 111
[2025-05-07 17:28:17,492 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:17,492 INFO  L225             Difference]: With dead ends: 106
[2025-05-07 17:28:17,492 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:17,492 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:28:17,493 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 0 mSDsluCounter, 496 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 598 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:17,493 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 598 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:17,493 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:17,493 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:17,493 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:28:17,493 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:17,493 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 111
[2025-05-07 17:28:17,493 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:17,493 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:17,493 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 8.166666666666666) internal successors, (49), 7 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 6 states have return successors, (31), 6 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:28:17,493 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:17,494 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:17,496 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:17,496 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:28:17,498 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:17,500 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:17,502 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:17 BoogieIcfgContainer
[2025-05-07 17:28:17,502 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:17,502 INFO  L158              Benchmark]: Toolchain (without parser) took 3974.16ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 140.0MB in the beginning and 192.6MB in the end (delta: -52.6MB). Peak memory consumption was 19.2MB. Max. memory is 33.6GB.
[2025-05-07 17:28:17,503 INFO  L158              Benchmark]: SmtParser took 0.32ms. Allocated memory is still 234.9MB. Free memory is still 171.4MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:17,503 INFO  L158              Benchmark]: ChcToBoogie took 43.24ms. Allocated memory is still 234.9MB. Free memory was 140.0MB in the beginning and 136.8MB in the end (delta: 3.3MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:17,503 INFO  L158              Benchmark]: Boogie Preprocessor took 72.09ms. Allocated memory is still 234.9MB. Free memory was 136.7MB in the beginning and 132.9MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:17,503 INFO  L158              Benchmark]: RCFGBuilder took 515.60ms. Allocated memory is still 234.9MB. Free memory was 132.9MB in the beginning and 148.2MB in the end (delta: -15.3MB). Peak memory consumption was 26.5MB. Max. memory is 33.6GB.
[2025-05-07 17:28:17,503 INFO  L158              Benchmark]: TraceAbstraction took 3339.50ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 147.8MB in the beginning and 192.6MB in the end (delta: -44.8MB). Peak memory consumption was 9.4MB. Max. memory is 33.6GB.
[2025-05-07 17:28:17,504 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.32ms. Allocated memory is still 234.9MB. Free memory is still 171.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 43.24ms. Allocated memory is still 234.9MB. Free memory was 140.0MB in the beginning and 136.8MB in the end (delta: 3.3MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 72.09ms. Allocated memory is still 234.9MB. Free memory was 136.7MB in the beginning and 132.9MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 515.60ms. Allocated memory is still 234.9MB. Free memory was 132.9MB in the beginning and 148.2MB in the end (delta: -15.3MB). Peak memory consumption was 26.5MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3339.50ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 147.8MB in the beginning and 192.6MB in the end (delta: -44.8MB). Peak memory consumption was 9.4MB. 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 37 procedures, 165 locations, 281 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.3s, OverallIterations: 13, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 127 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 14 mSDsluCounter, 9816 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 7769 mSDsCounter, 20 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 488 IncrementalHoareTripleChecker+Invalid, 508 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 20 mSolverCounterUnsat, 2047 mSDtfsCounter, 488 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 86 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 60 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=165occurred in iteration=0, InterpolantAutomatonStates: 82, 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, 13 MinimizatonAttempts, 10 StatesRemovedByMinimization, 5 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.6s InterpolantComputationTime, 1178 NumberOfCodeBlocks, 1178 NumberOfCodeBlocksAsserted, 13 NumberOfCheckSat, 1165 ConstructedInterpolants, 0 QuantifiedInterpolants, 1441 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 13 InterpolantComputations, 13 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:28:17,515 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
