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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:29:10,430 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:29:10,481 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ff88c18-6fdb-4827-9ccb-eeffe8a99016/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:29:10,486 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:29:10,486 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:29:10,503 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:29:10,504 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:29:10,504 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:29:10,504 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:29:10,504 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:29:10,504 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:29:10,505 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:29:10,505 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:29:10,505 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:29:10,505 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:29:10,505 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:29:10,505 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:29:10,505 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:29:10,505 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:10,505 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:29:10,506 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:29:10,506 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:29:10,506 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:29:10,506 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:29:10,506 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:29:10,507 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:29:10,507 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:29:10,702 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:29:10,707 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:29:10,709 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:29:10,710 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:29:10,710 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:29:10,711 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ff88c18-6fdb-4827-9ccb-eeffe8a99016/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_empty_base.sol_1_no_adts_000.smt2
[2025-05-07 17:29:10,712 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:29:10,714 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:29:10,942 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ff88c18-6fdb-4827-9ccb-eeffe8a99016/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_empty_base.sol_1_no_adts_000.smt2
[2025-05-07 17:29:10,945 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:29:10,945 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:29:10,946 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:29:10,946 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:29:10,946 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:29:10,948 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:10,975 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10 Unit
[2025-05-07 17:29:10,975 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:29:10,976 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:29:10,976 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:29:10,976 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:29:10,987 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:10,987 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,009 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,010 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,015 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,016 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,017 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,020 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,021 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,032 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:29:11,033 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:29:11,033 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:29:11,033 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:29:11,034 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (1/1) ...
[2025-05-07 17:29:11,036 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:11,044 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:11,053 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:29:11,055 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:29:11,065 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:29:11,065 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:29:11,065 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:29:11,065 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_4_0 given in one single declaration
[2025-05-07 17:29:11,065 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_4_0
[2025-05-07 17:29:11,065 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_4_0
[2025-05-07 17:29:11,066 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_26_A_48_0 given in one single declaration
[2025-05-07 17:29:11,066 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_26_A_48_0
[2025-05-07 17:29:11,066 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_26_A_48_0
[2025-05-07 17:29:11,066 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_115_B_45_0 given in one single declaration
[2025-05-07 17:29:11,066 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_115_B_45_0
[2025-05-07 17:29:11,066 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_115_B_45_0
[2025-05-07 17:29:11,066 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_29_constructor_44_48_0 given in one single declaration
[2025-05-07 17:29:11,066 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_29_constructor_44_48_0
[2025-05-07 17:29:11,066 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_29_constructor_44_48_0
[2025-05-07 17:29:11,066 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_114_constructor_44_48_0 given in one single declaration
[2025-05-07 17:29:11,066 INFO  L130     BoogieDeclarations]: Found specification of procedure block_114_constructor_44_48_0
[2025-05-07 17:29:11,067 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_114_constructor_44_48_0
[2025-05-07 17:29:11,067 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_112__43_48_0 given in one single declaration
[2025-05-07 17:29:11,067 INFO  L130     BoogieDeclarations]: Found specification of procedure block_112__43_48_0
[2025-05-07 17:29:11,067 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_112__43_48_0
[2025-05-07 17:29:11,067 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_111_constructor_44_48_0 given in one single declaration
[2025-05-07 17:29:11,067 INFO  L130     BoogieDeclarations]: Found specification of procedure block_111_constructor_44_48_0
[2025-05-07 17:29:11,067 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_111_constructor_44_48_0
[2025-05-07 17:29:11,067 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_113_return_constructor_44_48_0 given in one single declaration
[2025-05-07 17:29:11,067 INFO  L130     BoogieDeclarations]: Found specification of procedure block_113_return_constructor_44_48_0
[2025-05-07 17:29:11,067 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_113_return_constructor_44_48_0
[2025-05-07 17:29:11,067 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_117_B_45_0 given in one single declaration
[2025-05-07 17:29:11,067 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_117_B_45_0
[2025-05-07 17:29:11,067 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_117_B_45_0
[2025-05-07 17:29:11,067 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_116_B_45_0 given in one single declaration
[2025-05-07 17:29:11,067 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_116_B_45_0
[2025-05-07 17:29:11,068 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_116_B_45_0
[2025-05-07 17:29:11,068 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_108_A_48_0 given in one single declaration
[2025-05-07 17:29:11,068 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_108_A_48_0
[2025-05-07 17:29:11,068 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_108_A_48_0
[2025-05-07 17:29:11,068 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_110_A_48_0 given in one single declaration
[2025-05-07 17:29:11,068 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_110_A_48_0
[2025-05-07 17:29:11,068 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_110_A_48_0
[2025-05-07 17:29:11,068 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_109_A_48_0 given in one single declaration
[2025-05-07 17:29:11,068 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_109_A_48_0
[2025-05-07 17:29:11,068 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_109_A_48_0
[2025-05-07 17:29:11,068 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_118_C_28_0 given in one single declaration
[2025-05-07 17:29:11,068 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_118_C_28_0
[2025-05-07 17:29:11,068 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_118_C_28_0
[2025-05-07 17:29:11,068 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_120_C_28_0 given in one single declaration
[2025-05-07 17:29:11,069 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_120_C_28_0
[2025-05-07 17:29:11,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_120_C_28_0
[2025-05-07 17:29:11,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_119_C_28_0 given in one single declaration
[2025-05-07 17:29:11,069 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_119_C_28_0
[2025-05-07 17:29:11,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_119_C_28_0
[2025-05-07 17:29:11,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_136_A_48_0 given in one single declaration
[2025-05-07 17:29:11,069 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_136_A_48_0
[2025-05-07 17:29:11,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_136_A_48_0
[2025-05-07 17:29:11,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_133_F_11_0 given in one single declaration
[2025-05-07 17:29:11,069 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_133_F_11_0
[2025-05-07 17:29:11,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_133_F_11_0
[2025-05-07 17:29:11,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_135_F_11_0 given in one single declaration
[2025-05-07 17:29:11,069 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_135_F_11_0
[2025-05-07 17:29:11,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_135_F_11_0
[2025-05-07 17:29:11,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_134_F_11_0 given in one single declaration
[2025-05-07 17:29:11,069 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_134_F_11_0
[2025-05-07 17:29:11,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_134_F_11_0
[2025-05-07 17:29:11,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_27_constructor_10_48_0 given in one single declaration
[2025-05-07 17:29:11,070 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_27_constructor_10_48_0
[2025-05-07 17:29:11,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_27_constructor_10_48_0
[2025-05-07 17:29:11,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_132_return_constructor_10_48_0 given in one single declaration
[2025-05-07 17:29:11,070 INFO  L130     BoogieDeclarations]: Found specification of procedure block_132_return_constructor_10_48_0
[2025-05-07 17:29:11,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_132_return_constructor_10_48_0
[2025-05-07 17:29:11,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_131__9_48_0 given in one single declaration
[2025-05-07 17:29:11,070 INFO  L130     BoogieDeclarations]: Found specification of procedure block_131__9_48_0
[2025-05-07 17:29:11,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_131__9_48_0
[2025-05-07 17:29:11,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_130_constructor_10_48_0 given in one single declaration
[2025-05-07 17:29:11,070 INFO  L130     BoogieDeclarations]: Found specification of procedure block_130_constructor_10_48_0
[2025-05-07 17:29:11,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_130_constructor_10_48_0
[2025-05-07 17:29:11,071 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_127_E_14_0 given in one single declaration
[2025-05-07 17:29:11,071 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_127_E_14_0
[2025-05-07 17:29:11,071 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_127_E_14_0
[2025-05-07 17:29:11,071 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_129_E_14_0 given in one single declaration
[2025-05-07 17:29:11,071 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_129_E_14_0
[2025-05-07 17:29:11,071 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_129_E_14_0
[2025-05-07 17:29:11,071 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_128_E_14_0 given in one single declaration
[2025-05-07 17:29:11,071 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_128_E_14_0
[2025-05-07 17:29:11,071 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_128_E_14_0
[2025-05-07 17:29:11,071 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_124_D_25_0 given in one single declaration
[2025-05-07 17:29:11,071 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_124_D_25_0
[2025-05-07 17:29:11,071 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_124_D_25_0
[2025-05-07 17:29:11,071 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_126_D_25_0 given in one single declaration
[2025-05-07 17:29:11,071 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_126_D_25_0
[2025-05-07 17:29:11,071 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_126_D_25_0
[2025-05-07 17:29:11,072 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_125_D_25_0 given in one single declaration
[2025-05-07 17:29:11,072 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_125_D_25_0
[2025-05-07 17:29:11,072 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_125_D_25_0
[2025-05-07 17:29:11,072 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_28_constructor_24_48_0 given in one single declaration
[2025-05-07 17:29:11,072 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_28_constructor_24_48_0
[2025-05-07 17:29:11,072 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_28_constructor_24_48_0
[2025-05-07 17:29:11,072 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_123_return_constructor_24_48_0 given in one single declaration
[2025-05-07 17:29:11,072 INFO  L130     BoogieDeclarations]: Found specification of procedure block_123_return_constructor_24_48_0
[2025-05-07 17:29:11,072 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_123_return_constructor_24_48_0
[2025-05-07 17:29:11,072 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_122__23_48_0 given in one single declaration
[2025-05-07 17:29:11,072 INFO  L130     BoogieDeclarations]: Found specification of procedure block_122__23_48_0
[2025-05-07 17:29:11,072 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_122__23_48_0
[2025-05-07 17:29:11,072 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_121_constructor_24_48_0 given in one single declaration
[2025-05-07 17:29:11,072 INFO  L130     BoogieDeclarations]: Found specification of procedure block_121_constructor_24_48_0
[2025-05-07 17:29:11,072 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_121_constructor_24_48_0
[2025-05-07 17:29:11,072 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:29:11,072 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:29:11,072 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:29:11,244 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:29:11,247 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:29:11,522 INFO  L?                        ?]: Removed 336 outVars from TransFormulas that were not future-live.
[2025-05-07 17:29:11,522 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:29:11,536 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:29:11,536 INFO  L312             CfgBuilder]: Removed 17 assume(true) statements.
[2025-05-07 17:29:11,536 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:11 BoogieIcfgContainer
[2025-05-07 17:29:11,536 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:29:11,539 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:29:11,539 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:29:11,542 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:29:11,542 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:10" (1/3) ...
[2025-05-07 17:29:11,542 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@64ce79fc and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:29:11, skipping insertion in model container
[2025-05-07 17:29:11,543 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:10" (2/3) ...
[2025-05-07 17:29:11,543 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@64ce79fc and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:29:11, skipping insertion in model container
[2025-05-07 17:29:11,543 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:11" (3/3) ...
[2025-05-07 17:29:11,544 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:29:11,558 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:29:11,560 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 36 procedures, 161 locations, 273 edges, 36 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:29:11,588 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:29:11,595 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;@34c15385, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:29:11,596 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:29:11,598 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 161 states, 56 states have (on average 1.1785714285714286) internal successors, (66), 66 states have internal predecessors, (66), 68 states have call successors, (69), 35 states have call predecessors, (69), 35 states have return successors, (69), 59 states have call predecessors, (69), 68 states have call successors, (69)
[2025-05-07 17:29:11,607 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:11,607 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:11,608 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:29:11,608 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:11,611 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:11,611 INFO  L85        PathProgramCache]: Analyzing trace with hash 1473062770, now seen corresponding path program 1 times
[2025-05-07 17:29:11,616 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:11,617 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1229370992]
[2025-05-07 17:29:11,617 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:11,617 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:11,648 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:11,668 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:11,669 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:11,669 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:11,806 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:29:11,806 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:11,806 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1229370992]
[2025-05-07 17:29:11,807 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1229370992] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:11,807 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:11,809 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:11,810 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1658913388]
[2025-05-07 17:29:11,810 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:11,813 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:11,813 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:11,841 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:11,842 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:11,843 INFO  L87              Difference]: Start difference. First operand  has 161 states, 56 states have (on average 1.1785714285714286) internal successors, (66), 66 states have internal predecessors, (66), 68 states have call successors, (69), 35 states have call predecessors, (69), 35 states have return successors, (69), 59 states have call predecessors, (69), 68 states have call successors, (69) 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:29:11,964 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:11,965 INFO  L93              Difference]: Finished difference Result 163 states and 211 transitions.
[2025-05-07 17:29:11,966 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:11,967 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:29:11,967 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:11,973 INFO  L225             Difference]: With dead ends: 163
[2025-05-07 17:29:11,973 INFO  L226             Difference]: Without dead ends: 163
[2025-05-07 17:29:11,975 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:29:11,977 INFO  L437           NwaCegarLoop]: 202 mSDtfsCounter, 1 mSDsluCounter, 357 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 559 SdHoareTripleChecker+Invalid, 31 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:11,978 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 559 Invalid, 31 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:11,989 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 163 states.
[2025-05-07 17:29:12,010 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 163 to 161.
[2025-05-07 17:29:12,011 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 161 states, 56 states have (on average 1.1607142857142858) internal successors, (65), 65 states have internal predecessors, (65), 68 states have call successors, (69), 35 states have call predecessors, (69), 36 states have return successors, (75), 60 states have call predecessors, (75), 68 states have call successors, (75)
[2025-05-07 17:29:12,016 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 209 transitions.
[2025-05-07 17:29:12,017 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 209 transitions. Word has length 41
[2025-05-07 17:29:12,017 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:12,017 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 209 transitions.
[2025-05-07 17:29:12,017 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:29:12,018 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 209 transitions.
[2025-05-07 17:29:12,019 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:12,020 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:12,020 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:29:12,020 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:29:12,020 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:12,020 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:12,021 INFO  L85        PathProgramCache]: Analyzing trace with hash 1871233526, now seen corresponding path program 1 times
[2025-05-07 17:29:12,021 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:12,021 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1294773941]
[2025-05-07 17:29:12,021 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:12,021 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:12,046 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:12,072 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:12,072 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:12,072 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:12,173 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:29:12,174 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:12,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1294773941]
[2025-05-07 17:29:12,174 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1294773941] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:12,174 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:12,174 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:12,174 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1828858090]
[2025-05-07 17:29:12,174 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:12,175 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:12,175 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:12,175 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:12,176 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:12,176 INFO  L87              Difference]: Start difference. First operand 161 states and 209 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:29:12,238 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:12,238 INFO  L93              Difference]: Finished difference Result 157 states and 196 transitions.
[2025-05-07 17:29:12,239 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:12,239 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:29:12,239 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:12,242 INFO  L225             Difference]: With dead ends: 157
[2025-05-07 17:29:12,242 INFO  L226             Difference]: Without dead ends: 155
[2025-05-07 17:29:12,242 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:29:12,243 INFO  L437           NwaCegarLoop]: 193 mSDtfsCounter, 0 mSDsluCounter, 754 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 947 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:29:12,243 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 947 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:12,244 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 155 states.
[2025-05-07 17:29:12,252 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 155 to 155.
[2025-05-07 17:29:12,252 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 155 states, 55 states have (on average 1.1272727272727272) internal successors, (62), 62 states have internal predecessors, (62), 64 states have call successors, (65), 35 states have call predecessors, (65), 35 states have return successors, (65), 57 states have call predecessors, (65), 64 states have call successors, (65)
[2025-05-07 17:29:12,253 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 155 states to 155 states and 192 transitions.
[2025-05-07 17:29:12,253 INFO  L79                 Accepts]: Start accepts. Automaton has 155 states and 192 transitions. Word has length 41
[2025-05-07 17:29:12,253 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:12,254 INFO  L485      AbstractCegarLoop]: Abstraction has 155 states and 192 transitions.
[2025-05-07 17:29:12,254 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:29:12,254 INFO  L278                IsEmpty]: Start isEmpty. Operand 155 states and 192 transitions.
[2025-05-07 17:29:12,255 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:29:12,255 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:12,255 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:29:12,255 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:12,255 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:12,256 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:12,256 INFO  L85        PathProgramCache]: Analyzing trace with hash -1351263710, now seen corresponding path program 1 times
[2025-05-07 17:29:12,256 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:12,256 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1006949077]
[2025-05-07 17:29:12,256 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:12,256 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:12,279 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:29:12,293 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:29:12,293 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:12,293 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:12,373 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:29:12,373 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:12,373 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1006949077]
[2025-05-07 17:29:12,373 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1006949077] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:12,373 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:12,373 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:12,373 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [945358019]
[2025-05-07 17:29:12,373 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:12,374 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:12,374 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:12,374 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:12,374 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:12,375 INFO  L87              Difference]: Start difference. First operand 155 states and 192 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:29:12,467 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:12,467 INFO  L93              Difference]: Finished difference Result 157 states and 193 transitions.
[2025-05-07 17:29:12,468 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:12,468 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:29:12,468 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:12,469 INFO  L225             Difference]: With dead ends: 157
[2025-05-07 17:29:12,469 INFO  L226             Difference]: Without dead ends: 154
[2025-05-07 17:29:12,470 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:29:12,470 INFO  L437           NwaCegarLoop]: 183 mSDtfsCounter, 1 mSDsluCounter, 693 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 876 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:29:12,470 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 876 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:12,471 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 154 states.
[2025-05-07 17:29:12,477 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 154 to 152.
[2025-05-07 17:29:12,477 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 152 states, 55 states have (on average 1.1090909090909091) internal successors, (61), 61 states have internal predecessors, (61), 61 states have call successors, (62), 35 states have call predecessors, (62), 35 states have return successors, (62), 55 states have call predecessors, (62), 61 states have call successors, (62)
[2025-05-07 17:29:12,478 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 152 states to 152 states and 185 transitions.
[2025-05-07 17:29:12,478 INFO  L79                 Accepts]: Start accepts. Automaton has 152 states and 185 transitions. Word has length 51
[2025-05-07 17:29:12,478 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:12,478 INFO  L485      AbstractCegarLoop]: Abstraction has 152 states and 185 transitions.
[2025-05-07 17:29:12,479 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:29:12,479 INFO  L278                IsEmpty]: Start isEmpty. Operand 152 states and 185 transitions.
[2025-05-07 17:29:12,480 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:29:12,480 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:12,480 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:29:12,480 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:12,480 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:12,481 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:12,481 INFO  L85        PathProgramCache]: Analyzing trace with hash 27161473, now seen corresponding path program 1 times
[2025-05-07 17:29:12,481 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:12,481 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1517736498]
[2025-05-07 17:29:12,481 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:12,481 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:12,517 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:29:12,526 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:29:12,526 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:12,526 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:12,608 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:29:12,608 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:12,608 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1517736498]
[2025-05-07 17:29:12,608 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1517736498] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:12,608 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:12,609 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:12,609 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [719102253]
[2025-05-07 17:29:12,609 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:12,609 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:12,609 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:12,610 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:12,610 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:12,610 INFO  L87              Difference]: Start difference. First operand 152 states and 185 transitions. Second operand  has 4 states, 3 states have (on average 12.666666666666666) internal successors, (38), 4 states have internal predecessors, (38), 4 states have call successors, (24), 1 states have call predecessors, (24), 3 states have return successors, (24), 4 states have call predecessors, (24), 4 states have call successors, (24)
[2025-05-07 17:29:12,655 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:12,655 INFO  L93              Difference]: Finished difference Result 154 states and 189 transitions.
[2025-05-07 17:29:12,656 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:12,656 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.666666666666666) internal successors, (38), 4 states have internal predecessors, (38), 4 states have call successors, (24), 1 states have call predecessors, (24), 3 states have return successors, (24), 4 states have call predecessors, (24), 4 states have call successors, (24) Word has length 86
[2025-05-07 17:29:12,656 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:12,657 INFO  L225             Difference]: With dead ends: 154
[2025-05-07 17:29:12,657 INFO  L226             Difference]: Without dead ends: 154
[2025-05-07 17:29:12,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:29:12,657 INFO  L437           NwaCegarLoop]: 184 mSDtfsCounter, 1 mSDsluCounter, 325 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 31 SdHoareTripleChecker+Valid, 509 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:12,658 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [31 Valid, 509 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:12,658 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 154 states.
[2025-05-07 17:29:12,663 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 154 to 154.
[2025-05-07 17:29:12,664 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 154 states, 56 states have (on average 1.1071428571428572) internal successors, (62), 62 states have internal predecessors, (62), 61 states have call successors, (62), 35 states have call predecessors, (62), 36 states have return successors, (65), 56 states have call predecessors, (65), 61 states have call successors, (65)
[2025-05-07 17:29:12,665 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 189 transitions.
[2025-05-07 17:29:12,665 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 189 transitions. Word has length 86
[2025-05-07 17:29:12,665 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:12,665 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 189 transitions.
[2025-05-07 17:29:12,665 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.666666666666666) internal successors, (38), 4 states have internal predecessors, (38), 4 states have call successors, (24), 1 states have call predecessors, (24), 3 states have return successors, (24), 4 states have call predecessors, (24), 4 states have call successors, (24)
[2025-05-07 17:29:12,665 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 189 transitions.
[2025-05-07 17:29:12,666 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:29:12,667 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:12,667 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:29:12,667 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:29:12,667 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:12,667 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:12,667 INFO  L85        PathProgramCache]: Analyzing trace with hash -1831517443, now seen corresponding path program 1 times
[2025-05-07 17:29:12,667 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:12,667 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [390913436]
[2025-05-07 17:29:12,667 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:12,668 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:12,702 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:29:12,720 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:29:12,720 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:12,720 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:12,812 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:29:12,812 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:12,812 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [390913436]
[2025-05-07 17:29:12,813 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [390913436] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:12,813 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:12,813 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:12,813 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [665205738]
[2025-05-07 17:29:12,813 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:12,813 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:12,813 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:12,814 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:12,814 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:12,814 INFO  L87              Difference]: Start difference. First operand 154 states and 189 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:29:12,876 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:12,876 INFO  L93              Difference]: Finished difference Result 156 states and 190 transitions.
[2025-05-07 17:29:12,876 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:12,876 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:29:12,877 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:12,878 INFO  L225             Difference]: With dead ends: 156
[2025-05-07 17:29:12,878 INFO  L226             Difference]: Without dead ends: 151
[2025-05-07 17:29:12,878 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:29:12,879 INFO  L437           NwaCegarLoop]: 178 mSDtfsCounter, 1 mSDsluCounter, 677 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 855 SdHoareTripleChecker+Invalid, 37 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:12,879 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 855 Invalid, 37 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:12,880 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 151 states.
[2025-05-07 17:29:12,888 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 151 to 149.
[2025-05-07 17:29:12,888 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 56 states have (on average 1.0892857142857142) internal successors, (61), 61 states have internal predecessors, (61), 56 states have call successors, (57), 35 states have call predecessors, (57), 36 states have return successors, (60), 52 states have call predecessors, (60), 56 states have call successors, (60)
[2025-05-07 17:29:12,890 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 178 transitions.
[2025-05-07 17:29:12,890 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 178 transitions. Word has length 86
[2025-05-07 17:29:12,890 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:12,890 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 178 transitions.
[2025-05-07 17:29:12,890 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:29:12,890 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 178 transitions.
[2025-05-07 17:29:12,892 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:29:12,892 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:12,892 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:29:12,892 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:29:12,892 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:12,892 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:12,893 INFO  L85        PathProgramCache]: Analyzing trace with hash 488760467, now seen corresponding path program 1 times
[2025-05-07 17:29:12,893 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:12,893 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1107222130]
[2025-05-07 17:29:12,893 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:12,893 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:12,918 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:29:12,920 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:29:12,920 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:12,920 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:12,965 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:29:12,965 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:12,965 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1107222130]
[2025-05-07 17:29:12,965 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1107222130] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:12,965 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:12,965 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:12,966 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [857394571]
[2025-05-07 17:29:12,966 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:12,966 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:12,966 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:12,967 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:12,967 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:12,967 INFO  L87              Difference]: Start difference. First operand 149 states and 178 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:29:13,002 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:13,002 INFO  L93              Difference]: Finished difference Result 151 states and 179 transitions.
[2025-05-07 17:29:13,003 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:13,003 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:29:13,003 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:13,004 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:29:13,004 INFO  L226             Difference]: Without dead ends: 151
[2025-05-07 17:29:13,004 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:29:13,004 INFO  L437           NwaCegarLoop]: 173 mSDtfsCounter, 1 mSDsluCounter, 316 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 489 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:13,004 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 489 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:13,005 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 151 states.
[2025-05-07 17:29:13,009 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 151 to 149.
[2025-05-07 17:29:13,009 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 56 states have (on average 1.0892857142857142) internal successors, (61), 61 states have internal predecessors, (61), 56 states have call successors, (57), 35 states have call predecessors, (57), 36 states have return successors, (59), 52 states have call predecessors, (59), 56 states have call successors, (59)
[2025-05-07 17:29:13,010 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 177 transitions.
[2025-05-07 17:29:13,010 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 177 transitions. Word has length 76
[2025-05-07 17:29:13,010 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:13,010 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 177 transitions.
[2025-05-07 17:29:13,010 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:29:13,010 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 177 transitions.
[2025-05-07 17:29:13,011 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:29:13,011 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:13,011 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:29:13,011 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:29:13,011 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:13,012 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:13,012 INFO  L85        PathProgramCache]: Analyzing trace with hash -871818353, now seen corresponding path program 1 times
[2025-05-07 17:29:13,012 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:13,012 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1727053000]
[2025-05-07 17:29:13,012 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:13,012 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:13,036 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:29:13,056 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:29:13,056 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:13,056 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:13,131 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:29:13,131 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:13,131 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1727053000]
[2025-05-07 17:29:13,131 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1727053000] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:13,131 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:13,131 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:13,131 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [678285105]
[2025-05-07 17:29:13,131 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:13,132 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:13,132 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:13,132 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:13,132 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:13,133 INFO  L87              Difference]: Start difference. First operand 149 states and 177 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:29:13,171 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:13,171 INFO  L93              Difference]: Finished difference Result 143 states and 164 transitions.
[2025-05-07 17:29:13,172 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:13,172 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:29:13,172 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:13,173 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:29:13,173 INFO  L226             Difference]: Without dead ends: 141
[2025-05-07 17:29:13,173 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:29:13,174 INFO  L437           NwaCegarLoop]: 161 mSDtfsCounter, 0 mSDsluCounter, 629 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 790 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:13,174 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 790 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:13,175 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-05-07 17:29:13,180 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 141.
[2025-05-07 17:29:13,180 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 141 states, 55 states have (on average 1.0545454545454545) internal successors, (58), 58 states have internal predecessors, (58), 50 states have call successors, (51), 35 states have call predecessors, (51), 35 states have return successors, (51), 47 states have call predecessors, (51), 50 states have call successors, (51)
[2025-05-07 17:29:13,181 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 141 states to 141 states and 160 transitions.
[2025-05-07 17:29:13,181 INFO  L79                 Accepts]: Start accepts. Automaton has 141 states and 160 transitions. Word has length 76
[2025-05-07 17:29:13,181 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:13,182 INFO  L485      AbstractCegarLoop]: Abstraction has 141 states and 160 transitions.
[2025-05-07 17:29:13,182 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:29:13,182 INFO  L278                IsEmpty]: Start isEmpty. Operand 141 states and 160 transitions.
[2025-05-07 17:29:13,183 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:29:13,183 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:13,183 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:29:13,183 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:29:13,183 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:13,184 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:13,184 INFO  L85        PathProgramCache]: Analyzing trace with hash -635338876, now seen corresponding path program 1 times
[2025-05-07 17:29:13,184 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:13,184 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [791716473]
[2025-05-07 17:29:13,184 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:13,184 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:13,224 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:29:13,227 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:29:13,227 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:13,227 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:13,301 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:29:13,301 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:13,301 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [791716473]
[2025-05-07 17:29:13,301 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [791716473] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:13,301 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:13,301 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:13,302 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1523144415]
[2025-05-07 17:29:13,302 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:13,302 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:13,302 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:13,303 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:13,303 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:13,303 INFO  L87              Difference]: Start difference. First operand 141 states and 160 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:29:13,311 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:13,311 INFO  L93              Difference]: Finished difference Result 143 states and 161 transitions.
[2025-05-07 17:29:13,311 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:13,311 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:29:13,312 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:13,312 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:29:13,312 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:29:13,312 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:29:13,313 INFO  L437           NwaCegarLoop]: 161 mSDtfsCounter, 1 mSDsluCounter, 307 mSDsCounter, 0 mSdLazyCounter, 3 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 468 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 3 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:13,313 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 468 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 3 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:13,313 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:29:13,316 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 134.
[2025-05-07 17:29:13,316 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 55 states have (on average 1.0363636363636364) internal successors, (57), 57 states have internal predecessors, (57), 43 states have call successors, (44), 35 states have call predecessors, (44), 35 states have return successors, (44), 41 states have call predecessors, (44), 43 states have call successors, (44)
[2025-05-07 17:29:13,317 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 145 transitions.
[2025-05-07 17:29:13,317 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 145 transitions. Word has length 121
[2025-05-07 17:29:13,317 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:13,317 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 145 transitions.
[2025-05-07 17:29:13,317 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:29:13,317 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 145 transitions.
[2025-05-07 17:29:13,318 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:29:13,318 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:13,318 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:29:13,318 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:29:13,318 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:13,318 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:13,318 INFO  L85        PathProgramCache]: Analyzing trace with hash -1332311967, now seen corresponding path program 1 times
[2025-05-07 17:29:13,318 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:13,318 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1302290738]
[2025-05-07 17:29:13,318 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:13,318 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:13,353 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:29:13,373 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:29:13,373 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:13,373 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:13,960 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:29:13,960 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:13,960 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1302290738]
[2025-05-07 17:29:13,960 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1302290738] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:13,960 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:13,960 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [] total 18
[2025-05-07 17:29:13,960 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [968451393]
[2025-05-07 17:29:13,960 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:13,960 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:29:13,960 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:13,961 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:29:13,961 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=273, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:29:13,961 INFO  L87              Difference]: Start difference. First operand 134 states and 145 transitions. Second operand  has 18 states, 14 states have (on average 3.5) internal successors, (49), 15 states have internal predecessors, (49), 9 states have call successors, (31), 1 states have call predecessors, (31), 14 states have return successors, (31), 15 states have call predecessors, (31), 9 states have call successors, (31)
[2025-05-07 17:29:14,270 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:14,270 INFO  L93              Difference]: Finished difference Result 140 states and 152 transitions.
[2025-05-07 17:29:14,271 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:29:14,271 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), 9 states have call successors, (31), 1 states have call predecessors, (31), 14 states have return successors, (31), 15 states have call predecessors, (31), 9 states have call successors, (31) Word has length 111
[2025-05-07 17:29:14,271 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:14,272 INFO  L225             Difference]: With dead ends: 140
[2025-05-07 17:29:14,272 INFO  L226             Difference]: Without dead ends: 140
[2025-05-07 17:29:14,272 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:29:14,273 INFO  L437           NwaCegarLoop]: 127 mSDtfsCounter, 5 mSDsluCounter, 1985 mSDsCounter, 0 mSdLazyCounter, 327 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 2112 SdHoareTripleChecker+Invalid, 337 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 327 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:14,273 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 2112 Invalid, 337 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 327 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:29:14,273 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-05-07 17:29:14,276 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 138.
[2025-05-07 17:29:14,277 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 57 states have (on average 1.0350877192982457) internal successors, (59), 59 states have internal predecessors, (59), 43 states have call successors, (44), 35 states have call predecessors, (44), 37 states have return successors, (47), 43 states have call predecessors, (47), 43 states have call successors, (47)
[2025-05-07 17:29:14,277 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 150 transitions.
[2025-05-07 17:29:14,277 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 150 transitions. Word has length 111
[2025-05-07 17:29:14,278 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:14,278 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 150 transitions.
[2025-05-07 17:29:14,278 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), 9 states have call successors, (31), 1 states have call predecessors, (31), 14 states have return successors, (31), 15 states have call predecessors, (31), 9 states have call successors, (31)
[2025-05-07 17:29:14,278 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 150 transitions.
[2025-05-07 17:29:14,280 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:29:14,280 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:14,280 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:29:14,280 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:29:14,280 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:14,280 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:14,280 INFO  L85        PathProgramCache]: Analyzing trace with hash -1332230200, now seen corresponding path program 1 times
[2025-05-07 17:29:14,280 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:14,280 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1339958966]
[2025-05-07 17:29:14,280 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:14,280 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:14,324 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:29:14,344 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:29:14,345 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:14,345 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:14,431 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:29:14,431 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:14,431 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1339958966]
[2025-05-07 17:29:14,431 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1339958966] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:14,431 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:14,431 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:14,431 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [788360434]
[2025-05-07 17:29:14,431 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:14,432 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:14,432 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:14,432 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:14,432 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:14,433 INFO  L87              Difference]: Start difference. First operand 138 states and 150 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:29:14,448 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:14,448 INFO  L93              Difference]: Finished difference Result 142 states and 153 transitions.
[2025-05-07 17:29:14,449 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:14,449 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:29:14,449 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:14,450 INFO  L225             Difference]: With dead ends: 142
[2025-05-07 17:29:14,450 INFO  L226             Difference]: Without dead ends: 140
[2025-05-07 17:29:14,450 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:29:14,450 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 269 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 415 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:29:14,450 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 415 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:14,451 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-05-07 17:29:14,454 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 140.
[2025-05-07 17:29:14,455 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 58 states have (on average 1.0344827586206897) internal successors, (60), 60 states have internal predecessors, (60), 43 states have call successors, (44), 35 states have call predecessors, (44), 38 states have return successors, (47), 44 states have call predecessors, (47), 43 states have call successors, (47)
[2025-05-07 17:29:14,455 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 151 transitions.
[2025-05-07 17:29:14,455 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 151 transitions. Word has length 121
[2025-05-07 17:29:14,456 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:14,456 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 151 transitions.
[2025-05-07 17:29:14,456 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:29:14,456 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 151 transitions.
[2025-05-07 17:29:14,457 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:29:14,457 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:14,457 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:29:14,457 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:29:14,457 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:14,457 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:14,457 INFO  L85        PathProgramCache]: Analyzing trace with hash 1887658499, now seen corresponding path program 1 times
[2025-05-07 17:29:14,457 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:14,457 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [744131302]
[2025-05-07 17:29:14,457 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:14,458 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:14,484 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:29:14,495 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:29:14,495 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:14,495 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:14,549 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:29:14,549 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:14,549 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [744131302]
[2025-05-07 17:29:14,549 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [744131302] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:14,549 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:14,549 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:14,549 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [333025152]
[2025-05-07 17:29:14,549 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:14,550 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:14,550 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:14,550 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:14,550 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:14,550 INFO  L87              Difference]: Start difference. First operand 140 states and 151 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:29:14,571 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:14,571 INFO  L93              Difference]: Finished difference Result 140 states and 150 transitions.
[2025-05-07 17:29:14,572 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:14,572 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:29:14,572 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:14,573 INFO  L225             Difference]: With dead ends: 140
[2025-05-07 17:29:14,573 INFO  L226             Difference]: Without dead ends: 140
[2025-05-07 17:29:14,573 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:29:14,574 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 1 mSDsluCounter, 264 mSDsCounter, 0 mSdLazyCounter, 9 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 407 SdHoareTripleChecker+Invalid, 10 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 9 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:14,574 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 407 Invalid, 10 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 9 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:14,574 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-05-07 17:29:14,576 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 138.
[2025-05-07 17:29:14,577 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 57 states have (on average 1.0350877192982457) internal successors, (59), 59 states have internal predecessors, (59), 43 states have call successors, (44), 35 states have call predecessors, (44), 37 states have return successors, (45), 43 states have call predecessors, (45), 43 states have call successors, (45)
[2025-05-07 17:29:14,577 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 148 transitions.
[2025-05-07 17:29:14,577 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 148 transitions. Word has length 111
[2025-05-07 17:29:14,577 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:14,577 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 148 transitions.
[2025-05-07 17:29:14,578 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:29:14,578 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 148 transitions.
[2025-05-07 17:29:14,578 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:29:14,578 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:14,578 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:29:14,579 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:29:14,579 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:14,579 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:14,579 INFO  L85        PathProgramCache]: Analyzing trace with hash -1436718593, now seen corresponding path program 1 times
[2025-05-07 17:29:14,579 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:14,579 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1453720799]
[2025-05-07 17:29:14,579 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:14,579 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:14,612 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:29:14,637 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:29:14,637 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:14,637 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:14,730 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:29:14,730 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:14,730 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1453720799]
[2025-05-07 17:29:14,730 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1453720799] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:14,730 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:14,730 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:14,730 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [121449068]
[2025-05-07 17:29:14,731 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:14,731 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:14,731 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:14,731 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:14,732 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:14,732 INFO  L87              Difference]: Start difference. First operand 138 states and 148 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:29:14,775 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:14,776 INFO  L93              Difference]: Finished difference Result 133 states and 139 transitions.
[2025-05-07 17:29:14,776 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:14,776 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:29:14,776 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:14,777 INFO  L225             Difference]: With dead ends: 133
[2025-05-07 17:29:14,777 INFO  L226             Difference]: Without dead ends: 128
[2025-05-07 17:29:14,777 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:29:14,777 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 647 mSDsCounter, 0 mSdLazyCounter, 31 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 780 SdHoareTripleChecker+Invalid, 31 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 31 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:14,777 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 780 Invalid, 31 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 31 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:14,777 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 128 states.
[2025-05-07 17:29:14,779 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 128 to 126.
[2025-05-07 17:29:14,779 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 126 states, 55 states have (on average 1.0) internal successors, (55), 55 states have internal predecessors, (55), 35 states have call successors, (36), 35 states have call predecessors, (36), 35 states have return successors, (36), 35 states have call predecessors, (36), 35 states have call successors, (36)
[2025-05-07 17:29:14,780 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 126 states to 126 states and 127 transitions.
[2025-05-07 17:29:14,780 INFO  L79                 Accepts]: Start accepts. Automaton has 126 states and 127 transitions. Word has length 111
[2025-05-07 17:29:14,780 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:14,780 INFO  L485      AbstractCegarLoop]: Abstraction has 126 states and 127 transitions.
[2025-05-07 17:29:14,780 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:29:14,780 INFO  L278                IsEmpty]: Start isEmpty. Operand 126 states and 127 transitions.
[2025-05-07 17:29:14,781 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:29:14,781 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:14,781 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:29:14,781 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:29:14,781 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:14,781 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:14,781 INFO  L85        PathProgramCache]: Analyzing trace with hash 1902272972, now seen corresponding path program 1 times
[2025-05-07 17:29:14,781 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:14,781 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1665244263]
[2025-05-07 17:29:14,781 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:14,782 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:14,815 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:29:14,830 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:29:14,830 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:14,830 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:14,911 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:29:14,911 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:14,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1665244263]
[2025-05-07 17:29:14,911 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1665244263] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:14,911 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:14,911 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:14,911 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1846613331]
[2025-05-07 17:29:14,911 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:14,912 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:14,912 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:14,912 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:14,912 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:14,913 INFO  L87              Difference]: Start difference. First operand 126 states and 127 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), 5 states have call predecessors, (34), 3 states have call successors, (34)
[2025-05-07 17:29:14,933 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:14,933 INFO  L93              Difference]: Finished difference Result 54 states and 53 transitions.
[2025-05-07 17:29:14,934 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:14,934 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), 5 states have call predecessors, (34), 3 states have call successors, (34) Word has length 121
[2025-05-07 17:29:14,934 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:14,934 INFO  L225             Difference]: With dead ends: 54
[2025-05-07 17:29:14,934 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:29:14,934 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:29:14,934 INFO  L437           NwaCegarLoop]: 51 mSDtfsCounter, 0 mSDsluCounter, 192 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 243 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:14,935 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 243 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:14,935 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:29:14,935 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:29:14,935 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:29:14,935 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:29:14,935 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 121
[2025-05-07 17:29:14,935 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:14,935 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:29:14,935 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), 5 states have call predecessors, (34), 3 states have call successors, (34)
[2025-05-07 17:29:14,935 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:29:14,935 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:29:14,937 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:29:14,937 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:29:14,940 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:14,942 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:29:14,944 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:29:14 BoogieIcfgContainer
[2025-05-07 17:29:14,944 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:29:14,945 INFO  L158              Benchmark]: Toolchain (without parser) took 3999.52ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 143.9MB in the beginning and 100.8MB in the end (delta: 43.1MB). Peak memory consumption was 117.2MB. Max. memory is 33.6GB.
[2025-05-07 17:29:14,945 INFO  L158              Benchmark]: SmtParser took 0.21ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:14,945 INFO  L158              Benchmark]: ChcToBoogie took 29.37ms. Allocated memory is still 234.9MB. Free memory was 143.8MB in the beginning and 140.7MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:14,945 INFO  L158              Benchmark]: Boogie Preprocessor took 56.72ms. Allocated memory is still 234.9MB. Free memory was 140.7MB in the beginning and 137.0MB in the end (delta: 3.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:29:14,945 INFO  L158              Benchmark]: RCFGBuilder took 503.71ms. Allocated memory is still 234.9MB. Free memory was 137.0MB in the beginning and 154.1MB in the end (delta: -17.1MB). Peak memory consumption was 26.2MB. Max. memory is 33.6GB.
[2025-05-07 17:29:14,946 INFO  L158              Benchmark]: TraceAbstraction took 3405.93ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 153.7MB in the beginning and 100.8MB in the end (delta: 52.9MB). Peak memory consumption was 107.8MB. Max. memory is 33.6GB.
[2025-05-07 17:29:14,946 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.21ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 29.37ms. Allocated memory is still 234.9MB. Free memory was 143.8MB in the beginning and 140.7MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 56.72ms. Allocated memory is still 234.9MB. Free memory was 140.7MB in the beginning and 137.0MB in the end (delta: 3.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 503.71ms. Allocated memory is still 234.9MB. Free memory was 137.0MB in the beginning and 154.1MB in the end (delta: -17.1MB). Peak memory consumption was 26.2MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3405.93ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 153.7MB in the beginning and 100.8MB in the end (delta: 52.9MB). Peak memory consumption was 107.8MB. 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 36 procedures, 161 locations, 273 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.4s, OverallIterations: 13, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 155 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 14 mSDsluCounter, 9450 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 7415 mSDsCounter, 31 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 567 IncrementalHoareTripleChecker+Invalid, 598 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 31 mSolverCounterUnsat, 2035 mSDtfsCounter, 567 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 83 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 57 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=161occurred in iteration=0, InterpolantAutomatonStates: 79, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 13 MinimizatonAttempts, 14 StatesRemovedByMinimization, 7 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.6s InterpolantComputationTime, 1153 NumberOfCodeBlocks, 1153 NumberOfCodeBlocksAsserted, 13 NumberOfCheckSat, 1140 ConstructedInterpolants, 0 QuantifiedInterpolants, 1405 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 13 InterpolantComputations, 13 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:29:14,957 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
