./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_1.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:59,984 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:00,029 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d4c736ac-4057-4286-a6aa-8b342bc58f94/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:00,032 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:00,032 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:00,045 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:00,046 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:00,046 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:00,046 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:00,046 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:00,046 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:00,046 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:00,046 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:00,046 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:00,046 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:00,047 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:00,047 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:00,047 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:00,048 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:00,048 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:00,227 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:00,233 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:00,234 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:00,235 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:00,236 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:00,237 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d4c736ac-4057-4286-a6aa-8b342bc58f94/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_1.sol_0_no_adts_000.smt2
[2025-05-07 17:28:00,238 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:00,240 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:00,500 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d4c736ac-4057-4286-a6aa-8b342bc58f94/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_1.sol_0_no_adts_000.smt2
[2025-05-07 17:28:00,503 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:00,504 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:00,504 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:00,504 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:00,505 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:00,506 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,541 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00 Unit
[2025-05-07 17:28:00,541 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:00,541 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:00,542 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:00,542 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:00,553 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,553 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,577 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,577 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,584 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,586 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,588 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,593 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,595 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,612 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:00,612 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:00,612 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:00,612 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:00,613 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (1/1) ...
[2025-05-07 17:28:00,615 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:00,624 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:00,633 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:00,635 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:00,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:00,643 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:00,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:00,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_6_0 given in one single declaration
[2025-05-07 17:28:00,643 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_6_0
[2025-05-07 17:28:00,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_6_0
[2025-05-07 17:28:00,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_g__28_29_0 given in one single declaration
[2025-05-07 17:28:00,643 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_g__28_29_0
[2025-05-07 17:28:00,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_g__28_29_0
[2025-05-07 17:28:00,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_g__28_29_0 given in one single declaration
[2025-05-07 17:28:00,643 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_g__28_29_0
[2025-05-07 17:28:00,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_g__28_29_0 given in one single declaration
[2025-05-07 17:28:00,644 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_28_return_function_g__28_29_0 given in one single declaration
[2025-05-07 17:28:00,644 INFO  L130     BoogieDeclarations]: Found specification of procedure block_28_return_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_28_return_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_27_g_27_29_0 given in one single declaration
[2025-05-07 17:28:00,644 INFO  L130     BoogieDeclarations]: Found specification of procedure block_27_g_27_29_0
[2025-05-07 17:28:00,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_27_g_27_29_0
[2025-05-07 17:28:00,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_function_g__28_29_0 given in one single declaration
[2025-05-07 17:28:00,644 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_function_g__28_29_0
[2025-05-07 17:28:00,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_29_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,644 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_29_function_f__12_29_0
[2025-05-07 17:28:00,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_29_function_f__12_29_0
[2025-05-07 17:28:00,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_8_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,644 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_8_function_f__12_29_0
[2025-05-07 17:28:00,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_8_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_return_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_return_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_return_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_f_11_29_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_f_11_29_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_f_11_29_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_f__12_29_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_B_13_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_B_13_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_B_13_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_B_13_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_B_13_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_B_13_0
[2025-05-07 17:28:00,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_20_B_13_0 given in one single declaration
[2025-05-07 17:28:00,645 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_20_B_13_0
[2025-05-07 17:28:00,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_20_B_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_17_B_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_17_B_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_17_B_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_19_B_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_19_B_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_19_B_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_18_B_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_18_B_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_18_B_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__12_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__12_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__12_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__12_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__12_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__12_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_return_function_f__12_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_return_function_f__12_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_return_function_f__12_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_f_11_13_0 given in one single declaration
[2025-05-07 17:28:00,646 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_f_11_13_0
[2025-05-07 17:28:00,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_f_11_13_0
[2025-05-07 17:28:00,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__12_13_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__12_13_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__12_13_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__12_13_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__12_13_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__12_13_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_f__12_13_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_f__12_13_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_f__12_13_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_5_C_29_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_5_C_29_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_5_C_29_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_7_C_29_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_7_C_29_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_7_C_29_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_31_C_29_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_31_C_29_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_31_C_29_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_33_C_29_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_33_C_29_0
[2025-05-07 17:28:00,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_33_C_29_0
[2025-05-07 17:28:00,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_32_C_29_0 given in one single declaration
[2025-05-07 17:28:00,647 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_32_C_29_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_32_C_29_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_34_B_13_0 given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_34_B_13_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_34_B_13_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_36_B_13_0 given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_36_B_13_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_36_B_13_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_35_B_13_0 given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_35_B_13_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_35_B_13_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_37_C_29_0 given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_37_C_29_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_37_C_29_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_f__12_29_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_f__12_29_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_function_f__12_29_0 given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_function_f__12_29_0
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_function_f__12_29_0
[2025-05-07 17:28:00,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:00,648 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:00,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:00,827 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:00,829 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:01,095 INFO  L?                        ?]: Removed 329 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:01,095 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:01,104 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:01,104 INFO  L312             CfgBuilder]: Removed 19 assume(true) statements.
[2025-05-07 17:28:01,104 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:01 BoogieIcfgContainer
[2025-05-07 17:28:01,104 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:01,105 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:01,106 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:01,108 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:01,108 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:00" (1/3) ...
[2025-05-07 17:28:01,109 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6a588bcd and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:01, skipping insertion in model container
[2025-05-07 17:28:01,109 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:00" (2/3) ...
[2025-05-07 17:28:01,109 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6a588bcd and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:01, skipping insertion in model container
[2025-05-07 17:28:01,109 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:01" (3/3) ...
[2025-05-07 17:28:01,110 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:01,120 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:01,122 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 39 procedures, 156 locations, 242 edges, 39 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:01,153 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:01,162 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;@2a69f539, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:01,162 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:01,165 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 156 states, 62 states have (on average 1.1451612903225807) internal successors, (71), 71 states have internal predecessors, (71), 55 states have call successors, (57), 38 states have call predecessors, (57), 38 states have return successors, (57), 46 states have call predecessors, (57), 55 states have call successors, (57)
[2025-05-07 17:28:01,173 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:01,173 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:01,173 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:01,174 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:01,177 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:01,178 INFO  L85        PathProgramCache]: Analyzing trace with hash -1784394038, now seen corresponding path program 1 times
[2025-05-07 17:28:01,183 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:01,184 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [405376991]
[2025-05-07 17:28:01,184 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:01,184 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:01,221 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:01,276 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:01,276 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:01,276 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:01,536 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:01,536 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:01,536 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [405376991]
[2025-05-07 17:28:01,537 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [405376991] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:01,537 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:01,539 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:01,540 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1479195185]
[2025-05-07 17:28:01,541 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:01,544 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:01,544 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:01,563 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:01,563 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:01,565 INFO  L87              Difference]: Start difference. First operand  has 156 states, 62 states have (on average 1.1451612903225807) internal successors, (71), 71 states have internal predecessors, (71), 55 states have call successors, (57), 38 states have call predecessors, (57), 38 states have return successors, (57), 46 states have call predecessors, (57), 55 states have call successors, (57) Second operand  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 5 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 6 states have call predecessors, (14), 5 states have call successors, (14)
[2025-05-07 17:28:01,689 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:01,690 INFO  L93              Difference]: Finished difference Result 158 states and 187 transitions.
[2025-05-07 17:28:01,691 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:01,693 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 5 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 6 states have call predecessors, (14), 5 states have call successors, (14) Word has length 51
[2025-05-07 17:28:01,693 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:01,702 INFO  L225             Difference]: With dead ends: 158
[2025-05-07 17:28:01,702 INFO  L226             Difference]: Without dead ends: 158
[2025-05-07 17:28:01,703 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:01,705 INFO  L437           NwaCegarLoop]: 179 mSDtfsCounter, 2 mSDsluCounter, 1050 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1229 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:01,706 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1229 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:01,715 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-05-07 17:28:01,735 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 158.
[2025-05-07 17:28:01,736 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 63 states have (on average 1.126984126984127) internal successors, (71), 71 states have internal predecessors, (71), 55 states have call successors, (57), 38 states have call predecessors, (57), 40 states have return successors, (59), 48 states have call predecessors, (59), 55 states have call successors, (59)
[2025-05-07 17:28:01,740 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 187 transitions.
[2025-05-07 17:28:01,741 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 187 transitions. Word has length 51
[2025-05-07 17:28:01,741 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:01,741 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 187 transitions.
[2025-05-07 17:28:01,742 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 5 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 6 states have call predecessors, (14), 5 states have call successors, (14)
[2025-05-07 17:28:01,742 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 187 transitions.
[2025-05-07 17:28:01,744 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:01,744 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:01,744 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:01,744 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:01,744 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:01,745 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:01,745 INFO  L85        PathProgramCache]: Analyzing trace with hash 261300508, now seen corresponding path program 1 times
[2025-05-07 17:28:01,745 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:01,745 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1532712957]
[2025-05-07 17:28:01,745 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:01,745 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:01,770 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:01,785 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:01,786 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:01,786 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:01,876 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:01,876 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:01,876 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1532712957]
[2025-05-07 17:28:01,876 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1532712957] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:01,876 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:01,876 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:01,877 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1144701921]
[2025-05-07 17:28:01,877 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:01,877 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:01,878 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:01,878 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:01,878 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:01,878 INFO  L87              Difference]: Start difference. First operand 158 states and 187 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:01,892 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:01,892 INFO  L93              Difference]: Finished difference Result 162 states and 191 transitions.
[2025-05-07 17:28:01,893 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:01,893 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:01,893 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:01,895 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:28:01,895 INFO  L226             Difference]: Without dead ends: 158
[2025-05-07 17:28:01,895 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:01,895 INFO  L437           NwaCegarLoop]: 183 mSDtfsCounter, 1 mSDsluCounter, 359 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 542 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:01,896 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 542 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:01,896 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-05-07 17:28:01,903 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 156.
[2025-05-07 17:28:01,903 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 63 states have (on average 1.1111111111111112) internal successors, (70), 70 states have internal predecessors, (70), 53 states have call successors, (55), 38 states have call predecessors, (55), 40 states have return successors, (57), 47 states have call predecessors, (57), 53 states have call successors, (57)
[2025-05-07 17:28:01,904 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 182 transitions.
[2025-05-07 17:28:01,904 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 182 transitions. Word has length 51
[2025-05-07 17:28:01,904 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:01,904 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 182 transitions.
[2025-05-07 17:28:01,905 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:01,905 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 182 transitions.
[2025-05-07 17:28:01,906 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:01,906 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:01,906 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:01,906 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:01,906 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:01,906 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:01,907 INFO  L85        PathProgramCache]: Analyzing trace with hash -467829856, now seen corresponding path program 1 times
[2025-05-07 17:28:01,907 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:01,907 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1419673412]
[2025-05-07 17:28:01,907 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:01,907 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:01,927 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:01,937 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:01,937 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:01,937 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:02,247 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:02,248 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:02,248 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1419673412]
[2025-05-07 17:28:02,248 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1419673412] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:02,248 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:02,248 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [] total 16
[2025-05-07 17:28:02,248 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1509308508]
[2025-05-07 17:28:02,248 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:02,249 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:28:02,249 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:02,249 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:28:02,249 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=211, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:28:02,250 INFO  L87              Difference]: Start difference. First operand 156 states and 182 transitions. Second operand  has 16 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 14 states have internal predecessors, (23), 6 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (14), 12 states have call predecessors, (14), 6 states have call successors, (14)
[2025-05-07 17:28:02,464 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:02,464 INFO  L93              Difference]: Finished difference Result 160 states and 186 transitions.
[2025-05-07 17:28:02,464 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:28:02,465 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 14 states have internal predecessors, (23), 6 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (14), 12 states have call predecessors, (14), 6 states have call successors, (14) Word has length 51
[2025-05-07 17:28:02,465 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:02,466 INFO  L225             Difference]: With dead ends: 160
[2025-05-07 17:28:02,466 INFO  L226             Difference]: Without dead ends: 160
[2025-05-07 17:28:02,466 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-05-07 17:28:02,467 INFO  L437           NwaCegarLoop]: 168 mSDtfsCounter, 5 mSDsluCounter, 2314 mSDsCounter, 0 mSdLazyCounter, 188 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 2482 SdHoareTripleChecker+Invalid, 188 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 188 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:02,467 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 2482 Invalid, 188 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 188 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:28:02,468 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 160 states.
[2025-05-07 17:28:02,474 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 160 to 158.
[2025-05-07 17:28:02,474 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 64 states have (on average 1.109375) internal successors, (71), 71 states have internal predecessors, (71), 53 states have call successors, (55), 38 states have call predecessors, (55), 41 states have return successors, (58), 48 states have call predecessors, (58), 53 states have call successors, (58)
[2025-05-07 17:28:02,475 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 184 transitions.
[2025-05-07 17:28:02,475 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 184 transitions. Word has length 51
[2025-05-07 17:28:02,476 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:02,476 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 184 transitions.
[2025-05-07 17:28:02,476 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 14 states have internal predecessors, (23), 6 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (14), 12 states have call predecessors, (14), 6 states have call successors, (14)
[2025-05-07 17:28:02,476 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 184 transitions.
[2025-05-07 17:28:02,477 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:28:02,477 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:02,477 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]
[2025-05-07 17:28:02,478 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:02,478 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:02,478 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:02,478 INFO  L85        PathProgramCache]: Analyzing trace with hash 185468445, now seen corresponding path program 1 times
[2025-05-07 17:28:02,478 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:02,478 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1942890200]
[2025-05-07 17:28:02,478 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,478 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:02,498 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:28:02,508 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:28:02,508 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:02,508 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:02,569 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:02,569 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:02,569 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1942890200]
[2025-05-07 17:28:02,569 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1942890200] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:02,569 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:02,569 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:02,569 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1243080518]
[2025-05-07 17:28:02,569 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:02,569 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:02,570 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:02,570 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:02,570 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:02,570 INFO  L87              Difference]: Start difference. First operand 158 states and 184 transitions. Second operand  has 4 states, 3 states have (on average 9.666666666666666) internal successors, (29), 4 states have internal predecessors, (29), 3 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:28:02,578 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:02,578 INFO  L93              Difference]: Finished difference Result 162 states and 190 transitions.
[2025-05-07 17:28:02,579 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:02,579 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.666666666666666) internal successors, (29), 4 states have internal predecessors, (29), 3 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 3 states have call successors, (18) Word has length 65
[2025-05-07 17:28:02,579 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:02,580 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:28:02,580 INFO  L226             Difference]: Without dead ends: 155
[2025-05-07 17:28:02,580 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:02,581 INFO  L437           NwaCegarLoop]: 178 mSDtfsCounter, 1 mSDsluCounter, 345 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 523 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:02,581 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 523 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:02,581 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 155 states.
[2025-05-07 17:28:02,587 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 155 to 153.
[2025-05-07 17:28:02,587 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 153 states, 64 states have (on average 1.078125) internal successors, (69), 69 states have internal predecessors, (69), 48 states have call successors, (50), 38 states have call predecessors, (50), 41 states have return successors, (53), 45 states have call predecessors, (53), 48 states have call successors, (53)
[2025-05-07 17:28:02,588 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 153 states to 153 states and 172 transitions.
[2025-05-07 17:28:02,588 INFO  L79                 Accepts]: Start accepts. Automaton has 153 states and 172 transitions. Word has length 65
[2025-05-07 17:28:02,588 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:02,588 INFO  L485      AbstractCegarLoop]: Abstraction has 153 states and 172 transitions.
[2025-05-07 17:28:02,588 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.666666666666666) internal successors, (29), 4 states have internal predecessors, (29), 3 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:28:02,588 INFO  L278                IsEmpty]: Start isEmpty. Operand 153 states and 172 transitions.
[2025-05-07 17:28:02,589 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:28:02,589 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:02,590 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]
[2025-05-07 17:28:02,590 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:02,590 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:02,590 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:02,590 INFO  L85        PathProgramCache]: Analyzing trace with hash -1130956213, now seen corresponding path program 1 times
[2025-05-07 17:28:02,590 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:02,590 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [974119541]
[2025-05-07 17:28:02,590 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,590 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:02,612 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:02,622 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:02,622 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:02,622 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:03,062 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-05-07 17:28:03,063 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:03,063 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [974119541]
[2025-05-07 17:28:03,063 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [974119541] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:03,063 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1164396148]
[2025-05-07 17:28:03,063 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:03,063 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:03,066 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:03,068 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:03,069 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:28:03,291 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:28:03,400 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:28:03,400 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:03,400 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:03,404 INFO  L256         TraceCheckSpWp]: Trace formula consists of 987 conjuncts, 64 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:03,411 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:03,505 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-05-07 17:28:03,505 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:04,788 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 3 proven. 6 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:28:04,788 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1164396148] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:04,788 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:04,788 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [20, 20, 22] total 33
[2025-05-07 17:28:04,789 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [220621578]
[2025-05-07 17:28:04,789 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:04,790 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-05-07 17:28:04,790 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,791 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-05-07 17:28:04,791 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=86, Invalid=970, Unknown=0, NotChecked=0, Total=1056
[2025-05-07 17:28:04,792 INFO  L87              Difference]: Start difference. First operand 153 states and 172 transitions. Second operand  has 33 states, 23 states have (on average 1.826086956521739) internal successors, (42), 28 states have internal predecessors, (42), 14 states have call successors, (27), 1 states have call predecessors, (27), 23 states have return successors, (34), 27 states have call predecessors, (34), 14 states have call successors, (34)
[2025-05-07 17:28:05,033 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,033 INFO  L93              Difference]: Finished difference Result 154 states and 174 transitions.
[2025-05-07 17:28:05,033 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-05-07 17:28:05,033 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 23 states have (on average 1.826086956521739) internal successors, (42), 28 states have internal predecessors, (42), 14 states have call successors, (27), 1 states have call predecessors, (27), 23 states have return successors, (34), 27 states have call predecessors, (34), 14 states have call successors, (34) Word has length 76
[2025-05-07 17:28:05,033 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,034 INFO  L225             Difference]: With dead ends: 154
[2025-05-07 17:28:05,034 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:28:05,035 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 179 GetRequests, 143 SyntacticMatches, 0 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 91 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=115, Invalid=1291, Unknown=0, NotChecked=0, Total=1406
[2025-05-07 17:28:05,035 INFO  L437           NwaCegarLoop]: 156 mSDtfsCounter, 5 mSDsluCounter, 2717 mSDsCounter, 0 mSdLazyCounter, 343 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 2873 SdHoareTripleChecker+Invalid, 344 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 343 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:05,036 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 2873 Invalid, 344 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 343 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:28:05,036 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:28:05,041 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:28:05,042 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 40 states have (on average 1.075) internal successors, (43), 43 states have internal predecessors, (43), 33 states have call successors, (34), 25 states have call predecessors, (34), 25 states have return successors, (34), 29 states have call predecessors, (34), 33 states have call successors, (34)
[2025-05-07 17:28:05,042 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 111 transitions.
[2025-05-07 17:28:05,043 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 111 transitions. Word has length 76
[2025-05-07 17:28:05,043 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,043 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 111 transitions.
[2025-05-07 17:28:05,043 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 23 states have (on average 1.826086956521739) internal successors, (42), 28 states have internal predecessors, (42), 14 states have call successors, (27), 1 states have call predecessors, (27), 23 states have return successors, (34), 27 states have call predecessors, (34), 14 states have call successors, (34)
[2025-05-07 17:28:05,043 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 111 transitions.
[2025-05-07 17:28:05,044 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 62
[2025-05-07 17:28:05,044 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,044 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]
[2025-05-07 17:28:05,051 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:28:05,245 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-05-07 17:28:05,246 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,247 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,248 INFO  L85        PathProgramCache]: Analyzing trace with hash -1464617341, now seen corresponding path program 1 times
[2025-05-07 17:28:05,248 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,248 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [121483414]
[2025-05-07 17:28:05,249 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,249 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,307 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-05-07 17:28:05,317 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-05-07 17:28:05,317 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,317 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,674 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:05,674 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:05,674 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [121483414]
[2025-05-07 17:28:05,674 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [121483414] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,674 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:05,674 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [20] imperfect sequences [] total 20
[2025-05-07 17:28:05,674 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1360432541]
[2025-05-07 17:28:05,674 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,675 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-05-07 17:28:05,675 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,675 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-05-07 17:28:05,676 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=342, Unknown=0, NotChecked=0, Total=380
[2025-05-07 17:28:05,676 INFO  L87              Difference]: Start difference. First operand 98 states and 111 transitions. Second operand  has 20 states, 15 states have (on average 1.8) internal successors, (27), 17 states have internal predecessors, (27), 8 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (17), 14 states have call predecessors, (17), 8 states have call successors, (17)
[2025-05-07 17:28:05,958 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,958 INFO  L93              Difference]: Finished difference Result 108 states and 128 transitions.
[2025-05-07 17:28:05,958 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-05-07 17:28:05,958 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 15 states have (on average 1.8) internal successors, (27), 17 states have internal predecessors, (27), 8 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (17), 14 states have call predecessors, (17), 8 states have call successors, (17) Word has length 61
[2025-05-07 17:28:05,959 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,959 INFO  L225             Difference]: With dead ends: 108
[2025-05-07 17:28:05,959 INFO  L226             Difference]: Without dead ends: 108
[2025-05-07 17:28:05,960 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 23 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=51, Invalid=455, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:28:05,960 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 4 mSDsluCounter, 1779 mSDsCounter, 0 mSdLazyCounter, 409 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1881 SdHoareTripleChecker+Invalid, 409 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 409 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:05,960 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1881 Invalid, 409 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 409 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:28:05,961 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 108 states.
[2025-05-07 17:28:05,965 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 108 to 106.
[2025-05-07 17:28:05,965 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 43 states have (on average 1.069767441860465) internal successors, (46), 46 states have internal predecessors, (46), 35 states have call successors, (36), 25 states have call predecessors, (36), 28 states have return successors, (44), 34 states have call predecessors, (44), 35 states have call successors, (44)
[2025-05-07 17:28:05,966 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 126 transitions.
[2025-05-07 17:28:05,966 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 126 transitions. Word has length 61
[2025-05-07 17:28:05,966 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,966 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 126 transitions.
[2025-05-07 17:28:05,966 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 15 states have (on average 1.8) internal successors, (27), 17 states have internal predecessors, (27), 8 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (17), 14 states have call predecessors, (17), 8 states have call successors, (17)
[2025-05-07 17:28:05,967 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 126 transitions.
[2025-05-07 17:28:05,967 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 62
[2025-05-07 17:28:05,967 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,967 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]
[2025-05-07 17:28:05,967 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:05,967 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,968 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,968 INFO  L85        PathProgramCache]: Analyzing trace with hash 1317751553, now seen corresponding path program 1 times
[2025-05-07 17:28:05,968 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,968 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2130470076]
[2025-05-07 17:28:05,968 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,968 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,988 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-05-07 17:28:05,998 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-05-07 17:28:05,998 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,998 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,073 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:06,073 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,073 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2130470076]
[2025-05-07 17:28:06,073 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2130470076] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,073 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,073 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:06,073 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1085437131]
[2025-05-07 17:28:06,073 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,073 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:06,073 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,074 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:06,074 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:06,074 INFO  L87              Difference]: Start difference. First operand 106 states and 126 transitions. Second operand  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 6 states have call successors, (17), 1 states have call predecessors, (17), 6 states have return successors, (17), 6 states have call predecessors, (17), 6 states have call successors, (17)
[2025-05-07 17:28:06,131 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,131 INFO  L93              Difference]: Finished difference Result 105 states and 122 transitions.
[2025-05-07 17:28:06,132 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:06,132 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 6 states have call successors, (17), 1 states have call predecessors, (17), 6 states have return successors, (17), 6 states have call predecessors, (17), 6 states have call successors, (17) Word has length 61
[2025-05-07 17:28:06,132 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,133 INFO  L225             Difference]: With dead ends: 105
[2025-05-07 17:28:06,133 INFO  L226             Difference]: Without dead ends: 105
[2025-05-07 17:28:06,133 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:06,133 INFO  L437           NwaCegarLoop]: 105 mSDtfsCounter, 2 mSDsluCounter, 609 mSDsCounter, 0 mSdLazyCounter, 47 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 714 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 47 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:06,133 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 714 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 47 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:06,134 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 105 states.
[2025-05-07 17:28:06,137 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 105 to 105.
[2025-05-07 17:28:06,137 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 43 states have (on average 1.069767441860465) internal successors, (46), 46 states have internal predecessors, (46), 34 states have call successors, (35), 25 states have call predecessors, (35), 28 states have return successors, (41), 33 states have call predecessors, (41), 34 states have call successors, (41)
[2025-05-07 17:28:06,138 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 122 transitions.
[2025-05-07 17:28:06,138 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 122 transitions. Word has length 61
[2025-05-07 17:28:06,138 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,138 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 122 transitions.
[2025-05-07 17:28:06,138 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 6 states have call successors, (17), 1 states have call predecessors, (17), 6 states have return successors, (17), 6 states have call predecessors, (17), 6 states have call successors, (17)
[2025-05-07 17:28:06,138 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 122 transitions.
[2025-05-07 17:28:06,139 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:28:06,139 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,139 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]
[2025-05-07 17:28:06,139 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:06,139 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,139 INFO  L85        PathProgramCache]: Analyzing trace with hash -139114745, now seen corresponding path program 1 times
[2025-05-07 17:28:06,139 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,139 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [203169519]
[2025-05-07 17:28:06,139 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,140 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,161 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:28:06,169 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:28:06,169 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,169 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,248 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:06,248 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,248 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [203169519]
[2025-05-07 17:28:06,248 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [203169519] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,248 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,248 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:06,248 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1408284643]
[2025-05-07 17:28:06,248 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,249 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:06,249 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,249 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:06,249 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:06,250 INFO  L87              Difference]: Start difference. First operand 105 states and 122 transitions. Second operand  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 6 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (21), 7 states have call predecessors, (21), 6 states have call successors, (21)
[2025-05-07 17:28:06,316 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,317 INFO  L93              Difference]: Finished difference Result 113 states and 133 transitions.
[2025-05-07 17:28:06,317 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:06,317 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 6 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (21), 7 states have call predecessors, (21), 6 states have call successors, (21) Word has length 75
[2025-05-07 17:28:06,317 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,318 INFO  L225             Difference]: With dead ends: 113
[2025-05-07 17:28:06,318 INFO  L226             Difference]: Without dead ends: 113
[2025-05-07 17:28:06,318 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:06,318 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 1 mSDsluCounter, 677 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 794 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:06,319 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 794 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:06,319 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-05-07 17:28:06,322 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 113.
[2025-05-07 17:28:06,322 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 46 states have (on average 1.065217391304348) internal successors, (49), 49 states have internal predecessors, (49), 36 states have call successors, (37), 25 states have call predecessors, (37), 31 states have return successors, (47), 38 states have call predecessors, (47), 36 states have call successors, (47)
[2025-05-07 17:28:06,323 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 133 transitions.
[2025-05-07 17:28:06,323 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 133 transitions. Word has length 75
[2025-05-07 17:28:06,323 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,323 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 133 transitions.
[2025-05-07 17:28:06,323 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 6 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (21), 7 states have call predecessors, (21), 6 states have call successors, (21)
[2025-05-07 17:28:06,323 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 133 transitions.
[2025-05-07 17:28:06,324 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:28:06,324 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,324 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]
[2025-05-07 17:28:06,324 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:06,324 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,324 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,324 INFO  L85        PathProgramCache]: Analyzing trace with hash -1836542007, now seen corresponding path program 1 times
[2025-05-07 17:28:06,324 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,324 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [827704776]
[2025-05-07 17:28:06,324 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,324 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,347 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:28:06,355 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:28:06,355 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,356 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,439 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:06,440 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,440 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [827704776]
[2025-05-07 17:28:06,440 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [827704776] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,440 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,440 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:06,440 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2113412056]
[2025-05-07 17:28:06,440 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,440 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:06,440 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,441 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:06,441 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:06,441 INFO  L87              Difference]: Start difference. First operand 113 states and 133 transitions. Second operand  has 8 states, 6 states have (on average 5.5) internal successors, (33), 8 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 6 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:28:06,515 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,516 INFO  L93              Difference]: Finished difference Result 112 states and 130 transitions.
[2025-05-07 17:28:06,516 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:06,516 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 5.5) internal successors, (33), 8 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 6 states have call predecessors, (21), 5 states have call successors, (21) Word has length 75
[2025-05-07 17:28:06,516 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,517 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:28:06,517 INFO  L226             Difference]: Without dead ends: 112
[2025-05-07 17:28:06,517 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:06,517 INFO  L437           NwaCegarLoop]: 104 mSDtfsCounter, 2 mSDsluCounter, 606 mSDsCounter, 0 mSdLazyCounter, 55 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 710 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 55 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:06,517 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 710 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 55 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:06,518 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-05-07 17:28:06,520 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 112.
[2025-05-07 17:28:06,520 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 112 states, 46 states have (on average 1.065217391304348) internal successors, (49), 49 states have internal predecessors, (49), 35 states have call successors, (36), 25 states have call predecessors, (36), 31 states have return successors, (45), 37 states have call predecessors, (45), 35 states have call successors, (45)
[2025-05-07 17:28:06,521 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 112 states to 112 states and 130 transitions.
[2025-05-07 17:28:06,521 INFO  L79                 Accepts]: Start accepts. Automaton has 112 states and 130 transitions. Word has length 75
[2025-05-07 17:28:06,521 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,521 INFO  L485      AbstractCegarLoop]: Abstraction has 112 states and 130 transitions.
[2025-05-07 17:28:06,521 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 5.5) internal successors, (33), 8 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 6 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:28:06,521 INFO  L278                IsEmpty]: Start isEmpty. Operand 112 states and 130 transitions.
[2025-05-07 17:28:06,522 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 79
[2025-05-07 17:28:06,522 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,522 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]
[2025-05-07 17:28:06,522 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:06,522 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,522 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,522 INFO  L85        PathProgramCache]: Analyzing trace with hash 1881416237, now seen corresponding path program 1 times
[2025-05-07 17:28:06,522 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,522 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [203694645]
[2025-05-07 17:28:06,523 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,523 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,548 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 78 statements into 1 equivalence classes.
[2025-05-07 17:28:06,555 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 78 of 78 statements.
[2025-05-07 17:28:06,555 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,555 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,612 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:06,612 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,612 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [203694645]
[2025-05-07 17:28:06,612 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [203694645] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,612 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,612 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:06,612 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [266555270]
[2025-05-07 17:28:06,612 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,613 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:06,613 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,613 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:06,613 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:06,613 INFO  L87              Difference]: Start difference. First operand 112 states and 130 transitions. Second operand  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 5 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:28:06,644 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,644 INFO  L93              Difference]: Finished difference Result 111 states and 126 transitions.
[2025-05-07 17:28:06,644 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:06,644 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 5 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 5 states have call successors, (22) Word has length 78
[2025-05-07 17:28:06,644 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,645 INFO  L225             Difference]: With dead ends: 111
[2025-05-07 17:28:06,645 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:28:06,645 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:06,645 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 423 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 533 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:06,645 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 533 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:06,646 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:28:06,648 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 105.
[2025-05-07 17:28:06,648 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 44 states have (on average 1.0454545454545454) internal successors, (46), 46 states have internal predecessors, (46), 32 states have call successors, (33), 25 states have call predecessors, (33), 29 states have return successors, (39), 33 states have call predecessors, (39), 32 states have call successors, (39)
[2025-05-07 17:28:06,649 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 118 transitions.
[2025-05-07 17:28:06,649 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 118 transitions. Word has length 78
[2025-05-07 17:28:06,649 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,649 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 118 transitions.
[2025-05-07 17:28:06,649 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 5 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (22), 5 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:28:06,649 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 118 transitions.
[2025-05-07 17:28:06,650 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 101
[2025-05-07 17:28:06,650 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,650 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:06,650 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:06,650 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,650 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,650 INFO  L85        PathProgramCache]: Analyzing trace with hash 11404589, now seen corresponding path program 1 times
[2025-05-07 17:28:06,650 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,650 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2054454526]
[2025-05-07 17:28:06,650 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,650 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,682 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 100 statements into 1 equivalence classes.
[2025-05-07 17:28:06,687 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 100 of 100 statements.
[2025-05-07 17:28:06,687 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,687 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,828 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:28:06,828 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,828 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2054454526]
[2025-05-07 17:28:06,828 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2054454526] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,829 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,829 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:06,829 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [104295401]
[2025-05-07 17:28:06,829 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,829 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:06,829 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,830 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:06,830 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:06,830 INFO  L87              Difference]: Start difference. First operand 105 states and 118 transitions. Second operand  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 6 states have call successors, (25), 1 states have call predecessors, (25), 5 states have return successors, (25), 5 states have call predecessors, (25), 6 states have call successors, (25)
[2025-05-07 17:28:06,863 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,863 INFO  L93              Difference]: Finished difference Result 110 states and 123 transitions.
[2025-05-07 17:28:06,863 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:06,863 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 6 states have call successors, (25), 1 states have call predecessors, (25), 5 states have return successors, (25), 5 states have call predecessors, (25), 6 states have call successors, (25) Word has length 100
[2025-05-07 17:28:06,864 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,864 INFO  L225             Difference]: With dead ends: 110
[2025-05-07 17:28:06,864 INFO  L226             Difference]: Without dead ends: 103
[2025-05-07 17:28:06,865 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 4 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:06,865 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 418 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 528 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:06,865 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 528 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:06,866 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 103 states.
[2025-05-07 17:28:06,868 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 103 to 101.
[2025-05-07 17:28:06,869 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 101 states, 42 states have (on average 1.0476190476190477) internal successors, (44), 44 states have internal predecessors, (44), 30 states have call successors, (31), 25 states have call predecessors, (31), 28 states have return successors, (36), 31 states have call predecessors, (36), 30 states have call successors, (36)
[2025-05-07 17:28:06,869 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 101 states to 101 states and 111 transitions.
[2025-05-07 17:28:06,869 INFO  L79                 Accepts]: Start accepts. Automaton has 101 states and 111 transitions. Word has length 100
[2025-05-07 17:28:06,869 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,869 INFO  L485      AbstractCegarLoop]: Abstraction has 101 states and 111 transitions.
[2025-05-07 17:28:06,870 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 6 states have call successors, (25), 1 states have call predecessors, (25), 5 states have return successors, (25), 5 states have call predecessors, (25), 6 states have call successors, (25)
[2025-05-07 17:28:06,870 INFO  L278                IsEmpty]: Start isEmpty. Operand 101 states and 111 transitions.
[2025-05-07 17:28:06,870 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:28:06,870 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,870 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]
[2025-05-07 17:28:06,870 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:06,871 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,871 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,871 INFO  L85        PathProgramCache]: Analyzing trace with hash 1864156137, now seen corresponding path program 1 times
[2025-05-07 17:28:06,871 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,871 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2081523128]
[2025-05-07 17:28:06,871 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,871 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,907 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:28:06,920 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:28:06,920 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,920 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,427 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:28:07,427 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:07,427 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2081523128]
[2025-05-07 17:28:07,427 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2081523128] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:07,427 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1217808091]
[2025-05-07 17:28:07,427 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,427 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:07,429 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:07,430 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:07,431 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:28:07,717 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:28:07,817 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:28:07,817 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:07,817 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,820 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1218 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:07,823 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:07,890 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 16 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:28:07,890 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:07,890 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1217808091] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:07,890 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:07,890 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [24] total 28
[2025-05-07 17:28:07,890 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [952629618]
[2025-05-07 17:28:07,891 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:07,892 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:07,892 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:07,893 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:07,893 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=702, Unknown=0, NotChecked=0, Total=756
[2025-05-07 17:28:07,893 INFO  L87              Difference]: Start difference. First operand 101 states and 111 transitions. Second operand  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 5 states have call successors, (24), 2 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 5 states have call successors, (24)
[2025-05-07 17:28:07,906 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,906 INFO  L93              Difference]: Finished difference Result 33 states and 34 transitions.
[2025-05-07 17:28:07,906 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:07,906 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), 5 states have call successors, (24), 2 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 5 states have call successors, (24) Word has length 86
[2025-05-07 17:28:07,907 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,907 INFO  L225             Difference]: With dead ends: 33
[2025-05-07 17:28:07,907 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:07,907 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 112 GetRequests, 86 SyntacticMatches, 0 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=54, Invalid=702, Unknown=0, NotChecked=0, Total=756
[2025-05-07 17:28:07,907 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 0 mSDsluCounter, 102 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 129 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:07,907 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 129 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:07,908 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:07,908 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:07,908 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:07,908 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:07,908 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 86
[2025-05-07 17:28:07,908 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,908 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:07,908 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), 5 states have call successors, (24), 2 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 5 states have call successors, (24)
[2025-05-07 17:28:07,908 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:07,908 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:07,910 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:07,916 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:28:08,110 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:08,122 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:08,128 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:08,135 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:08 BoogieIcfgContainer
[2025-05-07 17:28:08,135 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:08,137 INFO  L158              Benchmark]: Toolchain (without parser) took 7631.94ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 141.0MB in the beginning and 153.2MB in the end (delta: -12.2MB). Peak memory consumption was 52.4MB. Max. memory is 33.6GB.
[2025-05-07 17:28:08,137 INFO  L158              Benchmark]: SmtParser took 0.23ms. Allocated memory is still 234.9MB. Free memory is still 171.8MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:08,138 INFO  L158              Benchmark]: ChcToBoogie took 36.82ms. Allocated memory is still 234.9MB. Free memory was 141.0MB in the beginning and 137.2MB in the end (delta: 3.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:08,138 INFO  L158              Benchmark]: Boogie Preprocessor took 70.21ms. Allocated memory is still 234.9MB. Free memory was 137.2MB in the beginning and 133.4MB in the end (delta: 3.8MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:08,139 INFO  L158              Benchmark]: RCFGBuilder took 492.05ms. Allocated memory is still 234.9MB. Free memory was 133.4MB in the beginning and 153.5MB in the end (delta: -20.1MB). Peak memory consumption was 26.9MB. Max. memory is 33.6GB.
[2025-05-07 17:28:08,140 INFO  L158              Benchmark]: TraceAbstraction took 7029.55ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 152.9MB in the beginning and 153.2MB in the end (delta: -265.2kB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
[2025-05-07 17:28:08,142 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.23ms. Allocated memory is still 234.9MB. Free memory is still 171.8MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 36.82ms. Allocated memory is still 234.9MB. Free memory was 141.0MB in the beginning and 137.2MB in the end (delta: 3.8MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 70.21ms. Allocated memory is still 234.9MB. Free memory was 137.2MB in the beginning and 133.4MB in the end (delta: 3.8MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 492.05ms. Allocated memory is still 234.9MB. Free memory was 133.4MB in the beginning and 153.5MB in the end (delta: -20.1MB). Peak memory consumption was 26.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 7029.55ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 152.9MB in the beginning and 153.2MB in the end (delta: -265.2kB). Peak memory consumption was 42.3MB. 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 39 procedures, 156 locations, 242 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 7.0s, OverallIterations: 12, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.2s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 71 SdHoareTripleChecker+Valid, 0.9s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 25 mSDsluCounter, 12938 SdHoareTripleChecker+Invalid, 0.8s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 11399 mSDsCounter, 8 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1186 IncrementalHoareTripleChecker+Invalid, 1194 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 8 mSolverCounterUnsat, 1539 mSDtfsCounter, 1186 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 390 GetRequests, 251 SyntacticMatches, 0 SemanticMatches, 139 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 113 ImplicationChecksByTransitivity, 1.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=158occurred in iteration=1, InterpolantAutomatonStates: 116, 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, 12 MinimizatonAttempts, 15 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.2s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 3.9s InterpolantComputationTime, 992 NumberOfCodeBlocks, 992 NumberOfCodeBlocksAsserted, 14 NumberOfCheckSat, 1053 ConstructedInterpolants, 0 QuantifiedInterpolants, 1875 SizeOfPredicates, 5 NumberOfNonLiveVariables, 2205 ConjunctsInSsa, 69 ConjunctsInUnsatCore, 15 InterpolantComputations, 11 PerfectInterpolantSequences, 92/111 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:08,174 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
