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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:25:20,435 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:25:20,481 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a7e63eee-a228-4a68-ac92-657ee39fe965/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:25:20,484 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:25:20,485 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:25:20,497 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:25:20,498 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:25:20,498 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:25:20,498 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:25:20,498 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:25:20,498 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:25:20,498 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:25:20,498 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:25:20,498 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:25:20,499 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:20,499 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:25:20,499 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:25:20,500 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:25:20,500 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:25:20,500 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:25:20,681 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:25:20,688 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:25:20,689 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:25:20,690 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:25:20,690 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:25:20,691 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a7e63eee-a228-4a68-ac92-657ee39fe965/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/function_inline_chain.sol_0_no_adts_000.smt2
[2025-05-07 17:25:20,692 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:25:20,695 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:25:20,940 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a7e63eee-a228-4a68-ac92-657ee39fe965/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/function_inline_chain.sol_0_no_adts_000.smt2
[2025-05-07 17:25:20,942 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:25:20,943 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:25:20,944 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:25:20,944 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:25:20,944 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:25:20,946 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:20,975 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20 Unit
[2025-05-07 17:25:20,975 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:25:20,976 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:25:20,976 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:25:20,976 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:25:20,987 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:20,987 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,008 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,009 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,013 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,014 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,015 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,017 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,018 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,028 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:25:21,029 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:25:21,029 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:25:21,029 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:25:21,030 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (1/1) ...
[2025-05-07 17:25:21,032 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:21,040 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:21,048 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:21,050 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:21,057 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:25:21,058 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:25:21,058 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:25:21,058 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_5_0 given in one single declaration
[2025-05-07 17:25:21,058 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_5_0
[2025-05-07 17:25:21,058 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_5_0
[2025-05-07 17:25:21,058 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,058 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__19_44_0
[2025-05-07 17:25:21,058 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__19_44_0
[2025-05-07 17:25:21,058 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,058 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__19_44_0
[2025-05-07 17:25:21,058 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__19_44_0
[2025-05-07 17:25:21,059 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,059 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__19_44_0
[2025-05-07 17:25:21,059 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__19_44_0
[2025-05-07 17:25:21,059 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_f_18_44_0 given in one single declaration
[2025-05-07 17:25:21,059 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_f_18_44_0
[2025-05-07 17:25:21,059 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_f_18_44_0
[2025-05-07 17:25:21,059 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_if_header_f_11_44_0 given in one single declaration
[2025-05-07 17:25:21,059 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_if_header_f_11_44_0
[2025-05-07 17:25:21,059 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_if_header_f_11_44_0
[2025-05-07 17:25:21,059 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_18_44_0 given in one single declaration
[2025-05-07 17:25:21,059 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_18_44_0
[2025-05-07 17:25:21,059 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_18_44_0
[2025-05-07 17:25:21,060 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,060 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__19_44_0
[2025-05-07 17:25:21,060 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__19_44_0
[2025-05-07 17:25:21,060 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,060 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__19_44_0
[2025-05-07 17:25:21,060 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__19_44_0
[2025-05-07 17:25:21,060 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_g__30_44_0 given in one single declaration
[2025-05-07 17:25:21,060 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_g__30_44_0
[2025-05-07 17:25:21,060 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_g__30_44_0
[2025-05-07 17:25:21,060 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_g__30_44_0 given in one single declaration
[2025-05-07 17:25:21,060 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_g__30_44_0
[2025-05-07 17:25:21,060 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_g__30_44_0
[2025-05-07 17:25:21,060 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_return_function_g__30_44_0 given in one single declaration
[2025-05-07 17:25:21,060 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_return_function_g__30_44_0
[2025-05-07 17:25:21,060 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_return_function_g__30_44_0
[2025-05-07 17:25:21,060 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_h__43_44_0 given in one single declaration
[2025-05-07 17:25:21,060 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_h__43_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_h__43_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_return_function_h__43_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_return_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_return_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_23_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_23_function_f__19_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_23_function_f__19_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_h_42_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_h_42_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_h_42_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_function_h__43_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_function_h__43_44_0
[2025-05-07 17:25:21,061 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_g_29_44_0 given in one single declaration
[2025-05-07 17:25:21,061 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_g_29_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_g_29_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_g__30_44_0 given in one single declaration
[2025-05-07 17:25:21,062 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_g__30_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_g__30_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_if_true_f_10_44_0 given in one single declaration
[2025-05-07 17:25:21,062 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_if_true_f_10_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_if_true_f_10_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__19_44_0 given in one single declaration
[2025-05-07 17:25:21,062 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__19_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__19_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_44_0 given in one single declaration
[2025-05-07 17:25:21,062 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_44_0 given in one single declaration
[2025-05-07 17:25:21,062 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_25_C_44_0 given in one single declaration
[2025-05-07 17:25:21,062 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_25_C_44_0
[2025-05-07 17:25:21,062 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_25_C_44_0
[2025-05-07 17:25:21,062 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_27_C_44_0 given in one single declaration
[2025-05-07 17:25:21,063 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_27_C_44_0
[2025-05-07 17:25:21,063 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_27_C_44_0
[2025-05-07 17:25:21,063 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_26_C_44_0 given in one single declaration
[2025-05-07 17:25:21,063 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_26_C_44_0
[2025-05-07 17:25:21,063 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_26_C_44_0
[2025-05-07 17:25:21,063 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_28_C_44_0 given in one single declaration
[2025-05-07 17:25:21,063 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_28_C_44_0
[2025-05-07 17:25:21,063 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_28_C_44_0
[2025-05-07 17:25:21,063 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:25:21,063 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:25:21,063 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:25:21,208 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:25:21,210 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:25:21,429 INFO  L?                        ?]: Removed 181 outVars from TransFormulas that were not future-live.
[2025-05-07 17:25:21,429 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:25:21,438 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:25:21,438 INFO  L312             CfgBuilder]: Removed 16 assume(true) statements.
[2025-05-07 17:25:21,438 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:21 BoogieIcfgContainer
[2025-05-07 17:25:21,438 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:25:21,440 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:25:21,440 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:25:21,443 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:25:21,443 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:20" (1/3) ...
[2025-05-07 17:25:21,443 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@454dfd3b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:25:21, skipping insertion in model container
[2025-05-07 17:25:21,443 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:20" (2/3) ...
[2025-05-07 17:25:21,443 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@454dfd3b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:25:21, skipping insertion in model container
[2025-05-07 17:25:21,443 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:21" (3/3) ...
[2025-05-07 17:25:21,444 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:25:21,454 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:25:21,456 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 31 procedures, 123 locations, 190 edges, 31 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:25:21,486 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:25:21,495 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;@7ad3de3a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:25:21,495 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:25:21,498 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 123 states, 51 states have (on average 1.0784313725490196) internal successors, (55), 55 states have internal predecessors, (55), 43 states have call successors, (45), 30 states have call predecessors, (45), 30 states have return successors, (45), 37 states have call predecessors, (45), 43 states have call successors, (45)
[2025-05-07 17:25:21,505 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:25:21,505 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,506 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]
[2025-05-07 17:25:21,506 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,510 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,510 INFO  L85        PathProgramCache]: Analyzing trace with hash 1300017642, now seen corresponding path program 1 times
[2025-05-07 17:25:21,515 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,515 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [590739395]
[2025-05-07 17:25:21,516 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,516 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,561 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:25:21,579 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:25:21,579 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:21,579 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:21,770 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,771 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:21,771 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [590739395]
[2025-05-07 17:25:21,771 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [590739395] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:21,771 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:21,773 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:21,774 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1972077108]
[2025-05-07 17:25:21,775 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:21,778 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:21,778 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:21,808 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:21,809 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:21,810 INFO  L87              Difference]: Start difference. First operand  has 123 states, 51 states have (on average 1.0784313725490196) internal successors, (55), 55 states have internal predecessors, (55), 43 states have call successors, (45), 30 states have call predecessors, (45), 30 states have return successors, (45), 37 states have call predecessors, (45), 43 states have call successors, (45) Second operand  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:25:21,866 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:21,867 INFO  L93              Difference]: Finished difference Result 125 states and 147 transitions.
[2025-05-07 17:25:21,868 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:21,870 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16) Word has length 58
[2025-05-07 17:25:21,870 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:21,878 INFO  L225             Difference]: With dead ends: 125
[2025-05-07 17:25:21,878 INFO  L226             Difference]: Without dead ends: 121
[2025-05-07 17:25:21,880 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,883 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 1 mSDsluCounter, 280 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 424 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:21,884 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 424 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:21,896 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-05-07 17:25:21,925 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 119.
[2025-05-07 17:25:21,926 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 119 states, 50 states have (on average 1.04) internal successors, (52), 52 states have internal predecessors, (52), 41 states have call successors, (43), 30 states have call predecessors, (43), 30 states have return successors, (43), 36 states have call predecessors, (43), 41 states have call successors, (43)
[2025-05-07 17:25:21,932 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 119 states to 119 states and 138 transitions.
[2025-05-07 17:25:21,933 INFO  L79                 Accepts]: Start accepts. Automaton has 119 states and 138 transitions. Word has length 58
[2025-05-07 17:25:21,933 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:21,933 INFO  L485      AbstractCegarLoop]: Abstraction has 119 states and 138 transitions.
[2025-05-07 17:25:21,934 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:25:21,934 INFO  L278                IsEmpty]: Start isEmpty. Operand 119 states and 138 transitions.
[2025-05-07 17:25:21,936 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:25:21,937 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,937 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]
[2025-05-07 17:25:21,937 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:25:21,937 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,938 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,938 INFO  L85        PathProgramCache]: Analyzing trace with hash 2080591622, now seen corresponding path program 1 times
[2025-05-07 17:25:21,938 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:21,938 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1431593697]
[2025-05-07 17:25:21,938 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:21,938 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:21,974 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:25:22,006 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:25:22,006 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,006 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,196 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,196 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,196 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1431593697]
[2025-05-07 17:25:22,196 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1431593697] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,197 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,197 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:22,197 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1765843183]
[2025-05-07 17:25:22,197 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,198 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:22,198 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,199 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:22,199 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:22,199 INFO  L87              Difference]: Start difference. First operand 119 states and 138 transitions. Second operand  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:25:22,237 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,238 INFO  L93              Difference]: Finished difference Result 121 states and 140 transitions.
[2025-05-07 17:25:22,238 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:22,239 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16) Word has length 58
[2025-05-07 17:25:22,239 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,241 INFO  L225             Difference]: With dead ends: 121
[2025-05-07 17:25:22,241 INFO  L226             Difference]: Without dead ends: 121
[2025-05-07 17:25:22,241 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:22,242 INFO  L437           NwaCegarLoop]: 136 mSDtfsCounter, 1 mSDsluCounter, 264 mSDsCounter, 0 mSdLazyCounter, 9 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 400 SdHoareTripleChecker+Invalid, 9 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 9 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,242 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 400 Invalid, 9 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 9 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,243 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-05-07 17:25:22,253 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 121.
[2025-05-07 17:25:22,253 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 121 states, 51 states have (on average 1.0392156862745099) internal successors, (53), 53 states have internal predecessors, (53), 41 states have call successors, (43), 30 states have call predecessors, (43), 31 states have return successors, (44), 37 states have call predecessors, (44), 41 states have call successors, (44)
[2025-05-07 17:25:22,255 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 121 states to 121 states and 140 transitions.
[2025-05-07 17:25:22,255 INFO  L79                 Accepts]: Start accepts. Automaton has 121 states and 140 transitions. Word has length 58
[2025-05-07 17:25:22,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,256 INFO  L485      AbstractCegarLoop]: Abstraction has 121 states and 140 transitions.
[2025-05-07 17:25:22,256 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:25:22,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 121 states and 140 transitions.
[2025-05-07 17:25:22,258 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:25:22,259 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,259 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]
[2025-05-07 17:25:22,259 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:25:22,259 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,259 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,260 INFO  L85        PathProgramCache]: Analyzing trace with hash 1432954214, now seen corresponding path program 1 times
[2025-05-07 17:25:22,260 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,260 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [178511119]
[2025-05-07 17:25:22,260 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,260 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,290 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:25:22,312 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:25:22,312 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,312 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,812 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:22,812 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,812 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [178511119]
[2025-05-07 17:25:22,812 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [178511119] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,812 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,812 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [] total 18
[2025-05-07 17:25:22,812 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [628525961]
[2025-05-07 17:25:22,812 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,813 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:25:22,813 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,813 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:25:22,814 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=34, Invalid=272, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:25:22,814 INFO  L87              Difference]: Start difference. First operand 121 states and 140 transitions. Second operand  has 18 states, 14 states have (on average 1.8571428571428572) internal successors, (26), 16 states have internal predecessors, (26), 6 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (16), 14 states have call predecessors, (16), 6 states have call successors, (16)
[2025-05-07 17:25:23,095 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,095 INFO  L93              Difference]: Finished difference Result 132 states and 155 transitions.
[2025-05-07 17:25:23,095 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:25:23,095 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 14 states have (on average 1.8571428571428572) internal successors, (26), 16 states have internal predecessors, (26), 6 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (16), 14 states have call predecessors, (16), 6 states have call successors, (16) Word has length 58
[2025-05-07 17:25:23,096 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,097 INFO  L225             Difference]: With dead ends: 132
[2025-05-07 17:25:23,097 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:25:23,098 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 21 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=338, Unknown=0, NotChecked=0, Total=380
[2025-05-07 17:25:23,098 INFO  L437           NwaCegarLoop]: 122 mSDtfsCounter, 4 mSDsluCounter, 1796 mSDsCounter, 0 mSdLazyCounter, 281 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 1918 SdHoareTripleChecker+Invalid, 281 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 281 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,098 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 1918 Invalid, 281 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 281 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:25:23,099 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:25:23,109 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 130.
[2025-05-07 17:25:23,110 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 55 states have (on average 1.0363636363636364) internal successors, (57), 57 states have internal predecessors, (57), 42 states have call successors, (44), 30 states have call predecessors, (44), 35 states have return successors, (52), 42 states have call predecessors, (52), 42 states have call successors, (52)
[2025-05-07 17:25:23,111 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 153 transitions.
[2025-05-07 17:25:23,111 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 153 transitions. Word has length 58
[2025-05-07 17:25:23,111 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,112 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 153 transitions.
[2025-05-07 17:25:23,112 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 14 states have (on average 1.8571428571428572) internal successors, (26), 16 states have internal predecessors, (26), 6 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (16), 14 states have call predecessors, (16), 6 states have call successors, (16)
[2025-05-07 17:25:23,112 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 153 transitions.
[2025-05-07 17:25:23,114 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:25:23,114 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,114 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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,115 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:25:23,115 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,115 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,115 INFO  L85        PathProgramCache]: Analyzing trace with hash 987980272, now seen corresponding path program 1 times
[2025-05-07 17:25:23,115 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,115 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1140525806]
[2025-05-07 17:25:23,115 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,116 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,150 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:25:23,164 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:25:23,164 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,164 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,600 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 2 proven. 16 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:25:23,600 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,600 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1140525806]
[2025-05-07 17:25:23,600 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1140525806] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:23,600 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [608779503]
[2025-05-07 17:25:23,600 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,600 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:23,602 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:23,604 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:23,605 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:25:23,834 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:25:23,978 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:25:23,978 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,978 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,984 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1188 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:23,991 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:24,358 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 29 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:24,358 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:24,358 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [608779503] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:24,358 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:24,358 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [18] total 34
[2025-05-07 17:25:24,359 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1824367734]
[2025-05-07 17:25:24,359 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:24,359 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:25:24,359 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:24,360 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:25:24,360 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=81, Invalid=1041, Unknown=0, NotChecked=0, Total=1122
[2025-05-07 17:25:24,360 INFO  L87              Difference]: Start difference. First operand 130 states and 153 transitions. Second operand  has 18 states, 14 states have (on average 2.857142857142857) internal successors, (40), 16 states have internal predecessors, (40), 7 states have call successors, (25), 2 states have call predecessors, (25), 14 states have return successors, (25), 14 states have call predecessors, (25), 7 states have call successors, (25)
[2025-05-07 17:25:24,638 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:24,638 INFO  L93              Difference]: Finished difference Result 133 states and 158 transitions.
[2025-05-07 17:25:24,639 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:25:24,639 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 14 states have (on average 2.857142857142857) internal successors, (40), 16 states have internal predecessors, (40), 7 states have call successors, (25), 2 states have call predecessors, (25), 14 states have return successors, (25), 14 states have call predecessors, (25), 7 states have call successors, (25) Word has length 90
[2025-05-07 17:25:24,639 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:24,641 INFO  L225             Difference]: With dead ends: 133
[2025-05-07 17:25:24,641 INFO  L226             Difference]: Without dead ends: 133
[2025-05-07 17:25:24,642 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 111 GetRequests, 75 SyntacticMatches, 0 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 126 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=97, Invalid=1309, Unknown=0, NotChecked=0, Total=1406
[2025-05-07 17:25:24,642 INFO  L437           NwaCegarLoop]: 122 mSDtfsCounter, 6 mSDsluCounter, 1915 mSDsCounter, 0 mSdLazyCounter, 314 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 2037 SdHoareTripleChecker+Invalid, 315 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 314 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:24,643 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 2037 Invalid, 315 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 314 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:25:24,644 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-05-07 17:25:24,653 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 131.
[2025-05-07 17:25:24,653 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 131 states, 55 states have (on average 1.0363636363636364) internal successors, (57), 57 states have internal predecessors, (57), 43 states have call successors, (45), 30 states have call predecessors, (45), 35 states have return successors, (53), 43 states have call predecessors, (53), 43 states have call successors, (53)
[2025-05-07 17:25:24,654 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 131 states to 131 states and 155 transitions.
[2025-05-07 17:25:24,655 INFO  L79                 Accepts]: Start accepts. Automaton has 131 states and 155 transitions. Word has length 90
[2025-05-07 17:25:24,655 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:24,655 INFO  L485      AbstractCegarLoop]: Abstraction has 131 states and 155 transitions.
[2025-05-07 17:25:24,655 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 14 states have (on average 2.857142857142857) internal successors, (40), 16 states have internal predecessors, (40), 7 states have call successors, (25), 2 states have call predecessors, (25), 14 states have return successors, (25), 14 states have call predecessors, (25), 7 states have call successors, (25)
[2025-05-07 17:25:24,655 INFO  L278                IsEmpty]: Start isEmpty. Operand 131 states and 155 transitions.
[2025-05-07 17:25:24,657 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 108
[2025-05-07 17:25:24,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:24,657 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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,664 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:25:24,858 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:24,858 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:24,860 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:24,860 INFO  L85        PathProgramCache]: Analyzing trace with hash 1241249872, now seen corresponding path program 1 times
[2025-05-07 17:25:24,860 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:24,860 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2088414901]
[2025-05-07 17:25:24,861 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:24,861 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:24,931 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:25:24,952 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:25:24,953 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:24,953 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:25,144 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:25:25,144 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:25,144 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2088414901]
[2025-05-07 17:25:25,144 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2088414901] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:25,144 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:25,144 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:25:25,144 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [532149767]
[2025-05-07 17:25:25,144 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:25,145 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:25:25,145 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:25,146 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:25:25,146 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:25:25,146 INFO  L87              Difference]: Start difference. First operand 131 states and 155 transitions. Second operand  has 10 states, 8 states have (on average 5.75) internal successors, (46), 10 states have internal predecessors, (46), 4 states have call successors, (29), 1 states have call predecessors, (29), 8 states have return successors, (30), 9 states have call predecessors, (30), 4 states have call successors, (30)
[2025-05-07 17:25:25,258 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:25,258 INFO  L93              Difference]: Finished difference Result 137 states and 163 transitions.
[2025-05-07 17:25:25,259 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:25:25,259 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 5.75) internal successors, (46), 10 states have internal predecessors, (46), 4 states have call successors, (29), 1 states have call predecessors, (29), 8 states have return successors, (30), 9 states have call predecessors, (30), 4 states have call successors, (30) Word has length 107
[2025-05-07 17:25:25,259 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:25,260 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:25:25,260 INFO  L226             Difference]: Without dead ends: 137
[2025-05-07 17:25:25,260 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:25:25,261 INFO  L437           NwaCegarLoop]: 129 mSDtfsCounter, 2 mSDsluCounter, 1003 mSDsCounter, 0 mSdLazyCounter, 108 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1132 SdHoareTripleChecker+Invalid, 109 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 108 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:25,261 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1132 Invalid, 109 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 108 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:25,262 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-05-07 17:25:25,271 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 135.
[2025-05-07 17:25:25,272 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 135 states, 57 states have (on average 1.0350877192982457) internal successors, (59), 59 states have internal predecessors, (59), 43 states have call successors, (45), 30 states have call predecessors, (45), 37 states have return successors, (57), 45 states have call predecessors, (57), 43 states have call successors, (57)
[2025-05-07 17:25:25,273 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 135 states to 135 states and 161 transitions.
[2025-05-07 17:25:25,273 INFO  L79                 Accepts]: Start accepts. Automaton has 135 states and 161 transitions. Word has length 107
[2025-05-07 17:25:25,274 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:25,274 INFO  L485      AbstractCegarLoop]: Abstraction has 135 states and 161 transitions.
[2025-05-07 17:25:25,274 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 5.75) internal successors, (46), 10 states have internal predecessors, (46), 4 states have call successors, (29), 1 states have call predecessors, (29), 8 states have return successors, (30), 9 states have call predecessors, (30), 4 states have call successors, (30)
[2025-05-07 17:25:25,274 INFO  L278                IsEmpty]: Start isEmpty. Operand 135 states and 161 transitions.
[2025-05-07 17:25:25,276 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 111
[2025-05-07 17:25:25,276 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:25,276 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25,276 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:25:25,276 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:25,277 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:25,277 INFO  L85        PathProgramCache]: Analyzing trace with hash -1075480041, now seen corresponding path program 1 times
[2025-05-07 17:25:25,277 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:25,277 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [793494270]
[2025-05-07 17:25:25,277 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:25,277 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:25,313 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 110 statements into 1 equivalence classes.
[2025-05-07 17:25:25,327 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 110 of 110 statements.
[2025-05-07 17:25:25,327 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:25,327 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:25,439 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:25:25,439 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:25,439 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [793494270]
[2025-05-07 17:25:25,439 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [793494270] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:25,439 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:25,439 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:25,439 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [910269071]
[2025-05-07 17:25:25,439 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:25,440 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:25,440 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:25,440 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:25,441 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:25,441 INFO  L87              Difference]: Start difference. First operand 135 states and 161 transitions. Second operand  has 6 states, 5 states have (on average 8.8) internal successors, (44), 6 states have internal predecessors, (44), 3 states have call successors, (29), 1 states have call predecessors, (29), 5 states have return successors, (29), 6 states have call predecessors, (29), 3 states have call successors, (29)
[2025-05-07 17:25:25,476 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:25,476 INFO  L93              Difference]: Finished difference Result 141 states and 167 transitions.
[2025-05-07 17:25:25,477 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:25,477 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), 3 states have call successors, (29), 1 states have call predecessors, (29), 5 states have return successors, (29), 6 states have call predecessors, (29), 3 states have call successors, (29) Word has length 110
[2025-05-07 17:25:25,478 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:25,479 INFO  L225             Difference]: With dead ends: 141
[2025-05-07 17:25:25,479 INFO  L226             Difference]: Without dead ends: 141
[2025-05-07 17:25:25,479 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:25,480 INFO  L437           NwaCegarLoop]: 134 mSDtfsCounter, 1 mSDsluCounter, 524 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 658 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:25,480 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 658 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:25,480 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-05-07 17:25:25,489 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 139.
[2025-05-07 17:25:25,489 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 59 states have (on average 1.0338983050847457) internal successors, (61), 61 states have internal predecessors, (61), 43 states have call successors, (45), 30 states have call predecessors, (45), 39 states have return successors, (59), 47 states have call predecessors, (59), 43 states have call successors, (59)
[2025-05-07 17:25:25,490 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 165 transitions.
[2025-05-07 17:25:25,490 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 165 transitions. Word has length 110
[2025-05-07 17:25:25,491 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:25,491 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 165 transitions.
[2025-05-07 17:25:25,491 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), 3 states have call successors, (29), 1 states have call predecessors, (29), 5 states have return successors, (29), 6 states have call predecessors, (29), 3 states have call successors, (29)
[2025-05-07 17:25:25,491 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 165 transitions.
[2025-05-07 17:25:25,493 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 111
[2025-05-07 17:25:25,493 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:25,493 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25,493 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:25:25,493 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:25,493 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:25,494 INFO  L85        PathProgramCache]: Analyzing trace with hash -107758743, now seen corresponding path program 1 times
[2025-05-07 17:25:25,494 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:25,494 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [234968434]
[2025-05-07 17:25:25,494 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:25,494 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:25,520 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 110 statements into 1 equivalence classes.
[2025-05-07 17:25:25,532 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 110 of 110 statements.
[2025-05-07 17:25:25,532 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:25,532 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:25,685 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:25:25,685 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:25,685 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [234968434]
[2025-05-07 17:25:25,685 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [234968434] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:25,685 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:25,685 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:25,686 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1767950231]
[2025-05-07 17:25:25,686 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:25,686 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:25,686 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:25,686 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:25,686 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:25,686 INFO  L87              Difference]: Start difference. First operand 139 states and 165 transitions. Second operand  has 7 states, 6 states have (on average 7.333333333333333) internal successors, (44), 7 states have internal predecessors, (44), 4 states have call successors, (29), 1 states have call predecessors, (29), 6 states have return successors, (29), 6 states have call predecessors, (29), 4 states have call successors, (29)
[2025-05-07 17:25:25,745 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:25,745 INFO  L93              Difference]: Finished difference Result 141 states and 167 transitions.
[2025-05-07 17:25:25,746 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:25,746 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 7.333333333333333) internal successors, (44), 7 states have internal predecessors, (44), 4 states have call successors, (29), 1 states have call predecessors, (29), 6 states have return successors, (29), 6 states have call predecessors, (29), 4 states have call successors, (29) Word has length 110
[2025-05-07 17:25:25,746 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:25,747 INFO  L225             Difference]: With dead ends: 141
[2025-05-07 17:25:25,747 INFO  L226             Difference]: Without dead ends: 141
[2025-05-07 17:25:25,747 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:25,748 INFO  L437           NwaCegarLoop]: 132 mSDtfsCounter, 1 mSDsluCounter, 647 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 779 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:25,748 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 779 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:25,748 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-05-07 17:25:25,753 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 141.
[2025-05-07 17:25:25,753 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 141 states, 60 states have (on average 1.0333333333333334) internal successors, (62), 62 states have internal predecessors, (62), 43 states have call successors, (45), 30 states have call predecessors, (45), 40 states have return successors, (60), 48 states have call predecessors, (60), 43 states have call successors, (60)
[2025-05-07 17:25:25,754 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 141 states to 141 states and 167 transitions.
[2025-05-07 17:25:25,754 INFO  L79                 Accepts]: Start accepts. Automaton has 141 states and 167 transitions. Word has length 110
[2025-05-07 17:25:25,755 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:25,755 INFO  L485      AbstractCegarLoop]: Abstraction has 141 states and 167 transitions.
[2025-05-07 17:25:25,755 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 7.333333333333333) internal successors, (44), 7 states have internal predecessors, (44), 4 states have call successors, (29), 1 states have call predecessors, (29), 6 states have return successors, (29), 6 states have call predecessors, (29), 4 states have call successors, (29)
[2025-05-07 17:25:25,755 INFO  L278                IsEmpty]: Start isEmpty. Operand 141 states and 167 transitions.
[2025-05-07 17:25:25,756 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 114
[2025-05-07 17:25:25,756 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:25,756 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25,756 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:25:25,756 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:25,756 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:25,756 INFO  L85        PathProgramCache]: Analyzing trace with hash 917910548, now seen corresponding path program 1 times
[2025-05-07 17:25:25,757 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:25,757 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [903582553]
[2025-05-07 17:25:25,757 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:25,757 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:25,791 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 113 statements into 1 equivalence classes.
[2025-05-07 17:25:25,804 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 113 of 113 statements.
[2025-05-07 17:25:25,804 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:25,804 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:25,923 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:25:25,923 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:25,923 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [903582553]
[2025-05-07 17:25:25,923 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [903582553] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:25,923 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:25,923 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:25,923 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [453741531]
[2025-05-07 17:25:25,923 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:25,924 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:25,924 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:25,924 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:25,924 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:25,924 INFO  L87              Difference]: Start difference. First operand 141 states and 167 transitions. Second operand  has 6 states, 5 states have (on average 9.0) internal successors, (45), 6 states have internal predecessors, (45), 3 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 3 states have call successors, (30)
[2025-05-07 17:25:25,967 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:25,967 INFO  L93              Difference]: Finished difference Result 147 states and 174 transitions.
[2025-05-07 17:25:25,967 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:25,968 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.0) internal successors, (45), 6 states have internal predecessors, (45), 3 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 3 states have call successors, (30) Word has length 113
[2025-05-07 17:25:25,968 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:25,969 INFO  L225             Difference]: With dead ends: 147
[2025-05-07 17:25:25,970 INFO  L226             Difference]: Without dead ends: 147
[2025-05-07 17:25:25,970 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:25,970 INFO  L437           NwaCegarLoop]: 136 mSDtfsCounter, 1 mSDsluCounter, 530 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 666 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:25,971 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 666 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:25,972 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 147 states.
[2025-05-07 17:25:25,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 147 to 145.
[2025-05-07 17:25:25,980 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 145 states, 62 states have (on average 1.032258064516129) internal successors, (64), 64 states have internal predecessors, (64), 43 states have call successors, (45), 30 states have call predecessors, (45), 42 states have return successors, (62), 50 states have call predecessors, (62), 43 states have call successors, (62)
[2025-05-07 17:25:25,982 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 145 states to 145 states and 171 transitions.
[2025-05-07 17:25:25,982 INFO  L79                 Accepts]: Start accepts. Automaton has 145 states and 171 transitions. Word has length 113
[2025-05-07 17:25:25,982 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:25,982 INFO  L485      AbstractCegarLoop]: Abstraction has 145 states and 171 transitions.
[2025-05-07 17:25:25,983 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.0) internal successors, (45), 6 states have internal predecessors, (45), 3 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 3 states have call successors, (30)
[2025-05-07 17:25:25,983 INFO  L278                IsEmpty]: Start isEmpty. Operand 145 states and 171 transitions.
[2025-05-07 17:25:25,984 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:25,985 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:25,985 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25,985 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:25:25,985 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:25,986 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:25,986 INFO  L85        PathProgramCache]: Analyzing trace with hash 851877893, now seen corresponding path program 1 times
[2025-05-07 17:25:25,986 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:25,986 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1045735277]
[2025-05-07 17:25:25,986 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:25,986 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:26,022 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:26,039 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:26,039 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:26,039 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:26,575 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 7 proven. 2 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:25:26,575 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:26,575 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1045735277]
[2025-05-07 17:25:26,575 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1045735277] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:26,575 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1850397149]
[2025-05-07 17:25:26,575 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:26,575 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:26,578 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:26,579 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:26,580 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:25:26,819 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:26,991 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:26,991 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:26,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:26,996 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1625 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:27,004 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:27,085 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:25:27,085 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:27,085 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1850397149] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:27,085 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:27,085 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [19] total 23
[2025-05-07 17:25:27,085 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1766551916]
[2025-05-07 17:25:27,085 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:27,086 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:27,086 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:27,086 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:27,087 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=463, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:25:27,087 INFO  L87              Difference]: Start difference. First operand 145 states and 171 transitions. Second operand  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 3 states have call successors, (32), 1 states have call predecessors, (32), 5 states have return successors, (32), 6 states have call predecessors, (32), 3 states have call successors, (32)
[2025-05-07 17:25:27,121 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:27,122 INFO  L93              Difference]: Finished difference Result 149 states and 177 transitions.
[2025-05-07 17:25:27,122 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:27,122 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 3 states have call successors, (32), 1 states have call predecessors, (32), 5 states have return successors, (32), 6 states have call predecessors, (32), 3 states have call successors, (32) Word has length 120
[2025-05-07 17:25:27,123 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:27,124 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:25:27,124 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:25:27,125 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 138 GetRequests, 117 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=43, Invalid=463, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:25:27,125 INFO  L437           NwaCegarLoop]: 139 mSDtfsCounter, 1 mSDsluCounter, 541 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 680 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:27,125 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 680 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:27,126 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:25:27,134 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 149.
[2025-05-07 17:25:27,134 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 43 states have call successors, (45), 30 states have call predecessors, (45), 44 states have return successors, (66), 52 states have call predecessors, (66), 43 states have call successors, (66)
[2025-05-07 17:25:27,136 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 177 transitions.
[2025-05-07 17:25:27,136 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 177 transitions. Word has length 120
[2025-05-07 17:25:27,136 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:27,136 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 177 transitions.
[2025-05-07 17:25:27,137 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 3 states have call successors, (32), 1 states have call predecessors, (32), 5 states have return successors, (32), 6 states have call predecessors, (32), 3 states have call successors, (32)
[2025-05-07 17:25:27,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 177 transitions.
[2025-05-07 17:25:27,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 121
[2025-05-07 17:25:27,138 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:27,139 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27,145 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:25:27,339 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:27,340 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:27,341 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:27,342 INFO  L85        PathProgramCache]: Analyzing trace with hash -1442583259, now seen corresponding path program 1 times
[2025-05-07 17:25:27,342 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:27,342 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [583201772]
[2025-05-07 17:25:27,342 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:27,342 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:27,444 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:27,457 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:27,457 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:27,457 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:27,573 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:25:27,573 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:27,573 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [583201772]
[2025-05-07 17:25:27,573 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [583201772] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:27,573 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1984497793]
[2025-05-07 17:25:27,573 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:27,573 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:27,576 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:27,577 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:27,578 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:25:27,789 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 120 statements into 1 equivalence classes.
[2025-05-07 17:25:27,928 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 120 of 120 statements.
[2025-05-07 17:25:27,928 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:27,928 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:27,932 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1624 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:27,936 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:27,966 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:25:27,967 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:25:28,886 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:25:28,886 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1984497793] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:25:28,886 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:25:28,886 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 10
[2025-05-07 17:25:28,887 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1992747022]
[2025-05-07 17:25:28,887 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:25:28,887 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:25:28,887 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:28,888 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:25:28,888 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=70, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:25:28,888 INFO  L87              Difference]: Start difference. First operand 149 states and 177 transitions. Second operand  has 10 states, 6 states have (on average 8.333333333333334) internal successors, (50), 10 states have internal predecessors, (50), 6 states have call successors, (34), 1 states have call predecessors, (34), 6 states have return successors, (35), 8 states have call predecessors, (35), 6 states have call successors, (35)
[2025-05-07 17:25:28,972 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:28,972 INFO  L93              Difference]: Finished difference Result 151 states and 180 transitions.
[2025-05-07 17:25:28,972 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:25:28,973 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 8.333333333333334) internal successors, (50), 10 states have internal predecessors, (50), 6 states have call successors, (34), 1 states have call predecessors, (34), 6 states have return successors, (35), 8 states have call predecessors, (35), 6 states have call successors, (35) Word has length 120
[2025-05-07 17:25:28,973 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:28,973 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:25:28,973 INFO  L226             Difference]: Without dead ends: 151
[2025-05-07 17:25:28,974 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 248 GetRequests, 235 SyntacticMatches, 4 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=25, Invalid=85, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:25:28,974 INFO  L437           NwaCegarLoop]: 140 mSDtfsCounter, 3 mSDsluCounter, 949 mSDsCounter, 0 mSdLazyCounter, 63 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1089 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 63 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:28,974 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1089 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 63 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:28,975 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 151 states.
[2025-05-07 17:25:28,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 151 to 149.
[2025-05-07 17:25:28,979 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 43 states have call successors, (45), 30 states have call predecessors, (45), 44 states have return successors, (66), 52 states have call predecessors, (66), 43 states have call successors, (66)
[2025-05-07 17:25:28,980 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 177 transitions.
[2025-05-07 17:25:28,980 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 177 transitions. Word has length 120
[2025-05-07 17:25:28,980 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:28,980 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 177 transitions.
[2025-05-07 17:25:28,980 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 8.333333333333334) internal successors, (50), 10 states have internal predecessors, (50), 6 states have call successors, (34), 1 states have call predecessors, (34), 6 states have return successors, (35), 8 states have call predecessors, (35), 6 states have call successors, (35)
[2025-05-07 17:25:28,980 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 177 transitions.
[2025-05-07 17:25:28,981 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 153
[2025-05-07 17:25:28,981 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:28,981 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:28,988 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:25:29,182 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:29,182 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:29,183 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:29,183 INFO  L85        PathProgramCache]: Analyzing trace with hash 1806959567, now seen corresponding path program 1 times
[2025-05-07 17:25:29,184 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:29,184 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [714229034]
[2025-05-07 17:25:29,184 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:29,184 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:29,264 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 152 statements into 1 equivalence classes.
[2025-05-07 17:25:29,275 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 152 of 152 statements.
[2025-05-07 17:25:29,275 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:29,275 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:29,760 INFO  L134       CoverageAnalysis]: Checked inductivity of 60 backedges. 9 proven. 19 refuted. 0 times theorem prover too weak. 32 trivial. 0 not checked.
[2025-05-07 17:25:29,760 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:29,761 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [714229034]
[2025-05-07 17:25:29,761 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [714229034] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:29,761 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [781347139]
[2025-05-07 17:25:29,761 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:29,761 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:29,763 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:29,764 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:29,765 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:25:30,074 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 152 statements into 1 equivalence classes.
[2025-05-07 17:25:30,288 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 152 of 152 statements.
[2025-05-07 17:25:30,288 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:30,288 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:30,293 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2077 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:30,296 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:30,369 INFO  L134       CoverageAnalysis]: Checked inductivity of 60 backedges. 46 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:25:30,370 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:30,370 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [781347139] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:30,370 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:30,370 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [19] total 23
[2025-05-07 17:25:30,370 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1499304049]
[2025-05-07 17:25:30,370 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:30,371 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:30,371 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:30,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:30,372 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=463, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:25:30,372 INFO  L87              Difference]: Start difference. First operand 149 states and 177 transitions. Second operand  has 6 states, 5 states have (on average 12.2) internal successors, (61), 6 states have internal predecessors, (61), 4 states have call successors, (41), 2 states have call predecessors, (41), 5 states have return successors, (41), 6 states have call predecessors, (41), 4 states have call successors, (41)
[2025-05-07 17:25:30,407 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:30,407 INFO  L93              Difference]: Finished difference Result 151 states and 176 transitions.
[2025-05-07 17:25:30,408 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:30,408 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 12.2) internal successors, (61), 6 states have internal predecessors, (61), 4 states have call successors, (41), 2 states have call predecessors, (41), 5 states have return successors, (41), 6 states have call predecessors, (41), 4 states have call successors, (41) Word has length 152
[2025-05-07 17:25:30,408 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:30,409 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:25:30,410 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:25:30,410 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 170 GetRequests, 149 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=43, Invalid=463, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:25:30,411 INFO  L437           NwaCegarLoop]: 141 mSDtfsCounter, 1 mSDsluCounter, 545 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 686 SdHoareTripleChecker+Invalid, 25 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:30,411 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 686 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:30,411 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:25:30,417 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 149.
[2025-05-07 17:25:30,417 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 43 states have call successors, (45), 30 states have call predecessors, (45), 44 states have return successors, (63), 52 states have call predecessors, (63), 43 states have call successors, (63)
[2025-05-07 17:25:30,419 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 174 transitions.
[2025-05-07 17:25:30,419 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 174 transitions. Word has length 152
[2025-05-07 17:25:30,419 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:30,419 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 174 transitions.
[2025-05-07 17:25:30,419 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 12.2) internal successors, (61), 6 states have internal predecessors, (61), 4 states have call successors, (41), 2 states have call predecessors, (41), 5 states have return successors, (41), 6 states have call predecessors, (41), 4 states have call successors, (41)
[2025-05-07 17:25:30,419 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 174 transitions.
[2025-05-07 17:25:30,421 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 153
[2025-05-07 17:25:30,421 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:30,422 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:30,427 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:25:30,622 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-05-07 17:25:30,623 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:30,624 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:30,624 INFO  L85        PathProgramCache]: Analyzing trace with hash -75130641, now seen corresponding path program 1 times
[2025-05-07 17:25:30,624 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:30,624 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1945613681]
[2025-05-07 17:25:30,624 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:30,625 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:30,708 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 152 statements into 1 equivalence classes.
[2025-05-07 17:25:30,724 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 152 of 152 statements.
[2025-05-07 17:25:30,724 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:30,724 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:30,894 INFO  L134       CoverageAnalysis]: Checked inductivity of 68 backedges. 26 proven. 0 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-05-07 17:25:30,894 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:30,894 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1945613681]
[2025-05-07 17:25:30,894 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1945613681] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:30,894 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:30,894 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:25:30,894 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1065749470]
[2025-05-07 17:25:30,894 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:30,894 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:25:30,894 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:30,895 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:25:30,895 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:25:30,895 INFO  L87              Difference]: Start difference. First operand 149 states and 174 transitions. Second operand  has 10 states, 8 states have (on average 6.625) internal successors, (53), 10 states have internal predecessors, (53), 4 states have call successors, (34), 1 states have call predecessors, (34), 8 states have return successors, (38), 9 states have call predecessors, (38), 4 states have call successors, (38)
[2025-05-07 17:25:30,973 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:30,973 INFO  L93              Difference]: Finished difference Result 149 states and 173 transitions.
[2025-05-07 17:25:30,973 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:25:30,973 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 6.625) internal successors, (53), 10 states have internal predecessors, (53), 4 states have call successors, (34), 1 states have call predecessors, (34), 8 states have return successors, (38), 9 states have call predecessors, (38), 4 states have call successors, (38) Word has length 152
[2025-05-07 17:25:30,974 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:30,974 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:25:30,974 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:25:30,974 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:25:30,975 INFO  L437           NwaCegarLoop]: 129 mSDtfsCounter, 2 mSDsluCounter, 1005 mSDsCounter, 0 mSdLazyCounter, 88 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1134 SdHoareTripleChecker+Invalid, 89 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 88 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:30,975 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1134 Invalid, 89 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 88 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:30,975 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:25:30,978 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 148.
[2025-05-07 17:25:30,979 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 148 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 42 states have call successors, (44), 30 states have call predecessors, (44), 44 states have return successors, (61), 51 states have call predecessors, (61), 42 states have call successors, (61)
[2025-05-07 17:25:30,980 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 148 states to 148 states and 171 transitions.
[2025-05-07 17:25:30,980 INFO  L79                 Accepts]: Start accepts. Automaton has 148 states and 171 transitions. Word has length 152
[2025-05-07 17:25:30,980 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:30,980 INFO  L485      AbstractCegarLoop]: Abstraction has 148 states and 171 transitions.
[2025-05-07 17:25:30,980 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 6.625) internal successors, (53), 10 states have internal predecessors, (53), 4 states have call successors, (34), 1 states have call predecessors, (34), 8 states have return successors, (38), 9 states have call predecessors, (38), 4 states have call successors, (38)
[2025-05-07 17:25:30,980 INFO  L278                IsEmpty]: Start isEmpty. Operand 148 states and 171 transitions.
[2025-05-07 17:25:30,981 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 170
[2025-05-07 17:25:30,981 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:30,981 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:30,981 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:25:30,981 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:30,982 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:30,982 INFO  L85        PathProgramCache]: Analyzing trace with hash 1855874799, now seen corresponding path program 1 times
[2025-05-07 17:25:30,982 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:30,982 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1940270226]
[2025-05-07 17:25:30,982 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:30,982 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:31,021 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 169 statements into 1 equivalence classes.
[2025-05-07 17:25:31,032 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 169 of 169 statements.
[2025-05-07 17:25:31,040 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:31,040 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:31,480 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 27 proven. 2 refuted. 0 times theorem prover too weak. 41 trivial. 0 not checked.
[2025-05-07 17:25:31,480 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:31,480 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1940270226]
[2025-05-07 17:25:31,480 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1940270226] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:31,480 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1098106720]
[2025-05-07 17:25:31,480 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:31,480 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:31,482 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:31,483 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:31,489 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-05-07 17:25:31,748 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 169 statements into 1 equivalence classes.
[2025-05-07 17:25:31,904 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 169 of 169 statements.
[2025-05-07 17:25:31,904 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:31,905 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:31,911 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2308 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:31,915 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:32,072 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 56 trivial. 0 not checked.
[2025-05-07 17:25:32,072 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:32,072 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1098106720] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:32,072 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:32,072 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [19] total 28
[2025-05-07 17:25:32,072 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1864419529]
[2025-05-07 17:25:32,072 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:32,073 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-05-07 17:25:32,073 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:32,073 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-05-07 17:25:32,074 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=703, Unknown=0, NotChecked=0, Total=756
[2025-05-07 17:25:32,074 INFO  L87              Difference]: Start difference. First operand 148 states and 171 transitions. Second operand  has 11 states, 10 states have (on average 5.5) internal successors, (55), 11 states have internal predecessors, (55), 3 states have call successors, (38), 1 states have call predecessors, (38), 10 states have return successors, (41), 11 states have call predecessors, (41), 3 states have call successors, (41)
[2025-05-07 17:25:32,160 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:32,160 INFO  L93              Difference]: Finished difference Result 162 states and 189 transitions.
[2025-05-07 17:25:32,161 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-05-07 17:25:32,161 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 5.5) internal successors, (55), 11 states have internal predecessors, (55), 3 states have call successors, (38), 1 states have call predecessors, (38), 10 states have return successors, (41), 11 states have call predecessors, (41), 3 states have call successors, (41) Word has length 169
[2025-05-07 17:25:32,161 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:32,162 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:25:32,162 INFO  L226             Difference]: Without dead ends: 160
[2025-05-07 17:25:32,162 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 187 GetRequests, 161 SyntacticMatches, 0 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=53, Invalid=703, Unknown=0, NotChecked=0, Total=756
[2025-05-07 17:25:32,162 INFO  L437           NwaCegarLoop]: 140 mSDtfsCounter, 1 mSDsluCounter, 1232 mSDsCounter, 0 mSdLazyCounter, 129 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1372 SdHoareTripleChecker+Invalid, 129 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 129 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:32,162 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1372 Invalid, 129 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 129 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:32,163 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 160 states.
[2025-05-07 17:25:32,167 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 160 to 158.
[2025-05-07 17:25:32,167 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 69 states have (on average 1.0289855072463767) internal successors, (71), 71 states have internal predecessors, (71), 42 states have call successors, (44), 30 states have call predecessors, (44), 49 states have return successors, (70), 56 states have call predecessors, (70), 42 states have call successors, (70)
[2025-05-07 17:25:32,167 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 185 transitions.
[2025-05-07 17:25:32,168 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 185 transitions. Word has length 169
[2025-05-07 17:25:32,168 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:32,168 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 185 transitions.
[2025-05-07 17:25:32,168 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 5.5) internal successors, (55), 11 states have internal predecessors, (55), 3 states have call successors, (38), 1 states have call predecessors, (38), 10 states have return successors, (41), 11 states have call predecessors, (41), 3 states have call successors, (41)
[2025-05-07 17:25:32,168 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 185 transitions.
[2025-05-07 17:25:32,169 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 173
[2025-05-07 17:25:32,169 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:32,169 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:32,175 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-05-07 17:25:32,369 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:32,370 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:32,371 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:32,372 INFO  L85        PathProgramCache]: Analyzing trace with hash 537732394, now seen corresponding path program 1 times
[2025-05-07 17:25:32,372 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:32,372 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [688025169]
[2025-05-07 17:25:32,373 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:32,373 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:32,449 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 172 statements into 1 equivalence classes.
[2025-05-07 17:25:32,460 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 172 of 172 statements.
[2025-05-07 17:25:32,460 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:32,460 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:32,938 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 14 proven. 15 refuted. 0 times theorem prover too weak. 41 trivial. 0 not checked.
[2025-05-07 17:25:32,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:32,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [688025169]
[2025-05-07 17:25:32,939 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [688025169] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:32,939 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [700008824]
[2025-05-07 17:25:32,939 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:32,939 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:32,941 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:32,943 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:32,943 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-05-07 17:25:33,266 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 172 statements into 1 equivalence classes.
[2025-05-07 17:25:33,507 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 172 of 172 statements.
[2025-05-07 17:25:33,508 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:33,508 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:33,514 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2365 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:33,518 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:33,594 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 22 proven. 0 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-05-07 17:25:33,594 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:33,594 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [700008824] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:33,594 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:33,594 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [22] total 26
[2025-05-07 17:25:33,595 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [803346604]
[2025-05-07 17:25:33,595 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:33,595 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:33,595 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:33,595 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:33,596 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=597, Unknown=0, NotChecked=0, Total=650
[2025-05-07 17:25:33,596 INFO  L87              Difference]: Start difference. First operand 158 states and 185 transitions. Second operand  has 6 states, 5 states have (on average 12.0) internal successors, (60), 6 states have internal predecessors, (60), 4 states have call successors, (40), 2 states have call predecessors, (40), 5 states have return successors, (43), 5 states have call predecessors, (43), 4 states have call successors, (43)
[2025-05-07 17:25:33,638 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:33,638 INFO  L93              Difference]: Finished difference Result 158 states and 183 transitions.
[2025-05-07 17:25:33,638 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:33,639 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 12.0) internal successors, (60), 6 states have internal predecessors, (60), 4 states have call successors, (40), 2 states have call predecessors, (40), 5 states have return successors, (43), 5 states have call predecessors, (43), 4 states have call successors, (43) Word has length 172
[2025-05-07 17:25:33,639 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:33,640 INFO  L225             Difference]: With dead ends: 158
[2025-05-07 17:25:33,640 INFO  L226             Difference]: Without dead ends: 158
[2025-05-07 17:25:33,640 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 194 GetRequests, 170 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=53, Invalid=597, Unknown=0, NotChecked=0, Total=650
[2025-05-07 17:25:33,641 INFO  L437           NwaCegarLoop]: 138 mSDtfsCounter, 1 mSDsluCounter, 534 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 672 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:33,641 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 672 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:33,641 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-05-07 17:25:33,647 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 158.
[2025-05-07 17:25:33,647 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 69 states have (on average 1.0289855072463767) internal successors, (71), 71 states have internal predecessors, (71), 42 states have call successors, (44), 30 states have call predecessors, (44), 49 states have return successors, (68), 56 states have call predecessors, (68), 42 states have call successors, (68)
[2025-05-07 17:25:33,648 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 183 transitions.
[2025-05-07 17:25:33,648 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 183 transitions. Word has length 172
[2025-05-07 17:25:33,648 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:33,649 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 183 transitions.
[2025-05-07 17:25:33,649 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 12.0) internal successors, (60), 6 states have internal predecessors, (60), 4 states have call successors, (40), 2 states have call predecessors, (40), 5 states have return successors, (43), 5 states have call predecessors, (43), 4 states have call successors, (43)
[2025-05-07 17:25:33,649 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 183 transitions.
[2025-05-07 17:25:33,650 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 173
[2025-05-07 17:25:33,650 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:33,650 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:33,656 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-05-07 17:25:33,851 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-05-07 17:25:33,851 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:33,852 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:33,852 INFO  L85        PathProgramCache]: Analyzing trace with hash -1966519286, now seen corresponding path program 1 times
[2025-05-07 17:25:33,852 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:33,852 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [250140724]
[2025-05-07 17:25:33,852 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:33,852 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:33,942 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 172 statements into 1 equivalence classes.
[2025-05-07 17:25:33,952 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 172 of 172 statements.
[2025-05-07 17:25:33,952 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:33,952 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:34,537 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 22 proven. 11 refuted. 0 times theorem prover too weak. 41 trivial. 0 not checked.
[2025-05-07 17:25:34,538 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:34,538 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [250140724]
[2025-05-07 17:25:34,538 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [250140724] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:34,538 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2050323101]
[2025-05-07 17:25:34,538 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:34,538 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:34,540 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:34,542 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:34,542 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-05-07 17:25:34,857 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 172 statements into 1 equivalence classes.
[2025-05-07 17:25:35,037 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 172 of 172 statements.
[2025-05-07 17:25:35,037 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:35,037 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:35,044 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2364 conjuncts, 44 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:35,057 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:35,267 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 31 proven. 5 refuted. 0 times theorem prover too weak. 38 trivial. 0 not checked.
[2025-05-07 17:25:35,267 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:25:37,838 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 31 proven. 5 refuted. 0 times theorem prover too weak. 38 trivial. 0 not checked.
[2025-05-07 17:25:37,838 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2050323101] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:25:37,838 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:25:37,838 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [22, 16, 16] total 38
[2025-05-07 17:25:37,838 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [859778315]
[2025-05-07 17:25:37,838 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:25:37,839 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 38 states
[2025-05-07 17:25:37,839 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:37,840 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 38 interpolants.
[2025-05-07 17:25:37,840 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=80, Invalid=1326, Unknown=0, NotChecked=0, Total=1406
[2025-05-07 17:25:37,841 INFO  L87              Difference]: Start difference. First operand 158 states and 183 transitions. Second operand  has 38 states, 30 states have (on average 3.0) internal successors, (90), 35 states have internal predecessors, (90), 15 states have call successors, (52), 1 states have call predecessors, (52), 30 states have return successors, (75), 35 states have call predecessors, (75), 15 states have call successors, (75)
[2025-05-07 17:25:38,449 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:38,449 INFO  L93              Difference]: Finished difference Result 169 states and 195 transitions.
[2025-05-07 17:25:38,449 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 36 states. 
[2025-05-07 17:25:38,450 INFO  L79                 Accepts]: Start accepts. Automaton has  has 38 states, 30 states have (on average 3.0) internal successors, (90), 35 states have internal predecessors, (90), 15 states have call successors, (52), 1 states have call predecessors, (52), 30 states have return successors, (75), 35 states have call predecessors, (75), 15 states have call successors, (75) Word has length 172
[2025-05-07 17:25:38,450 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:38,450 INFO  L225             Difference]: With dead ends: 169
[2025-05-07 17:25:38,450 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:25:38,451 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 379 GetRequests, 330 SyntacticMatches, 0 SemanticMatches, 49 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 87 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=137, Invalid=2413, Unknown=0, NotChecked=0, Total=2550
[2025-05-07 17:25:38,451 INFO  L437           NwaCegarLoop]: 119 mSDtfsCounter, 7 mSDsluCounter, 3599 mSDsCounter, 0 mSdLazyCounter, 987 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 3718 SdHoareTripleChecker+Invalid, 994 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 987 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:38,451 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 3718 Invalid, 994 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 987 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:25:38,452 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:25:38,452 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:25:38,452 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:38,452 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:25:38,452 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 172
[2025-05-07 17:25:38,452 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:38,452 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:25:38,452 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 38 states, 30 states have (on average 3.0) internal successors, (90), 35 states have internal predecessors, (90), 15 states have call successors, (52), 1 states have call predecessors, (52), 30 states have return successors, (75), 35 states have call predecessors, (75), 15 states have call successors, (75)
[2025-05-07 17:25:38,452 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:25:38,452 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:25:38,454 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:25:38,460 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-05-07 17:25:38,655 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-05-07 17:25:38,663 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:38,669 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:25:38,676 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:25:38 BoogieIcfgContainer
[2025-05-07 17:25:38,677 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:25:38,678 INFO  L158              Benchmark]: Toolchain (without parser) took 17734.36ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 147.6MB in the beginning and 211.1MB in the end (delta: -63.5MB). Peak memory consumption was 150.8MB. Max. memory is 33.6GB.
[2025-05-07 17:25:38,679 INFO  L158              Benchmark]: SmtParser took 0.20ms. Allocated memory is still 234.9MB. Free memory is still 171.6MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:38,679 INFO  L158              Benchmark]: ChcToBoogie took 31.75ms. Allocated memory is still 234.9MB. Free memory was 147.6MB in the beginning and 144.6MB in the end (delta: 2.9MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:38,680 INFO  L158              Benchmark]: Boogie Preprocessor took 52.78ms. Allocated memory is still 234.9MB. Free memory was 144.6MB in the beginning and 141.2MB in the end (delta: 3.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:38,681 INFO  L158              Benchmark]: RCFGBuilder took 409.42ms. Allocated memory is still 234.9MB. Free memory was 141.1MB in the beginning and 173.9MB in the end (delta: -32.8MB). Peak memory consumption was 43.2MB. Max. memory is 33.6GB.
[2025-05-07 17:25:38,681 INFO  L158              Benchmark]: TraceAbstraction took 17236.91ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 173.1MB in the beginning and 211.1MB in the end (delta: -38.0MB). Peak memory consumption was 157.9MB. Max. memory is 33.6GB.
[2025-05-07 17:25:38,684 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.20ms. Allocated memory is still 234.9MB. Free memory is still 171.6MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 31.75ms. Allocated memory is still 234.9MB. Free memory was 147.6MB in the beginning and 144.6MB in the end (delta: 2.9MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 52.78ms. Allocated memory is still 234.9MB. Free memory was 144.6MB in the beginning and 141.2MB in the end (delta: 3.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 409.42ms. Allocated memory is still 234.9MB. Free memory was 141.1MB in the beginning and 173.9MB in the end (delta: -32.8MB). Peak memory consumption was 43.2MB. Max. memory is 33.6GB.
 * TraceAbstraction took 17236.91ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 173.1MB in the beginning and 211.1MB in the end (delta: -38.0MB). Peak memory consumption was 157.9MB. 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 31 procedures, 123 locations, 190 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 17.2s, OverallIterations: 15, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 2.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 76 SdHoareTripleChecker+Valid, 1.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 33 mSDsluCounter, 17365 SdHoareTripleChecker+Invalid, 1.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 15364 mSDsCounter, 13 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 2155 IncrementalHoareTripleChecker+Invalid, 2168 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 13 mSolverCounterUnsat, 2001 mSDtfsCounter, 2155 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 1497 GetRequests, 1254 SyntacticMatches, 4 SemanticMatches, 239 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 231 ImplicationChecksByTransitivity, 2.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=158occurred in iteration=13, InterpolantAutomatonStates: 156, 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, 15 MinimizatonAttempts, 17 StatesRemovedByMinimization, 9 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.7s SsaConstructionTime, 1.5s SatisfiabilityAnalysisTime, 9.3s InterpolantComputationTime, 2756 NumberOfCodeBlocks, 2756 NumberOfCodeBlocksAsserted, 22 NumberOfCheckSat, 3024 ConstructedInterpolants, 0 QuantifiedInterpolants, 4112 SizeOfPredicates, 7 NumberOfNonLiveVariables, 13551 ConjunctsInSsa, 102 ConjunctsInUnsatCore, 24 InterpolantComputations, 13 PerfectInterpolantSequences, 807/885 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:38,702 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
