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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:01,959 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:01,997 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e68a35a-77c5-4268-80c3-d699777a303d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:02,000 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:02,000 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:02,014 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:02,014 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:02,014 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:02,014 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:02,014 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:02,015 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:02,015 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:02,015 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:02,015 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:02,015 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:02,015 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:02,015 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:02,015 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:02,015 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:02,016 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:02,016 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:02,016 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:02,016 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:02,016 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:02,016 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:02,017 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:02,017 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:02,214 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:02,222 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:02,224 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:02,225 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:02,226 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:02,227 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e68a35a-77c5-4268-80c3-d699777a303d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol_0_no_adts_000.smt2
[2025-05-07 17:28:02,228 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:02,231 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:02,634 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e68a35a-77c5-4268-80c3-d699777a303d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol_0_no_adts_000.smt2
[2025-05-07 17:28:02,636 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:02,638 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:02,638 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:02,638 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:02,638 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:02,640 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,686 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02 Unit
[2025-05-07 17:28:02,686 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:02,687 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:02,687 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:02,687 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:02,698 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,698 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,734 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,734 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,747 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,750 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,753 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,758 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,761 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,782 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:02,783 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:02,783 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:02,783 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:02,784 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (1/1) ...
[2025-05-07 17:28:02,787 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:02,799 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:02,809 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:02,812 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:02,821 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:02,822 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:02,822 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:02,822 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_5_0 given in one single declaration
[2025-05-07 17:28:02,822 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_5_0
[2025-05-07 17:28:02,822 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_5_0
[2025-05-07 17:28:02,822 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_26_A_55_0 given in one single declaration
[2025-05-07 17:28:02,822 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_26_A_55_0
[2025-05-07 17:28:02,822 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_26_A_55_0
[2025-05-07 17:28:02,822 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_109_A_55_0 given in one single declaration
[2025-05-07 17:28:02,822 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_109_A_55_0
[2025-05-07 17:28:02,823 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_109_A_55_0
[2025-05-07 17:28:02,823 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:02,823 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_111_A_55_0
[2025-05-07 17:28:02,823 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_111_A_55_0
[2025-05-07 17:28:02,823 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:02,823 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_110_A_55_0
[2025-05-07 17:28:02,823 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_110_A_55_0
[2025-05-07 17:28:02,823 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_117_B_52_0 given in one single declaration
[2025-05-07 17:28:02,823 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_117_B_52_0
[2025-05-07 17:28:02,823 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_117_B_52_0
[2025-05-07 17:28:02,823 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:02,823 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_119_B_52_0
[2025-05-07 17:28:02,823 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_119_B_52_0
[2025-05-07 17:28:02,823 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:02,824 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_118_B_52_0
[2025-05-07 17:28:02,824 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_118_B_52_0
[2025-05-07 17:28:02,824 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_29_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:02,824 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_29_constructor_51_55_0
[2025-05-07 17:28:02,824 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_29_constructor_51_55_0
[2025-05-07 17:28:02,824 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_116_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:02,824 INFO  L130     BoogieDeclarations]: Found specification of procedure block_116_constructor_51_55_0
[2025-05-07 17:28:02,824 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_116_constructor_51_55_0
[2025-05-07 17:28:02,824 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_113__50_55_0 given in one single declaration
[2025-05-07 17:28:02,824 INFO  L130     BoogieDeclarations]: Found specification of procedure block_113__50_55_0
[2025-05-07 17:28:02,824 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_113__50_55_0
[2025-05-07 17:28:02,824 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_112_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:02,824 INFO  L130     BoogieDeclarations]: Found specification of procedure block_112_constructor_51_55_0
[2025-05-07 17:28:02,825 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_112_constructor_51_55_0
[2025-05-07 17:28:02,825 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_115_constructor_51_55_0 given in one single declaration
[2025-05-07 17:28:02,825 INFO  L130     BoogieDeclarations]: Found specification of procedure block_115_constructor_51_55_0
[2025-05-07 17:28:02,825 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_115_constructor_51_55_0
[2025-05-07 17:28:02,825 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:02,825 INFO  L130     BoogieDeclarations]: Found specification of procedure block_114_return_constructor_51_55_0
[2025-05-07 17:28:02,825 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_114_return_constructor_51_55_0
[2025-05-07 17:28:02,825 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_120_C_30_0 given in one single declaration
[2025-05-07 17:28:02,825 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_120_C_30_0
[2025-05-07 17:28:02,825 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_120_C_30_0
[2025-05-07 17:28:02,825 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:02,825 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_122_C_30_0
[2025-05-07 17:28:02,825 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_122_C_30_0
[2025-05-07 17:28:02,825 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:02,825 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_121_C_30_0
[2025-05-07 17:28:02,825 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_121_C_30_0
[2025-05-07 17:28:02,826 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_126_D_27_0 given in one single declaration
[2025-05-07 17:28:02,826 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_126_D_27_0
[2025-05-07 17:28:02,826 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_126_D_27_0
[2025-05-07 17:28:02,826 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:02,826 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_128_D_27_0
[2025-05-07 17:28:02,826 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_128_D_27_0
[2025-05-07 17:28:02,826 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:02,826 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_127_D_27_0
[2025-05-07 17:28:02,826 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_127_D_27_0
[2025-05-07 17:28:02,826 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_28_constructor_26_55_0 given in one single declaration
[2025-05-07 17:28:02,826 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_28_constructor_26_55_0
[2025-05-07 17:28:02,826 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_28_constructor_26_55_0
[2025-05-07 17:28:02,826 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:02,826 INFO  L130     BoogieDeclarations]: Found specification of procedure block_125_return_constructor_26_55_0
[2025-05-07 17:28:02,826 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_125_return_constructor_26_55_0
[2025-05-07 17:28:02,827 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_124__25_55_0 given in one single declaration
[2025-05-07 17:28:02,827 INFO  L130     BoogieDeclarations]: Found specification of procedure block_124__25_55_0
[2025-05-07 17:28:02,827 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_124__25_55_0
[2025-05-07 17:28:02,827 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_123_constructor_26_55_0 given in one single declaration
[2025-05-07 17:28:02,827 INFO  L130     BoogieDeclarations]: Found specification of procedure block_123_constructor_26_55_0
[2025-05-07 17:28:02,827 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_123_constructor_26_55_0
[2025-05-07 17:28:02,827 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_129_E_16_0 given in one single declaration
[2025-05-07 17:28:02,827 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_129_E_16_0
[2025-05-07 17:28:02,827 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_129_E_16_0
[2025-05-07 17:28:02,827 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:02,827 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_131_E_16_0
[2025-05-07 17:28:02,827 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_131_E_16_0
[2025-05-07 17:28:02,827 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:02,827 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_130_E_16_0
[2025-05-07 17:28:02,827 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_130_E_16_0
[2025-05-07 17:28:02,827 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:02,828 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_138_A_55_0
[2025-05-07 17:28:02,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_138_A_55_0
[2025-05-07 17:28:02,828 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_135_F_13_0 given in one single declaration
[2025-05-07 17:28:02,828 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_135_F_13_0
[2025-05-07 17:28:02,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_135_F_13_0
[2025-05-07 17:28:02,828 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:02,828 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_137_F_13_0
[2025-05-07 17:28:02,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_137_F_13_0
[2025-05-07 17:28:02,828 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:02,828 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_136_F_13_0
[2025-05-07 17:28:02,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_136_F_13_0
[2025-05-07 17:28:02,828 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_27_constructor_12_55_0 given in one single declaration
[2025-05-07 17:28:02,828 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_27_constructor_12_55_0
[2025-05-07 17:28:02,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_27_constructor_12_55_0
[2025-05-07 17:28:02,828 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:02,828 INFO  L130     BoogieDeclarations]: Found specification of procedure block_134_return_constructor_12_55_0
[2025-05-07 17:28:02,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_134_return_constructor_12_55_0
[2025-05-07 17:28:02,828 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_133__11_55_0 given in one single declaration
[2025-05-07 17:28:02,829 INFO  L130     BoogieDeclarations]: Found specification of procedure block_133__11_55_0
[2025-05-07 17:28:02,829 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_133__11_55_0
[2025-05-07 17:28:02,829 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_132_constructor_12_55_0 given in one single declaration
[2025-05-07 17:28:02,829 INFO  L130     BoogieDeclarations]: Found specification of procedure block_132_constructor_12_55_0
[2025-05-07 17:28:02,829 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_132_constructor_12_55_0
[2025-05-07 17:28:02,829 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_20_B_52_0 given in one single declaration
[2025-05-07 17:28:02,829 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_20_B_52_0
[2025-05-07 17:28:02,829 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_20_B_52_0
[2025-05-07 17:28:02,829 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_87_B_52_0 given in one single declaration
[2025-05-07 17:28:02,829 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_87_B_52_0
[2025-05-07 17:28:02,829 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_87_B_52_0
[2025-05-07 17:28:02,829 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_23_constructor_51_52_0 given in one single declaration
[2025-05-07 17:28:02,829 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_23_constructor_51_52_0
[2025-05-07 17:28:02,829 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_23_constructor_51_52_0
[2025-05-07 17:28:02,829 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_86_constructor_51_52_0 given in one single declaration
[2025-05-07 17:28:02,829 INFO  L130     BoogieDeclarations]: Found specification of procedure block_86_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_86_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_83__50_52_0 given in one single declaration
[2025-05-07 17:28:02,830 INFO  L130     BoogieDeclarations]: Found specification of procedure block_83__50_52_0
[2025-05-07 17:28:02,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_83__50_52_0
[2025-05-07 17:28:02,830 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_82_constructor_51_52_0 given in one single declaration
[2025-05-07 17:28:02,830 INFO  L130     BoogieDeclarations]: Found specification of procedure block_82_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_82_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_84_return_constructor_51_52_0 given in one single declaration
[2025-05-07 17:28:02,830 INFO  L130     BoogieDeclarations]: Found specification of procedure block_84_return_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_84_return_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_85_constructor_51_52_0 given in one single declaration
[2025-05-07 17:28:02,830 INFO  L130     BoogieDeclarations]: Found specification of procedure block_85_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_85_constructor_51_52_0
[2025-05-07 17:28:02,830 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_89_B_52_0 given in one single declaration
[2025-05-07 17:28:02,830 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_89_B_52_0
[2025-05-07 17:28:02,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_89_B_52_0
[2025-05-07 17:28:02,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_88_B_52_0 given in one single declaration
[2025-05-07 17:28:02,831 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_88_B_52_0
[2025-05-07 17:28:02,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_88_B_52_0
[2025-05-07 17:28:02,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_99_E_16_0 given in one single declaration
[2025-05-07 17:28:02,831 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_99_E_16_0
[2025-05-07 17:28:02,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_99_E_16_0
[2025-05-07 17:28:02,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_101_E_16_0 given in one single declaration
[2025-05-07 17:28:02,831 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_101_E_16_0
[2025-05-07 17:28:02,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_101_E_16_0
[2025-05-07 17:28:02,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_100_E_16_0 given in one single declaration
[2025-05-07 17:28:02,831 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_100_E_16_0
[2025-05-07 17:28:02,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_100_E_16_0
[2025-05-07 17:28:02,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_96_D_27_0 given in one single declaration
[2025-05-07 17:28:02,831 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_96_D_27_0
[2025-05-07 17:28:02,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_96_D_27_0
[2025-05-07 17:28:02,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_constructor_26_52_0 given in one single declaration
[2025-05-07 17:28:02,831 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_constructor_26_52_0
[2025-05-07 17:28:02,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_constructor_26_52_0
[2025-05-07 17:28:02,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_95_return_constructor_26_52_0 given in one single declaration
[2025-05-07 17:28:02,832 INFO  L130     BoogieDeclarations]: Found specification of procedure block_95_return_constructor_26_52_0
[2025-05-07 17:28:02,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_95_return_constructor_26_52_0
[2025-05-07 17:28:02,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_94__25_52_0 given in one single declaration
[2025-05-07 17:28:02,832 INFO  L130     BoogieDeclarations]: Found specification of procedure block_94__25_52_0
[2025-05-07 17:28:02,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_94__25_52_0
[2025-05-07 17:28:02,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_93_constructor_26_52_0 given in one single declaration
[2025-05-07 17:28:02,832 INFO  L130     BoogieDeclarations]: Found specification of procedure block_93_constructor_26_52_0
[2025-05-07 17:28:02,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_93_constructor_26_52_0
[2025-05-07 17:28:02,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_98_D_27_0 given in one single declaration
[2025-05-07 17:28:02,832 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_98_D_27_0
[2025-05-07 17:28:02,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_98_D_27_0
[2025-05-07 17:28:02,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_97_D_27_0 given in one single declaration
[2025-05-07 17:28:02,832 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_97_D_27_0
[2025-05-07 17:28:02,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_97_D_27_0
[2025-05-07 17:28:02,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_105_F_13_0 given in one single declaration
[2025-05-07 17:28:02,833 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_105_F_13_0
[2025-05-07 17:28:02,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_105_F_13_0
[2025-05-07 17:28:02,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_constructor_12_52_0 given in one single declaration
[2025-05-07 17:28:02,833 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_constructor_12_52_0
[2025-05-07 17:28:02,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_constructor_12_52_0
[2025-05-07 17:28:02,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_104_return_constructor_12_52_0 given in one single declaration
[2025-05-07 17:28:02,833 INFO  L130     BoogieDeclarations]: Found specification of procedure block_104_return_constructor_12_52_0
[2025-05-07 17:28:02,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_104_return_constructor_12_52_0
[2025-05-07 17:28:02,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_103__11_52_0 given in one single declaration
[2025-05-07 17:28:02,833 INFO  L130     BoogieDeclarations]: Found specification of procedure block_103__11_52_0
[2025-05-07 17:28:02,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_103__11_52_0
[2025-05-07 17:28:02,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_102_constructor_12_52_0 given in one single declaration
[2025-05-07 17:28:02,833 INFO  L130     BoogieDeclarations]: Found specification of procedure block_102_constructor_12_52_0
[2025-05-07 17:28:02,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_102_constructor_12_52_0
[2025-05-07 17:28:02,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_107_F_13_0 given in one single declaration
[2025-05-07 17:28:02,833 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_107_F_13_0
[2025-05-07 17:28:02,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_107_F_13_0
[2025-05-07 17:28:02,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_106_F_13_0 given in one single declaration
[2025-05-07 17:28:02,834 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_106_F_13_0
[2025-05-07 17:28:02,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_106_F_13_0
[2025-05-07 17:28:02,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_108_B_52_0 given in one single declaration
[2025-05-07 17:28:02,834 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_108_B_52_0
[2025-05-07 17:28:02,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_108_B_52_0
[2025-05-07 17:28:02,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_90_C_30_0 given in one single declaration
[2025-05-07 17:28:02,834 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_90_C_30_0
[2025-05-07 17:28:02,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_90_C_30_0
[2025-05-07 17:28:02,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_92_C_30_0 given in one single declaration
[2025-05-07 17:28:02,834 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_92_C_30_0
[2025-05-07 17:28:02,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_92_C_30_0
[2025-05-07 17:28:02,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_91_C_30_0 given in one single declaration
[2025-05-07 17:28:02,834 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_91_C_30_0
[2025-05-07 17:28:02,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_91_C_30_0
[2025-05-07 17:28:02,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:02,834 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:02,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:03,140 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:03,142 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:03,583 INFO  L?                        ?]: Removed 667 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:03,583 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:03,594 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:03,594 INFO  L312             CfgBuilder]: Removed 33 assume(true) statements.
[2025-05-07 17:28:03,594 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:03 BoogieIcfgContainer
[2025-05-07 17:28:03,594 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:03,596 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:03,596 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:03,598 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:03,599 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:02" (1/3) ...
[2025-05-07 17:28:03,599 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5cbdfdff and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:03, skipping insertion in model container
[2025-05-07 17:28:03,599 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:02" (2/3) ...
[2025-05-07 17:28:03,599 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5cbdfdff and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:03, skipping insertion in model container
[2025-05-07 17:28:03,599 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:03" (3/3) ...
[2025-05-07 17:28:03,600 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:03,610 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:03,612 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 68 procedures, 302 locations, 516 edges, 68 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:03,646 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:03,655 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;@3ee5b6dc, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:03,656 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:03,659 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 302 states, 107 states have (on average 1.1775700934579438) internal successors, (126), 126 states have internal predecessors, (126), 126 states have call successors, (130), 67 states have call predecessors, (130), 67 states have return successors, (130), 108 states have call predecessors, (130), 126 states have call successors, (130)
[2025-05-07 17:28:03,673 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:03,673 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:03,673 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:03,674 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:03,677 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:03,678 INFO  L85        PathProgramCache]: Analyzing trace with hash -175757862, now seen corresponding path program 1 times
[2025-05-07 17:28:03,683 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:03,683 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1278654477]
[2025-05-07 17:28:03,684 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:03,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:03,732 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:03,790 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:03,791 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:03,791 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:03,976 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:03,977 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:03,977 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1278654477]
[2025-05-07 17:28:03,978 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1278654477] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:03,978 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:03,980 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:03,981 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [700582809]
[2025-05-07 17:28:03,982 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:03,985 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:03,985 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,020 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:04,021 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:04,024 INFO  L87              Difference]: Start difference. First operand  has 302 states, 107 states have (on average 1.1775700934579438) internal successors, (126), 126 states have internal predecessors, (126), 126 states have call successors, (130), 67 states have call predecessors, (130), 67 states have return successors, (130), 108 states have call predecessors, (130), 126 states have call successors, (130) Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:04,180 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,180 INFO  L93              Difference]: Finished difference Result 301 states and 383 transitions.
[2025-05-07 17:28:04,181 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:04,183 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), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:04,183 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:04,190 INFO  L225             Difference]: With dead ends: 301
[2025-05-07 17:28:04,190 INFO  L226             Difference]: Without dead ends: 299
[2025-05-07 17:28:04,192 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:04,194 INFO  L437           NwaCegarLoop]: 374 mSDtfsCounter, 1 mSDsluCounter, 1463 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 1837 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:04,194 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 1837 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:04,205 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 299 states.
[2025-05-07 17:28:04,230 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 299 to 297.
[2025-05-07 17:28:04,231 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 297 states, 106 states have (on average 1.1603773584905661) internal successors, (123), 123 states have internal predecessors, (123), 123 states have call successors, (127), 67 states have call predecessors, (127), 67 states have return successors, (127), 106 states have call predecessors, (127), 123 states have call successors, (127)
[2025-05-07 17:28:04,235 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 297 states to 297 states and 377 transitions.
[2025-05-07 17:28:04,236 INFO  L79                 Accepts]: Start accepts. Automaton has 297 states and 377 transitions. Word has length 51
[2025-05-07 17:28:04,237 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:04,237 INFO  L485      AbstractCegarLoop]: Abstraction has 297 states and 377 transitions.
[2025-05-07 17:28:04,237 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), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:04,237 INFO  L278                IsEmpty]: Start isEmpty. Operand 297 states and 377 transitions.
[2025-05-07 17:28:04,239 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:04,239 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:04,239 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:04,240 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:04,240 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:04,240 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:04,240 INFO  L85        PathProgramCache]: Analyzing trace with hash 1921651614, now seen corresponding path program 1 times
[2025-05-07 17:28:04,240 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:04,240 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1512075728]
[2025-05-07 17:28:04,241 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,241 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:04,262 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:04,286 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:04,286 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,286 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:04,390 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:04,390 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:04,390 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1512075728]
[2025-05-07 17:28:04,390 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1512075728] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:04,390 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:04,390 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:04,390 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [270280684]
[2025-05-07 17:28:04,390 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:04,392 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:04,392 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,392 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:04,392 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:04,392 INFO  L87              Difference]: Start difference. First operand 297 states and 377 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:04,459 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,459 INFO  L93              Difference]: Finished difference Result 296 states and 374 transitions.
[2025-05-07 17:28:04,460 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:04,460 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:04,460 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:04,463 INFO  L225             Difference]: With dead ends: 296
[2025-05-07 17:28:04,463 INFO  L226             Difference]: Without dead ends: 295
[2025-05-07 17:28:04,463 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:04,464 INFO  L437           NwaCegarLoop]: 371 mSDtfsCounter, 0 mSDsluCounter, 1466 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1837 SdHoareTripleChecker+Invalid, 25 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:04,464 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1837 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:04,466 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 295 states.
[2025-05-07 17:28:04,484 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 295 to 295.
[2025-05-07 17:28:04,485 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 295 states, 106 states have (on average 1.150943396226415) internal successors, (122), 122 states have internal predecessors, (122), 121 states have call successors, (125), 67 states have call predecessors, (125), 67 states have return successors, (125), 105 states have call predecessors, (125), 121 states have call successors, (125)
[2025-05-07 17:28:04,488 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 295 states to 295 states and 372 transitions.
[2025-05-07 17:28:04,488 INFO  L79                 Accepts]: Start accepts. Automaton has 295 states and 372 transitions. Word has length 41
[2025-05-07 17:28:04,488 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:04,488 INFO  L485      AbstractCegarLoop]: Abstraction has 295 states and 372 transitions.
[2025-05-07 17:28:04,488 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:04,488 INFO  L278                IsEmpty]: Start isEmpty. Operand 295 states and 372 transitions.
[2025-05-07 17:28:04,490 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:04,491 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:04,491 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:04,491 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:04,491 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:04,491 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:04,491 INFO  L85        PathProgramCache]: Analyzing trace with hash -1975144926, now seen corresponding path program 1 times
[2025-05-07 17:28:04,492 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:04,492 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [140853846]
[2025-05-07 17:28:04,492 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,492 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:04,516 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:04,522 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:04,522 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,522 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:04,580 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:04,580 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:04,580 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [140853846]
[2025-05-07 17:28:04,580 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [140853846] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:04,580 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:04,580 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:04,580 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1698648149]
[2025-05-07 17:28:04,580 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:04,581 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:04,581 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,581 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:04,581 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:04,581 INFO  L87              Difference]: Start difference. First operand 295 states and 372 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:04,654 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,654 INFO  L93              Difference]: Finished difference Result 296 states and 371 transitions.
[2025-05-07 17:28:04,654 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:04,654 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:04,654 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:04,656 INFO  L225             Difference]: With dead ends: 296
[2025-05-07 17:28:04,656 INFO  L226             Difference]: Without dead ends: 295
[2025-05-07 17:28:04,657 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:04,657 INFO  L437           NwaCegarLoop]: 362 mSDtfsCounter, 1 mSDsluCounter, 685 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 1047 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:04,657 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 1047 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:04,658 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 295 states.
[2025-05-07 17:28:04,672 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 295 to 293.
[2025-05-07 17:28:04,673 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 293 states, 106 states have (on average 1.1415094339622642) internal successors, (121), 121 states have internal predecessors, (121), 119 states have call successors, (123), 67 states have call predecessors, (123), 67 states have return successors, (123), 104 states have call predecessors, (123), 119 states have call successors, (123)
[2025-05-07 17:28:04,675 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 293 states to 293 states and 367 transitions.
[2025-05-07 17:28:04,676 INFO  L79                 Accepts]: Start accepts. Automaton has 293 states and 367 transitions. Word has length 41
[2025-05-07 17:28:04,676 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:04,676 INFO  L485      AbstractCegarLoop]: Abstraction has 293 states and 367 transitions.
[2025-05-07 17:28:04,676 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:04,676 INFO  L278                IsEmpty]: Start isEmpty. Operand 293 states and 367 transitions.
[2025-05-07 17:28:04,678 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:04,678 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:04,678 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:04,678 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:04,678 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:04,679 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:04,679 INFO  L85        PathProgramCache]: Analyzing trace with hash -1535585072, now seen corresponding path program 1 times
[2025-05-07 17:28:04,679 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:04,679 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [837362543]
[2025-05-07 17:28:04,679 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,679 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:04,700 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:04,709 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:04,709 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,709 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:04,762 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:04,762 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:04,762 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [837362543]
[2025-05-07 17:28:04,762 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [837362543] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:04,762 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:04,762 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:04,762 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1883079264]
[2025-05-07 17:28:04,762 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:04,762 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:04,762 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,763 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:04,763 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:04,763 INFO  L87              Difference]: Start difference. First operand 293 states and 367 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), 6 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:28:04,809 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,809 INFO  L93              Difference]: Finished difference Result 293 states and 366 transitions.
[2025-05-07 17:28:04,809 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:04,809 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), 6 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:28:04,809 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:04,811 INFO  L225             Difference]: With dead ends: 293
[2025-05-07 17:28:04,811 INFO  L226             Difference]: Without dead ends: 291
[2025-05-07 17:28:04,811 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:04,811 INFO  L437           NwaCegarLoop]: 363 mSDtfsCounter, 0 mSDsluCounter, 1435 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1798 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:04,811 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1798 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:04,812 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 291 states.
[2025-05-07 17:28:04,818 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 291 to 291.
[2025-05-07 17:28:04,819 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 291 states, 106 states have (on average 1.1320754716981132) internal successors, (120), 120 states have internal predecessors, (120), 117 states have call successors, (121), 67 states have call predecessors, (121), 67 states have return successors, (121), 103 states have call predecessors, (121), 117 states have call successors, (121)
[2025-05-07 17:28:04,820 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 291 states to 291 states and 362 transitions.
[2025-05-07 17:28:04,821 INFO  L79                 Accepts]: Start accepts. Automaton has 291 states and 362 transitions. Word has length 41
[2025-05-07 17:28:04,821 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:04,821 INFO  L485      AbstractCegarLoop]: Abstraction has 291 states and 362 transitions.
[2025-05-07 17:28:04,821 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), 6 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:28:04,821 INFO  L278                IsEmpty]: Start isEmpty. Operand 291 states and 362 transitions.
[2025-05-07 17:28:04,822 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:04,822 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:04,822 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:04,822 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:04,822 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:04,822 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:04,822 INFO  L85        PathProgramCache]: Analyzing trace with hash -459850156, now seen corresponding path program 1 times
[2025-05-07 17:28:04,822 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:04,822 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1357449515]
[2025-05-07 17:28:04,822 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,822 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:04,839 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:04,842 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:04,842 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,842 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:04,891 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:04,892 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:04,892 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1357449515]
[2025-05-07 17:28:04,892 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1357449515] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:04,892 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:04,892 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:04,892 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1641781901]
[2025-05-07 17:28:04,892 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:04,892 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:04,892 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,893 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:04,893 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:04,893 INFO  L87              Difference]: Start difference. First operand 291 states and 362 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:04,937 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,937 INFO  L93              Difference]: Finished difference Result 292 states and 361 transitions.
[2025-05-07 17:28:04,937 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:04,938 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:04,938 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:04,939 INFO  L225             Difference]: With dead ends: 292
[2025-05-07 17:28:04,939 INFO  L226             Difference]: Without dead ends: 291
[2025-05-07 17:28:04,939 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:04,940 INFO  L437           NwaCegarLoop]: 354 mSDtfsCounter, 1 mSDsluCounter, 681 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 1035 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:04,940 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 1035 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:04,940 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 291 states.
[2025-05-07 17:28:04,946 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 291 to 289.
[2025-05-07 17:28:04,946 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 289 states, 106 states have (on average 1.1226415094339623) internal successors, (119), 119 states have internal predecessors, (119), 115 states have call successors, (119), 67 states have call predecessors, (119), 67 states have return successors, (119), 102 states have call predecessors, (119), 115 states have call successors, (119)
[2025-05-07 17:28:04,948 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 289 states to 289 states and 357 transitions.
[2025-05-07 17:28:04,948 INFO  L79                 Accepts]: Start accepts. Automaton has 289 states and 357 transitions. Word has length 41
[2025-05-07 17:28:04,948 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:04,948 INFO  L485      AbstractCegarLoop]: Abstraction has 289 states and 357 transitions.
[2025-05-07 17:28:04,948 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:04,948 INFO  L278                IsEmpty]: Start isEmpty. Operand 289 states and 357 transitions.
[2025-05-07 17:28:04,949 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:04,949 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:04,949 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:04,949 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:04,949 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:04,949 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:04,950 INFO  L85        PathProgramCache]: Analyzing trace with hash -225930870, now seen corresponding path program 1 times
[2025-05-07 17:28:04,950 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:04,950 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [542930741]
[2025-05-07 17:28:04,950 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,950 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:04,964 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:04,973 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:04,973 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,973 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,028 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:05,028 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,028 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [542930741]
[2025-05-07 17:28:05,029 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [542930741] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,029 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,029 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:05,029 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [575314637]
[2025-05-07 17:28:05,029 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,029 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:05,029 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,030 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:05,030 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:05,030 INFO  L87              Difference]: Start difference. First operand 289 states and 357 transitions. 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:05,109 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,109 INFO  L93              Difference]: Finished difference Result 291 states and 358 transitions.
[2025-05-07 17:28:05,110 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:05,110 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:05,110 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,111 INFO  L225             Difference]: With dead ends: 291
[2025-05-07 17:28:05,111 INFO  L226             Difference]: Without dead ends: 288
[2025-05-07 17:28:05,111 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:05,112 INFO  L437           NwaCegarLoop]: 348 mSDtfsCounter, 1 mSDsluCounter, 1353 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 1701 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:05,112 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 1701 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:05,112 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 288 states.
[2025-05-07 17:28:05,118 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 288 to 286.
[2025-05-07 17:28:05,119 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 286 states, 106 states have (on average 1.1132075471698113) internal successors, (118), 118 states have internal predecessors, (118), 112 states have call successors, (116), 67 states have call predecessors, (116), 67 states have return successors, (116), 100 states have call predecessors, (116), 112 states have call successors, (116)
[2025-05-07 17:28:05,120 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 286 states to 286 states and 350 transitions.
[2025-05-07 17:28:05,120 INFO  L79                 Accepts]: Start accepts. Automaton has 286 states and 350 transitions. Word has length 51
[2025-05-07 17:28:05,120 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,120 INFO  L485      AbstractCegarLoop]: Abstraction has 286 states and 350 transitions.
[2025-05-07 17:28:05,120 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:05,120 INFO  L278                IsEmpty]: Start isEmpty. Operand 286 states and 350 transitions.
[2025-05-07 17:28:05,121 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:28:05,121 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,122 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:05,122 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:05,122 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,122 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,122 INFO  L85        PathProgramCache]: Analyzing trace with hash -172906095, now seen corresponding path program 1 times
[2025-05-07 17:28:05,122 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,122 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1665580991]
[2025-05-07 17:28:05,122 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,122 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,154 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:28:05,166 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:28:05,166 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,166 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,258 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:05,258 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,258 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1665580991]
[2025-05-07 17:28:05,258 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1665580991] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,258 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,259 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:05,259 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1679226543]
[2025-05-07 17:28:05,259 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,259 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:05,259 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,260 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:05,260 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:05,260 INFO  L87              Difference]: Start difference. First operand 286 states and 350 transitions. Second operand  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 4 states have call predecessors, (24), 3 states have call successors, (24)
[2025-05-07 17:28:05,313 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,313 INFO  L93              Difference]: Finished difference Result 284 states and 343 transitions.
[2025-05-07 17:28:05,314 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:05,314 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), 3 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 4 states have call predecessors, (24), 3 states have call successors, (24) Word has length 86
[2025-05-07 17:28:05,314 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,316 INFO  L225             Difference]: With dead ends: 284
[2025-05-07 17:28:05,316 INFO  L226             Difference]: Without dead ends: 283
[2025-05-07 17:28:05,316 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:05,317 INFO  L437           NwaCegarLoop]: 336 mSDtfsCounter, 1 mSDsluCounter, 1321 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 1657 SdHoareTripleChecker+Invalid, 31 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:05,317 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 1657 Invalid, 31 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:05,318 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 283 states.
[2025-05-07 17:28:05,324 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 283 to 281.
[2025-05-07 17:28:05,325 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 281 states, 106 states have (on average 1.1037735849056605) internal successors, (117), 117 states have internal predecessors, (117), 107 states have call successors, (111), 67 states have call predecessors, (111), 67 states have return successors, (111), 96 states have call predecessors, (111), 107 states have call successors, (111)
[2025-05-07 17:28:05,326 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 281 states to 281 states and 339 transitions.
[2025-05-07 17:28:05,326 INFO  L79                 Accepts]: Start accepts. Automaton has 281 states and 339 transitions. Word has length 86
[2025-05-07 17:28:05,326 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,326 INFO  L485      AbstractCegarLoop]: Abstraction has 281 states and 339 transitions.
[2025-05-07 17:28:05,326 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), 3 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 4 states have call predecessors, (24), 3 states have call successors, (24)
[2025-05-07 17:28:05,326 INFO  L278                IsEmpty]: Start isEmpty. Operand 281 states and 339 transitions.
[2025-05-07 17:28:05,327 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:05,327 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,327 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:05,327 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:05,327 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,328 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,328 INFO  L85        PathProgramCache]: Analyzing trace with hash -861686250, now seen corresponding path program 1 times
[2025-05-07 17:28:05,328 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,328 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [529016454]
[2025-05-07 17:28:05,328 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,328 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,355 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:05,358 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:05,358 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,359 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,421 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:05,421 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,421 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [529016454]
[2025-05-07 17:28:05,421 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [529016454] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,421 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,421 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:05,421 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [334963501]
[2025-05-07 17:28:05,421 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,422 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:05,422 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,422 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:05,422 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:05,422 INFO  L87              Difference]: Start difference. First operand 281 states and 339 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), 3 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:05,454 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,454 INFO  L93              Difference]: Finished difference Result 285 states and 344 transitions.
[2025-05-07 17:28:05,454 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:05,454 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), 3 states have call predecessors, (21), 4 states have call successors, (21) Word has length 76
[2025-05-07 17:28:05,455 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,455 INFO  L225             Difference]: With dead ends: 285
[2025-05-07 17:28:05,456 INFO  L226             Difference]: Without dead ends: 285
[2025-05-07 17:28:05,456 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:05,456 INFO  L437           NwaCegarLoop]: 336 mSDtfsCounter, 1 mSDsluCounter, 652 mSDsCounter, 0 mSdLazyCounter, 14 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 988 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 14 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:05,456 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 988 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 14 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:05,457 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 285 states.
[2025-05-07 17:28:05,462 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 285 to 283.
[2025-05-07 17:28:05,463 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 283 states, 107 states have (on average 1.102803738317757) internal successors, (118), 118 states have internal predecessors, (118), 107 states have call successors, (111), 67 states have call predecessors, (111), 68 states have return successors, (113), 97 states have call predecessors, (113), 107 states have call successors, (113)
[2025-05-07 17:28:05,464 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 283 states to 283 states and 342 transitions.
[2025-05-07 17:28:05,464 INFO  L79                 Accepts]: Start accepts. Automaton has 283 states and 342 transitions. Word has length 76
[2025-05-07 17:28:05,464 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,464 INFO  L485      AbstractCegarLoop]: Abstraction has 283 states and 342 transitions.
[2025-05-07 17:28:05,464 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), 3 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:05,464 INFO  L278                IsEmpty]: Start isEmpty. Operand 283 states and 342 transitions.
[2025-05-07 17:28:05,465 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:05,465 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,465 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:05,465 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:05,466 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,466 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,466 INFO  L85        PathProgramCache]: Analyzing trace with hash 108903954, now seen corresponding path program 1 times
[2025-05-07 17:28:05,466 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,466 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2019619138]
[2025-05-07 17:28:05,466 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,466 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,490 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:05,507 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:05,507 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,507 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,605 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:05,605 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,605 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2019619138]
[2025-05-07 17:28:05,605 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2019619138] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,605 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,605 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:05,605 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [575636175]
[2025-05-07 17:28:05,606 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,606 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:05,606 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,606 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:05,606 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:05,607 INFO  L87              Difference]: Start difference. First operand 283 states and 342 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), 6 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:05,649 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,649 INFO  L93              Difference]: Finished difference Result 278 states and 331 transitions.
[2025-05-07 17:28:05,650 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:05,650 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), 6 states have call predecessors, (21), 4 states have call successors, (21) Word has length 76
[2025-05-07 17:28:05,650 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,652 INFO  L225             Difference]: With dead ends: 278
[2025-05-07 17:28:05,652 INFO  L226             Difference]: Without dead ends: 275
[2025-05-07 17:28:05,652 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:05,653 INFO  L437           NwaCegarLoop]: 328 mSDtfsCounter, 0 mSDsluCounter, 1297 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1625 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:05,653 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1625 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:05,654 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 275 states.
[2025-05-07 17:28:05,661 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 275 to 275.
[2025-05-07 17:28:05,662 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 275 states, 106 states have (on average 1.0849056603773586) internal successors, (115), 115 states have internal predecessors, (115), 101 states have call successors, (105), 67 states have call predecessors, (105), 67 states have return successors, (105), 92 states have call predecessors, (105), 101 states have call successors, (105)
[2025-05-07 17:28:05,664 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 275 states to 275 states and 325 transitions.
[2025-05-07 17:28:05,664 INFO  L79                 Accepts]: Start accepts. Automaton has 275 states and 325 transitions. Word has length 76
[2025-05-07 17:28:05,664 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,664 INFO  L485      AbstractCegarLoop]: Abstraction has 275 states and 325 transitions.
[2025-05-07 17:28:05,664 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), 6 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:28:05,664 INFO  L278                IsEmpty]: Start isEmpty. Operand 275 states and 325 transitions.
[2025-05-07 17:28:05,666 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:05,666 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,666 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:05,666 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:05,666 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,667 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,667 INFO  L85        PathProgramCache]: Analyzing trace with hash 2050180309, now seen corresponding path program 1 times
[2025-05-07 17:28:05,667 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,667 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [538853312]
[2025-05-07 17:28:05,667 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,667 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,688 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:05,694 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:05,694 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,694 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,735 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:05,735 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,735 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [538853312]
[2025-05-07 17:28:05,736 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [538853312] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,736 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,736 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:05,736 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [998007756]
[2025-05-07 17:28:05,736 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,736 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:05,736 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,736 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:05,736 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:05,736 INFO  L87              Difference]: Start difference. First operand 275 states and 325 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:05,780 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,781 INFO  L93              Difference]: Finished difference Result 279 states and 332 transitions.
[2025-05-07 17:28:05,781 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:05,781 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:05,781 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,782 INFO  L225             Difference]: With dead ends: 279
[2025-05-07 17:28:05,782 INFO  L226             Difference]: Without dead ends: 279
[2025-05-07 17:28:05,783 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:05,783 INFO  L437           NwaCegarLoop]: 325 mSDtfsCounter, 1 mSDsluCounter, 613 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 938 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:05,783 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 938 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:05,784 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 279 states.
[2025-05-07 17:28:05,788 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 279 to 277.
[2025-05-07 17:28:05,789 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 277 states, 107 states have (on average 1.0841121495327102) internal successors, (116), 116 states have internal predecessors, (116), 101 states have call successors, (105), 67 states have call predecessors, (105), 68 states have return successors, (109), 93 states have call predecessors, (109), 101 states have call successors, (109)
[2025-05-07 17:28:05,790 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 277 states to 277 states and 330 transitions.
[2025-05-07 17:28:05,790 INFO  L79                 Accepts]: Start accepts. Automaton has 277 states and 330 transitions. Word has length 76
[2025-05-07 17:28:05,790 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,790 INFO  L485      AbstractCegarLoop]: Abstraction has 277 states and 330 transitions.
[2025-05-07 17:28:05,790 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:05,790 INFO  L278                IsEmpty]: Start isEmpty. Operand 277 states and 330 transitions.
[2025-05-07 17:28:05,791 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:05,791 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,791 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:05,791 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:05,791 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,791 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,792 INFO  L85        PathProgramCache]: Analyzing trace with hash 1611263065, now seen corresponding path program 1 times
[2025-05-07 17:28:05,792 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,792 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [56690851]
[2025-05-07 17:28:05,792 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,792 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,815 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:05,825 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:05,825 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,825 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,891 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:05,891 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,891 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [56690851]
[2025-05-07 17:28:05,892 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [56690851] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,892 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,892 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:05,892 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1090765345]
[2025-05-07 17:28:05,892 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,892 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:05,892 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,893 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:05,893 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:05,893 INFO  L87              Difference]: Start difference. First operand 277 states and 330 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:05,933 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,933 INFO  L93              Difference]: Finished difference Result 273 states and 319 transitions.
[2025-05-07 17:28:05,933 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:05,933 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:05,934 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,935 INFO  L225             Difference]: With dead ends: 273
[2025-05-07 17:28:05,935 INFO  L226             Difference]: Without dead ends: 269
[2025-05-07 17:28:05,935 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:05,936 INFO  L437           NwaCegarLoop]: 316 mSDtfsCounter, 0 mSDsluCounter, 1248 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1564 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:05,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1564 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:05,937 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 269 states.
[2025-05-07 17:28:05,943 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 269 to 269.
[2025-05-07 17:28:05,944 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 269 states, 106 states have (on average 1.0660377358490567) internal successors, (113), 113 states have internal predecessors, (113), 95 states have call successors, (99), 67 states have call predecessors, (99), 67 states have return successors, (99), 88 states have call predecessors, (99), 95 states have call successors, (99)
[2025-05-07 17:28:05,946 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 269 states to 269 states and 311 transitions.
[2025-05-07 17:28:05,946 INFO  L79                 Accepts]: Start accepts. Automaton has 269 states and 311 transitions. Word has length 76
[2025-05-07 17:28:05,946 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,946 INFO  L485      AbstractCegarLoop]: Abstraction has 269 states and 311 transitions.
[2025-05-07 17:28:05,946 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:05,946 INFO  L278                IsEmpty]: Start isEmpty. Operand 269 states and 311 transitions.
[2025-05-07 17:28:05,948 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:28:05,948 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,948 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:05,948 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:05,948 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,949 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,949 INFO  L85        PathProgramCache]: Analyzing trace with hash -556308796, now seen corresponding path program 1 times
[2025-05-07 17:28:05,949 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,949 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1288583116]
[2025-05-07 17:28:05,949 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,949 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,980 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:28:05,995 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:28:05,995 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,995 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,061 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:06,061 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,061 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1288583116]
[2025-05-07 17:28:06,061 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1288583116] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,061 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,061 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:06,062 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1677592666]
[2025-05-07 17:28:06,062 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,062 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:06,062 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,062 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:06,063 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:06,063 INFO  L87              Difference]: Start difference. First operand 269 states and 311 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:06,115 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,115 INFO  L93              Difference]: Finished difference Result 271 states and 312 transitions.
[2025-05-07 17:28:06,115 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:06,115 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:06,115 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,116 INFO  L225             Difference]: With dead ends: 271
[2025-05-07 17:28:06,116 INFO  L226             Difference]: Without dead ends: 266
[2025-05-07 17:28:06,116 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:06,117 INFO  L437           NwaCegarLoop]: 304 mSDtfsCounter, 1 mSDsluCounter, 1186 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 1490 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:06,117 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 1490 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:06,117 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 266 states.
[2025-05-07 17:28:06,121 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 266 to 264.
[2025-05-07 17:28:06,122 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 264 states, 106 states have (on average 1.0566037735849056) internal successors, (112), 112 states have internal predecessors, (112), 90 states have call successors, (94), 67 states have call predecessors, (94), 67 states have return successors, (94), 84 states have call predecessors, (94), 90 states have call successors, (94)
[2025-05-07 17:28:06,123 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 264 states to 264 states and 300 transitions.
[2025-05-07 17:28:06,123 INFO  L79                 Accepts]: Start accepts. Automaton has 264 states and 300 transitions. Word has length 86
[2025-05-07 17:28:06,123 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,123 INFO  L485      AbstractCegarLoop]: Abstraction has 264 states and 300 transitions.
[2025-05-07 17:28:06,123 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:06,123 INFO  L278                IsEmpty]: Start isEmpty. Operand 264 states and 300 transitions.
[2025-05-07 17:28:06,124 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:28:06,124 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,124 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:06,124 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:28:06,124 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,125 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,125 INFO  L85        PathProgramCache]: Analyzing trace with hash 1983846113, now seen corresponding path program 1 times
[2025-05-07 17:28:06,125 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,125 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [766749452]
[2025-05-07 17:28:06,125 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,125 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,162 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:28:06,164 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:28:06,164 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,164 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,252 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:06,252 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,252 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [766749452]
[2025-05-07 17:28:06,252 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [766749452] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,252 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,252 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:06,252 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1070903109]
[2025-05-07 17:28:06,252 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,253 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:06,253 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,253 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:06,253 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:06,253 INFO  L87              Difference]: Start difference. First operand 264 states and 300 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:06,265 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,265 INFO  L93              Difference]: Finished difference Result 266 states and 301 transitions.
[2025-05-07 17:28:06,266 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:06,266 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:06,266 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,267 INFO  L225             Difference]: With dead ends: 266
[2025-05-07 17:28:06,267 INFO  L226             Difference]: Without dead ends: 257
[2025-05-07 17:28:06,267 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:06,268 INFO  L437           NwaCegarLoop]: 300 mSDtfsCounter, 1 mSDsluCounter, 584 mSDsCounter, 0 mSdLazyCounter, 3 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 884 SdHoareTripleChecker+Invalid, 4 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 3 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:06,268 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 884 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 3 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:06,268 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 257 states.
[2025-05-07 17:28:06,272 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 257 to 257.
[2025-05-07 17:28:06,272 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 257 states, 106 states have (on average 1.0471698113207548) internal successors, (111), 111 states have internal predecessors, (111), 83 states have call successors, (87), 67 states have call predecessors, (87), 67 states have return successors, (87), 78 states have call predecessors, (87), 83 states have call successors, (87)
[2025-05-07 17:28:06,273 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 257 states to 257 states and 285 transitions.
[2025-05-07 17:28:06,273 INFO  L79                 Accepts]: Start accepts. Automaton has 257 states and 285 transitions. Word has length 121
[2025-05-07 17:28:06,273 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,273 INFO  L485      AbstractCegarLoop]: Abstraction has 257 states and 285 transitions.
[2025-05-07 17:28:06,274 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:06,274 INFO  L278                IsEmpty]: Start isEmpty. Operand 257 states and 285 transitions.
[2025-05-07 17:28:06,275 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:28:06,275 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,275 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:06,275 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:28:06,275 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,275 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,275 INFO  L85        PathProgramCache]: Analyzing trace with hash -446874812, now seen corresponding path program 1 times
[2025-05-07 17:28:06,275 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,275 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [478617835]
[2025-05-07 17:28:06,275 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,275 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,314 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:28:06,324 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:28:06,324 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,324 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,409 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:06,409 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,409 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [478617835]
[2025-05-07 17:28:06,409 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [478617835] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,409 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,409 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:06,410 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [469998977]
[2025-05-07 17:28:06,410 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,410 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:06,410 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,411 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:06,411 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:06,411 INFO  L87              Difference]: Start difference. First operand 257 states and 285 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:06,431 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,431 INFO  L93              Difference]: Finished difference Result 259 states and 287 transitions.
[2025-05-07 17:28:06,432 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:06,432 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:06,432 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,434 INFO  L225             Difference]: With dead ends: 259
[2025-05-07 17:28:06,434 INFO  L226             Difference]: Without dead ends: 259
[2025-05-07 17:28:06,434 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:06,435 INFO  L437           NwaCegarLoop]: 284 mSDtfsCounter, 1 mSDsluCounter, 547 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 831 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:06,435 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 831 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:06,436 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 259 states.
[2025-05-07 17:28:06,445 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 259 to 259.
[2025-05-07 17:28:06,446 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 259 states, 107 states have (on average 1.0467289719626167) internal successors, (112), 112 states have internal predecessors, (112), 83 states have call successors, (87), 67 states have call predecessors, (87), 68 states have return successors, (88), 79 states have call predecessors, (88), 83 states have call successors, (88)
[2025-05-07 17:28:06,449 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 259 states to 259 states and 287 transitions.
[2025-05-07 17:28:06,449 INFO  L79                 Accepts]: Start accepts. Automaton has 259 states and 287 transitions. Word has length 121
[2025-05-07 17:28:06,450 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,450 INFO  L485      AbstractCegarLoop]: Abstraction has 259 states and 287 transitions.
[2025-05-07 17:28:06,450 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:06,450 INFO  L278                IsEmpty]: Start isEmpty. Operand 259 states and 287 transitions.
[2025-05-07 17:28:06,452 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:28:06,452 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,452 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:06,452 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:28:06,452 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,452 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,453 INFO  L85        PathProgramCache]: Analyzing trace with hash 906252348, now seen corresponding path program 1 times
[2025-05-07 17:28:06,453 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,453 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1019406969]
[2025-05-07 17:28:06,453 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,453 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,508 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:28:06,544 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:28:06,544 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,544 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,680 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:06,680 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,680 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1019406969]
[2025-05-07 17:28:06,680 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1019406969] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,680 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,680 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:06,680 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1922514876]
[2025-05-07 17:28:06,680 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,681 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:06,681 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,681 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:06,681 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:06,681 INFO  L87              Difference]: Start difference. First operand 259 states and 287 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:06,713 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,713 INFO  L93              Difference]: Finished difference Result 253 states and 274 transitions.
[2025-05-07 17:28:06,713 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:06,714 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:06,714 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,714 INFO  L225             Difference]: With dead ends: 253
[2025-05-07 17:28:06,714 INFO  L226             Difference]: Without dead ends: 243
[2025-05-07 17:28:06,715 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:06,715 INFO  L437           NwaCegarLoop]: 269 mSDtfsCounter, 1 mSDsluCounter, 1059 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1328 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:06,715 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1328 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:06,716 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 243 states.
[2025-05-07 17:28:06,720 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 243 to 241.
[2025-05-07 17:28:06,720 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 241 states, 102 states have (on average 1.0392156862745099) internal successors, (106), 106 states have internal predecessors, (106), 74 states have call successors, (78), 64 states have call predecessors, (78), 64 states have return successors, (78), 70 states have call predecessors, (78), 74 states have call successors, (78)
[2025-05-07 17:28:06,721 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 241 states to 241 states and 262 transitions.
[2025-05-07 17:28:06,721 INFO  L79                 Accepts]: Start accepts. Automaton has 241 states and 262 transitions. Word has length 121
[2025-05-07 17:28:06,721 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,721 INFO  L485      AbstractCegarLoop]: Abstraction has 241 states and 262 transitions.
[2025-05-07 17:28:06,721 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:06,721 INFO  L278                IsEmpty]: Start isEmpty. Operand 241 states and 262 transitions.
[2025-05-07 17:28:06,722 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:06,722 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,722 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:06,722 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:28:06,722 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,723 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,723 INFO  L85        PathProgramCache]: Analyzing trace with hash -1845561447, now seen corresponding path program 1 times
[2025-05-07 17:28:06,723 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,723 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [625412351]
[2025-05-07 17:28:06,723 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,723 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,759 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:06,776 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:06,776 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,776 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,838 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:06,838 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,838 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [625412351]
[2025-05-07 17:28:06,838 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [625412351] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,838 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,838 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:06,838 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [199780675]
[2025-05-07 17:28:06,838 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,839 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:06,839 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,839 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:06,839 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:06,839 INFO  L87              Difference]: Start difference. First operand 241 states and 262 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:06,851 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,851 INFO  L93              Difference]: Finished difference Result 243 states and 263 transitions.
[2025-05-07 17:28:06,852 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:06,852 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:06,852 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,853 INFO  L225             Difference]: With dead ends: 243
[2025-05-07 17:28:06,853 INFO  L226             Difference]: Without dead ends: 239
[2025-05-07 17:28:06,853 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:06,853 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 508 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 769 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:06,854 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 769 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:06,854 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 239 states.
[2025-05-07 17:28:06,857 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 239 to 239.
[2025-05-07 17:28:06,858 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 239 states, 102 states have (on average 1.0294117647058822) internal successors, (105), 105 states have internal predecessors, (105), 72 states have call successors, (76), 64 states have call predecessors, (76), 64 states have return successors, (76), 69 states have call predecessors, (76), 72 states have call successors, (76)
[2025-05-07 17:28:06,858 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 239 states to 239 states and 257 transitions.
[2025-05-07 17:28:06,858 INFO  L79                 Accepts]: Start accepts. Automaton has 239 states and 257 transitions. Word has length 111
[2025-05-07 17:28:06,859 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,859 INFO  L485      AbstractCegarLoop]: Abstraction has 239 states and 257 transitions.
[2025-05-07 17:28:06,859 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:06,859 INFO  L278                IsEmpty]: Start isEmpty. Operand 239 states and 257 transitions.
[2025-05-07 17:28:06,860 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:06,860 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,860 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:06,860 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:28:06,860 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,860 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,860 INFO  L85        PathProgramCache]: Analyzing trace with hash 494871631, now seen corresponding path program 1 times
[2025-05-07 17:28:06,860 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,860 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1583129077]
[2025-05-07 17:28:06,860 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,860 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,894 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:06,906 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:06,906 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,906 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,332 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:07,332 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:07,332 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1583129077]
[2025-05-07 17:28:07,332 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1583129077] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:07,332 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:07,332 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [] total 18
[2025-05-07 17:28:07,332 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1741655949]
[2025-05-07 17:28:07,332 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:07,333 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:28:07,333 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:07,333 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:28:07,334 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=273, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:28:07,334 INFO  L87              Difference]: Start difference. First operand 239 states and 257 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:07,544 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,544 INFO  L93              Difference]: Finished difference Result 244 states and 262 transitions.
[2025-05-07 17:28:07,545 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:28:07,545 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:07,545 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,546 INFO  L225             Difference]: With dead ends: 244
[2025-05-07 17:28:07,546 INFO  L226             Difference]: Without dead ends: 235
[2025-05-07 17:28:07,547 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:07,547 INFO  L437           NwaCegarLoop]: 244 mSDtfsCounter, 4 mSDsluCounter, 3866 mSDsCounter, 0 mSdLazyCounter, 224 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 4110 SdHoareTripleChecker+Invalid, 226 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 224 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:07,547 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 4110 Invalid, 226 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 224 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:28:07,548 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 235 states.
[2025-05-07 17:28:07,554 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 235 to 235.
[2025-05-07 17:28:07,554 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 235 states, 100 states have (on average 1.03) internal successors, (103), 103 states have internal predecessors, (103), 71 states have call successors, (74), 63 states have call predecessors, (74), 63 states have return successors, (74), 68 states have call predecessors, (74), 71 states have call successors, (74)
[2025-05-07 17:28:07,555 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 235 states to 235 states and 251 transitions.
[2025-05-07 17:28:07,556 INFO  L79                 Accepts]: Start accepts. Automaton has 235 states and 251 transitions. Word has length 111
[2025-05-07 17:28:07,556 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,556 INFO  L485      AbstractCegarLoop]: Abstraction has 235 states and 251 transitions.
[2025-05-07 17:28:07,556 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:07,556 INFO  L278                IsEmpty]: Start isEmpty. Operand 235 states and 251 transitions.
[2025-05-07 17:28:07,558 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:07,558 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:07,558 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:07,558 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:28:07,558 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:07,558 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:07,558 INFO  L85        PathProgramCache]: Analyzing trace with hash -1072494431, now seen corresponding path program 1 times
[2025-05-07 17:28:07,559 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:07,559 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [381377913]
[2025-05-07 17:28:07,559 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,559 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:07,597 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:07,623 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:07,624 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:07,624 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,715 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:07,715 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:07,715 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [381377913]
[2025-05-07 17:28:07,715 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [381377913] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:07,716 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:07,716 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:07,716 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1170911484]
[2025-05-07 17:28:07,716 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:07,716 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:07,716 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:07,716 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:07,716 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:07,716 INFO  L87              Difference]: Start difference. First operand 235 states and 251 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:07,753 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,753 INFO  L93              Difference]: Finished difference Result 242 states and 258 transitions.
[2025-05-07 17:28:07,754 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:07,754 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:07,754 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,755 INFO  L225             Difference]: With dead ends: 242
[2025-05-07 17:28:07,755 INFO  L226             Difference]: Without dead ends: 231
[2025-05-07 17:28:07,756 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:07,756 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 1228 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1476 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:07,756 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1476 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:07,757 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 231 states.
[2025-05-07 17:28:07,761 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 231 to 231.
[2025-05-07 17:28:07,762 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 231 states, 98 states have (on average 1.030612244897959) internal successors, (101), 101 states have internal predecessors, (101), 70 states have call successors, (72), 62 states have call predecessors, (72), 62 states have return successors, (72), 67 states have call predecessors, (72), 70 states have call successors, (72)
[2025-05-07 17:28:07,763 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 231 states to 231 states and 245 transitions.
[2025-05-07 17:28:07,763 INFO  L79                 Accepts]: Start accepts. Automaton has 231 states and 245 transitions. Word has length 111
[2025-05-07 17:28:07,764 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,764 INFO  L485      AbstractCegarLoop]: Abstraction has 231 states and 245 transitions.
[2025-05-07 17:28:07,764 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:07,764 INFO  L278                IsEmpty]: Start isEmpty. Operand 231 states and 245 transitions.
[2025-05-07 17:28:07,765 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:07,765 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:07,765 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:07,765 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:28:07,765 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:07,766 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:07,766 INFO  L85        PathProgramCache]: Analyzing trace with hash -1584106467, now seen corresponding path program 1 times
[2025-05-07 17:28:07,766 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:07,766 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1995313947]
[2025-05-07 17:28:07,766 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,766 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:07,807 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:07,822 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:07,823 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:07,823 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,920 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:07,920 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:07,920 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1995313947]
[2025-05-07 17:28:07,920 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1995313947] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:07,920 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:07,920 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:07,920 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [213376626]
[2025-05-07 17:28:07,920 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:07,920 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:07,920 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:07,921 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:07,921 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:07,921 INFO  L87              Difference]: Start difference. First operand 231 states and 245 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:07,952 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,952 INFO  L93              Difference]: Finished difference Result 220 states and 233 transitions.
[2025-05-07 17:28:07,953 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:07,953 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:07,953 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,954 INFO  L225             Difference]: With dead ends: 220
[2025-05-07 17:28:07,954 INFO  L226             Difference]: Without dead ends: 128
[2025-05-07 17:28:07,954 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:07,954 INFO  L437           NwaCegarLoop]: 231 mSDtfsCounter, 1 mSDsluCounter, 1141 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1372 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:07,954 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1372 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:07,955 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 128 states.
[2025-05-07 17:28:07,956 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 128 to 128.
[2025-05-07 17:28:07,957 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 53 states have (on average 1.0377358490566038) internal successors, (55), 55 states have internal predecessors, (55), 41 states have call successors, (43), 33 states have call predecessors, (43), 33 states have return successors, (43), 39 states have call predecessors, (43), 41 states have call successors, (43)
[2025-05-07 17:28:07,957 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 141 transitions.
[2025-05-07 17:28:07,957 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 141 transitions. Word has length 111
[2025-05-07 17:28:07,957 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,957 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 141 transitions.
[2025-05-07 17:28:07,957 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:07,958 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 141 transitions.
[2025-05-07 17:28:07,958 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:07,958 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:07,958 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:07,958 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:28:07,958 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:07,959 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:07,959 INFO  L85        PathProgramCache]: Analyzing trace with hash -1559320952, now seen corresponding path program 1 times
[2025-05-07 17:28:07,959 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:07,959 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1639888226]
[2025-05-07 17:28:07,959 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,959 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:07,991 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:08,006 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:08,006 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,006 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,126 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:08,126 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,126 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1639888226]
[2025-05-07 17:28:08,126 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1639888226] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,126 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,126 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:08,126 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [358845354]
[2025-05-07 17:28:08,126 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:08,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,127 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:08,127 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:08,127 INFO  L87              Difference]: Start difference. First operand 128 states and 141 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), 6 states have call predecessors, (31), 5 states have call successors, (31)
[2025-05-07 17:28:08,182 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:08,182 INFO  L93              Difference]: Finished difference Result 132 states and 146 transitions.
[2025-05-07 17:28:08,182 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:08,182 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), 6 states have call predecessors, (31), 5 states have call successors, (31) Word has length 111
[2025-05-07 17:28:08,183 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:08,183 INFO  L225             Difference]: With dead ends: 132
[2025-05-07 17:28:08,183 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:28:08,183 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:08,183 INFO  L437           NwaCegarLoop]: 137 mSDtfsCounter, 1 mSDsluCounter, 530 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 667 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:08,184 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 667 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:08,184 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:28:08,186 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 130.
[2025-05-07 17:28:08,186 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 54 states have (on average 1.037037037037037) internal successors, (56), 56 states have internal predecessors, (56), 41 states have call successors, (43), 33 states have call predecessors, (43), 34 states have return successors, (44), 40 states have call predecessors, (44), 41 states have call successors, (44)
[2025-05-07 17:28:08,186 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 143 transitions.
[2025-05-07 17:28:08,187 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 143 transitions. Word has length 111
[2025-05-07 17:28:08,187 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:08,187 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 143 transitions.
[2025-05-07 17:28:08,187 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), 6 states have call predecessors, (31), 5 states have call successors, (31)
[2025-05-07 17:28:08,187 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 143 transitions.
[2025-05-07 17:28:08,188 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:08,188 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:08,188 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:08,188 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:28:08,188 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:08,188 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:08,188 INFO  L85        PathProgramCache]: Analyzing trace with hash -1296419550, now seen corresponding path program 1 times
[2025-05-07 17:28:08,188 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:08,188 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [396975757]
[2025-05-07 17:28:08,188 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:08,188 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:08,225 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:08,234 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:08,234 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,234 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,281 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:08,281 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [396975757]
[2025-05-07 17:28:08,282 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [396975757] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,282 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,282 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:08,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1735045452]
[2025-05-07 17:28:08,282 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,282 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:08,282 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,283 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:08,283 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:08,283 INFO  L87              Difference]: Start difference. First operand 130 states and 143 transitions. Second operand  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 4 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:28:08,302 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:08,302 INFO  L93              Difference]: Finished difference Result 134 states and 147 transitions.
[2025-05-07 17:28:08,302 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:08,302 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), 4 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 4 states have call predecessors, (31), 4 states have call successors, (31) Word has length 111
[2025-05-07 17:28:08,303 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:08,303 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:28:08,303 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:28:08,303 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:08,304 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 1 mSDsluCounter, 269 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 412 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:08,304 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 412 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:08,304 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:28:08,306 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 132.
[2025-05-07 17:28:08,306 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 132 states, 55 states have (on average 1.0363636363636364) internal successors, (57), 57 states have internal predecessors, (57), 41 states have call successors, (43), 33 states have call predecessors, (43), 35 states have return successors, (45), 41 states have call predecessors, (45), 41 states have call successors, (45)
[2025-05-07 17:28:08,307 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 132 states to 132 states and 145 transitions.
[2025-05-07 17:28:08,307 INFO  L79                 Accepts]: Start accepts. Automaton has 132 states and 145 transitions. Word has length 111
[2025-05-07 17:28:08,307 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:08,307 INFO  L485      AbstractCegarLoop]: Abstraction has 132 states and 145 transitions.
[2025-05-07 17:28:08,307 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), 4 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 4 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:28:08,307 INFO  L278                IsEmpty]: Start isEmpty. Operand 132 states and 145 transitions.
[2025-05-07 17:28:08,307 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:08,308 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:08,308 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:08,308 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:28:08,308 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:08,308 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:08,308 INFO  L85        PathProgramCache]: Analyzing trace with hash 142119706, now seen corresponding path program 1 times
[2025-05-07 17:28:08,308 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:08,308 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [105845378]
[2025-05-07 17:28:08,308 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:08,308 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:08,339 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:08,341 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:08,341 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,341 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,387 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:08,388 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,388 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [105845378]
[2025-05-07 17:28:08,388 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [105845378] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,388 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,388 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:08,388 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [500827667]
[2025-05-07 17:28:08,388 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,388 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:08,388 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,389 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:08,389 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:08,389 INFO  L87              Difference]: Start difference. First operand 132 states and 145 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), 3 states have call predecessors, (31), 3 states have call successors, (31)
[2025-05-07 17:28:08,396 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:08,396 INFO  L93              Difference]: Finished difference Result 134 states and 146 transitions.
[2025-05-07 17:28:08,396 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:08,397 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), 3 states have call predecessors, (31), 3 states have call successors, (31) Word has length 111
[2025-05-07 17:28:08,397 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:08,398 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:28:08,398 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:28:08,398 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:08,399 INFO  L437           NwaCegarLoop]: 142 mSDtfsCounter, 1 mSDsluCounter, 271 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 413 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:08,400 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 413 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:08,401 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:28:08,403 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 116.
[2025-05-07 17:28:08,404 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:08,405 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 117 transitions.
[2025-05-07 17:28:08,405 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 117 transitions. Word has length 111
[2025-05-07 17:28:08,405 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:08,405 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 117 transitions.
[2025-05-07 17:28:08,405 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), 3 states have call predecessors, (31), 3 states have call successors, (31)
[2025-05-07 17:28:08,405 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 117 transitions.
[2025-05-07 17:28:08,406 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:08,406 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:08,406 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:08,406 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:28:08,406 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:08,406 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:08,407 INFO  L85        PathProgramCache]: Analyzing trace with hash -870842722, now seen corresponding path program 1 times
[2025-05-07 17:28:08,407 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:08,407 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1243434729]
[2025-05-07 17:28:08,407 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:08,407 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:08,443 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:08,467 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:08,467 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,467 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,939 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:08,939 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,939 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1243434729]
[2025-05-07 17:28:08,939 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1243434729] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,939 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,939 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [] total 18
[2025-05-07 17:28:08,939 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [417128415]
[2025-05-07 17:28:08,939 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,940 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:28:08,940 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,940 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:28:08,940 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=273, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:28:08,940 INFO  L87              Difference]: Start difference. First operand 116 states and 117 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:09,120 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:09,121 INFO  L93              Difference]: Finished difference Result 120 states and 120 transitions.
[2025-05-07 17:28:09,121 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:28:09,121 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:09,122 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:09,122 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:28:09,122 INFO  L226             Difference]: Without dead ends: 112
[2025-05-07 17:28:09,122 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 21 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=45, Invalid=375, Unknown=0, NotChecked=0, Total=420
[2025-05-07 17:28:09,123 INFO  L437           NwaCegarLoop]: 104 mSDtfsCounter, 5 mSDsluCounter, 1624 mSDsCounter, 0 mSdLazyCounter, 222 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1728 SdHoareTripleChecker+Invalid, 226 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 222 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:09,123 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1728 Invalid, 226 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 222 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:09,124 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-05-07 17:28:09,126 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 112.
[2025-05-07 17:28:09,126 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:09,127 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 112 states to 112 states and 111 transitions.
[2025-05-07 17:28:09,127 INFO  L79                 Accepts]: Start accepts. Automaton has 112 states and 111 transitions. Word has length 111
[2025-05-07 17:28:09,127 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:09,127 INFO  L485      AbstractCegarLoop]: Abstraction has 112 states and 111 transitions.
[2025-05-07 17:28:09,127 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:09,127 INFO  L278                IsEmpty]: Start isEmpty. Operand 112 states and 111 transitions.
[2025-05-07 17:28:09,128 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:28:09,128 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:09,128 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:09,128 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:28:09,128 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:09,128 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:09,129 INFO  L85        PathProgramCache]: Analyzing trace with hash -1255050214, now seen corresponding path program 1 times
[2025-05-07 17:28:09,129 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:09,129 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1515119016]
[2025-05-07 17:28:09,129 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:09,129 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:09,166 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:28:09,179 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:28:09,179 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:09,179 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:09,286 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:09,286 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:09,286 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1515119016]
[2025-05-07 17:28:09,286 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1515119016] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:09,286 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:09,286 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:09,286 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [960089147]
[2025-05-07 17:28:09,286 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:09,287 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:09,287 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:09,287 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:09,287 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:09,287 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:09,313 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:09,313 INFO  L93              Difference]: Finished difference Result 106 states and 105 transitions.
[2025-05-07 17:28:09,314 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:09,314 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:09,314 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:09,314 INFO  L225             Difference]: With dead ends: 106
[2025-05-07 17:28:09,314 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:09,314 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:09,315 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:09,315 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:09,315 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:09,316 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:09,316 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:09,316 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:09,316 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 111
[2025-05-07 17:28:09,316 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:09,316 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:09,316 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:09,316 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:09,316 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:09,318 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:09,319 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24
[2025-05-07 17:28:09,322 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:09,324 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:09,326 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:09 BoogieIcfgContainer
[2025-05-07 17:28:09,327 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:09,327 INFO  L158              Benchmark]: Toolchain (without parser) took 6689.91ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 173.5MB in the beginning and 342.8MB in the end (delta: -169.3MB). Peak memory consumption was 23.2MB. Max. memory is 33.6GB.
[2025-05-07 17:28:09,327 INFO  L158              Benchmark]: SmtParser took 0.28ms. Allocated memory is still 234.9MB. Free memory is still 167.9MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:09,328 INFO  L158              Benchmark]: ChcToBoogie took 48.47ms. Allocated memory is still 234.9MB. Free memory was 173.5MB in the beginning and 168.2MB in the end (delta: 5.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:09,328 INFO  L158              Benchmark]: Boogie Preprocessor took 95.27ms. Allocated memory is still 234.9MB. Free memory was 168.2MB in the beginning and 162.9MB in the end (delta: 5.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:09,328 INFO  L158              Benchmark]: RCFGBuilder took 811.42ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 162.9MB in the beginning and 221.0MB in the end (delta: -58.1MB). Peak memory consumption was 75.9MB. Max. memory is 33.6GB.
[2025-05-07 17:28:09,328 INFO  L158              Benchmark]: TraceAbstraction took 5730.99ms. Allocated memory was 318.8MB in the beginning and 436.2MB in the end (delta: 117.4MB). Free memory was 220.2MB in the beginning and 342.8MB in the end (delta: -122.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:09,329 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.28ms. Allocated memory is still 234.9MB. Free memory is still 167.9MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 48.47ms. Allocated memory is still 234.9MB. Free memory was 173.5MB in the beginning and 168.2MB in the end (delta: 5.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 95.27ms. Allocated memory is still 234.9MB. Free memory was 168.2MB in the beginning and 162.9MB in the end (delta: 5.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 811.42ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 162.9MB in the beginning and 221.0MB in the end (delta: -58.1MB). Peak memory consumption was 75.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 5730.99ms. Allocated memory was 318.8MB in the beginning and 436.2MB in the end (delta: 117.4MB). Free memory was 220.2MB in the beginning and 342.8MB in the end (delta: -122.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 68 procedures, 302 locations, 516 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 5.7s, OverallIterations: 24, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 196 SdHoareTripleChecker+Valid, 1.0s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 26 mSDsluCounter, 32105 SdHoareTripleChecker+Invalid, 0.9s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 25523 mSDsCounter, 34 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 906 IncrementalHoareTripleChecker+Invalid, 940 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 34 mSolverCounterUnsat, 6582 mSDtfsCounter, 906 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 161 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 113 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.5s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=302occurred in iteration=0, InterpolantAutomatonStates: 154, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 24 MinimizatonAttempts, 22 StatesRemovedByMinimization, 11 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.2s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 2.7s InterpolantComputationTime, 2104 NumberOfCodeBlocks, 2104 NumberOfCodeBlocksAsserted, 24 NumberOfCheckSat, 2080 ConstructedInterpolants, 0 QuantifiedInterpolants, 2593 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 24 InterpolantComputations, 24 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:09,342 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
