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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:32,834 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:32,872 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a5d806b8-6264-4b38-92e8-2ea9152e48c2/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:32,875 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:32,875 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:32,888 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:32,888 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:32,888 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:32,888 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:32,889 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:32,889 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:32,889 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:32,889 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:32,889 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:32,889 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:32,889 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:32,889 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:32,890 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:32,890 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:32,891 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:32,891 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:33,073 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:33,081 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:33,083 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:33,084 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:33,084 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:33,085 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a5d806b8-6264-4b38-92e8-2ea9152e48c2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/internal_call_with_assertion_1.sol_1_no_adts_000.smt2
[2025-05-07 17:28:33,086 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:33,088 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:33,388 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a5d806b8-6264-4b38-92e8-2ea9152e48c2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/internal_call_with_assertion_1.sol_1_no_adts_000.smt2
[2025-05-07 17:28:33,390 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:33,391 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:33,392 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:33,392 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:33,392 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:33,394 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,435 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33 Unit
[2025-05-07 17:28:33,435 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:33,436 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:33,436 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:33,436 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:33,447 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,447 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,477 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,478 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,485 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,486 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,488 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,490 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,491 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,501 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:33,502 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:33,502 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:33,502 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:33,502 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (1/1) ...
[2025-05-07 17:28:33,504 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:33,514 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:33,522 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:33,524 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:33,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:33,535 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:33,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:33,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_10_0 given in one single declaration
[2025-05-07 17:28:33,535 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_10_0
[2025-05-07 17:28:33,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_10_0
[2025-05-07 17:28:33,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,535 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_f__40_60_0
[2025-05-07 17:28:33,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,536 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,536 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,536 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__40_60_0
[2025-05-07 17:28:33,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,536 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_f__40_60_0
[2025-05-07 17:28:33,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_f__40_60_0
[2025-05-07 17:28:33,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_39_60_0 given in one single declaration
[2025-05-07 17:28:33,537 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_39_60_0
[2025-05-07 17:28:33,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_39_60_0
[2025-05-07 17:28:33,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,537 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__40_60_0
[2025-05-07 17:28:33,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__40_60_0
[2025-05-07 17:28:33,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_g__59_60_0 given in one single declaration
[2025-05-07 17:28:33,537 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_g__59_60_0
[2025-05-07 17:28:33,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_g__59_60_0
[2025-05-07 17:28:33,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_g__59_60_0 given in one single declaration
[2025-05-07 17:28:33,537 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_g__59_60_0
[2025-05-07 17:28:33,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_g__59_60_0 given in one single declaration
[2025-05-07 17:28:33,538 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_g_58_60_0 given in one single declaration
[2025-05-07 17:28:33,538 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_g_58_60_0
[2025-05-07 17:28:33,538 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_g_58_60_0
[2025-05-07 17:28:33,538 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_g__59_60_0 given in one single declaration
[2025-05-07 17:28:33,538 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_function_g__59_60_0 given in one single declaration
[2025-05-07 17:28:33,538 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_function_g__59_60_0
[2025-05-07 17:28:33,538 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_return_function_g__59_60_0 given in one single declaration
[2025-05-07 17:28:33,538 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_return_function_g__59_60_0
[2025-05-07 17:28:33,539 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_return_function_g__59_60_0
[2025-05-07 17:28:33,539 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__40_60_0 given in one single declaration
[2025-05-07 17:28:33,539 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__40_60_0
[2025-05-07 17:28:33,539 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__40_60_0
[2025-05-07 17:28:33,539 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_60_0 given in one single declaration
[2025-05-07 17:28:33,539 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_60_0
[2025-05-07 17:28:33,539 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_60_0
[2025-05-07 17:28:33,539 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_60_0 given in one single declaration
[2025-05-07 17:28:33,539 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_60_0
[2025-05-07 17:28:33,539 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_60_0
[2025-05-07 17:28:33,539 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_26_C_60_0 given in one single declaration
[2025-05-07 17:28:33,539 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_26_C_60_0
[2025-05-07 17:28:33,539 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_26_C_60_0
[2025-05-07 17:28:33,540 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_23_C_60_0 given in one single declaration
[2025-05-07 17:28:33,540 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_23_C_60_0
[2025-05-07 17:28:33,540 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_23_C_60_0
[2025-05-07 17:28:33,540 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_25_C_60_0 given in one single declaration
[2025-05-07 17:28:33,540 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_25_C_60_0
[2025-05-07 17:28:33,540 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_25_C_60_0
[2025-05-07 17:28:33,540 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_24_C_60_0 given in one single declaration
[2025-05-07 17:28:33,540 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_24_C_60_0
[2025-05-07 17:28:33,540 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_24_C_60_0
[2025-05-07 17:28:33,540 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_constructor_18_60_0 given in one single declaration
[2025-05-07 17:28:33,540 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_constructor_18_60_0
[2025-05-07 17:28:33,540 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_return_constructor_18_60_0 given in one single declaration
[2025-05-07 17:28:33,541 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_return_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_return_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20__17_60_0 given in one single declaration
[2025-05-07 17:28:33,541 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20__17_60_0
[2025-05-07 17:28:33,541 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20__17_60_0
[2025-05-07 17:28:33,541 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_constructor_18_60_0 given in one single declaration
[2025-05-07 17:28:33,541 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_constructor_18_60_0 given in one single declaration
[2025-05-07 17:28:33,541 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_constructor_18_60_0
[2025-05-07 17:28:33,541 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:33,541 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:33,542 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:33,687 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:33,688 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:33,934 INFO  L?                        ?]: Removed 216 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:33,934 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:33,942 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:33,942 INFO  L312             CfgBuilder]: Removed 15 assume(true) statements.
[2025-05-07 17:28:33,942 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:33 BoogieIcfgContainer
[2025-05-07 17:28:33,943 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:33,944 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:33,944 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:33,946 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:33,947 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:33" (1/3) ...
[2025-05-07 17:28:33,947 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@764dad28 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:33, skipping insertion in model container
[2025-05-07 17:28:33,947 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:33" (2/3) ...
[2025-05-07 17:28:33,947 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@764dad28 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:33, skipping insertion in model container
[2025-05-07 17:28:33,947 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:33" (3/3) ...
[2025-05-07 17:28:33,948 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:33,958 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:33,960 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 29 procedures, 115 locations, 179 edges, 29 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:33,987 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:33,995 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;@7ab7fa6b, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:33,995 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:33,997 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 115 states, 49 states have (on average 1.0816326530612246) internal successors, (53), 53 states have internal predecessors, (53), 37 states have call successors, (42), 28 states have call predecessors, (42), 28 states have return successors, (42), 33 states have call predecessors, (42), 37 states have call successors, (42)
[2025-05-07 17:28:34,005 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:34,005 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,005 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,005 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,009 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,009 INFO  L85        PathProgramCache]: Analyzing trace with hash -349146166, now seen corresponding path program 1 times
[2025-05-07 17:28:34,014 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,014 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1981366723]
[2025-05-07 17:28:34,014 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,015 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,061 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:34,091 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:34,091 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,091 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,260 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:34,260 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,260 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1981366723]
[2025-05-07 17:28:34,261 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1981366723] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,261 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,263 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:34,264 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [510791833]
[2025-05-07 17:28:34,264 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,267 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:34,267 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,296 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:34,296 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,298 INFO  L87              Difference]: Start difference. First operand  has 115 states, 49 states have (on average 1.0816326530612246) internal successors, (53), 53 states have internal predecessors, (53), 37 states have call successors, (42), 28 states have call predecessors, (42), 28 states have return successors, (42), 33 states have call predecessors, (42), 37 states have call successors, (42) Second operand  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:34,370 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,370 INFO  L93              Difference]: Finished difference Result 117 states and 139 transitions.
[2025-05-07 17:28:34,372 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:34,373 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:28:34,374 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,381 INFO  L225             Difference]: With dead ends: 117
[2025-05-07 17:28:34,382 INFO  L226             Difference]: Without dead ends: 117
[2025-05-07 17:28:34,383 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:34,387 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 255 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 388 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:34,387 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 388 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:34,401 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-05-07 17:28:34,421 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 115.
[2025-05-07 17:28:34,422 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 115 states, 49 states have (on average 1.0612244897959184) internal successors, (52), 52 states have internal predecessors, (52), 37 states have call successors, (42), 28 states have call predecessors, (42), 29 states have return successors, (43), 34 states have call predecessors, (43), 37 states have call successors, (43)
[2025-05-07 17:28:34,425 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 115 states to 115 states and 137 transitions.
[2025-05-07 17:28:34,426 INFO  L79                 Accepts]: Start accepts. Automaton has 115 states and 137 transitions. Word has length 66
[2025-05-07 17:28:34,427 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,427 INFO  L485      AbstractCegarLoop]: Abstraction has 115 states and 137 transitions.
[2025-05-07 17:28:34,427 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:34,427 INFO  L278                IsEmpty]: Start isEmpty. Operand 115 states and 137 transitions.
[2025-05-07 17:28:34,430 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:34,430 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,430 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,430 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:34,430 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,431 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,431 INFO  L85        PathProgramCache]: Analyzing trace with hash 860576384, now seen corresponding path program 1 times
[2025-05-07 17:28:34,431 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,431 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [331217916]
[2025-05-07 17:28:34,431 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,431 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,474 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:34,521 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:34,522 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,522 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,698 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:34,698 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [331217916]
[2025-05-07 17:28:34,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [331217916] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,698 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,699 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:34,699 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1295485459]
[2025-05-07 17:28:34,699 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,700 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:34,700 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,701 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:34,701 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:34,701 INFO  L87              Difference]: Start difference. First operand 115 states and 137 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:34,749 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,750 INFO  L93              Difference]: Finished difference Result 120 states and 143 transitions.
[2025-05-07 17:28:34,750 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:34,750 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:28:34,751 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,752 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:28:34,752 INFO  L226             Difference]: Without dead ends: 120
[2025-05-07 17:28:34,752 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:34,753 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 521 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 654 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:34,753 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 654 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:34,754 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-05-07 17:28:34,762 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 120.
[2025-05-07 17:28:34,763 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 120 states, 51 states have (on average 1.0588235294117647) internal successors, (54), 54 states have internal predecessors, (54), 38 states have call successors, (43), 28 states have call predecessors, (43), 31 states have return successors, (46), 37 states have call predecessors, (46), 38 states have call successors, (46)
[2025-05-07 17:28:34,764 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 120 states to 120 states and 143 transitions.
[2025-05-07 17:28:34,765 INFO  L79                 Accepts]: Start accepts. Automaton has 120 states and 143 transitions. Word has length 66
[2025-05-07 17:28:34,765 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,765 INFO  L485      AbstractCegarLoop]: Abstraction has 120 states and 143 transitions.
[2025-05-07 17:28:34,765 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:34,765 INFO  L278                IsEmpty]: Start isEmpty. Operand 120 states and 143 transitions.
[2025-05-07 17:28:34,767 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:28:34,767 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,767 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,768 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:34,768 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,768 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,768 INFO  L85        PathProgramCache]: Analyzing trace with hash 821037505, now seen corresponding path program 1 times
[2025-05-07 17:28:34,768 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,769 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1140525806]
[2025-05-07 17:28:34,769 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,769 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,797 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:28:34,800 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:28:34,800 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,800 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,866 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:34,866 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,866 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1140525806]
[2025-05-07 17:28:34,866 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1140525806] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,866 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,866 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:34,866 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [329275879]
[2025-05-07 17:28:34,866 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,867 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:34,867 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,867 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:34,867 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,867 INFO  L87              Difference]: Start difference. First operand 120 states and 143 transitions. Second operand  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:28:34,877 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,877 INFO  L93              Difference]: Finished difference Result 124 states and 147 transitions.
[2025-05-07 17:28:34,877 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:34,878 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22) Word has length 80
[2025-05-07 17:28:34,878 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,879 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:28:34,879 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:28:34,879 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:34,879 INFO  L437           NwaCegarLoop]: 136 mSDtfsCounter, 1 mSDsluCounter, 264 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 400 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:34,879 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 400 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:34,880 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:28:34,884 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 114.
[2025-05-07 17:28:34,885 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 114 states, 50 states have (on average 1.02) internal successors, (51), 51 states have internal predecessors, (51), 34 states have call successors, (39), 28 states have call predecessors, (39), 30 states have return successors, (41), 34 states have call predecessors, (41), 34 states have call successors, (41)
[2025-05-07 17:28:34,885 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 131 transitions.
[2025-05-07 17:28:34,885 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 131 transitions. Word has length 80
[2025-05-07 17:28:34,886 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,886 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 131 transitions.
[2025-05-07 17:28:34,886 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:28:34,886 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 131 transitions.
[2025-05-07 17:28:34,887 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:28:34,887 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,887 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,887 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:34,887 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,887 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,887 INFO  L85        PathProgramCache]: Analyzing trace with hash 1428821749, now seen corresponding path program 1 times
[2025-05-07 17:28:34,888 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,888 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1499995297]
[2025-05-07 17:28:34,888 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,888 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,911 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:28:34,929 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:28:34,929 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,929 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:35,084 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:35,084 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:35,085 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1499995297]
[2025-05-07 17:28:35,085 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1499995297] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:35,085 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:35,085 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:35,085 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1973721689]
[2025-05-07 17:28:35,085 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:35,085 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:35,085 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:35,086 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:35,086 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:35,086 INFO  L87              Difference]: Start difference. First operand 114 states and 131 transitions. Second operand  has 8 states, 6 states have (on average 6.0) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 6 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:28:35,186 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:35,186 INFO  L93              Difference]: Finished difference Result 120 states and 138 transitions.
[2025-05-07 17:28:35,187 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:35,187 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 6.0) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 6 states have call predecessors, (22), 5 states have call successors, (22) Word has length 80
[2025-05-07 17:28:35,188 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:35,189 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:28:35,189 INFO  L226             Difference]: Without dead ends: 120
[2025-05-07 17:28:35,189 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:35,190 INFO  L437           NwaCegarLoop]: 119 mSDtfsCounter, 2 mSDsluCounter, 694 mSDsCounter, 0 mSdLazyCounter, 63 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 813 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 63 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:35,190 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 813 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 63 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:35,191 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-05-07 17:28:35,198 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 118.
[2025-05-07 17:28:35,198 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 118 states, 52 states have (on average 1.0192307692307692) internal successors, (53), 53 states have internal predecessors, (53), 34 states have call successors, (39), 28 states have call predecessors, (39), 32 states have return successors, (44), 36 states have call predecessors, (44), 34 states have call successors, (44)
[2025-05-07 17:28:35,199 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 136 transitions.
[2025-05-07 17:28:35,199 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 136 transitions. Word has length 80
[2025-05-07 17:28:35,200 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:35,200 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 136 transitions.
[2025-05-07 17:28:35,201 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 6.0) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 6 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:28:35,201 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 136 transitions.
[2025-05-07 17:28:35,202 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:28:35,202 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:35,202 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:35,202 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:35,202 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:35,203 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:35,203 INFO  L85        PathProgramCache]: Analyzing trace with hash -1966076929, now seen corresponding path program 1 times
[2025-05-07 17:28:35,203 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:35,203 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [49239541]
[2025-05-07 17:28:35,203 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:35,203 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:35,232 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:28:35,252 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:28:35,252 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:35,252 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:35,362 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:35,362 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:35,362 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [49239541]
[2025-05-07 17:28:35,362 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [49239541] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:35,363 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:35,363 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:35,363 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [392030403]
[2025-05-07 17:28:35,363 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:35,363 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:35,363 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:35,364 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:35,364 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:35,364 INFO  L87              Difference]: Start difference. First operand 118 states and 136 transitions. Second operand  has 8 states, 7 states have (on average 5.142857142857143) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (22), 8 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:28:35,435 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:35,435 INFO  L93              Difference]: Finished difference Result 128 states and 150 transitions.
[2025-05-07 17:28:35,436 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:35,436 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 5.142857142857143) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (22), 8 states have call predecessors, (22), 5 states have call successors, (22) Word has length 80
[2025-05-07 17:28:35,436 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:35,437 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:28:35,437 INFO  L226             Difference]: Without dead ends: 128
[2025-05-07 17:28:35,438 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:35,438 INFO  L437           NwaCegarLoop]: 123 mSDtfsCounter, 1 mSDsluCounter, 721 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 844 SdHoareTripleChecker+Invalid, 54 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:35,439 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 844 Invalid, 54 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:35,439 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 128 states.
[2025-05-07 17:28:35,446 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 128 to 123.
[2025-05-07 17:28:35,447 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 123 states, 54 states have (on average 1.0185185185185186) internal successors, (55), 55 states have internal predecessors, (55), 35 states have call successors, (40), 28 states have call predecessors, (40), 34 states have return successors, (49), 39 states have call predecessors, (49), 35 states have call successors, (49)
[2025-05-07 17:28:35,448 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 123 states to 123 states and 144 transitions.
[2025-05-07 17:28:35,448 INFO  L79                 Accepts]: Start accepts. Automaton has 123 states and 144 transitions. Word has length 80
[2025-05-07 17:28:35,448 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:35,448 INFO  L485      AbstractCegarLoop]: Abstraction has 123 states and 144 transitions.
[2025-05-07 17:28:35,448 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 5.142857142857143) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (22), 8 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:28:35,448 INFO  L278                IsEmpty]: Start isEmpty. Operand 123 states and 144 transitions.
[2025-05-07 17:28:35,450 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:28:35,450 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:35,450 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:35,450 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:35,450 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:35,450 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:35,450 INFO  L85        PathProgramCache]: Analyzing trace with hash 389935869, now seen corresponding path program 1 times
[2025-05-07 17:28:35,451 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:35,451 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1033767118]
[2025-05-07 17:28:35,451 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:35,451 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:35,487 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:28:35,504 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:28:35,504 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:35,504 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:36,191 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:36,192 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:36,192 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1033767118]
[2025-05-07 17:28:36,192 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1033767118] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:36,192 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:36,192 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [19] imperfect sequences [] total 19
[2025-05-07 17:28:36,192 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [963076387]
[2025-05-07 17:28:36,192 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:36,193 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-05-07 17:28:36,193 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:36,193 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-05-07 17:28:36,193 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=307, Unknown=0, NotChecked=0, Total=342
[2025-05-07 17:28:36,194 INFO  L87              Difference]: Start difference. First operand 123 states and 144 transitions. Second operand  has 19 states, 14 states have (on average 2.5714285714285716) internal successors, (36), 17 states have internal predecessors, (36), 12 states have call successors, (22), 1 states have call predecessors, (22), 14 states have return successors, (22), 16 states have call predecessors, (22), 12 states have call successors, (22)
[2025-05-07 17:28:36,610 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:36,610 INFO  L93              Difference]: Finished difference Result 143 states and 170 transitions.
[2025-05-07 17:28:36,611 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-05-07 17:28:36,611 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 14 states have (on average 2.5714285714285716) internal successors, (36), 17 states have internal predecessors, (36), 12 states have call successors, (22), 1 states have call predecessors, (22), 14 states have return successors, (22), 16 states have call predecessors, (22), 12 states have call successors, (22) Word has length 80
[2025-05-07 17:28:36,611 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:36,612 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:28:36,612 INFO  L226             Difference]: Without dead ends: 143
[2025-05-07 17:28:36,613 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 23 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=53, Invalid=453, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:28:36,613 INFO  L437           NwaCegarLoop]: 127 mSDtfsCounter, 5 mSDsluCounter, 2098 mSDsCounter, 0 mSdLazyCounter, 426 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 2225 SdHoareTripleChecker+Invalid, 427 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 426 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:36,613 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 2225 Invalid, 427 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 426 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:28:36,614 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-05-07 17:28:36,620 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 139.
[2025-05-07 17:28:36,621 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 60 states have (on average 1.0166666666666666) internal successors, (61), 61 states have internal predecessors, (61), 39 states have call successors, (44), 28 states have call predecessors, (44), 40 states have return successors, (61), 49 states have call predecessors, (61), 39 states have call successors, (61)
[2025-05-07 17:28:36,621 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 166 transitions.
[2025-05-07 17:28:36,621 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 166 transitions. Word has length 80
[2025-05-07 17:28:36,622 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:36,622 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 166 transitions.
[2025-05-07 17:28:36,622 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 14 states have (on average 2.5714285714285716) internal successors, (36), 17 states have internal predecessors, (36), 12 states have call successors, (22), 1 states have call predecessors, (22), 14 states have return successors, (22), 16 states have call predecessors, (22), 12 states have call successors, (22)
[2025-05-07 17:28:36,622 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 166 transitions.
[2025-05-07 17:28:36,623 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:28:36,623 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:36,623 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:36,623 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:36,623 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:36,623 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:36,623 INFO  L85        PathProgramCache]: Analyzing trace with hash -1826264381, now seen corresponding path program 1 times
[2025-05-07 17:28:36,623 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:36,624 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1014074959]
[2025-05-07 17:28:36,624 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:36,624 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:36,652 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:28:36,658 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:28:36,658 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:36,658 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:36,904 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:36,904 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:36,904 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1014074959]
[2025-05-07 17:28:36,905 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1014074959] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:36,905 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:36,905 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-05-07 17:28:36,905 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2135469622]
[2025-05-07 17:28:36,905 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:36,905 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-05-07 17:28:36,905 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:36,906 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-05-07 17:28:36,906 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-05-07 17:28:36,906 INFO  L87              Difference]: Start difference. First operand 139 states and 166 transitions. Second operand  has 12 states, 9 states have (on average 4.0) internal successors, (36), 10 states have internal predecessors, (36), 6 states have call successors, (22), 1 states have call predecessors, (22), 9 states have return successors, (22), 9 states have call predecessors, (22), 6 states have call successors, (22)
[2025-05-07 17:28:37,007 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:37,007 INFO  L93              Difference]: Finished difference Result 137 states and 163 transitions.
[2025-05-07 17:28:37,008 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-05-07 17:28:37,008 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 9 states have (on average 4.0) internal successors, (36), 10 states have internal predecessors, (36), 6 states have call successors, (22), 1 states have call predecessors, (22), 9 states have return successors, (22), 9 states have call predecessors, (22), 6 states have call successors, (22) Word has length 80
[2025-05-07 17:28:37,008 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:37,009 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:28:37,010 INFO  L226             Difference]: Without dead ends: 127
[2025-05-07 17:28:37,010 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=29, Invalid=153, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:28:37,010 INFO  L437           NwaCegarLoop]: 120 mSDtfsCounter, 2 mSDsluCounter, 1178 mSDsCounter, 0 mSdLazyCounter, 101 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1298 SdHoareTripleChecker+Invalid, 101 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 101 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:37,011 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1298 Invalid, 101 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 101 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:37,011 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-05-07 17:28:37,018 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 127.
[2025-05-07 17:28:37,019 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 127 states, 55 states have (on average 1.018181818181818) internal successors, (56), 56 states have internal predecessors, (56), 36 states have call successors, (40), 27 states have call predecessors, (40), 36 states have return successors, (54), 43 states have call predecessors, (54), 36 states have call successors, (54)
[2025-05-07 17:28:37,020 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 150 transitions.
[2025-05-07 17:28:37,020 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 150 transitions. Word has length 80
[2025-05-07 17:28:37,020 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:37,020 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 150 transitions.
[2025-05-07 17:28:37,020 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 9 states have (on average 4.0) internal successors, (36), 10 states have internal predecessors, (36), 6 states have call successors, (22), 1 states have call predecessors, (22), 9 states have return successors, (22), 9 states have call predecessors, (22), 6 states have call successors, (22)
[2025-05-07 17:28:37,020 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 150 transitions.
[2025-05-07 17:28:37,022 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 106
[2025-05-07 17:28:37,022 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:37,022 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:37,022 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:37,022 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:37,022 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:37,022 INFO  L85        PathProgramCache]: Analyzing trace with hash 246631747, now seen corresponding path program 1 times
[2025-05-07 17:28:37,023 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:37,023 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [450109405]
[2025-05-07 17:28:37,023 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:37,023 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:37,059 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 105 statements into 1 equivalence classes.
[2025-05-07 17:28:37,075 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 105 of 105 statements.
[2025-05-07 17:28:37,075 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:37,075 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:37,173 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:28:37,173 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:37,173 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [450109405]
[2025-05-07 17:28:37,173 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [450109405] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:37,173 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1472246231]
[2025-05-07 17:28:37,173 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:37,173 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:37,176 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:37,178 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:37,179 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:28:37,446 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 105 statements into 1 equivalence classes.
[2025-05-07 17:28:37,597 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 105 of 105 statements.
[2025-05-07 17:28:37,597 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:37,597 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:37,603 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1472 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:37,612 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:37,654 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 18 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:28:37,654 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:37,654 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1472246231] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:37,654 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:37,654 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 6
[2025-05-07 17:28:37,654 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1356319330]
[2025-05-07 17:28:37,654 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:37,655 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:37,655 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:37,655 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:37,655 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:37,655 INFO  L87              Difference]: Start difference. First operand 127 states and 150 transitions. Second operand  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (29), 2 states have call predecessors, (29), 5 states have return successors, (29), 6 states have call predecessors, (29), 5 states have call successors, (29)
[2025-05-07 17:28:37,686 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:37,687 INFO  L93              Difference]: Finished difference Result 127 states and 148 transitions.
[2025-05-07 17:28:37,687 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:37,687 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (29), 2 states have call predecessors, (29), 5 states have return successors, (29), 6 states have call predecessors, (29), 5 states have call successors, (29) Word has length 105
[2025-05-07 17:28:37,688 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:37,688 INFO  L225             Difference]: With dead ends: 127
[2025-05-07 17:28:37,688 INFO  L226             Difference]: Without dead ends: 117
[2025-05-07 17:28:37,688 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 110 GetRequests, 106 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:37,689 INFO  L437           NwaCegarLoop]: 120 mSDtfsCounter, 1 mSDsluCounter, 465 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 585 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:37,689 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 585 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:37,689 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-05-07 17:28:37,692 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 113.
[2025-05-07 17:28:37,693 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 49 states have (on average 1.0204081632653061) internal successors, (50), 50 states have internal predecessors, (50), 33 states have call successors, (36), 26 states have call predecessors, (36), 31 states have return successors, (43), 36 states have call predecessors, (43), 33 states have call successors, (43)
[2025-05-07 17:28:37,693 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 129 transitions.
[2025-05-07 17:28:37,693 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 129 transitions. Word has length 105
[2025-05-07 17:28:37,693 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:37,693 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 129 transitions.
[2025-05-07 17:28:37,694 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (29), 2 states have call predecessors, (29), 5 states have return successors, (29), 6 states have call predecessors, (29), 5 states have call successors, (29)
[2025-05-07 17:28:37,694 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 129 transitions.
[2025-05-07 17:28:37,694 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:37,694 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:37,695 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:37,702 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:28:37,895 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:37,896 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:37,896 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:37,897 INFO  L85        PathProgramCache]: Analyzing trace with hash 1761481307, now seen corresponding path program 1 times
[2025-05-07 17:28:37,897 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:37,897 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1480180737]
[2025-05-07 17:28:37,897 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:37,897 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:37,994 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:38,027 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:38,027 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,027 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,331 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:38,331 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,332 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1480180737]
[2025-05-07 17:28:38,332 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1480180737] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,332 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,332 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:28:38,332 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1856535579]
[2025-05-07 17:28:38,332 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,332 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:28:38,332 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,333 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:28:38,333 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:38,333 INFO  L87              Difference]: Start difference. First operand 113 states and 129 transitions. Second operand  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 7 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:28:38,414 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,414 INFO  L93              Difference]: Finished difference Result 113 states and 128 transitions.
[2025-05-07 17:28:38,414 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:28:38,415 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 7 states have call predecessors, (23), 5 states have call successors, (23) Word has length 83
[2025-05-07 17:28:38,415 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,416 INFO  L225             Difference]: With dead ends: 113
[2025-05-07 17:28:38,416 INFO  L226             Difference]: Without dead ends: 113
[2025-05-07 17:28:38,416 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 18 GetRequests, 10 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:38,417 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 846 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 955 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,417 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 955 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:38,417 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-05-07 17:28:38,421 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 113.
[2025-05-07 17:28:38,422 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 49 states have (on average 1.0204081632653061) internal successors, (50), 50 states have internal predecessors, (50), 33 states have call successors, (36), 26 states have call predecessors, (36), 31 states have return successors, (42), 36 states have call predecessors, (42), 33 states have call successors, (42)
[2025-05-07 17:28:38,423 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 128 transitions.
[2025-05-07 17:28:38,423 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 128 transitions. Word has length 83
[2025-05-07 17:28:38,423 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,423 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 128 transitions.
[2025-05-07 17:28:38,423 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 7 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:28:38,423 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 128 transitions.
[2025-05-07 17:28:38,424 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:38,424 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,425 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,425 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:38,425 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,425 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,425 INFO  L85        PathProgramCache]: Analyzing trace with hash 1080947421, now seen corresponding path program 1 times
[2025-05-07 17:28:38,425 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,425 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1435748865]
[2025-05-07 17:28:38,426 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,426 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,452 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:38,464 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:38,465 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,465 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,689 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:38,689 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,689 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1435748865]
[2025-05-07 17:28:38,689 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1435748865] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,689 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,689 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:28:38,690 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1715615833]
[2025-05-07 17:28:38,690 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,690 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:28:38,690 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,690 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:28:38,690 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:38,690 INFO  L87              Difference]: Start difference. First operand 113 states and 128 transitions. Second operand  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 7 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:28:38,753 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,753 INFO  L93              Difference]: Finished difference Result 117 states and 132 transitions.
[2025-05-07 17:28:38,753 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:28:38,754 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 7 states have call predecessors, (23), 5 states have call successors, (23) Word has length 83
[2025-05-07 17:28:38,754 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,754 INFO  L225             Difference]: With dead ends: 117
[2025-05-07 17:28:38,754 INFO  L226             Difference]: Without dead ends: 117
[2025-05-07 17:28:38,755 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 18 GetRequests, 10 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:38,755 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 854 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 964 SdHoareTripleChecker+Invalid, 69 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,755 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 964 Invalid, 69 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:38,756 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-05-07 17:28:38,759 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 117.
[2025-05-07 17:28:38,759 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 51 states have (on average 1.0196078431372548) internal successors, (52), 52 states have internal predecessors, (52), 33 states have call successors, (36), 26 states have call predecessors, (36), 33 states have return successors, (44), 38 states have call predecessors, (44), 33 states have call successors, (44)
[2025-05-07 17:28:38,760 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 132 transitions.
[2025-05-07 17:28:38,760 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 132 transitions. Word has length 83
[2025-05-07 17:28:38,760 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,760 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 132 transitions.
[2025-05-07 17:28:38,760 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 7 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:28:38,760 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 132 transitions.
[2025-05-07 17:28:38,761 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:38,761 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,761 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,761 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:38,761 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,761 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,762 INFO  L85        PathProgramCache]: Analyzing trace with hash -596567981, now seen corresponding path program 1 times
[2025-05-07 17:28:38,762 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,762 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1438890968]
[2025-05-07 17:28:38,762 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,762 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,789 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:38,801 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:38,801 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,801 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,041 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:39,041 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,041 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1438890968]
[2025-05-07 17:28:39,041 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1438890968] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,041 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,042 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:28:39,042 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [591557730]
[2025-05-07 17:28:39,042 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,042 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:28:39,042 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,043 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:28:39,043 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:39,043 INFO  L87              Difference]: Start difference. First operand 117 states and 132 transitions. Second operand  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 8 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:28:39,109 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,109 INFO  L93              Difference]: Finished difference Result 122 states and 138 transitions.
[2025-05-07 17:28:39,110 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:28:39,110 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 8 states have call predecessors, (23), 5 states have call successors, (23) Word has length 83
[2025-05-07 17:28:39,110 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,111 INFO  L225             Difference]: With dead ends: 122
[2025-05-07 17:28:39,111 INFO  L226             Difference]: Without dead ends: 122
[2025-05-07 17:28:39,111 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 17 GetRequests, 9 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:39,112 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 1 mSDsluCounter, 868 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 980 SdHoareTripleChecker+Invalid, 69 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,112 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 980 Invalid, 69 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:39,112 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 122 states.
[2025-05-07 17:28:39,116 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 122 to 122.
[2025-05-07 17:28:39,117 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 53 states have (on average 1.0188679245283019) internal successors, (54), 54 states have internal predecessors, (54), 34 states have call successors, (37), 26 states have call predecessors, (37), 35 states have return successors, (47), 41 states have call predecessors, (47), 34 states have call successors, (47)
[2025-05-07 17:28:39,118 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 138 transitions.
[2025-05-07 17:28:39,118 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 138 transitions. Word has length 83
[2025-05-07 17:28:39,118 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,118 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 138 transitions.
[2025-05-07 17:28:39,118 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 4.111111111111111) internal successors, (37), 10 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (23), 8 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:28:39,118 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 138 transitions.
[2025-05-07 17:28:39,119 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:39,119 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,119 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,119 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:39,120 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,120 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,120 INFO  L85        PathProgramCache]: Analyzing trace with hash 316398515, now seen corresponding path program 1 times
[2025-05-07 17:28:39,120 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,120 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [864285295]
[2025-05-07 17:28:39,120 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,120 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,148 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:39,157 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:39,157 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,157 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,218 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:39,218 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,218 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [864285295]
[2025-05-07 17:28:39,218 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [864285295] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,218 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,218 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:39,218 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [312268286]
[2025-05-07 17:28:39,218 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,219 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:39,219 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,219 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:39,219 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:39,219 INFO  L87              Difference]: Start difference. First operand 122 states and 138 transitions. Second operand  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:39,249 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,249 INFO  L93              Difference]: Finished difference Result 122 states and 136 transitions.
[2025-05-07 17:28:39,249 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:39,249 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23) Word has length 83
[2025-05-07 17:28:39,249 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,250 INFO  L225             Difference]: With dead ends: 122
[2025-05-07 17:28:39,250 INFO  L226             Difference]: Without dead ends: 121
[2025-05-07 17:28:39,250 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:39,251 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 1 mSDsluCounter, 444 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 559 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,251 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 559 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,252 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-05-07 17:28:39,255 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 116.
[2025-05-07 17:28:39,256 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 116 states, 51 states have (on average 1.0196078431372548) internal successors, (52), 52 states have internal predecessors, (52), 32 states have call successors, (35), 26 states have call predecessors, (35), 33 states have return successors, (41), 37 states have call predecessors, (41), 32 states have call successors, (41)
[2025-05-07 17:28:39,257 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 128 transitions.
[2025-05-07 17:28:39,257 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 128 transitions. Word has length 83
[2025-05-07 17:28:39,257 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,257 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 128 transitions.
[2025-05-07 17:28:39,257 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:39,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 128 transitions.
[2025-05-07 17:28:39,258 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:28:39,259 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,259 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:39,259 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:28:39,259 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,259 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,259 INFO  L85        PathProgramCache]: Analyzing trace with hash 1155491200, now seen corresponding path program 1 times
[2025-05-07 17:28:39,259 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,259 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1225141698]
[2025-05-07 17:28:39,260 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,260 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,302 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:28:39,329 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:28:39,329 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,329 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:40,538 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-05-07 17:28:40,539 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:40,539 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1225141698]
[2025-05-07 17:28:40,539 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1225141698] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:40,539 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [321833246]
[2025-05-07 17:28:40,539 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:40,539 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:40,541 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:40,542 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:40,543 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:28:40,778 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:28:40,953 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:28:40,953 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:40,953 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:40,960 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1755 conjuncts, 102 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:40,966 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:41,085 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-05-07 17:28:41,085 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:43,740 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 16 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-05-07 17:28:43,740 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [321833246] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:43,740 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:43,740 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [29, 29, 32] total 46
[2025-05-07 17:28:43,740 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [36890265]
[2025-05-07 17:28:43,740 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:43,741 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 46 states
[2025-05-07 17:28:43,741 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:43,741 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 46 interpolants.
[2025-05-07 17:28:43,742 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=123, Invalid=1947, Unknown=0, NotChecked=0, Total=2070
[2025-05-07 17:28:43,742 INFO  L87              Difference]: Start difference. First operand 116 states and 128 transitions. Second operand  has 46 states, 28 states have (on average 2.1785714285714284) internal successors, (61), 39 states have internal predecessors, (61), 29 states have call successors, (42), 1 states have call predecessors, (42), 28 states have return successors, (48), 35 states have call predecessors, (48), 29 states have call successors, (48)
[2025-05-07 17:28:44,452 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:44,452 INFO  L93              Difference]: Finished difference Result 127 states and 144 transitions.
[2025-05-07 17:28:44,452 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 30 states. 
[2025-05-07 17:28:44,453 INFO  L79                 Accepts]: Start accepts. Automaton has  has 46 states, 28 states have (on average 2.1785714285714284) internal successors, (61), 39 states have internal predecessors, (61), 29 states have call successors, (42), 1 states have call predecessors, (42), 28 states have return successors, (48), 35 states have call predecessors, (48), 29 states have call successors, (48) Word has length 122
[2025-05-07 17:28:44,453 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:44,454 INFO  L225             Difference]: With dead ends: 127
[2025-05-07 17:28:44,454 INFO  L226             Difference]: Without dead ends: 126
[2025-05-07 17:28:44,454 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 285 GetRequests, 232 SyntacticMatches, 0 SemanticMatches, 53 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 164 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=181, Invalid=2789, Unknown=0, NotChecked=0, Total=2970
[2025-05-07 17:28:44,454 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 13 mSDsluCounter, 3067 mSDsCounter, 0 mSdLazyCounter, 856 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 3169 SdHoareTripleChecker+Invalid, 866 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 856 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:44,455 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 3169 Invalid, 866 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 856 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-05-07 17:28:44,455 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 126 states.
[2025-05-07 17:28:44,458 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 126 to 122.
[2025-05-07 17:28:44,458 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 53 states have (on average 1.0188679245283019) internal successors, (54), 54 states have internal predecessors, (54), 34 states have call successors, (37), 26 states have call predecessors, (37), 35 states have return successors, (46), 41 states have call predecessors, (46), 34 states have call successors, (46)
[2025-05-07 17:28:44,458 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 137 transitions.
[2025-05-07 17:28:44,458 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 137 transitions. Word has length 122
[2025-05-07 17:28:44,459 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:44,459 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 137 transitions.
[2025-05-07 17:28:44,459 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 46 states, 28 states have (on average 2.1785714285714284) internal successors, (61), 39 states have internal predecessors, (61), 29 states have call successors, (42), 1 states have call predecessors, (42), 28 states have return successors, (48), 35 states have call predecessors, (48), 29 states have call successors, (48)
[2025-05-07 17:28:44,459 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 137 transitions.
[2025-05-07 17:28:44,459 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:28:44,460 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:44,460 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:44,467 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:28:44,660 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:44,660 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:44,661 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:44,662 INFO  L85        PathProgramCache]: Analyzing trace with hash 352140832, now seen corresponding path program 1 times
[2025-05-07 17:28:44,662 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:44,662 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1741057684]
[2025-05-07 17:28:44,662 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:44,662 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:44,696 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:28:44,706 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:28:44,707 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:44,707 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:44,779 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 24 trivial. 0 not checked.
[2025-05-07 17:28:44,780 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:44,780 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1741057684]
[2025-05-07 17:28:44,780 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1741057684] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:44,780 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [253424154]
[2025-05-07 17:28:44,780 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:44,780 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:44,782 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:44,784 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:44,785 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:28:45,056 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:28:45,191 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:28:45,191 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:45,191 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:45,195 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1756 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:45,198 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:45,217 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 30 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:28:45,217 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:45,217 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [253424154] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:45,217 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:45,217 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 6
[2025-05-07 17:28:45,217 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1960192169]
[2025-05-07 17:28:45,217 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:45,218 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:45,218 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:45,218 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:45,218 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:45,218 INFO  L87              Difference]: Start difference. First operand 122 states and 137 transitions. Second operand  has 6 states, 5 states have (on average 10.8) internal successors, (54), 6 states have internal predecessors, (54), 5 states have call successors, (34), 2 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 5 states have call successors, (34)
[2025-05-07 17:28:45,239 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:45,239 INFO  L93              Difference]: Finished difference Result 114 states and 125 transitions.
[2025-05-07 17:28:45,239 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:45,240 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.8) internal successors, (54), 6 states have internal predecessors, (54), 5 states have call successors, (34), 2 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 5 states have call successors, (34) Word has length 122
[2025-05-07 17:28:45,240 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:45,240 INFO  L225             Difference]: With dead ends: 114
[2025-05-07 17:28:45,240 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:45,240 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 127 GetRequests, 123 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:45,240 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 423 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 533 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:45,240 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 533 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:45,241 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:45,241 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:45,241 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:45,241 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:45,241 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 122
[2025-05-07 17:28:45,241 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:45,241 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:45,241 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.8) internal successors, (54), 6 states have internal predecessors, (54), 5 states have call successors, (34), 2 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 5 states have call successors, (34)
[2025-05-07 17:28:45,241 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:45,241 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:45,243 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:45,248 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:28:45,444 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:45,452 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:45,458 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:45,466 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:45 BoogieIcfgContainer
[2025-05-07 17:28:45,466 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:45,468 INFO  L158              Benchmark]: Toolchain (without parser) took 12075.43ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 146.7MB in the beginning and 124.9MB in the end (delta: 21.7MB). Peak memory consumption was 135.6MB. Max. memory is 33.6GB.
[2025-05-07 17:28:45,468 INFO  L158              Benchmark]: SmtParser took 0.22ms. Allocated memory is still 234.9MB. Free memory is still 173.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:45,469 INFO  L158              Benchmark]: ChcToBoogie took 43.20ms. Allocated memory is still 234.9MB. Free memory was 146.6MB in the beginning and 143.4MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:45,469 INFO  L158              Benchmark]: Boogie Preprocessor took 65.57ms. Allocated memory is still 234.9MB. Free memory was 143.4MB in the beginning and 139.9MB in the end (delta: 3.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:45,470 INFO  L158              Benchmark]: RCFGBuilder took 440.88ms. Allocated memory is still 234.9MB. Free memory was 139.9MB in the beginning and 171.6MB in the end (delta: -31.7MB). Peak memory consumption was 43.1MB. Max. memory is 33.6GB.
[2025-05-07 17:28:45,470 INFO  L158              Benchmark]: TraceAbstraction took 11522.22ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 170.8MB in the beginning and 124.9MB in the end (delta: 45.8MB). Peak memory consumption was 159.6MB. Max. memory is 33.6GB.
[2025-05-07 17:28:45,473 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.22ms. Allocated memory is still 234.9MB. Free memory is still 173.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 43.20ms. Allocated memory is still 234.9MB. Free memory was 146.6MB in the beginning and 143.4MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 65.57ms. Allocated memory is still 234.9MB. Free memory was 143.4MB in the beginning and 139.9MB in the end (delta: 3.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 440.88ms. Allocated memory is still 234.9MB. Free memory was 139.9MB in the beginning and 171.6MB in the end (delta: -31.7MB). Peak memory consumption was 43.1MB. Max. memory is 33.6GB.
 * TraceAbstraction took 11522.22ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 170.8MB in the beginning and 124.9MB in the end (delta: 45.8MB). Peak memory consumption was 159.6MB. 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 29 procedures, 115 locations, 179 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 11.5s, OverallIterations: 14, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 68 SdHoareTripleChecker+Valid, 1.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 32 mSDsluCounter, 14367 SdHoareTripleChecker+Invalid, 1.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 12698 mSDsCounter, 12 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1796 IncrementalHoareTripleChecker+Invalid, 1808 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 12 mSolverCounterUnsat, 1669 mSDtfsCounter, 1796 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 649 GetRequests, 506 SyntacticMatches, 0 SemanticMatches, 143 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 170 ImplicationChecksByTransitivity, 1.4s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=139occurred in iteration=6, InterpolantAutomatonStates: 139, 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, 14 MinimizatonAttempts, 28 StatesRemovedByMinimization, 8 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.3s SsaConstructionTime, 0.7s SatisfiabilityAnalysisTime, 6.7s InterpolantComputationTime, 1562 NumberOfCodeBlocks, 1562 NumberOfCodeBlocksAsserted, 17 NumberOfCheckSat, 1666 ConstructedInterpolants, 0 QuantifiedInterpolants, 2706 SizeOfPredicates, 16 NumberOfNonLiveVariables, 4983 ConjunctsInSsa, 112 ConjunctsInUnsatCore, 18 InterpolantComputations, 13 PerfectInterpolantSequences, 149/193 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:45,493 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
