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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:25:17,097 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:25:17,137 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9ad01920-6127-4f91-a050-e379e8528407/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:25:17,140 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:25:17,140 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:25:17,157 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:25:17,158 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:25:17,158 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:25:17,158 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:25:17,158 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:25:17,159 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:25:17,159 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:25:17,159 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:25:17,159 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:25:17,159 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:25:17,159 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:25:17,159 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:25:17,159 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:25:17,160 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:17,160 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:25:17,160 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:25:17,160 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:25:17,160 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:25:17,160 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:25:17,160 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:25:17,161 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:25:17,161 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:25:17,361 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:25:17,366 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:25:17,368 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:25:17,369 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:25:17,369 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:25:17,370 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9ad01920-6127-4f91-a050-e379e8528407/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/super_function_assert.sol_0_no_adts_000.smt2
[2025-05-07 17:25:17,371 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:25:17,373 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:25:17,734 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9ad01920-6127-4f91-a050-e379e8528407/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/super_function_assert.sol_0_no_adts_000.smt2
[2025-05-07 17:25:17,736 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:25:17,737 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:25:17,738 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:25:17,738 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:25:17,738 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:25:17,740 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,793 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17 Unit
[2025-05-07 17:25:17,793 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:25:17,794 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:25:17,794 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:25:17,794 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:25:17,805 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,805 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,842 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,843 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,857 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,860 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,863 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,869 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,873 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,897 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:25:17,898 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:25:17,898 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:25:17,898 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:25:17,899 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (1/1) ...
[2025-05-07 17:25:17,902 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:17,912 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:17,922 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:25:17,924 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:25:17,935 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:25:17,935 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:25:17,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:25:17,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_11_0 given in one single declaration
[2025-05-07 17:25:17,936 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_11_0
[2025-05-07 17:25:17,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_11_0
[2025-05-07 17:25:17,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_proxy__18_44_0 given in one single declaration
[2025-05-07 17:25:17,936 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_proxy__18_44_0
[2025-05-07 17:25:17,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_proxy__18_44_0
[2025-05-07 17:25:17,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_function_proxy__18_44_0 given in one single declaration
[2025-05-07 17:25:17,936 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_function_proxy__18_44_0
[2025-05-07 17:25:17,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_function_proxy__18_44_0
[2025-05-07 17:25:17,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_proxy__18_44_0 given in one single declaration
[2025-05-07 17:25:17,936 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_proxy__18_44_0
[2025-05-07 17:25:17,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_proxy__18_44_0
[2025-05-07 17:25:17,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_return_function_proxy__18_44_0 given in one single declaration
[2025-05-07 17:25:17,937 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_return_function_proxy__18_44_0
[2025-05-07 17:25:17,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_return_function_proxy__18_44_0
[2025-05-07 17:25:17,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_proxy_17_44_0 given in one single declaration
[2025-05-07 17:25:17,937 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_proxy_17_44_0
[2025-05-07 17:25:17,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_proxy_17_44_0
[2025-05-07 17:25:17,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36_function_proxy__18_44_0 given in one single declaration
[2025-05-07 17:25:17,937 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36_function_proxy__18_44_0
[2025-05-07 17:25:17,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36_function_proxy__18_44_0
[2025-05-07 17:25:17,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_39_function_f__43_44_0 given in one single declaration
[2025-05-07 17:25:17,937 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_39_function_f__43_44_0
[2025-05-07 17:25:17,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_39_function_f__43_44_0
[2025-05-07 17:25:17,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_12_function_f__43_44_0 given in one single declaration
[2025-05-07 17:25:17,937 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_12_function_f__43_44_0
[2025-05-07 17:25:17,938 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_12_function_f__43_44_0
[2025-05-07 17:25:17,938 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_f_42_44_0 given in one single declaration
[2025-05-07 17:25:17,938 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_f_42_44_0
[2025-05-07 17:25:17,938 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_f_42_44_0
[2025-05-07 17:25:17,938 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_function_f__43_44_0 given in one single declaration
[2025-05-07 17:25:17,938 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_function_f__43_44_0
[2025-05-07 17:25:17,938 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_function_f__43_44_0
[2025-05-07 17:25:17,938 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_44_function_f__11_44_0 given in one single declaration
[2025-05-07 17:25:17,938 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_44_function_f__11_44_0
[2025-05-07 17:25:17,938 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_44_function_f__11_44_0
[2025-05-07 17:25:17,938 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_f__11_44_0 given in one single declaration
[2025-05-07 17:25:17,938 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_f__11_44_0
[2025-05-07 17:25:17,938 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_f__11_44_0
[2025-05-07 17:25:17,938 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_return_function_f__11_44_0 given in one single declaration
[2025-05-07 17:25:17,938 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_return_function_f__11_44_0
[2025-05-07 17:25:17,938 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_return_function_f__11_44_0
[2025-05-07 17:25:17,939 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_34_f_10_44_0 given in one single declaration
[2025-05-07 17:25:17,939 INFO  L130     BoogieDeclarations]: Found specification of procedure block_34_f_10_44_0
[2025-05-07 17:25:17,939 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_34_f_10_44_0
[2025-05-07 17:25:17,939 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_33_function_f__11_44_0 given in one single declaration
[2025-05-07 17:25:17,939 INFO  L130     BoogieDeclarations]: Found specification of procedure block_33_function_f__11_44_0
[2025-05-07 17:25:17,939 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_33_function_f__11_44_0
[2025-05-07 17:25:17,939 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_function_f__43_44_0 given in one single declaration
[2025-05-07 17:25:17,939 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_function_f__43_44_0
[2025-05-07 17:25:17,939 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_function_f__43_44_0
[2025-05-07 17:25:17,939 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_function_f__43_44_0 given in one single declaration
[2025-05-07 17:25:17,939 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_function_f__43_44_0
[2025-05-07 17:25:17,939 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_function_f__43_44_0
[2025-05-07 17:25:17,939 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_return_function_f__43_44_0 given in one single declaration
[2025-05-07 17:25:17,939 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_return_function_f__43_44_0
[2025-05-07 17:25:17,939 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_return_function_f__43_44_0
[2025-05-07 17:25:17,939 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_6_C_44_0 given in one single declaration
[2025-05-07 17:25:17,940 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_6_C_44_0
[2025-05-07 17:25:17,940 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_6_C_44_0
[2025-05-07 17:25:17,940 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_8_C_44_0 given in one single declaration
[2025-05-07 17:25:17,940 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_8_C_44_0
[2025-05-07 17:25:17,940 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_8_C_44_0
[2025-05-07 17:25:17,940 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_53_C_44_0 given in one single declaration
[2025-05-07 17:25:17,940 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_53_C_44_0
[2025-05-07 17:25:17,940 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_53_C_44_0
[2025-05-07 17:25:17,940 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_50_A_19_0 given in one single declaration
[2025-05-07 17:25:17,940 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_50_A_19_0
[2025-05-07 17:25:17,940 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_50_A_19_0
[2025-05-07 17:25:17,940 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_52_A_19_0 given in one single declaration
[2025-05-07 17:25:17,940 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_52_A_19_0
[2025-05-07 17:25:17,940 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_52_A_19_0
[2025-05-07 17:25:17,940 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_51_A_19_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_51_A_19_0
[2025-05-07 17:25:17,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_51_A_19_0
[2025-05-07 17:25:17,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_47_C_44_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_47_C_44_0
[2025-05-07 17:25:17,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_47_C_44_0
[2025-05-07 17:25:17,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_49_C_44_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_49_C_44_0
[2025-05-07 17:25:17,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_49_C_44_0
[2025-05-07 17:25:17,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_48_C_44_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_48_C_44_0
[2025-05-07 17:25:17,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_48_C_44_0
[2025-05-07 17:25:17,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_13_D_69_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_13_D_69_0
[2025-05-07 17:25:17,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_13_D_69_0
[2025-05-07 17:25:17,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_15_D_69_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_15_D_69_0
[2025-05-07 17:25:17,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_15_D_69_0
[2025-05-07 17:25:17,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_74_D_69_0 given in one single declaration
[2025-05-07 17:25:17,941 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_74_D_69_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_74_D_69_0
[2025-05-07 17:25:17,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_76_D_69_0 given in one single declaration
[2025-05-07 17:25:17,942 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_76_D_69_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_76_D_69_0
[2025-05-07 17:25:17,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_75_D_69_0 given in one single declaration
[2025-05-07 17:25:17,942 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_75_D_69_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_75_D_69_0
[2025-05-07 17:25:17,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_77_C_44_0 given in one single declaration
[2025-05-07 17:25:17,942 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_77_C_44_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_77_C_44_0
[2025-05-07 17:25:17,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_79_C_44_0 given in one single declaration
[2025-05-07 17:25:17,942 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_79_C_44_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_79_C_44_0
[2025-05-07 17:25:17,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_78_C_44_0 given in one single declaration
[2025-05-07 17:25:17,942 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_78_C_44_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_78_C_44_0
[2025-05-07 17:25:17,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_83_D_69_0 given in one single declaration
[2025-05-07 17:25:17,942 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_83_D_69_0
[2025-05-07 17:25:17,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_83_D_69_0
[2025-05-07 17:25:17,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_80_A_19_0 given in one single declaration
[2025-05-07 17:25:17,943 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_80_A_19_0
[2025-05-07 17:25:17,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_80_A_19_0
[2025-05-07 17:25:17,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_82_A_19_0 given in one single declaration
[2025-05-07 17:25:17,943 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_82_A_19_0
[2025-05-07 17:25:17,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_82_A_19_0
[2025-05-07 17:25:17,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_81_A_19_0 given in one single declaration
[2025-05-07 17:25:17,943 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_81_A_19_0
[2025-05-07 17:25:17,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_81_A_19_0
[2025-05-07 17:25:17,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_proxy__18_69_0 given in one single declaration
[2025-05-07 17:25:17,943 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_proxy__18_69_0
[2025-05-07 17:25:17,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_proxy__18_69_0
[2025-05-07 17:25:17,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_61_function_proxy__18_69_0 given in one single declaration
[2025-05-07 17:25:17,943 INFO  L130     BoogieDeclarations]: Found specification of procedure block_61_function_proxy__18_69_0
[2025-05-07 17:25:17,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_61_function_proxy__18_69_0
[2025-05-07 17:25:17,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_17_function_proxy__18_69_0 given in one single declaration
[2025-05-07 17:25:17,943 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_17_function_proxy__18_69_0
[2025-05-07 17:25:17,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_17_function_proxy__18_69_0
[2025-05-07 17:25:17,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_59_return_function_proxy__18_69_0 given in one single declaration
[2025-05-07 17:25:17,944 INFO  L130     BoogieDeclarations]: Found specification of procedure block_59_return_function_proxy__18_69_0
[2025-05-07 17:25:17,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_59_return_function_proxy__18_69_0
[2025-05-07 17:25:17,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_60_function_f__68_69_0 given in one single declaration
[2025-05-07 17:25:17,944 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_60_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_60_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_f__68_69_0 given in one single declaration
[2025-05-07 17:25:17,944 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_73_function_f__68_69_0 given in one single declaration
[2025-05-07 17:25:17,944 INFO  L130     BoogieDeclarations]: Found specification of procedure block_73_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_73_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_72_function_f__68_69_0 given in one single declaration
[2025-05-07 17:25:17,944 INFO  L130     BoogieDeclarations]: Found specification of procedure block_72_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_72_function_f__68_69_0
[2025-05-07 17:25:17,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_return_function_f__68_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_return_function_f__68_69_0
[2025-05-07 17:25:17,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_return_function_f__68_69_0
[2025-05-07 17:25:17,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_f_67_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_f_67_69_0
[2025-05-07 17:25:17,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_f_67_69_0
[2025-05-07 17:25:17,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_function_f__68_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_function_f__68_69_0
[2025-05-07 17:25:17,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_function_f__68_69_0
[2025-05-07 17:25:17,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_71_function_f__43_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_71_function_f__43_69_0
[2025-05-07 17:25:17,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_71_function_f__43_69_0
[2025-05-07 17:25:17,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_f__43_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_f__43_69_0
[2025-05-07 17:25:17,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_f__43_69_0
[2025-05-07 17:25:17,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_63_f_42_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure block_63_f_42_69_0
[2025-05-07 17:25:17,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_63_f_42_69_0
[2025-05-07 17:25:17,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_62_function_f__43_69_0 given in one single declaration
[2025-05-07 17:25:17,945 INFO  L130     BoogieDeclarations]: Found specification of procedure block_62_function_f__43_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_62_function_f__43_69_0
[2025-05-07 17:25:17,946 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_65_function_f__11_69_0 given in one single declaration
[2025-05-07 17:25:17,946 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_65_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_65_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_16_function_f__11_69_0 given in one single declaration
[2025-05-07 17:25:17,946 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_16_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_16_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_return_function_f__11_69_0 given in one single declaration
[2025-05-07 17:25:17,946 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_return_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_return_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_f_10_69_0 given in one single declaration
[2025-05-07 17:25:17,946 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_f_10_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_f_10_69_0
[2025-05-07 17:25:17,946 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_function_f__11_69_0 given in one single declaration
[2025-05-07 17:25:17,946 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_function_f__11_69_0
[2025-05-07 17:25:17,946 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_64_return_function_f__43_69_0 given in one single declaration
[2025-05-07 17:25:17,946 INFO  L130     BoogieDeclarations]: Found specification of procedure block_64_return_function_f__43_69_0
[2025-05-07 17:25:17,946 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_64_return_function_f__43_69_0
[2025-05-07 17:25:17,947 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_66_function_f__43_69_0 given in one single declaration
[2025-05-07 17:25:17,947 INFO  L130     BoogieDeclarations]: Found specification of procedure block_66_function_f__43_69_0
[2025-05-07 17:25:17,947 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_66_function_f__43_69_0
[2025-05-07 17:25:17,947 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_function_f__43_69_0 given in one single declaration
[2025-05-07 17:25:17,947 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_function_f__43_69_0
[2025-05-07 17:25:17,947 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_function_f__43_69_0
[2025-05-07 17:25:17,947 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_58_proxy_17_69_0 given in one single declaration
[2025-05-07 17:25:17,947 INFO  L130     BoogieDeclarations]: Found specification of procedure block_58_proxy_17_69_0
[2025-05-07 17:25:17,947 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_58_proxy_17_69_0
[2025-05-07 17:25:17,947 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_function_proxy__18_69_0 given in one single declaration
[2025-05-07 17:25:17,947 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_function_proxy__18_69_0
[2025-05-07 17:25:17,947 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_function_proxy__18_69_0
[2025-05-07 17:25:17,947 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_proxy__18_19_0 given in one single declaration
[2025-05-07 17:25:17,947 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_proxy__18_19_0
[2025-05-07 17:25:17,947 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_proxy__18_19_0
[2025-05-07 17:25:17,947 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_28_function_proxy__18_19_0 given in one single declaration
[2025-05-07 17:25:17,947 INFO  L130     BoogieDeclarations]: Found specification of procedure block_28_function_proxy__18_19_0
[2025-05-07 17:25:17,947 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_28_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_proxy__18_19_0 given in one single declaration
[2025-05-07 17:25:17,948 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_return_function_proxy__18_19_0 given in one single declaration
[2025-05-07 17:25:17,948 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_return_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_return_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_proxy_17_19_0 given in one single declaration
[2025-05-07 17:25:17,948 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_proxy_17_19_0
[2025-05-07 17:25:17,948 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_proxy_17_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_proxy__18_19_0 given in one single declaration
[2025-05-07 17:25:17,948 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_proxy__18_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_27_function_f__11_19_0 given in one single declaration
[2025-05-07 17:25:17,948 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_27_function_f__11_19_0
[2025-05-07 17:25:17,948 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_27_function_f__11_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__11_19_0 given in one single declaration
[2025-05-07 17:25:17,948 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__11_19_0
[2025-05-07 17:25:17,948 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__11_19_0
[2025-05-07 17:25:17,948 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_return_function_f__11_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_return_function_f__11_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_return_function_f__11_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_f_10_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_f_10_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_f_10_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_function_f__11_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_function_f__11_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_function_f__11_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_A_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_A_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_A_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_A_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_A_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_A_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_32_A_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_32_A_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_32_A_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_29_A_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_29_A_19_0
[2025-05-07 17:25:17,949 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_29_A_19_0
[2025-05-07 17:25:17,949 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_31_A_19_0 given in one single declaration
[2025-05-07 17:25:17,949 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_31_A_19_0
[2025-05-07 17:25:17,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_31_A_19_0
[2025-05-07 17:25:17,950 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_30_A_19_0 given in one single declaration
[2025-05-07 17:25:17,950 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_30_A_19_0
[2025-05-07 17:25:17,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_30_A_19_0
[2025-05-07 17:25:17,950 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:25:17,950 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:25:17,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:25:18,249 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:25:18,251 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:25:18,683 INFO  L?                        ?]: Removed 648 outVars from TransFormulas that were not future-live.
[2025-05-07 17:25:18,683 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:25:18,700 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:25:18,700 INFO  L312             CfgBuilder]: Removed 43 assume(true) statements.
[2025-05-07 17:25:18,701 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:18 BoogieIcfgContainer
[2025-05-07 17:25:18,701 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:25:18,703 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:25:18,703 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:25:18,706 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:25:18,706 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:17" (1/3) ...
[2025-05-07 17:25:18,707 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@45fc6a5d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:25:18, skipping insertion in model container
[2025-05-07 17:25:18,707 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:17" (2/3) ...
[2025-05-07 17:25:18,707 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@45fc6a5d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:25:18, skipping insertion in model container
[2025-05-07 17:25:18,707 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:18" (3/3) ...
[2025-05-07 17:25:18,708 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:25:18,723 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:25:18,725 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 84 procedures, 339 locations, 536 edges, 84 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:25:18,759 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:25:18,767 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;@1b745c88, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:25:18,767 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:25:18,770 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 339 states, 137 states have (on average 1.0875912408759123) internal successors, (149), 149 states have internal predecessors, (149), 123 states have call successors, (129), 83 states have call predecessors, (129), 83 states have return successors, (129), 106 states have call predecessors, (129), 123 states have call successors, (129)
[2025-05-07 17:25:18,781 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:25:18,781 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:18,782 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]
[2025-05-07 17:25:18,782 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:18,785 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:18,785 INFO  L85        PathProgramCache]: Analyzing trace with hash -727109406, now seen corresponding path program 1 times
[2025-05-07 17:25:18,790 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:18,791 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1735890582]
[2025-05-07 17:25:18,791 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:18,791 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:18,840 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:25:18,858 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:25:18,858 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:18,858 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:19,073 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:25:19,073 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:19,074 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1735890582]
[2025-05-07 17:25:19,074 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1735890582] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:19,074 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:19,077 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:19,079 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1262984405]
[2025-05-07 17:25:19,079 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:19,084 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:19,084 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:19,117 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:19,118 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:19,121 INFO  L87              Difference]: Start difference. First operand  has 339 states, 137 states have (on average 1.0875912408759123) internal successors, (149), 149 states have internal predecessors, (149), 123 states have call successors, (129), 83 states have call predecessors, (129), 83 states have return successors, (129), 106 states have call predecessors, (129), 123 states have call successors, (129) Second operand  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:25:19,190 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:19,190 INFO  L93              Difference]: Finished difference Result 341 states and 409 transitions.
[2025-05-07 17:25:19,191 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:19,192 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:25:19,193 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:19,203 INFO  L225             Difference]: With dead ends: 341
[2025-05-07 17:25:19,203 INFO  L226             Difference]: Without dead ends: 337
[2025-05-07 17:25:19,205 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:25:19,208 INFO  L437           NwaCegarLoop]: 405 mSDtfsCounter, 1 mSDsluCounter, 803 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1208 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:19,208 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1208 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:19,223 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 337 states.
[2025-05-07 17:25:19,258 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 337 to 335.
[2025-05-07 17:25:19,260 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 335 states, 136 states have (on average 1.0735294117647058) internal successors, (146), 146 states have internal predecessors, (146), 121 states have call successors, (127), 83 states have call predecessors, (127), 83 states have return successors, (127), 105 states have call predecessors, (127), 121 states have call successors, (127)
[2025-05-07 17:25:19,265 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 335 states to 335 states and 400 transitions.
[2025-05-07 17:25:19,266 INFO  L79                 Accepts]: Start accepts. Automaton has 335 states and 400 transitions. Word has length 66
[2025-05-07 17:25:19,267 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:19,267 INFO  L485      AbstractCegarLoop]: Abstraction has 335 states and 400 transitions.
[2025-05-07 17:25:19,267 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:25:19,267 INFO  L278                IsEmpty]: Start isEmpty. Operand 335 states and 400 transitions.
[2025-05-07 17:25:19,272 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:25:19,272 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:19,272 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]
[2025-05-07 17:25:19,272 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:25:19,272 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:19,273 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:19,273 INFO  L85        PathProgramCache]: Analyzing trace with hash 2137230054, now seen corresponding path program 1 times
[2025-05-07 17:25:19,273 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:19,273 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [650396100]
[2025-05-07 17:25:19,273 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:19,273 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:19,306 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:25:19,345 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:25:19,345 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:19,345 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:19,527 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:25:19,527 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:19,527 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [650396100]
[2025-05-07 17:25:19,528 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [650396100] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:19,528 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:19,528 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:19,528 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [349988126]
[2025-05-07 17:25:19,528 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:19,529 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:19,529 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:19,530 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:19,530 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:19,530 INFO  L87              Difference]: Start difference. First operand 335 states and 400 transitions. Second operand  has 7 states, 6 states have (on average 5.0) internal successors, (30), 7 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:25:19,600 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:19,600 INFO  L93              Difference]: Finished difference Result 334 states and 397 transitions.
[2025-05-07 17:25:19,601 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:19,601 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.0) internal successors, (30), 7 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:25:19,601 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:19,604 INFO  L225             Difference]: With dead ends: 334
[2025-05-07 17:25:19,604 INFO  L226             Difference]: Without dead ends: 333
[2025-05-07 17:25:19,604 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:19,605 INFO  L437           NwaCegarLoop]: 393 mSDtfsCounter, 0 mSDsluCounter, 1952 mSDsCounter, 0 mSdLazyCounter, 27 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2345 SdHoareTripleChecker+Invalid, 27 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 27 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:19,605 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2345 Invalid, 27 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 27 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:19,606 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 333 states.
[2025-05-07 17:25:19,624 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 333 to 333.
[2025-05-07 17:25:19,625 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 333 states, 135 states have (on average 1.0740740740740742) internal successors, (145), 145 states have internal predecessors, (145), 119 states have call successors, (125), 83 states have call predecessors, (125), 83 states have return successors, (125), 104 states have call predecessors, (125), 119 states have call successors, (125)
[2025-05-07 17:25:19,628 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 333 states to 333 states and 395 transitions.
[2025-05-07 17:25:19,628 INFO  L79                 Accepts]: Start accepts. Automaton has 333 states and 395 transitions. Word has length 66
[2025-05-07 17:25:19,628 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:19,628 INFO  L485      AbstractCegarLoop]: Abstraction has 333 states and 395 transitions.
[2025-05-07 17:25:19,629 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.0) internal successors, (30), 7 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:25:19,629 INFO  L278                IsEmpty]: Start isEmpty. Operand 333 states and 395 transitions.
[2025-05-07 17:25:19,631 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-05-07 17:25:19,631 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:19,631 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]
[2025-05-07 17:25:19,631 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:25:19,631 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:19,631 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:19,631 INFO  L85        PathProgramCache]: Analyzing trace with hash 2056932191, now seen corresponding path program 1 times
[2025-05-07 17:25:19,632 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:19,632 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [819587991]
[2025-05-07 17:25:19,632 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:19,632 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:19,654 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-05-07 17:25:19,674 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-05-07 17:25:19,674 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:19,674 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:19,766 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:25:19,766 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:19,766 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [819587991]
[2025-05-07 17:25:19,766 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [819587991] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:19,766 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:19,766 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:19,766 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1990362503]
[2025-05-07 17:25:19,767 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:19,767 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:19,767 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:19,768 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:19,768 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:19,768 INFO  L87              Difference]: Start difference. First operand 333 states and 395 transitions. Second operand  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:25:19,812 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:19,812 INFO  L93              Difference]: Finished difference Result 333 states and 394 transitions.
[2025-05-07 17:25:19,813 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:19,813 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 4 states have call successors, (19) Word has length 69
[2025-05-07 17:25:19,813 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:19,815 INFO  L225             Difference]: With dead ends: 333
[2025-05-07 17:25:19,815 INFO  L226             Difference]: Without dead ends: 270
[2025-05-07 17:25:19,815 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:25:19,816 INFO  L437           NwaCegarLoop]: 391 mSDtfsCounter, 1 mSDsluCounter, 1544 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1935 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:25:19,817 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1935 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:19,818 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 270 states.
[2025-05-07 17:25:19,829 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 270 to 270.
[2025-05-07 17:25:19,830 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 270 states, 108 states have (on average 1.0740740740740742) internal successors, (116), 116 states have internal predecessors, (116), 100 states have call successors, (106), 66 states have call predecessors, (106), 66 states have return successors, (106), 87 states have call predecessors, (106), 100 states have call successors, (106)
[2025-05-07 17:25:19,832 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 270 states to 270 states and 328 transitions.
[2025-05-07 17:25:19,832 INFO  L79                 Accepts]: Start accepts. Automaton has 270 states and 328 transitions. Word has length 69
[2025-05-07 17:25:19,832 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:19,832 INFO  L485      AbstractCegarLoop]: Abstraction has 270 states and 328 transitions.
[2025-05-07 17:25:19,833 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:25:19,833 INFO  L278                IsEmpty]: Start isEmpty. Operand 270 states and 328 transitions.
[2025-05-07 17:25:19,835 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:25:19,835 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:19,835 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]
[2025-05-07 17:25:19,835 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:25:19,835 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:19,835 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:19,836 INFO  L85        PathProgramCache]: Analyzing trace with hash 412170479, now seen corresponding path program 1 times
[2025-05-07 17:25:19,836 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:19,836 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1712352373]
[2025-05-07 17:25:19,836 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:19,836 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:19,874 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:25:19,878 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:25:19,878 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:19,878 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:19,954 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:25:19,954 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:19,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1712352373]
[2025-05-07 17:25:19,954 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1712352373] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:19,954 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:19,954 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:19,954 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1612377955]
[2025-05-07 17:25:19,954 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:19,955 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:19,955 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:19,955 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:19,955 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:19,955 INFO  L87              Difference]: Start difference. First operand 270 states and 328 transitions. Second operand  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 3 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:25:19,969 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:19,969 INFO  L93              Difference]: Finished difference Result 274 states and 332 transitions.
[2025-05-07 17:25:19,970 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:19,970 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 3 states have call predecessors, (23), 4 states have call successors, (23) Word has length 83
[2025-05-07 17:25:19,970 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:19,972 INFO  L225             Difference]: With dead ends: 274
[2025-05-07 17:25:19,972 INFO  L226             Difference]: Without dead ends: 267
[2025-05-07 17:25:19,972 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:25:19,973 INFO  L437           NwaCegarLoop]: 328 mSDtfsCounter, 1 mSDsluCounter, 645 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 973 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:19,973 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 973 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:19,974 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 267 states.
[2025-05-07 17:25:19,983 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 267 to 265.
[2025-05-07 17:25:19,984 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 265 states, 108 states have (on average 1.0555555555555556) internal successors, (114), 114 states have internal predecessors, (114), 95 states have call successors, (101), 66 states have call predecessors, (101), 66 states have return successors, (101), 84 states have call predecessors, (101), 95 states have call successors, (101)
[2025-05-07 17:25:19,986 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 265 states to 265 states and 316 transitions.
[2025-05-07 17:25:19,986 INFO  L79                 Accepts]: Start accepts. Automaton has 265 states and 316 transitions. Word has length 83
[2025-05-07 17:25:19,986 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:19,986 INFO  L485      AbstractCegarLoop]: Abstraction has 265 states and 316 transitions.
[2025-05-07 17:25:19,986 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 3 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:25:19,986 INFO  L278                IsEmpty]: Start isEmpty. Operand 265 states and 316 transitions.
[2025-05-07 17:25:19,987 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 101
[2025-05-07 17:25:19,988 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:19,988 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]
[2025-05-07 17:25:19,988 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:25:19,988 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:19,988 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:19,988 INFO  L85        PathProgramCache]: Analyzing trace with hash -1872178363, now seen corresponding path program 1 times
[2025-05-07 17:25:19,988 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:19,988 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [35033773]
[2025-05-07 17:25:19,988 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:19,989 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:20,021 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 100 statements into 1 equivalence classes.
[2025-05-07 17:25:20,027 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 100 of 100 statements.
[2025-05-07 17:25:20,028 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:20,028 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:20,148 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:25:20,148 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:20,149 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [35033773]
[2025-05-07 17:25:20,149 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [35033773] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:20,149 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:20,149 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:20,149 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1602381654]
[2025-05-07 17:25:20,149 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:20,149 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:20,149 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:20,150 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:20,150 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:20,150 INFO  L87              Difference]: Start difference. First operand 265 states and 316 transitions. Second operand  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 4 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (28), 6 states have call predecessors, (28), 4 states have call successors, (28)
[2025-05-07 17:25:20,200 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:20,200 INFO  L93              Difference]: Finished difference Result 269 states and 322 transitions.
[2025-05-07 17:25:20,200 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:20,200 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 4 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (28), 6 states have call predecessors, (28), 4 states have call successors, (28) Word has length 100
[2025-05-07 17:25:20,201 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:20,202 INFO  L225             Difference]: With dead ends: 269
[2025-05-07 17:25:20,202 INFO  L226             Difference]: Without dead ends: 269
[2025-05-07 17:25:20,202 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:25:20,202 INFO  L437           NwaCegarLoop]: 311 mSDtfsCounter, 1 mSDsluCounter, 1230 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1541 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:20,202 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1541 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:20,203 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 269 states.
[2025-05-07 17:25:20,209 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 269 to 269.
[2025-05-07 17:25:20,209 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 269 states, 110 states have (on average 1.0545454545454545) internal successors, (116), 116 states have internal predecessors, (116), 95 states have call successors, (101), 66 states have call predecessors, (101), 68 states have return successors, (105), 86 states have call predecessors, (105), 95 states have call successors, (105)
[2025-05-07 17:25:20,210 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 269 states to 269 states and 322 transitions.
[2025-05-07 17:25:20,210 INFO  L79                 Accepts]: Start accepts. Automaton has 269 states and 322 transitions. Word has length 100
[2025-05-07 17:25:20,211 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:20,211 INFO  L485      AbstractCegarLoop]: Abstraction has 269 states and 322 transitions.
[2025-05-07 17:25:20,211 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 4 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (28), 6 states have call predecessors, (28), 4 states have call successors, (28)
[2025-05-07 17:25:20,211 INFO  L278                IsEmpty]: Start isEmpty. Operand 269 states and 322 transitions.
[2025-05-07 17:25:20,212 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 101
[2025-05-07 17:25:20,212 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:20,212 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]
[2025-05-07 17:25:20,213 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:25:20,213 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:20,213 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:20,213 INFO  L85        PathProgramCache]: Analyzing trace with hash 1924422525, now seen corresponding path program 1 times
[2025-05-07 17:25:20,213 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:20,213 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1395052834]
[2025-05-07 17:25:20,213 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:20,213 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:20,248 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 100 statements into 1 equivalence classes.
[2025-05-07 17:25:20,254 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 100 of 100 statements.
[2025-05-07 17:25:20,254 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:20,254 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:20,381 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:25:20,381 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:20,381 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1395052834]
[2025-05-07 17:25:20,381 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1395052834] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:20,381 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:20,381 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:20,381 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1725531431]
[2025-05-07 17:25:20,381 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:20,382 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:20,382 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:20,382 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:20,382 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:20,382 INFO  L87              Difference]: Start difference. First operand 269 states and 322 transitions. Second operand  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 4 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (28), 6 states have call predecessors, (28), 4 states have call successors, (28)
[2025-05-07 17:25:20,429 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:20,429 INFO  L93              Difference]: Finished difference Result 269 states and 321 transitions.
[2025-05-07 17:25:20,429 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:20,430 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 4 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (28), 6 states have call predecessors, (28), 4 states have call successors, (28) Word has length 100
[2025-05-07 17:25:20,430 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:20,431 INFO  L225             Difference]: With dead ends: 269
[2025-05-07 17:25:20,431 INFO  L226             Difference]: Without dead ends: 269
[2025-05-07 17:25:20,432 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:25:20,432 INFO  L437           NwaCegarLoop]: 312 mSDtfsCounter, 1 mSDsluCounter, 1234 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1546 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:25:20,432 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1546 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:20,433 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 269 states.
[2025-05-07 17:25:20,441 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 269 to 269.
[2025-05-07 17:25:20,441 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 269 states, 110 states have (on average 1.0545454545454545) internal successors, (116), 116 states have internal predecessors, (116), 95 states have call successors, (101), 66 states have call predecessors, (101), 68 states have return successors, (104), 86 states have call predecessors, (104), 95 states have call successors, (104)
[2025-05-07 17:25:20,443 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 269 states to 269 states and 321 transitions.
[2025-05-07 17:25:20,444 INFO  L79                 Accepts]: Start accepts. Automaton has 269 states and 321 transitions. Word has length 100
[2025-05-07 17:25:20,444 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:20,444 INFO  L485      AbstractCegarLoop]: Abstraction has 269 states and 321 transitions.
[2025-05-07 17:25:20,444 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 4 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (28), 6 states have call predecessors, (28), 4 states have call successors, (28)
[2025-05-07 17:25:20,444 INFO  L278                IsEmpty]: Start isEmpty. Operand 269 states and 321 transitions.
[2025-05-07 17:25:20,446 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 98
[2025-05-07 17:25:20,446 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:20,446 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]
[2025-05-07 17:25:20,446 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:25:20,446 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:20,447 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:20,447 INFO  L85        PathProgramCache]: Analyzing trace with hash 1748742734, now seen corresponding path program 1 times
[2025-05-07 17:25:20,447 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:20,447 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1747783667]
[2025-05-07 17:25:20,447 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:20,447 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:20,474 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 97 statements into 1 equivalence classes.
[2025-05-07 17:25:20,482 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 97 of 97 statements.
[2025-05-07 17:25:20,482 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:20,483 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:20,616 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:20,616 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:20,616 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1747783667]
[2025-05-07 17:25:20,616 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1747783667] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:20,616 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:20,616 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:20,617 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [834001122]
[2025-05-07 17:25:20,617 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:20,617 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:20,617 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:20,618 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:20,618 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:20,618 INFO  L87              Difference]: Start difference. First operand 269 states and 321 transitions. Second operand  has 6 states, 5 states have (on average 8.6) internal successors, (43), 6 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:20,667 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:20,667 INFO  L93              Difference]: Finished difference Result 263 states and 313 transitions.
[2025-05-07 17:25:20,668 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:20,668 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.6) internal successors, (43), 6 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 4 states have call successors, (27) Word has length 97
[2025-05-07 17:25:20,668 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:20,669 INFO  L225             Difference]: With dead ends: 263
[2025-05-07 17:25:20,669 INFO  L226             Difference]: Without dead ends: 260
[2025-05-07 17:25:20,669 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:25:20,670 INFO  L437           NwaCegarLoop]: 308 mSDtfsCounter, 0 mSDsluCounter, 1218 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1526 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:20,670 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1526 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:20,670 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 260 states.
[2025-05-07 17:25:20,675 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 260 to 260.
[2025-05-07 17:25:20,675 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 260 states, 106 states have (on average 1.0566037735849056) internal successors, (112), 112 states have internal predecessors, (112), 93 states have call successors, (98), 65 states have call predecessors, (98), 65 states have return successors, (98), 82 states have call predecessors, (98), 93 states have call successors, (98)
[2025-05-07 17:25:20,676 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 260 states to 260 states and 308 transitions.
[2025-05-07 17:25:20,676 INFO  L79                 Accepts]: Start accepts. Automaton has 260 states and 308 transitions. Word has length 97
[2025-05-07 17:25:20,677 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:20,677 INFO  L485      AbstractCegarLoop]: Abstraction has 260 states and 308 transitions.
[2025-05-07 17:25:20,677 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.6) internal successors, (43), 6 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:20,677 INFO  L278                IsEmpty]: Start isEmpty. Operand 260 states and 308 transitions.
[2025-05-07 17:25:20,678 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:25:20,678 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:20,678 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:20,678 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:25:20,678 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:20,678 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:20,678 INFO  L85        PathProgramCache]: Analyzing trace with hash -1778068619, now seen corresponding path program 1 times
[2025-05-07 17:25:20,678 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:20,678 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [721894748]
[2025-05-07 17:25:20,679 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:20,679 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:20,709 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:25:20,720 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:25:20,720 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:20,720 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:20,837 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:25:20,837 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:20,837 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [721894748]
[2025-05-07 17:25:20,837 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [721894748] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:20,837 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:20,837 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:25:20,837 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1930538850]
[2025-05-07 17:25:20,837 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:20,838 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:25:20,838 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:20,838 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:25:20,838 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:20,839 INFO  L87              Difference]: Start difference. First operand 260 states and 308 transitions. Second operand  has 8 states, 7 states have (on average 5.857142857142857) internal successors, (41), 8 states have internal predecessors, (41), 5 states have call successors, (26), 1 states have call predecessors, (26), 7 states have return successors, (26), 8 states have call predecessors, (26), 5 states have call successors, (26)
[2025-05-07 17:25:20,908 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:20,908 INFO  L93              Difference]: Finished difference Result 270 states and 321 transitions.
[2025-05-07 17:25:20,908 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:25:20,908 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 5.857142857142857) internal successors, (41), 8 states have internal predecessors, (41), 5 states have call successors, (26), 1 states have call predecessors, (26), 7 states have return successors, (26), 8 states have call predecessors, (26), 5 states have call successors, (26) Word has length 93
[2025-05-07 17:25:20,909 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:20,910 INFO  L225             Difference]: With dead ends: 270
[2025-05-07 17:25:20,910 INFO  L226             Difference]: Without dead ends: 270
[2025-05-07 17:25:20,911 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:20,911 INFO  L437           NwaCegarLoop]: 309 mSDtfsCounter, 1 mSDsluCounter, 1833 mSDsCounter, 0 mSdLazyCounter, 47 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 2142 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 47 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:20,911 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 2142 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 47 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:20,912 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 270 states.
[2025-05-07 17:25:20,920 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 270 to 270.
[2025-05-07 17:25:20,920 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 270 states, 110 states have (on average 1.0545454545454545) internal successors, (116), 116 states have internal predecessors, (116), 95 states have call successors, (100), 65 states have call predecessors, (100), 69 states have return successors, (105), 88 states have call predecessors, (105), 95 states have call successors, (105)
[2025-05-07 17:25:20,922 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 270 states to 270 states and 321 transitions.
[2025-05-07 17:25:20,923 INFO  L79                 Accepts]: Start accepts. Automaton has 270 states and 321 transitions. Word has length 93
[2025-05-07 17:25:20,923 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:20,923 INFO  L485      AbstractCegarLoop]: Abstraction has 270 states and 321 transitions.
[2025-05-07 17:25:20,923 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 5.857142857142857) internal successors, (41), 8 states have internal predecessors, (41), 5 states have call successors, (26), 1 states have call predecessors, (26), 7 states have return successors, (26), 8 states have call predecessors, (26), 5 states have call successors, (26)
[2025-05-07 17:25:20,923 INFO  L278                IsEmpty]: Start isEmpty. Operand 270 states and 321 transitions.
[2025-05-07 17:25:20,925 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:25:20,925 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:20,925 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]
[2025-05-07 17:25:20,925 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:25:20,925 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:20,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:20,926 INFO  L85        PathProgramCache]: Analyzing trace with hash -1692147819, now seen corresponding path program 1 times
[2025-05-07 17:25:20,926 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:20,926 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1529776447]
[2025-05-07 17:25:20,926 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:20,926 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:20,958 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:25:20,970 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:25:20,970 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:20,970 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,082 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:25:21,082 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,083 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1529776447]
[2025-05-07 17:25:21,083 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1529776447] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,083 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,083 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:21,083 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [670619618]
[2025-05-07 17:25:21,083 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,083 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:21,083 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,084 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:21,084 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:21,084 INFO  L87              Difference]: Start difference. First operand 270 states and 321 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26)
[2025-05-07 17:25:21,126 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,127 INFO  L93              Difference]: Finished difference Result 276 states and 327 transitions.
[2025-05-07 17:25:21,127 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:21,127 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26) Word has length 93
[2025-05-07 17:25:21,127 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,128 INFO  L225             Difference]: With dead ends: 276
[2025-05-07 17:25:21,128 INFO  L226             Difference]: Without dead ends: 276
[2025-05-07 17:25:21,128 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:25:21,129 INFO  L437           NwaCegarLoop]: 308 mSDtfsCounter, 1 mSDsluCounter, 1217 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1525 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:21,129 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1525 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:21,130 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 276 states.
[2025-05-07 17:25:21,135 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 276 to 274.
[2025-05-07 17:25:21,135 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 274 states, 112 states have (on average 1.0535714285714286) internal successors, (118), 118 states have internal predecessors, (118), 95 states have call successors, (100), 65 states have call predecessors, (100), 71 states have return successors, (107), 90 states have call predecessors, (107), 95 states have call successors, (107)
[2025-05-07 17:25:21,136 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 274 states to 274 states and 325 transitions.
[2025-05-07 17:25:21,137 INFO  L79                 Accepts]: Start accepts. Automaton has 274 states and 325 transitions. Word has length 93
[2025-05-07 17:25:21,137 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,137 INFO  L485      AbstractCegarLoop]: Abstraction has 274 states and 325 transitions.
[2025-05-07 17:25:21,137 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26)
[2025-05-07 17:25:21,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 274 states and 325 transitions.
[2025-05-07 17:25:21,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 98
[2025-05-07 17:25:21,138 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,138 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]
[2025-05-07 17:25:21,138 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:25:21,138 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,139 INFO  L85        PathProgramCache]: Analyzing trace with hash 1432682280, now seen corresponding path program 1 times
[2025-05-07 17:25:21,139 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,139 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2106016521]
[2025-05-07 17:25:21,139 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,139 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,174 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 97 statements into 1 equivalence classes.
[2025-05-07 17:25:21,179 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 97 of 97 statements.
[2025-05-07 17:25:21,179 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,179 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,281 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:21,281 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2106016521]
[2025-05-07 17:25:21,282 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2106016521] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,282 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,282 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:25:21,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [182730404]
[2025-05-07 17:25:21,282 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,282 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:25:21,282 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,282 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:25:21,282 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:25:21,283 INFO  L87              Difference]: Start difference. First operand 274 states and 325 transitions. Second operand  has 5 states, 4 states have (on average 10.75) internal successors, (43), 5 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 4 states have return successors, (27), 5 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:21,324 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,324 INFO  L93              Difference]: Finished difference Result 278 states and 331 transitions.
[2025-05-07 17:25:21,325 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:21,325 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 10.75) internal successors, (43), 5 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 4 states have return successors, (27), 5 states have call predecessors, (27), 4 states have call successors, (27) Word has length 97
[2025-05-07 17:25:21,325 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,327 INFO  L225             Difference]: With dead ends: 278
[2025-05-07 17:25:21,327 INFO  L226             Difference]: Without dead ends: 278
[2025-05-07 17:25:21,328 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:25:21,328 INFO  L437           NwaCegarLoop]: 304 mSDtfsCounter, 1 mSDsluCounter, 901 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1205 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:21,328 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1205 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:21,329 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 278 states.
[2025-05-07 17:25:21,340 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 278 to 278.
[2025-05-07 17:25:21,341 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 278 states, 114 states have (on average 1.0526315789473684) internal successors, (120), 120 states have internal predecessors, (120), 95 states have call successors, (100), 65 states have call predecessors, (100), 73 states have return successors, (111), 92 states have call predecessors, (111), 95 states have call successors, (111)
[2025-05-07 17:25:21,343 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 278 states to 278 states and 331 transitions.
[2025-05-07 17:25:21,344 INFO  L79                 Accepts]: Start accepts. Automaton has 278 states and 331 transitions. Word has length 97
[2025-05-07 17:25:21,344 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,344 INFO  L485      AbstractCegarLoop]: Abstraction has 278 states and 331 transitions.
[2025-05-07 17:25:21,344 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 10.75) internal successors, (43), 5 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 4 states have return successors, (27), 5 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:21,344 INFO  L278                IsEmpty]: Start isEmpty. Operand 278 states and 331 transitions.
[2025-05-07 17:25:21,345 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 98
[2025-05-07 17:25:21,345 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,345 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]
[2025-05-07 17:25:21,346 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:25:21,346 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,346 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,346 INFO  L85        PathProgramCache]: Analyzing trace with hash -654400472, now seen corresponding path program 1 times
[2025-05-07 17:25:21,346 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,346 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [813021192]
[2025-05-07 17:25:21,346 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,346 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,380 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 97 statements into 1 equivalence classes.
[2025-05-07 17:25:21,386 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 97 of 97 statements.
[2025-05-07 17:25:21,387 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,387 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,461 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:25:21,461 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,461 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [813021192]
[2025-05-07 17:25:21,461 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [813021192] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,461 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,461 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:25:21,461 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [729890210]
[2025-05-07 17:25:21,461 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,461 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:25:21,461 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,462 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:25:21,462 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:25:21,462 INFO  L87              Difference]: Start difference. First operand 278 states and 331 transitions. Second operand  has 5 states, 4 states have (on average 10.75) internal successors, (43), 5 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 4 states have return successors, (27), 5 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:21,489 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,489 INFO  L93              Difference]: Finished difference Result 278 states and 330 transitions.
[2025-05-07 17:25:21,489 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:21,489 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 10.75) internal successors, (43), 5 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 4 states have return successors, (27), 5 states have call predecessors, (27), 4 states have call successors, (27) Word has length 97
[2025-05-07 17:25:21,489 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,490 INFO  L225             Difference]: With dead ends: 278
[2025-05-07 17:25:21,490 INFO  L226             Difference]: Without dead ends: 278
[2025-05-07 17:25:21,491 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:25:21,491 INFO  L437           NwaCegarLoop]: 305 mSDtfsCounter, 1 mSDsluCounter, 904 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1209 SdHoareTripleChecker+Invalid, 16 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:21,491 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1209 Invalid, 16 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:21,491 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 278 states.
[2025-05-07 17:25:21,497 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 278 to 278.
[2025-05-07 17:25:21,497 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 278 states, 114 states have (on average 1.0526315789473684) internal successors, (120), 120 states have internal predecessors, (120), 95 states have call successors, (100), 65 states have call predecessors, (100), 73 states have return successors, (110), 92 states have call predecessors, (110), 95 states have call successors, (110)
[2025-05-07 17:25:21,498 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 278 states to 278 states and 330 transitions.
[2025-05-07 17:25:21,498 INFO  L79                 Accepts]: Start accepts. Automaton has 278 states and 330 transitions. Word has length 97
[2025-05-07 17:25:21,498 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,498 INFO  L485      AbstractCegarLoop]: Abstraction has 278 states and 330 transitions.
[2025-05-07 17:25:21,499 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 10.75) internal successors, (43), 5 states have internal predecessors, (43), 4 states have call successors, (27), 1 states have call predecessors, (27), 4 states have return successors, (27), 5 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:21,499 INFO  L278                IsEmpty]: Start isEmpty. Operand 278 states and 330 transitions.
[2025-05-07 17:25:21,500 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:25:21,500 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,500 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]
[2025-05-07 17:25:21,500 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:25:21,500 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,500 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,500 INFO  L85        PathProgramCache]: Analyzing trace with hash 812204834, now seen corresponding path program 1 times
[2025-05-07 17:25:21,500 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,500 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1731721173]
[2025-05-07 17:25:21,500 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,500 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,523 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:25:21,532 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:25:21,532 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,532 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,616 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:21,617 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,617 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1731721173]
[2025-05-07 17:25:21,617 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1731721173] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,617 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,617 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:21,617 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1901652128]
[2025-05-07 17:25:21,617 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,617 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:21,617 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,617 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:21,617 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:21,618 INFO  L87              Difference]: Start difference. First operand 278 states and 330 transitions. Second operand  has 7 states, 6 states have (on average 6.666666666666667) internal successors, (40), 7 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 6 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:25:21,672 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,672 INFO  L93              Difference]: Finished difference Result 277 states and 327 transitions.
[2025-05-07 17:25:21,673 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:21,673 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 6.666666666666667) internal successors, (40), 7 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 6 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25) Word has length 90
[2025-05-07 17:25:21,673 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,674 INFO  L225             Difference]: With dead ends: 277
[2025-05-07 17:25:21,674 INFO  L226             Difference]: Without dead ends: 276
[2025-05-07 17:25:21,674 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:21,674 INFO  L437           NwaCegarLoop]: 299 mSDtfsCounter, 0 mSDsluCounter, 1480 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1779 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:21,675 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1779 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:21,675 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 276 states.
[2025-05-07 17:25:21,680 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 276 to 276.
[2025-05-07 17:25:21,680 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 276 states, 113 states have (on average 1.0530973451327434) internal successors, (119), 119 states have internal predecessors, (119), 93 states have call successors, (98), 65 states have call predecessors, (98), 73 states have return successors, (108), 91 states have call predecessors, (108), 93 states have call successors, (108)
[2025-05-07 17:25:21,681 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 276 states to 276 states and 325 transitions.
[2025-05-07 17:25:21,681 INFO  L79                 Accepts]: Start accepts. Automaton has 276 states and 325 transitions. Word has length 90
[2025-05-07 17:25:21,681 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,681 INFO  L485      AbstractCegarLoop]: Abstraction has 276 states and 325 transitions.
[2025-05-07 17:25:21,682 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 6.666666666666667) internal successors, (40), 7 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 6 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:25:21,682 INFO  L278                IsEmpty]: Start isEmpty. Operand 276 states and 325 transitions.
[2025-05-07 17:25:21,683 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:25:21,683 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,683 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:21,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:25:21,683 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,683 INFO  L85        PathProgramCache]: Analyzing trace with hash 430124673, now seen corresponding path program 1 times
[2025-05-07 17:25:21,683 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,683 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [499544234]
[2025-05-07 17:25:21,683 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,683 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,713 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:25:21,722 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:25:21,722 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,722 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,789 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:25:21,789 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,789 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [499544234]
[2025-05-07 17:25:21,789 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [499544234] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,789 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,789 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:21,789 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [982866949]
[2025-05-07 17:25:21,789 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,789 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:21,790 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,790 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:21,790 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:21,790 INFO  L87              Difference]: Start difference. First operand 276 states and 325 transitions. Second operand  has 6 states, 5 states have (on average 8.4) internal successors, (42), 6 states have internal predecessors, (42), 4 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:21,826 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,826 INFO  L93              Difference]: Finished difference Result 281 states and 331 transitions.
[2025-05-07 17:25:21,826 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:21,826 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.4) internal successors, (42), 6 states have internal predecessors, (42), 4 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 4 states have call successors, (27) Word has length 96
[2025-05-07 17:25:21,827 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,828 INFO  L225             Difference]: With dead ends: 281
[2025-05-07 17:25:21,828 INFO  L226             Difference]: Without dead ends: 281
[2025-05-07 17:25:21,828 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:25:21,828 INFO  L437           NwaCegarLoop]: 305 mSDtfsCounter, 1 mSDsluCounter, 1201 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1506 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:21,828 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1506 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:21,829 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 281 states.
[2025-05-07 17:25:21,834 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 281 to 276.
[2025-05-07 17:25:21,834 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 276 states, 113 states have (on average 1.0530973451327434) internal successors, (119), 119 states have internal predecessors, (119), 93 states have call successors, (98), 65 states have call predecessors, (98), 73 states have return successors, (108), 91 states have call predecessors, (108), 93 states have call successors, (108)
[2025-05-07 17:25:21,835 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 276 states to 276 states and 325 transitions.
[2025-05-07 17:25:21,836 INFO  L79                 Accepts]: Start accepts. Automaton has 276 states and 325 transitions. Word has length 96
[2025-05-07 17:25:21,836 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,836 INFO  L485      AbstractCegarLoop]: Abstraction has 276 states and 325 transitions.
[2025-05-07 17:25:21,836 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.4) internal successors, (42), 6 states have internal predecessors, (42), 4 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 6 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:25:21,836 INFO  L278                IsEmpty]: Start isEmpty. Operand 276 states and 325 transitions.
[2025-05-07 17:25:21,837 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 95
[2025-05-07 17:25:21,837 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,837 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]
[2025-05-07 17:25:21,837 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:25:21,837 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,838 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,838 INFO  L85        PathProgramCache]: Analyzing trace with hash 308918957, now seen corresponding path program 1 times
[2025-05-07 17:25:21,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,838 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1542919897]
[2025-05-07 17:25:21,838 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,838 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,870 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 94 statements into 1 equivalence classes.
[2025-05-07 17:25:21,877 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 94 of 94 statements.
[2025-05-07 17:25:21,877 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,877 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,931 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:25:21,932 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,932 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1542919897]
[2025-05-07 17:25:21,932 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1542919897] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,932 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,932 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:21,932 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [779255021]
[2025-05-07 17:25:21,932 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,932 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:21,932 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,933 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:21,933 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:21,933 INFO  L87              Difference]: Start difference. First operand 276 states and 325 transitions. Second operand  has 4 states, 3 states have (on average 14.0) internal successors, (42), 4 states have internal predecessors, (42), 3 states have call successors, (26), 1 states have call predecessors, (26), 3 states have return successors, (26), 3 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:25:21,944 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,944 INFO  L93              Difference]: Finished difference Result 280 states and 329 transitions.
[2025-05-07 17:25:21,944 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:21,944 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 14.0) internal successors, (42), 4 states have internal predecessors, (42), 3 states have call successors, (26), 1 states have call predecessors, (26), 3 states have return successors, (26), 3 states have call predecessors, (26), 3 states have call successors, (26) Word has length 94
[2025-05-07 17:25:21,945 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,946 INFO  L225             Difference]: With dead ends: 280
[2025-05-07 17:25:21,946 INFO  L226             Difference]: Without dead ends: 269
[2025-05-07 17:25:21,946 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:25:21,946 INFO  L437           NwaCegarLoop]: 303 mSDtfsCounter, 1 mSDsluCounter, 590 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 893 SdHoareTripleChecker+Invalid, 4 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:21,946 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 893 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:21,947 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 269 states.
[2025-05-07 17:25:21,951 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 269 to 267.
[2025-05-07 17:25:21,951 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 267 states, 113 states have (on average 1.0265486725663717) internal successors, (116), 116 states have internal predecessors, (116), 84 states have call successors, (89), 65 states have call predecessors, (89), 73 states have return successors, (99), 85 states have call predecessors, (99), 84 states have call successors, (99)
[2025-05-07 17:25:21,952 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 267 states to 267 states and 304 transitions.
[2025-05-07 17:25:21,952 INFO  L79                 Accepts]: Start accepts. Automaton has 267 states and 304 transitions. Word has length 94
[2025-05-07 17:25:21,953 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,953 INFO  L485      AbstractCegarLoop]: Abstraction has 267 states and 304 transitions.
[2025-05-07 17:25:21,953 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 14.0) internal successors, (42), 4 states have internal predecessors, (42), 3 states have call successors, (26), 1 states have call predecessors, (26), 3 states have return successors, (26), 3 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:25:21,953 INFO  L278                IsEmpty]: Start isEmpty. Operand 267 states and 304 transitions.
[2025-05-07 17:25:21,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:25:21,954 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,954 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]
[2025-05-07 17:25:21,954 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:25:21,954 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,954 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,954 INFO  L85        PathProgramCache]: Analyzing trace with hash -437292847, now seen corresponding path program 1 times
[2025-05-07 17:25:21,954 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,954 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [136083364]
[2025-05-07 17:25:21,954 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,954 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,982 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:25:21,990 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:25:21,990 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,990 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,103 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:25:22,103 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [136083364]
[2025-05-07 17:25:22,104 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [136083364] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,104 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,104 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:22,104 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [769861657]
[2025-05-07 17:25:22,104 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,104 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:22,104 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,104 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:22,104 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:22,104 INFO  L87              Difference]: Start difference. First operand 267 states and 304 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26)
[2025-05-07 17:25:22,139 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,139 INFO  L93              Difference]: Finished difference Result 254 states and 285 transitions.
[2025-05-07 17:25:22,140 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:22,140 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26) Word has length 93
[2025-05-07 17:25:22,140 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,140 INFO  L225             Difference]: With dead ends: 254
[2025-05-07 17:25:22,141 INFO  L226             Difference]: Without dead ends: 151
[2025-05-07 17:25:22,141 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:25:22,141 INFO  L437           NwaCegarLoop]: 272 mSDtfsCounter, 0 mSDsluCounter, 1076 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1348 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,141 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1348 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,142 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 151 states.
[2025-05-07 17:25:22,145 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 151 to 151.
[2025-05-07 17:25:22,145 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 151 states, 64 states have (on average 1.015625) internal successors, (65), 65 states have internal predecessors, (65), 49 states have call successors, (52), 38 states have call predecessors, (52), 40 states have return successors, (55), 47 states have call predecessors, (55), 49 states have call successors, (55)
[2025-05-07 17:25:22,145 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 151 states to 151 states and 172 transitions.
[2025-05-07 17:25:22,146 INFO  L79                 Accepts]: Start accepts. Automaton has 151 states and 172 transitions. Word has length 93
[2025-05-07 17:25:22,146 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,146 INFO  L485      AbstractCegarLoop]: Abstraction has 151 states and 172 transitions.
[2025-05-07 17:25:22,146 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 4 states have call successors, (26)
[2025-05-07 17:25:22,146 INFO  L278                IsEmpty]: Start isEmpty. Operand 151 states and 172 transitions.
[2025-05-07 17:25:22,147 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 115
[2025-05-07 17:25:22,147 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,147 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]
[2025-05-07 17:25:22,147 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:25:22,147 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,147 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,147 INFO  L85        PathProgramCache]: Analyzing trace with hash -1668717279, now seen corresponding path program 1 times
[2025-05-07 17:25:22,147 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,147 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [561243096]
[2025-05-07 17:25:22,147 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,147 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,182 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 114 statements into 1 equivalence classes.
[2025-05-07 17:25:22,194 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 114 of 114 statements.
[2025-05-07 17:25:22,194 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,194 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,281 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:22,281 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [561243096]
[2025-05-07 17:25:22,281 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [561243096] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,281 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,282 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:22,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1616142443]
[2025-05-07 17:25:22,282 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,282 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:22,282 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,283 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:22,283 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:22,283 INFO  L87              Difference]: Start difference. First operand 151 states and 172 transitions. Second operand  has 7 states, 6 states have (on average 8.333333333333334) internal successors, (50), 7 states have internal predecessors, (50), 4 states have call successors, (32), 1 states have call predecessors, (32), 6 states have return successors, (32), 6 states have call predecessors, (32), 4 states have call successors, (32)
[2025-05-07 17:25:22,328 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,328 INFO  L93              Difference]: Finished difference Result 146 states and 164 transitions.
[2025-05-07 17:25:22,329 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:22,329 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 8.333333333333334) internal successors, (50), 7 states have internal predecessors, (50), 4 states have call successors, (32), 1 states have call predecessors, (32), 6 states have return successors, (32), 6 states have call predecessors, (32), 4 states have call successors, (32) Word has length 114
[2025-05-07 17:25:22,329 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,330 INFO  L225             Difference]: With dead ends: 146
[2025-05-07 17:25:22,330 INFO  L226             Difference]: Without dead ends: 145
[2025-05-07 17:25:22,330 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:22,330 INFO  L437           NwaCegarLoop]: 159 mSDtfsCounter, 0 mSDsluCounter, 781 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 940 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,330 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 940 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,331 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 145 states.
[2025-05-07 17:25:22,333 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 145 to 145.
[2025-05-07 17:25:22,333 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 145 states, 61 states have (on average 1.0163934426229508) internal successors, (62), 62 states have internal predecessors, (62), 47 states have call successors, (50), 38 states have call predecessors, (50), 38 states have return successors, (50), 44 states have call predecessors, (50), 47 states have call successors, (50)
[2025-05-07 17:25:22,334 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 145 states to 145 states and 162 transitions.
[2025-05-07 17:25:22,334 INFO  L79                 Accepts]: Start accepts. Automaton has 145 states and 162 transitions. Word has length 114
[2025-05-07 17:25:22,334 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,334 INFO  L485      AbstractCegarLoop]: Abstraction has 145 states and 162 transitions.
[2025-05-07 17:25:22,334 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 8.333333333333334) internal successors, (50), 7 states have internal predecessors, (50), 4 states have call successors, (32), 1 states have call predecessors, (32), 6 states have return successors, (32), 6 states have call predecessors, (32), 4 states have call successors, (32)
[2025-05-07 17:25:22,334 INFO  L278                IsEmpty]: Start isEmpty. Operand 145 states and 162 transitions.
[2025-05-07 17:25:22,335 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:22,335 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,335 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]
[2025-05-07 17:25:22,335 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:25:22,335 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,336 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,336 INFO  L85        PathProgramCache]: Analyzing trace with hash -1269247901, now seen corresponding path program 1 times
[2025-05-07 17:25:22,336 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,336 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [201646955]
[2025-05-07 17:25:22,336 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,336 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,373 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:22,387 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:22,387 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,387 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,504 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:25:22,504 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,504 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [201646955]
[2025-05-07 17:25:22,505 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [201646955] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,505 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,505 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:22,505 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1101488730]
[2025-05-07 17:25:22,505 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,505 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:22,505 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,506 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:22,506 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:22,506 INFO  L87              Difference]: Start difference. First operand 145 states and 162 transitions. Second operand  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:25:22,539 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,539 INFO  L93              Difference]: Finished difference Result 151 states and 168 transitions.
[2025-05-07 17:25:22,539 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:22,539 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34) Word has length 120
[2025-05-07 17:25:22,539 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,540 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:25:22,540 INFO  L226             Difference]: Without dead ends: 151
[2025-05-07 17:25:22,540 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:25:22,540 INFO  L437           NwaCegarLoop]: 161 mSDtfsCounter, 1 mSDsluCounter, 629 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 790 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,540 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 790 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,541 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 151 states.
[2025-05-07 17:25:22,543 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 151 to 149.
[2025-05-07 17:25:22,543 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 63 states have (on average 1.0158730158730158) internal successors, (64), 64 states have internal predecessors, (64), 47 states have call successors, (50), 38 states have call predecessors, (50), 40 states have return successors, (52), 46 states have call predecessors, (52), 47 states have call successors, (52)
[2025-05-07 17:25:22,544 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 166 transitions.
[2025-05-07 17:25:22,544 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 166 transitions. Word has length 120
[2025-05-07 17:25:22,544 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,545 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 166 transitions.
[2025-05-07 17:25:22,545 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:25:22,545 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 166 transitions.
[2025-05-07 17:25:22,545 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:22,545 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,546 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]
[2025-05-07 17:25:22,546 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:25:22,546 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,546 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,546 INFO  L85        PathProgramCache]: Analyzing trace with hash -449342949, now seen corresponding path program 1 times
[2025-05-07 17:25:22,546 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,546 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [272206925]
[2025-05-07 17:25:22,546 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,546 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,574 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:22,579 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:22,579 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,579 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,662 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:25:22,662 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,662 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [272206925]
[2025-05-07 17:25:22,662 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [272206925] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,662 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,662 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:22,663 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1483296730]
[2025-05-07 17:25:22,663 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:22,663 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,663 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:22,663 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:22,663 INFO  L87              Difference]: Start difference. First operand 149 states and 166 transitions. Second operand  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:25:22,702 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,702 INFO  L93              Difference]: Finished difference Result 153 states and 172 transitions.
[2025-05-07 17:25:22,703 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:22,703 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34) Word has length 120
[2025-05-07 17:25:22,703 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,704 INFO  L225             Difference]: With dead ends: 153
[2025-05-07 17:25:22,704 INFO  L226             Difference]: Without dead ends: 153
[2025-05-07 17:25:22,704 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:25:22,704 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 1 mSDsluCounter, 636 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 799 SdHoareTripleChecker+Invalid, 29 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,705 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 799 Invalid, 29 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,705 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-05-07 17:25:22,709 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 153.
[2025-05-07 17:25:22,709 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 153 states, 65 states have (on average 1.0153846153846153) internal successors, (66), 66 states have internal predecessors, (66), 47 states have call successors, (50), 38 states have call predecessors, (50), 42 states have return successors, (56), 48 states have call predecessors, (56), 47 states have call successors, (56)
[2025-05-07 17:25:22,710 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 153 states to 153 states and 172 transitions.
[2025-05-07 17:25:22,710 INFO  L79                 Accepts]: Start accepts. Automaton has 153 states and 172 transitions. Word has length 120
[2025-05-07 17:25:22,710 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,710 INFO  L485      AbstractCegarLoop]: Abstraction has 153 states and 172 transitions.
[2025-05-07 17:25:22,711 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:25:22,711 INFO  L278                IsEmpty]: Start isEmpty. Operand 153 states and 172 transitions.
[2025-05-07 17:25:22,711 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:22,711 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,711 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]
[2025-05-07 17:25:22,711 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:25:22,711 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,712 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,712 INFO  L85        PathProgramCache]: Analyzing trace with hash -2029646693, now seen corresponding path program 1 times
[2025-05-07 17:25:22,712 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,712 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [60282323]
[2025-05-07 17:25:22,712 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,712 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,748 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:22,758 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:22,758 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,758 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,867 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:25:22,867 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,867 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [60282323]
[2025-05-07 17:25:22,867 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [60282323] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,867 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,867 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:25:22,868 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2061755292]
[2025-05-07 17:25:22,868 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,868 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:25:22,868 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,869 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:25:22,869 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:22,869 INFO  L87              Difference]: Start difference. First operand 153 states and 172 transitions. Second operand  has 8 states, 7 states have (on average 7.428571428571429) internal successors, (52), 8 states have internal predecessors, (52), 5 states have call successors, (34), 1 states have call predecessors, (34), 7 states have return successors, (34), 7 states have call predecessors, (34), 5 states have call successors, (34)
[2025-05-07 17:25:22,926 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,926 INFO  L93              Difference]: Finished difference Result 162 states and 183 transitions.
[2025-05-07 17:25:22,926 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:25:22,927 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 7.428571428571429) internal successors, (52), 8 states have internal predecessors, (52), 5 states have call successors, (34), 1 states have call predecessors, (34), 7 states have return successors, (34), 7 states have call predecessors, (34), 5 states have call successors, (34) Word has length 120
[2025-05-07 17:25:22,927 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,928 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:25:22,928 INFO  L226             Difference]: Without dead ends: 162
[2025-05-07 17:25:22,928 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:22,928 INFO  L437           NwaCegarLoop]: 160 mSDtfsCounter, 1 mSDsluCounter, 943 mSDsCounter, 0 mSdLazyCounter, 47 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1103 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 47 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,929 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1103 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 47 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:22,929 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 162 states.
[2025-05-07 17:25:22,933 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 162 to 162.
[2025-05-07 17:25:22,934 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 69 states have (on average 1.0144927536231885) internal successors, (70), 70 states have internal predecessors, (70), 48 states have call successors, (51), 38 states have call predecessors, (51), 46 states have return successors, (62), 53 states have call predecessors, (62), 48 states have call successors, (62)
[2025-05-07 17:25:22,935 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 183 transitions.
[2025-05-07 17:25:22,935 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 183 transitions. Word has length 120
[2025-05-07 17:25:22,935 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,935 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 183 transitions.
[2025-05-07 17:25:22,935 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 7.428571428571429) internal successors, (52), 8 states have internal predecessors, (52), 5 states have call successors, (34), 1 states have call predecessors, (34), 7 states have return successors, (34), 7 states have call predecessors, (34), 5 states have call successors, (34)
[2025-05-07 17:25:22,935 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 183 transitions.
[2025-05-07 17:25:22,936 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 118
[2025-05-07 17:25:22,936 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,936 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]
[2025-05-07 17:25:22,936 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:25:22,936 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,937 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,937 INFO  L85        PathProgramCache]: Analyzing trace with hash 1911705048, now seen corresponding path program 1 times
[2025-05-07 17:25:22,937 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,937 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1923906570]
[2025-05-07 17:25:22,937 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,937 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,978 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 117 statements into 1 equivalence classes.
[2025-05-07 17:25:22,993 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 117 of 117 statements.
[2025-05-07 17:25:22,993 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,993 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,095 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:25:23,095 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,095 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1923906570]
[2025-05-07 17:25:23,095 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1923906570] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,095 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,095 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:23,095 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [23375984]
[2025-05-07 17:25:23,095 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,096 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:23,096 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,096 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:23,096 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:23,097 INFO  L87              Difference]: Start difference. First operand 162 states and 183 transitions. Second operand  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:25:23,146 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,146 INFO  L93              Difference]: Finished difference Result 164 states and 184 transitions.
[2025-05-07 17:25:23,146 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:23,146 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33) Word has length 117
[2025-05-07 17:25:23,147 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,148 INFO  L225             Difference]: With dead ends: 164
[2025-05-07 17:25:23,148 INFO  L226             Difference]: Without dead ends: 164
[2025-05-07 17:25:23,148 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:25:23,148 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 1 mSDsluCounter, 635 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 798 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,148 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 798 Invalid, 35 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:23,149 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 164 states.
[2025-05-07 17:25:23,154 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 164 to 162.
[2025-05-07 17:25:23,154 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 69 states have (on average 1.0144927536231885) internal successors, (70), 70 states have internal predecessors, (70), 48 states have call successors, (51), 38 states have call predecessors, (51), 46 states have return successors, (61), 53 states have call predecessors, (61), 48 states have call successors, (61)
[2025-05-07 17:25:23,155 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 182 transitions.
[2025-05-07 17:25:23,155 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 182 transitions. Word has length 117
[2025-05-07 17:25:23,155 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,155 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 182 transitions.
[2025-05-07 17:25:23,155 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:25:23,156 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 182 transitions.
[2025-05-07 17:25:23,156 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 124
[2025-05-07 17:25:23,156 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,157 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:23,157 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:25:23,157 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,157 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,157 INFO  L85        PathProgramCache]: Analyzing trace with hash 1896164953, now seen corresponding path program 1 times
[2025-05-07 17:25:23,157 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,157 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [125533307]
[2025-05-07 17:25:23,157 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,158 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,196 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 123 statements into 1 equivalence classes.
[2025-05-07 17:25:23,206 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 123 of 123 statements.
[2025-05-07 17:25:23,206 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,206 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,304 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:25:23,304 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,304 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [125533307]
[2025-05-07 17:25:23,304 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [125533307] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,304 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,305 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:23,305 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [290916936]
[2025-05-07 17:25:23,305 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,305 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:23,305 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,306 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:23,306 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:23,306 INFO  L87              Difference]: Start difference. First operand 162 states and 182 transitions. Second operand  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 5 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 5 states have call successors, (35)
[2025-05-07 17:25:23,334 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,334 INFO  L93              Difference]: Finished difference Result 167 states and 188 transitions.
[2025-05-07 17:25:23,334 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:23,334 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), 5 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 5 states have call successors, (35) Word has length 123
[2025-05-07 17:25:23,334 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,335 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:25:23,335 INFO  L226             Difference]: Without dead ends: 167
[2025-05-07 17:25:23,335 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:25:23,336 INFO  L437           NwaCegarLoop]: 165 mSDtfsCounter, 1 mSDsluCounter, 644 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 809 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,336 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 809 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:23,336 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 167 states.
[2025-05-07 17:25:23,340 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 167 to 162.
[2025-05-07 17:25:23,340 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 69 states have (on average 1.0144927536231885) internal successors, (70), 70 states have internal predecessors, (70), 48 states have call successors, (51), 38 states have call predecessors, (51), 46 states have return successors, (61), 53 states have call predecessors, (61), 48 states have call successors, (61)
[2025-05-07 17:25:23,341 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 182 transitions.
[2025-05-07 17:25:23,341 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 182 transitions. Word has length 123
[2025-05-07 17:25:23,341 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,341 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 182 transitions.
[2025-05-07 17:25:23,341 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), 5 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 5 states have call successors, (35)
[2025-05-07 17:25:23,341 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 182 transitions.
[2025-05-07 17:25:23,342 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 118
[2025-05-07 17:25:23,342 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,342 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]
[2025-05-07 17:25:23,342 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:25:23,342 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,343 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,343 INFO  L85        PathProgramCache]: Analyzing trace with hash 425211992, now seen corresponding path program 1 times
[2025-05-07 17:25:23,343 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,343 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2091043025]
[2025-05-07 17:25:23,343 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,343 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,388 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 117 statements into 1 equivalence classes.
[2025-05-07 17:25:23,402 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 117 of 117 statements.
[2025-05-07 17:25:23,402 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,402 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,552 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:25:23,552 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,552 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2091043025]
[2025-05-07 17:25:23,552 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2091043025] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,552 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,553 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:25:23,553 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2138504503]
[2025-05-07 17:25:23,553 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,553 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:25:23,553 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,554 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:25:23,554 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:25:23,554 INFO  L87              Difference]: Start difference. First operand 162 states and 182 transitions. Second operand  has 10 states, 9 states have (on average 5.666666666666667) internal successors, (51), 10 states have internal predecessors, (51), 6 states have call successors, (33), 1 states have call predecessors, (33), 9 states have return successors, (33), 9 states have call predecessors, (33), 6 states have call successors, (33)
[2025-05-07 17:25:23,652 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,652 INFO  L93              Difference]: Finished difference Result 171 states and 193 transitions.
[2025-05-07 17:25:23,653 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:25:23,653 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 5.666666666666667) internal successors, (51), 10 states have internal predecessors, (51), 6 states have call successors, (33), 1 states have call predecessors, (33), 9 states have return successors, (33), 9 states have call predecessors, (33), 6 states have call successors, (33) Word has length 117
[2025-05-07 17:25:23,653 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,654 INFO  L225             Difference]: With dead ends: 171
[2025-05-07 17:25:23,654 INFO  L226             Difference]: Without dead ends: 171
[2025-05-07 17:25:23,654 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:25:23,656 INFO  L437           NwaCegarLoop]: 161 mSDtfsCounter, 1 mSDsluCounter, 1261 mSDsCounter, 0 mSdLazyCounter, 98 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1422 SdHoareTripleChecker+Invalid, 98 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 98 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,656 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1422 Invalid, 98 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 98 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:23,657 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 171 states.
[2025-05-07 17:25:23,661 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 171 to 162.
[2025-05-07 17:25:23,661 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 69 states have (on average 1.0144927536231885) internal successors, (70), 70 states have internal predecessors, (70), 48 states have call successors, (51), 38 states have call predecessors, (51), 46 states have return successors, (61), 53 states have call predecessors, (61), 48 states have call successors, (61)
[2025-05-07 17:25:23,662 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 182 transitions.
[2025-05-07 17:25:23,662 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 182 transitions. Word has length 117
[2025-05-07 17:25:23,662 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,662 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 182 transitions.
[2025-05-07 17:25:23,662 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 5.666666666666667) internal successors, (51), 10 states have internal predecessors, (51), 6 states have call successors, (33), 1 states have call predecessors, (33), 9 states have return successors, (33), 9 states have call predecessors, (33), 6 states have call successors, (33)
[2025-05-07 17:25:23,663 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 182 transitions.
[2025-05-07 17:25:23,663 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:23,664 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,664 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]
[2025-05-07 17:25:23,664 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:25:23,664 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,664 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,664 INFO  L85        PathProgramCache]: Analyzing trace with hash 2007512685, now seen corresponding path program 1 times
[2025-05-07 17:25:23,664 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,664 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1520583294]
[2025-05-07 17:25:23,664 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,665 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,706 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:23,713 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:23,713 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,713 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,794 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:25:23,794 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,794 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1520583294]
[2025-05-07 17:25:23,794 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1520583294] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,794 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,794 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:23,794 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1762980112]
[2025-05-07 17:25:23,794 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,795 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:23,795 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,795 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:23,795 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:23,795 INFO  L87              Difference]: Start difference. First operand 162 states and 182 transitions. Second operand  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 5 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:25:23,829 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,829 INFO  L93              Difference]: Finished difference Result 162 states and 181 transitions.
[2025-05-07 17:25:23,830 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:23,830 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 5 states have call predecessors, (34), 4 states have call successors, (34) Word has length 120
[2025-05-07 17:25:23,830 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,831 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:25:23,831 INFO  L226             Difference]: Without dead ends: 162
[2025-05-07 17:25:23,831 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:25:23,832 INFO  L437           NwaCegarLoop]: 162 mSDtfsCounter, 1 mSDsluCounter, 632 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 794 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,832 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 794 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:23,832 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 162 states.
[2025-05-07 17:25:23,836 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 162 to 162.
[2025-05-07 17:25:23,837 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 69 states have (on average 1.0144927536231885) internal successors, (70), 70 states have internal predecessors, (70), 48 states have call successors, (51), 38 states have call predecessors, (51), 46 states have return successors, (60), 53 states have call predecessors, (60), 48 states have call successors, (60)
[2025-05-07 17:25:23,837 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 181 transitions.
[2025-05-07 17:25:23,838 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 181 transitions. Word has length 120
[2025-05-07 17:25:23,838 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,838 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 181 transitions.
[2025-05-07 17:25:23,838 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 5 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:25:23,838 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 181 transitions.
[2025-05-07 17:25:23,839 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:23,839 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,839 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]
[2025-05-07 17:25:23,839 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:25:23,839 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,840 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,840 INFO  L85        PathProgramCache]: Analyzing trace with hash 303229933, now seen corresponding path program 1 times
[2025-05-07 17:25:23,840 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,840 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [200715641]
[2025-05-07 17:25:23,840 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,840 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,887 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:23,894 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:23,894 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,894 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:24,042 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:25:24,042 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:24,042 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [200715641]
[2025-05-07 17:25:24,042 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [200715641] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:24,042 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:24,042 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:25:24,042 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1519141655]
[2025-05-07 17:25:24,042 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:24,043 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:25:24,043 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:24,043 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:25:24,043 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:25:24,043 INFO  L87              Difference]: Start difference. First operand 162 states and 181 transitions. Second operand  has 9 states, 8 states have (on average 6.5) internal successors, (52), 9 states have internal predecessors, (52), 5 states have call successors, (34), 1 states have call predecessors, (34), 8 states have return successors, (34), 8 states have call predecessors, (34), 5 states have call successors, (34)
[2025-05-07 17:25:24,106 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:24,107 INFO  L93              Difference]: Finished difference Result 99 states and 111 transitions.
[2025-05-07 17:25:24,107 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:25:24,107 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 6.5) internal successors, (52), 9 states have internal predecessors, (52), 5 states have call successors, (34), 1 states have call predecessors, (34), 8 states have return successors, (34), 8 states have call predecessors, (34), 5 states have call successors, (34) Word has length 120
[2025-05-07 17:25:24,107 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:24,107 INFO  L225             Difference]: With dead ends: 99
[2025-05-07 17:25:24,107 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:25:24,107 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:25:24,108 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 0 mSDsluCounter, 646 mSDsCounter, 0 mSdLazyCounter, 71 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 741 SdHoareTripleChecker+Invalid, 71 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 71 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:24,108 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 741 Invalid, 71 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 71 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:24,108 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:25:24,108 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:25:24,108 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:25:24,108 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:25:24,108 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 120
[2025-05-07 17:25:24,108 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:24,108 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:25:24,108 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 6.5) internal successors, (52), 9 states have internal predecessors, (52), 5 states have call successors, (34), 1 states have call predecessors, (34), 8 states have return successors, (34), 8 states have call predecessors, (34), 5 states have call successors, (34)
[2025-05-07 17:25:24,109 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:25:24,109 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:25:24,110 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:25:24,111 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24
[2025-05-07 17:25:24,113 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:24,114 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:25:24,117 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:25:24 BoogieIcfgContainer
[2025-05-07 17:25:24,117 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:25:24,117 INFO  L158              Benchmark]: Toolchain (without parser) took 6380.30ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 189.9MB in the beginning and 240.0MB in the end (delta: -50.1MB). Peak memory consumption was 153.4MB. Max. memory is 33.6GB.
[2025-05-07 17:25:24,117 INFO  L158              Benchmark]: SmtParser took 0.19ms. 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:25:24,117 INFO  L158              Benchmark]: ChcToBoogie took 55.82ms. Allocated memory is still 234.9MB. Free memory was 189.9MB in the beginning and 183.0MB in the end (delta: 6.9MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:24,118 INFO  L158              Benchmark]: Boogie Preprocessor took 103.64ms. Allocated memory is still 234.9MB. Free memory was 183.0MB in the beginning and 177.2MB in the end (delta: 5.8MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:25:24,118 INFO  L158              Benchmark]: RCFGBuilder took 802.57ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 176.8MB in the beginning and 230.8MB in the end (delta: -54.0MB). Peak memory consumption was 77.8MB. Max. memory is 33.6GB.
[2025-05-07 17:25:24,118 INFO  L158              Benchmark]: TraceAbstraction took 5414.07ms. Allocated memory was 318.8MB in the beginning and 436.2MB in the end (delta: 117.4MB). Free memory was 230.0MB in the beginning and 240.0MB in the end (delta: -10.0MB). Peak memory consumption was 109.2MB. Max. memory is 33.6GB.
[2025-05-07 17:25:24,118 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.19ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 55.82ms. Allocated memory is still 234.9MB. Free memory was 189.9MB in the beginning and 183.0MB in the end (delta: 6.9MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 103.64ms. Allocated memory is still 234.9MB. Free memory was 183.0MB in the beginning and 177.2MB in the end (delta: 5.8MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 802.57ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 176.8MB in the beginning and 230.8MB in the end (delta: -54.0MB). Peak memory consumption was 77.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 5414.07ms. Allocated memory was 318.8MB in the beginning and 436.2MB in the end (delta: 117.4MB). Free memory was 230.0MB in the beginning and 240.0MB in the end (delta: -10.0MB). Peak memory consumption was 109.2MB. 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 84 procedures, 339 locations, 536 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 5.4s, OverallIterations: 24, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.2s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 59 SdHoareTripleChecker+Valid, 0.8s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 18 mSDsluCounter, 30877 SdHoareTripleChecker+Invalid, 0.7s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 24635 mSDsCounter, 7 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 705 IncrementalHoareTripleChecker+Invalid, 712 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 7 mSolverCounterUnsat, 6242 mSDtfsCounter, 705 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 150 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 102 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=339occurred in iteration=0, InterpolantAutomatonStates: 150, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 24 MinimizatonAttempts, 31 StatesRemovedByMinimization, 9 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.2s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 2.6s InterpolantComputationTime, 2405 NumberOfCodeBlocks, 2405 NumberOfCodeBlocksAsserted, 24 NumberOfCheckSat, 2381 ConstructedInterpolants, 0 QuantifiedInterpolants, 2883 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 24 InterpolantComputations, 24 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:25:24,131 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
