./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/control_flow/short_circuit_or_inside_branch.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:15,904 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:15,959 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_14c7fdfe-8b73-46eb-b6ca-80e38241aaa6/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:15,963 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:15,963 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:15,981 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:15,981 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:15,981 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:15,981 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:15,982 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:15,982 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:15,982 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:15,982 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:15,982 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:15,982 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:15,982 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:15,982 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:15,983 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:15,983 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:15,984 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:15,984 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:16,207 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:16,212 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:16,214 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:16,215 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:16,215 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:16,216 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_14c7fdfe-8b73-46eb-b6ca-80e38241aaa6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/control_flow/short_circuit_or_inside_branch.sol_0_no_adts_000.smt2
[2025-05-07 17:28:16,217 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:16,219 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:16,501 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_14c7fdfe-8b73-46eb-b6ca-80e38241aaa6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/control_flow/short_circuit_or_inside_branch.sol_0_no_adts_000.smt2
[2025-05-07 17:28:16,503 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:16,504 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:16,504 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:16,504 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:16,504 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:16,506 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,540 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16 Unit
[2025-05-07 17:28:16,540 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:16,541 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:16,541 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:16,541 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:16,552 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,552 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,574 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,574 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,580 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,582 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,583 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,585 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,587 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,598 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:16,599 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:16,599 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:16,599 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:16,600 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (1/1) ...
[2025-05-07 17:28:16,602 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:16,610 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:16,619 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:28:16,621 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:28:16,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:16,629 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:16,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:16,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_8_0 given in one single declaration
[2025-05-07 17:28:16,629 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_8_0
[2025-05-07 17:28:16,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_8_0
[2025-05-07 17:28:16,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_c_91_0 given in one single declaration
[2025-05-07 17:28:16,629 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_c_91_0
[2025-05-07 17:28:16,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_c_91_0
[2025-05-07 17:28:16,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_c_91_0 given in one single declaration
[2025-05-07 17:28:16,629 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_c_91_0
[2025-05-07 17:28:16,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_c_91_0
[2025-05-07 17:28:16,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_30_c_91_0 given in one single declaration
[2025-05-07 17:28:16,629 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_30_c_91_0
[2025-05-07 17:28:16,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_30_c_91_0
[2025-05-07 17:28:16,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_27_c_91_0 given in one single declaration
[2025-05-07 17:28:16,630 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_27_c_91_0
[2025-05-07 17:28:16,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_27_c_91_0
[2025-05-07 17:28:16,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_29_c_91_0 given in one single declaration
[2025-05-07 17:28:16,630 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_29_c_91_0
[2025-05-07 17:28:16,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_29_c_91_0
[2025-05-07 17:28:16,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_28_c_91_0 given in one single declaration
[2025-05-07 17:28:16,630 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_28_c_91_0
[2025-05-07 17:28:16,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_28_c_91_0
[2025-05-07 17:28:16,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,630 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_g__90_91_0
[2025-05-07 17:28:16,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_g__90_91_0
[2025-05-07 17:28:16,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,630 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_g__90_91_0
[2025-05-07 17:28:16,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_g__90_91_0
[2025-05-07 17:28:16,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,630 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_return_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_return_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_return_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_f_15_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_f_15_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_f_15_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_function_g__90_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_function_g__90_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_f__16_91_0
[2025-05-07 17:28:16,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,631 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_function_g__90_91_0
[2025-05-07 17:28:16,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_function_g__90_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,632 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_g__90_91_0
[2025-05-07 17:28:16,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_g__90_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,632 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_function_f__16_91_0
[2025-05-07 17:28:16,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_function_f__16_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_if_false_g_85_91_0 given in one single declaration
[2025-05-07 17:28:16,632 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_if_false_g_85_91_0
[2025-05-07 17:28:16,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_if_false_g_85_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_if_header_g_86_91_0 given in one single declaration
[2025-05-07 17:28:16,632 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_if_header_g_86_91_0
[2025-05-07 17:28:16,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_if_header_g_86_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_g_89_91_0 given in one single declaration
[2025-05-07 17:28:16,632 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_g_89_91_0
[2025-05-07 17:28:16,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_g_89_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,632 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_g__90_91_0
[2025-05-07 17:28:16,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_g__90_91_0
[2025-05-07 17:28:16,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_function_g__90_91_0
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_function_g__90_91_0
[2025-05-07 17:28:16,633 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_if_true_g_55_91_0 given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_if_true_g_55_91_0
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_if_true_g_55_91_0
[2025-05-07 17:28:16,633 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_17_function_f__16_91_0 given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_17_function_f__16_91_0
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_17_function_f__16_91_0
[2025-05-07 17:28:16,633 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_return_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_return_function_g__90_91_0
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_return_function_g__90_91_0
[2025-05-07 17:28:16,633 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_g_89_91_0 given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_g_89_91_0
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_g_89_91_0
[2025-05-07 17:28:16,633 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_function_g__90_91_0 given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_function_g__90_91_0
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_function_g__90_91_0
[2025-05-07 17:28:16,633 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:16,633 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:16,633 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:16,797 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:16,799 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:17,083 INFO  L?                        ?]: Removed 288 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:17,083 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:17,092 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:17,093 INFO  L312             CfgBuilder]: Removed 16 assume(true) statements.
[2025-05-07 17:28:17,093 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:17 BoogieIcfgContainer
[2025-05-07 17:28:17,093 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:17,094 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:17,094 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:17,097 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:17,097 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:16" (1/3) ...
[2025-05-07 17:28:17,098 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35c4c2b5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:17, skipping insertion in model container
[2025-05-07 17:28:17,098 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:16" (2/3) ...
[2025-05-07 17:28:17,098 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35c4c2b5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:17, skipping insertion in model container
[2025-05-07 17:28:17,098 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:17" (3/3) ...
[2025-05-07 17:28:17,099 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:17,109 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:17,111 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 31 procedures, 138 locations, 238 edges, 31 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:17,143 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:17,151 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;@470f93b6, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:17,152 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:17,155 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 138 states, 51 states have (on average 1.1372549019607843) internal successors, (58), 58 states have internal predecessors, (58), 56 states have call successors, (60), 30 states have call predecessors, (60), 30 states have return successors, (60), 49 states have call predecessors, (60), 56 states have call successors, (60)
[2025-05-07 17:28:17,163 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 74
[2025-05-07 17:28:17,164 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:17,164 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:17,164 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:17,168 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:17,168 INFO  L85        PathProgramCache]: Analyzing trace with hash 839065473, now seen corresponding path program 1 times
[2025-05-07 17:28:17,174 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:17,174 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1494357391]
[2025-05-07 17:28:17,174 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:17,175 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:17,226 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 73 statements into 1 equivalence classes.
[2025-05-07 17:28:17,295 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 73 of 73 statements.
[2025-05-07 17:28:17,295 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:17,296 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:17,550 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:17,551 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:17,551 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1494357391]
[2025-05-07 17:28:17,552 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1494357391] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:17,552 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:17,556 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:17,558 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [834534864]
[2025-05-07 17:28:17,558 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:17,562 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:17,563 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:17,583 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:17,583 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:17,585 INFO  L87              Difference]: Start difference. First operand  has 138 states, 51 states have (on average 1.1372549019607843) internal successors, (58), 58 states have internal predecessors, (58), 56 states have call successors, (60), 30 states have call predecessors, (60), 30 states have return successors, (60), 49 states have call predecessors, (60), 56 states have call successors, (60) Second operand  has 4 states, 3 states have (on average 11.0) internal successors, (33), 4 states have internal predecessors, (33), 3 states have call successors, (20), 1 states have call predecessors, (20), 3 states have return successors, (20), 3 states have call predecessors, (20), 3 states have call successors, (20)
[2025-05-07 17:28:17,626 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:17,626 INFO  L93              Difference]: Finished difference Result 140 states and 180 transitions.
[2025-05-07 17:28:17,627 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:17,628 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 11.0) internal successors, (33), 4 states have internal predecessors, (33), 3 states have call successors, (20), 1 states have call predecessors, (20), 3 states have return successors, (20), 3 states have call predecessors, (20), 3 states have call successors, (20) Word has length 73
[2025-05-07 17:28:17,628 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:17,634 INFO  L225             Difference]: With dead ends: 140
[2025-05-07 17:28:17,634 INFO  L226             Difference]: Without dead ends: 136
[2025-05-07 17:28:17,635 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:17,637 INFO  L437           NwaCegarLoop]: 178 mSDtfsCounter, 1 mSDsluCounter, 348 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 526 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:17,637 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 526 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:17,647 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 136 states.
[2025-05-07 17:28:17,665 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 136 to 134.
[2025-05-07 17:28:17,665 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 50 states have (on average 1.1) internal successors, (55), 55 states have internal predecessors, (55), 54 states have call successors, (58), 30 states have call predecessors, (58), 30 states have return successors, (58), 48 states have call predecessors, (58), 54 states have call successors, (58)
[2025-05-07 17:28:17,669 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 171 transitions.
[2025-05-07 17:28:17,670 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 171 transitions. Word has length 73
[2025-05-07 17:28:17,670 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:17,670 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 171 transitions.
[2025-05-07 17:28:17,670 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 11.0) internal successors, (33), 4 states have internal predecessors, (33), 3 states have call successors, (20), 1 states have call predecessors, (20), 3 states have return successors, (20), 3 states have call predecessors, (20), 3 states have call successors, (20)
[2025-05-07 17:28:17,670 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 171 transitions.
[2025-05-07 17:28:17,672 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 74
[2025-05-07 17:28:17,673 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:17,673 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:17,673 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:17,673 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:17,673 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:17,674 INFO  L85        PathProgramCache]: Analyzing trace with hash 109935109, now seen corresponding path program 1 times
[2025-05-07 17:28:17,674 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:17,674 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [123485472]
[2025-05-07 17:28:17,674 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:17,674 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:17,708 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 73 statements into 1 equivalence classes.
[2025-05-07 17:28:17,733 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 73 of 73 statements.
[2025-05-07 17:28:17,733 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:17,733 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:17,876 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:17,876 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:17,876 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [123485472]
[2025-05-07 17:28:17,876 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [123485472] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:17,876 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:17,876 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:17,876 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [186190420]
[2025-05-07 17:28:17,876 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:17,877 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:17,877 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:17,878 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:17,878 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:17,878 INFO  L87              Difference]: Start difference. First operand 134 states and 171 transitions. Second operand  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:28:18,009 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:18,009 INFO  L93              Difference]: Finished difference Result 136 states and 172 transitions.
[2025-05-07 17:28:18,009 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:18,009 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20) Word has length 73
[2025-05-07 17:28:18,010 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:18,011 INFO  L225             Difference]: With dead ends: 136
[2025-05-07 17:28:18,011 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:28:18,011 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:18,011 INFO  L437           NwaCegarLoop]: 159 mSDtfsCounter, 1 mSDsluCounter, 765 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 924 SdHoareTripleChecker+Invalid, 77 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:18,012 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 924 Invalid, 77 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:18,012 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:28:18,018 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 132.
[2025-05-07 17:28:18,019 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 132 states, 50 states have (on average 1.08) internal successors, (54), 54 states have internal predecessors, (54), 52 states have call successors, (56), 30 states have call predecessors, (56), 30 states have return successors, (56), 47 states have call predecessors, (56), 52 states have call successors, (56)
[2025-05-07 17:28:18,020 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 132 states to 132 states and 166 transitions.
[2025-05-07 17:28:18,020 INFO  L79                 Accepts]: Start accepts. Automaton has 132 states and 166 transitions. Word has length 73
[2025-05-07 17:28:18,020 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:18,020 INFO  L485      AbstractCegarLoop]: Abstraction has 132 states and 166 transitions.
[2025-05-07 17:28:18,020 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:28:18,020 INFO  L278                IsEmpty]: Start isEmpty. Operand 132 states and 166 transitions.
[2025-05-07 17:28:18,022 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 74
[2025-05-07 17:28:18,022 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:18,022 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:18,022 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:18,022 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:18,023 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:18,023 INFO  L85        PathProgramCache]: Analyzing trace with hash -525172106, now seen corresponding path program 1 times
[2025-05-07 17:28:18,023 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:18,023 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1992357177]
[2025-05-07 17:28:18,023 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:18,023 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:18,052 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 73 statements into 1 equivalence classes.
[2025-05-07 17:28:18,065 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 73 of 73 statements.
[2025-05-07 17:28:18,065 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:18,065 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:18,186 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:18,187 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:18,187 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1992357177]
[2025-05-07 17:28:18,187 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1992357177] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:18,187 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:18,187 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:18,187 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2027624088]
[2025-05-07 17:28:18,187 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:18,187 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:18,187 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:18,188 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:18,188 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:18,188 INFO  L87              Difference]: Start difference. First operand 132 states and 166 transitions. Second operand  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:28:18,292 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:18,292 INFO  L93              Difference]: Finished difference Result 133 states and 165 transitions.
[2025-05-07 17:28:18,293 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:18,293 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 4 states have call successors, (20) Word has length 73
[2025-05-07 17:28:18,293 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:18,295 INFO  L225             Difference]: With dead ends: 133
[2025-05-07 17:28:18,296 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:28:18,296 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:18,296 INFO  L437           NwaCegarLoop]: 152 mSDtfsCounter, 1 mSDsluCounter, 734 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 886 SdHoareTripleChecker+Invalid, 76 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:18,297 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 886 Invalid, 76 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:18,297 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:28:18,303 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 130.
[2025-05-07 17:28:18,304 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 50 states have (on average 1.06) internal successors, (53), 53 states have internal predecessors, (53), 50 states have call successors, (54), 30 states have call predecessors, (54), 30 states have return successors, (54), 46 states have call predecessors, (54), 50 states have call successors, (54)
[2025-05-07 17:28:18,304 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 161 transitions.
[2025-05-07 17:28:18,305 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 161 transitions. Word has length 73
[2025-05-07 17:28:18,305 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:18,305 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 161 transitions.
[2025-05-07 17:28:18,305 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.5) internal successors, (33), 7 states have internal predecessors, (33), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:28:18,305 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 161 transitions.
[2025-05-07 17:28:18,307 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:28:18,307 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:18,307 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:18,307 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:18,307 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:18,308 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:18,308 INFO  L85        PathProgramCache]: Analyzing trace with hash 1691421393, now seen corresponding path program 1 times
[2025-05-07 17:28:18,308 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:18,308 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [384199703]
[2025-05-07 17:28:18,308 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:18,308 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:18,340 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:28:18,356 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:28:18,356 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:18,356 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:18,473 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:28:18,474 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:18,474 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [384199703]
[2025-05-07 17:28:18,474 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [384199703] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:18,474 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [153299473]
[2025-05-07 17:28:18,474 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:18,474 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:18,476 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:18,478 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:28:18,479 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:28:18,765 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:28:18,915 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:28:18,916 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:18,916 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:18,920 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1273 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:18,928 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:19,001 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:28:19,001 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:19,936 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:28:19,936 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [153299473] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:19,936 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:19,936 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 9, 9] total 11
[2025-05-07 17:28:19,937 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [634664616]
[2025-05-07 17:28:19,937 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:19,937 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-05-07 17:28:19,937 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:19,938 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-05-07 17:28:19,938 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:28:19,938 INFO  L87              Difference]: Start difference. First operand 130 states and 161 transitions. Second operand  has 11 states, 8 states have (on average 6.625) internal successors, (53), 11 states have internal predecessors, (53), 7 states have call successors, (34), 2 states have call predecessors, (34), 8 states have return successors, (37), 9 states have call predecessors, (37), 7 states have call successors, (37)
[2025-05-07 17:28:20,044 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:20,044 INFO  L93              Difference]: Finished difference Result 131 states and 160 transitions.
[2025-05-07 17:28:20,044 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:20,045 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 8 states have (on average 6.625) internal successors, (53), 11 states have internal predecessors, (53), 7 states have call successors, (34), 2 states have call predecessors, (34), 8 states have return successors, (37), 9 states have call predecessors, (37), 7 states have call successors, (37) Word has length 90
[2025-05-07 17:28:20,045 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:20,046 INFO  L225             Difference]: With dead ends: 131
[2025-05-07 17:28:20,046 INFO  L226             Difference]: Without dead ends: 129
[2025-05-07 17:28:20,047 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 186 GetRequests, 171 SyntacticMatches, 6 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:28:20,047 INFO  L437           NwaCegarLoop]: 150 mSDtfsCounter, 2 mSDsluCounter, 1309 mSDsCounter, 0 mSdLazyCounter, 117 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1459 SdHoareTripleChecker+Invalid, 118 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 117 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:20,048 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1459 Invalid, 118 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 117 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:20,048 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-05-07 17:28:20,057 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 127.
[2025-05-07 17:28:20,057 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 127 states, 50 states have (on average 1.04) internal successors, (52), 52 states have internal predecessors, (52), 47 states have call successors, (51), 30 states have call predecessors, (51), 30 states have return successors, (51), 44 states have call predecessors, (51), 47 states have call successors, (51)
[2025-05-07 17:28:20,058 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 154 transitions.
[2025-05-07 17:28:20,058 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 154 transitions. Word has length 90
[2025-05-07 17:28:20,058 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:20,059 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 154 transitions.
[2025-05-07 17:28:20,059 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 8 states have (on average 6.625) internal successors, (53), 11 states have internal predecessors, (53), 7 states have call successors, (34), 2 states have call predecessors, (34), 8 states have return successors, (37), 9 states have call predecessors, (37), 7 states have call successors, (37)
[2025-05-07 17:28:20,059 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 154 transitions.
[2025-05-07 17:28:20,060 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:28:20,061 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:20,061 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:20,066 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:28:20,262 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:28:20,262 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:20,264 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:20,264 INFO  L85        PathProgramCache]: Analyzing trace with hash 391499336, now seen corresponding path program 1 times
[2025-05-07 17:28:20,265 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:20,265 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1499134893]
[2025-05-07 17:28:20,265 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:20,266 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:20,340 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:28:20,360 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:28:20,361 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:20,361 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:20,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:28:20,464 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:20,464 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1499134893]
[2025-05-07 17:28:20,464 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1499134893] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:20,464 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:20,464 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:20,464 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1884317910]
[2025-05-07 17:28:20,464 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:20,465 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:20,465 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:20,466 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:20,466 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:20,466 INFO  L87              Difference]: Start difference. First operand 127 states and 154 transitions. Second operand  has 7 states, 6 states have (on average 6.333333333333333) internal successors, (38), 7 states have internal predecessors, (38), 4 states have call successors, (23), 1 states have call predecessors, (23), 6 states have return successors, (25), 7 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:20,534 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:20,535 INFO  L93              Difference]: Finished difference Result 126 states and 151 transitions.
[2025-05-07 17:28:20,535 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:20,535 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 6.333333333333333) internal successors, (38), 7 states have internal predecessors, (38), 4 states have call successors, (23), 1 states have call predecessors, (23), 6 states have return successors, (25), 7 states have call predecessors, (25), 4 states have call successors, (25) Word has length 90
[2025-05-07 17:28:20,536 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:20,537 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:28:20,537 INFO  L226             Difference]: Without dead ends: 124
[2025-05-07 17:28:20,537 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:20,538 INFO  L437           NwaCegarLoop]: 142 mSDtfsCounter, 0 mSDsluCounter, 691 mSDsCounter, 0 mSdLazyCounter, 62 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 833 SdHoareTripleChecker+Invalid, 62 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 62 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:20,538 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 833 Invalid, 62 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 62 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:20,539 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-05-07 17:28:20,545 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 124.
[2025-05-07 17:28:20,545 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 124 states, 49 states have (on average 1.0408163265306123) internal successors, (51), 51 states have internal predecessors, (51), 44 states have call successors, (48), 30 states have call predecessors, (48), 30 states have return successors, (48), 42 states have call predecessors, (48), 44 states have call successors, (48)
[2025-05-07 17:28:20,546 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 124 states to 124 states and 147 transitions.
[2025-05-07 17:28:20,546 INFO  L79                 Accepts]: Start accepts. Automaton has 124 states and 147 transitions. Word has length 90
[2025-05-07 17:28:20,546 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:20,546 INFO  L485      AbstractCegarLoop]: Abstraction has 124 states and 147 transitions.
[2025-05-07 17:28:20,546 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 6.333333333333333) internal successors, (38), 7 states have internal predecessors, (38), 4 states have call successors, (23), 1 states have call predecessors, (23), 6 states have return successors, (25), 7 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:20,546 INFO  L278                IsEmpty]: Start isEmpty. Operand 124 states and 147 transitions.
[2025-05-07 17:28:20,547 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:28:20,547 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:20,548 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:20,548 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:20,548 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:20,548 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:20,548 INFO  L85        PathProgramCache]: Analyzing trace with hash -668057552, now seen corresponding path program 1 times
[2025-05-07 17:28:20,548 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:20,548 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [560817520]
[2025-05-07 17:28:20,549 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:20,549 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:20,573 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:28:20,591 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:28:20,591 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:20,591 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:20,717 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:28:20,717 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:20,717 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [560817520]
[2025-05-07 17:28:20,717 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [560817520] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:20,717 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:20,717 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:20,717 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [873386908]
[2025-05-07 17:28:20,717 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:20,718 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:20,718 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:20,718 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:20,718 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:20,719 INFO  L87              Difference]: Start difference. First operand 124 states and 147 transitions. Second operand  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:20,752 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:20,752 INFO  L93              Difference]: Finished difference Result 128 states and 151 transitions.
[2025-05-07 17:28:20,753 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:20,753 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23) Word has length 93
[2025-05-07 17:28:20,753 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:20,754 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:28:20,754 INFO  L226             Difference]: Without dead ends: 128
[2025-05-07 17:28:20,754 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:20,755 INFO  L437           NwaCegarLoop]: 148 mSDtfsCounter, 1 mSDsluCounter, 577 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 725 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:20,755 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 725 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:20,756 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 128 states.
[2025-05-07 17:28:20,762 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 128 to 128.
[2025-05-07 17:28:20,762 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 51 states have (on average 1.0392156862745099) internal successors, (53), 53 states have internal predecessors, (53), 44 states have call successors, (48), 30 states have call predecessors, (48), 32 states have return successors, (50), 44 states have call predecessors, (50), 44 states have call successors, (50)
[2025-05-07 17:28:20,763 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 151 transitions.
[2025-05-07 17:28:20,764 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 151 transitions. Word has length 93
[2025-05-07 17:28:20,764 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:20,764 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 151 transitions.
[2025-05-07 17:28:20,765 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:20,765 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 151 transitions.
[2025-05-07 17:28:20,766 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:28:20,766 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:20,766 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:20,766 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:20,766 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:20,767 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:20,767 INFO  L85        PathProgramCache]: Analyzing trace with hash 679157358, now seen corresponding path program 1 times
[2025-05-07 17:28:20,767 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:20,767 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [377859598]
[2025-05-07 17:28:20,767 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:20,767 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:20,797 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:28:20,811 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:28:20,811 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:20,811 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:20,901 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:28:20,901 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:20,901 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [377859598]
[2025-05-07 17:28:20,902 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [377859598] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:20,902 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:20,902 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:20,902 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2131892469]
[2025-05-07 17:28:20,902 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:20,902 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:20,902 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:20,902 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:20,902 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:20,902 INFO  L87              Difference]: Start difference. First operand 128 states and 151 transitions. Second operand  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:20,933 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:20,933 INFO  L93              Difference]: Finished difference Result 132 states and 155 transitions.
[2025-05-07 17:28:20,934 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:20,934 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23) Word has length 93
[2025-05-07 17:28:20,934 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:20,935 INFO  L225             Difference]: With dead ends: 132
[2025-05-07 17:28:20,935 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:28:20,935 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:20,936 INFO  L437           NwaCegarLoop]: 145 mSDtfsCounter, 1 mSDsluCounter, 568 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 713 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:20,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 713 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:20,937 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:28:20,942 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 128.
[2025-05-07 17:28:20,942 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 51 states have (on average 1.0392156862745099) internal successors, (53), 53 states have internal predecessors, (53), 44 states have call successors, (48), 30 states have call predecessors, (48), 32 states have return successors, (50), 44 states have call predecessors, (50), 44 states have call successors, (50)
[2025-05-07 17:28:20,943 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 151 transitions.
[2025-05-07 17:28:20,943 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 151 transitions. Word has length 93
[2025-05-07 17:28:20,943 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:20,943 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 151 transitions.
[2025-05-07 17:28:20,944 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:20,944 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 151 transitions.
[2025-05-07 17:28:20,945 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:28:20,945 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:20,945 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:20,945 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:20,945 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:20,945 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:20,945 INFO  L85        PathProgramCache]: Analyzing trace with hash 1614736890, now seen corresponding path program 1 times
[2025-05-07 17:28:20,945 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:20,945 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [223156072]
[2025-05-07 17:28:20,945 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:20,946 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:20,977 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:28:20,999 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:28:20,999 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:20,999 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:21,915 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 5 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:28:21,915 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:21,915 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [223156072]
[2025-05-07 17:28:21,915 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [223156072] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:21,915 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:21,915 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:28:21,916 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1983938854]
[2025-05-07 17:28:21,916 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:21,916 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:28:21,916 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:21,916 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:28:21,917 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=130, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:28:21,917 INFO  L87              Difference]: Start difference. First operand 128 states and 151 transitions. Second operand  has 13 states, 9 states have (on average 4.222222222222222) internal successors, (38), 12 states have internal predecessors, (38), 7 states have call successors, (24), 1 states have call predecessors, (24), 9 states have return successors, (25), 10 states have call predecessors, (25), 7 states have call successors, (25)
[2025-05-07 17:28:22,061 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:22,062 INFO  L93              Difference]: Finished difference Result 125 states and 146 transitions.
[2025-05-07 17:28:22,062 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:28:22,062 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 9 states have (on average 4.222222222222222) internal successors, (38), 12 states have internal predecessors, (38), 7 states have call successors, (24), 1 states have call predecessors, (24), 9 states have return successors, (25), 10 states have call predecessors, (25), 7 states have call successors, (25) Word has length 93
[2025-05-07 17:28:22,063 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:22,063 INFO  L225             Difference]: With dead ends: 125
[2025-05-07 17:28:22,063 INFO  L226             Difference]: Without dead ends: 122
[2025-05-07 17:28:22,063 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 16 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 11 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=36, Invalid=174, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:28:22,064 INFO  L437           NwaCegarLoop]: 131 mSDtfsCounter, 2 mSDsluCounter, 1023 mSDsCounter, 0 mSdLazyCounter, 107 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1154 SdHoareTripleChecker+Invalid, 108 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 107 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:22,064 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1154 Invalid, 108 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 107 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:22,064 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 122 states.
[2025-05-07 17:28:22,067 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 122 to 122.
[2025-05-07 17:28:22,067 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 49 states have (on average 1.0408163265306123) internal successors, (51), 51 states have internal predecessors, (51), 41 states have call successors, (44), 29 states have call predecessors, (44), 31 states have return successors, (46), 41 states have call predecessors, (46), 41 states have call successors, (46)
[2025-05-07 17:28:22,068 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 141 transitions.
[2025-05-07 17:28:22,068 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 141 transitions. Word has length 93
[2025-05-07 17:28:22,068 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:22,068 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 141 transitions.
[2025-05-07 17:28:22,068 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 9 states have (on average 4.222222222222222) internal successors, (38), 12 states have internal predecessors, (38), 7 states have call successors, (24), 1 states have call predecessors, (24), 9 states have return successors, (25), 10 states have call predecessors, (25), 7 states have call successors, (25)
[2025-05-07 17:28:22,069 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 141 transitions.
[2025-05-07 17:28:22,069 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:28:22,069 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:22,069 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:22,069 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:22,070 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:22,070 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:22,070 INFO  L85        PathProgramCache]: Analyzing trace with hash 1645316050, now seen corresponding path program 1 times
[2025-05-07 17:28:22,070 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:22,070 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [423051579]
[2025-05-07 17:28:22,070 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:22,070 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:22,098 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:28:22,110 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:28:22,110 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:22,110 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:22,191 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:28:22,191 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:22,191 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [423051579]
[2025-05-07 17:28:22,191 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [423051579] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:22,191 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:22,191 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:22,191 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1821228385]
[2025-05-07 17:28:22,191 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:22,192 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:22,192 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:22,192 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:22,192 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:22,192 INFO  L87              Difference]: Start difference. First operand 122 states and 141 transitions. Second operand  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:22,220 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:22,220 INFO  L93              Difference]: Finished difference Result 126 states and 145 transitions.
[2025-05-07 17:28:22,221 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:22,221 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23) Word has length 93
[2025-05-07 17:28:22,221 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:22,222 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:28:22,222 INFO  L226             Difference]: Without dead ends: 126
[2025-05-07 17:28:22,222 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:22,222 INFO  L437           NwaCegarLoop]: 137 mSDtfsCounter, 1 mSDsluCounter, 533 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 670 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:22,222 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 670 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:22,223 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 126 states.
[2025-05-07 17:28:22,225 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 126 to 122.
[2025-05-07 17:28:22,226 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 49 states have (on average 1.0408163265306123) internal successors, (51), 51 states have internal predecessors, (51), 41 states have call successors, (44), 29 states have call predecessors, (44), 31 states have return successors, (46), 41 states have call predecessors, (46), 41 states have call successors, (46)
[2025-05-07 17:28:22,226 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 141 transitions.
[2025-05-07 17:28:22,226 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 141 transitions. Word has length 93
[2025-05-07 17:28:22,226 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:22,227 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 141 transitions.
[2025-05-07 17:28:22,227 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.0) internal successors, (35), 6 states have internal predecessors, (35), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:22,227 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 141 transitions.
[2025-05-07 17:28:22,228 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 98
[2025-05-07 17:28:22,228 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:22,228 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:22,228 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:22,228 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:22,228 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:22,228 INFO  L85        PathProgramCache]: Analyzing trace with hash -1001427642, now seen corresponding path program 1 times
[2025-05-07 17:28:22,228 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:22,229 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [906335660]
[2025-05-07 17:28:22,229 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:22,229 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:22,257 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 97 statements into 1 equivalence classes.
[2025-05-07 17:28:22,268 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 97 of 97 statements.
[2025-05-07 17:28:22,268 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:22,268 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:22,400 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:28:22,400 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:22,400 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [906335660]
[2025-05-07 17:28:22,400 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [906335660] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:22,400 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:22,400 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:22,401 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1332544259]
[2025-05-07 17:28:22,401 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:22,401 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:22,401 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:22,402 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:22,402 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:22,402 INFO  L87              Difference]: Start difference. First operand 122 states and 141 transitions. Second operand  has 7 states, 6 states have (on average 6.166666666666667) internal successors, (37), 7 states have internal predecessors, (37), 4 states have call successors, (24), 1 states have call predecessors, (24), 6 states have return successors, (24), 6 states have call predecessors, (24), 4 states have call successors, (24)
[2025-05-07 17:28:22,434 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:22,434 INFO  L93              Difference]: Finished difference Result 92 states and 107 transitions.
[2025-05-07 17:28:22,435 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:22,435 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 6.166666666666667) internal successors, (37), 7 states have internal predecessors, (37), 4 states have call successors, (24), 1 states have call predecessors, (24), 6 states have return successors, (24), 6 states have call predecessors, (24), 4 states have call successors, (24) Word has length 97
[2025-05-07 17:28:22,435 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:22,435 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:28:22,435 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:22,436 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:22,436 INFO  L437           NwaCegarLoop]: 104 mSDtfsCounter, 0 mSDsluCounter, 503 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 607 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:22,436 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 607 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:22,436 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:22,436 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:22,437 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:28:22,437 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:22,437 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 97
[2025-05-07 17:28:22,437 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:22,437 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:22,437 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 6.166666666666667) internal successors, (37), 7 states have internal predecessors, (37), 4 states have call successors, (24), 1 states have call predecessors, (24), 6 states have return successors, (24), 6 states have call predecessors, (24), 4 states have call successors, (24)
[2025-05-07 17:28:22,437 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:22,437 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:22,439 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:22,439 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:22,442 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:22,443 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:22,446 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:22 BoogieIcfgContainer
[2025-05-07 17:28:22,446 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:22,446 INFO  L158              Benchmark]: Toolchain (without parser) took 5942.82ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 134.0MB in the beginning and 181.5MB in the end (delta: -47.5MB). Peak memory consumption was 3.4MB. Max. memory is 33.6GB.
[2025-05-07 17:28:22,447 INFO  L158              Benchmark]: SmtParser took 0.21ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:22,447 INFO  L158              Benchmark]: ChcToBoogie took 36.50ms. Allocated memory is still 234.9MB. Free memory was 133.9MB in the beginning and 129.6MB in the end (delta: 4.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:22,447 INFO  L158              Benchmark]: Boogie Preprocessor took 57.65ms. Allocated memory is still 234.9MB. Free memory was 129.5MB in the beginning and 125.7MB in the end (delta: 3.9MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:22,447 INFO  L158              Benchmark]: RCFGBuilder took 494.01ms. Allocated memory is still 234.9MB. Free memory was 125.6MB in the beginning and 138.3MB in the end (delta: -12.7MB). Peak memory consumption was 25.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:22,447 INFO  L158              Benchmark]: TraceAbstraction took 5351.53ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 137.9MB in the beginning and 181.5MB in the end (delta: -43.6MB). Peak memory consumption was 11.2MB. Max. memory is 33.6GB.
[2025-05-07 17:28:22,448 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.21ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 36.50ms. Allocated memory is still 234.9MB. Free memory was 133.9MB in the beginning and 129.6MB in the end (delta: 4.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 57.65ms. Allocated memory is still 234.9MB. Free memory was 129.5MB in the beginning and 125.7MB in the end (delta: 3.9MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 494.01ms. Allocated memory is still 234.9MB. Free memory was 125.6MB in the beginning and 138.3MB in the end (delta: -12.7MB). Peak memory consumption was 25.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 5351.53ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 137.9MB in the beginning and 181.5MB in the end (delta: -43.6MB). Peak memory consumption was 11.2MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 31 procedures, 138 locations, 238 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 5.3s, OverallIterations: 10, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 41 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 10 mSDsluCounter, 8497 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 7051 mSDsCounter, 8 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 506 IncrementalHoareTripleChecker+Invalid, 514 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 8 mSolverCounterUnsat, 1446 mSDtfsCounter, 506 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 252 GetRequests, 190 SyntacticMatches, 6 SemanticMatches, 56 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=138occurred in iteration=0, InterpolantAutomatonStates: 68, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 10 MinimizatonAttempts, 16 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.2s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 3.1s InterpolantComputationTime, 958 NumberOfCodeBlocks, 958 NumberOfCodeBlocksAsserted, 11 NumberOfCheckSat, 1036 ConstructedInterpolants, 0 QuantifiedInterpolants, 1397 SizeOfPredicates, 0 NumberOfNonLiveVariables, 1273 ConjunctsInSsa, 8 ConjunctsInUnsatCore, 12 InterpolantComputations, 9 PerfectInterpolantSequences, 96/117 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:28:22,459 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
