./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/modifiers/modifier_overriding_4.sol_9_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:46,075 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:46,111 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e3d90e32-6d8a-484e-a38e-b561abfc59b3/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:46,114 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:46,114 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:46,126 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:46,126 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:46,127 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:46,127 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:46,127 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:46,127 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:46,127 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:46,127 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:46,127 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:46,127 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:46,127 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:46,127 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:46,128 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:46,128 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:46,128 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:46,308 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:46,314 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:46,315 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:46,316 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:46,316 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:46,317 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e3d90e32-6d8a-484e-a38e-b561abfc59b3/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/modifiers/modifier_overriding_4.sol_9_no_adts_000.smt2
[2025-05-07 17:28:46,318 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:46,320 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:46,683 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e3d90e32-6d8a-484e-a38e-b561abfc59b3/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/modifiers/modifier_overriding_4.sol_9_no_adts_000.smt2
[2025-05-07 17:28:46,685 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:46,686 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:46,687 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:46,687 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:46,687 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:46,689 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,731 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46 Unit
[2025-05-07 17:28:46,731 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:46,732 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:46,732 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:46,732 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:46,743 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,743 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,769 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,769 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,779 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,781 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,783 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,788 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,790 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,805 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:46,806 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:46,806 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:46,806 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:46,806 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (1/1) ...
[2025-05-07 17:28:46,808 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:46,817 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:46,826 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:46,829 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:46,839 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:46,839 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:46,839 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:46,839 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_22_0 given in one single declaration
[2025-05-07 17:28:46,839 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_22_0
[2025-05-07 17:28:46,839 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_22_0
[2025-05-07 17:28:46,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_15_D_78_0 given in one single declaration
[2025-05-07 17:28:46,840 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_15_D_78_0
[2025-05-07 17:28:46,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_15_D_78_0
[2025-05-07 17:28:46,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_D_78_0 given in one single declaration
[2025-05-07 17:28:46,840 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_D_78_0
[2025-05-07 17:28:46,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_D_78_0
[2025-05-07 17:28:46,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_79_B_50_0 given in one single declaration
[2025-05-07 17:28:46,840 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_79_B_50_0
[2025-05-07 17:28:46,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_79_B_50_0
[2025-05-07 17:28:46,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_81_B_50_0 given in one single declaration
[2025-05-07 17:28:46,840 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_81_B_50_0
[2025-05-07 17:28:46,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_81_B_50_0
[2025-05-07 17:28:46,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_80_B_50_0 given in one single declaration
[2025-05-07 17:28:46,840 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_80_B_50_0
[2025-05-07 17:28:46,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_80_B_50_0
[2025-05-07 17:28:46,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_73_D_78_0 given in one single declaration
[2025-05-07 17:28:46,841 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_73_D_78_0
[2025-05-07 17:28:46,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_73_D_78_0
[2025-05-07 17:28:46,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_75_D_78_0 given in one single declaration
[2025-05-07 17:28:46,841 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_75_D_78_0
[2025-05-07 17:28:46,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_75_D_78_0
[2025-05-07 17:28:46,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_74_D_78_0 given in one single declaration
[2025-05-07 17:28:46,841 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_74_D_78_0
[2025-05-07 17:28:46,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_74_D_78_0
[2025-05-07 17:28:46,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_85_D_78_0 given in one single declaration
[2025-05-07 17:28:46,841 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_85_D_78_0
[2025-05-07 17:28:46,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_85_D_78_0
[2025-05-07 17:28:46,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_82_A_38_0 given in one single declaration
[2025-05-07 17:28:46,841 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_82_A_38_0
[2025-05-07 17:28:46,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_82_A_38_0
[2025-05-07 17:28:46,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_84_A_38_0 given in one single declaration
[2025-05-07 17:28:46,842 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_84_A_38_0
[2025-05-07 17:28:46,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_84_A_38_0
[2025-05-07 17:28:46,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_83_A_38_0 given in one single declaration
[2025-05-07 17:28:46,842 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_83_A_38_0
[2025-05-07 17:28:46,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_83_A_38_0
[2025-05-07 17:28:46,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_76_C_62_0 given in one single declaration
[2025-05-07 17:28:46,842 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_76_C_62_0
[2025-05-07 17:28:46,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_76_C_62_0
[2025-05-07 17:28:46,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_78_C_62_0 given in one single declaration
[2025-05-07 17:28:46,842 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_78_C_62_0
[2025-05-07 17:28:46,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_78_C_62_0
[2025-05-07 17:28:46,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_77_C_62_0 given in one single declaration
[2025-05-07 17:28:46,843 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_77_C_62_0
[2025-05-07 17:28:46,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_77_C_62_0
[2025-05-07 17:28:46,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,843 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_f__33_78_0
[2025-05-07 17:28:46,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_f__33_78_0
[2025-05-07 17:28:46,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,843 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_f__33_78_0
[2025-05-07 17:28:46,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_f__33_78_0
[2025-05-07 17:28:46,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,843 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_function_f__33_78_0
[2025-05-07 17:28:46,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_function_f__33_78_0
[2025-05-07 17:28:46,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_65_f_32_78_0 given in one single declaration
[2025-05-07 17:28:46,843 INFO  L130     BoogieDeclarations]: Found specification of procedure block_65_f_32_78_0
[2025-05-07 17:28:46,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_65_f_32_78_0
[2025-05-07 17:28:46,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_64_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,844 INFO  L130     BoogieDeclarations]: Found specification of procedure block_64_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_64_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_71_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,844 INFO  L130     BoogieDeclarations]: Found specification of procedure block_71_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_71_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,844 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_66_return_f_77_78_0 given in one single declaration
[2025-05-07 17:28:46,844 INFO  L130     BoogieDeclarations]: Found specification of procedure block_66_return_f_77_78_0
[2025-05-07 17:28:46,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_66_return_f_77_78_0
[2025-05-07 17:28:46,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_return_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,844 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_return_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_return_function_f__33_78_0
[2025-05-07 17:28:46,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,844 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_function_f__33_78_0
[2025-05-07 17:28:46,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_function_f__33_78_0
[2025-05-07 17:28:46,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_72_function_f__33_78_0 given in one single declaration
[2025-05-07 17:28:46,845 INFO  L130     BoogieDeclarations]: Found specification of procedure block_72_function_f__33_78_0
[2025-05-07 17:28:46,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_72_function_f__33_78_0
[2025-05-07 17:28:46,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_14_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,845 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_14_function_f__33_62_0
[2025-05-07 17:28:46,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_14_function_f__33_62_0
[2025-05-07 17:28:46,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,845 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_f__33_62_0
[2025-05-07 17:28:46,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_f__33_62_0
[2025-05-07 17:28:46,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,845 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_function_f__33_62_0
[2025-05-07 17:28:46,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_function_f__33_62_0
[2025-05-07 17:28:46,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_f_32_62_0 given in one single declaration
[2025-05-07 17:28:46,845 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_f_32_62_0
[2025-05-07 17:28:46,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_f_32_62_0
[2025-05-07 17:28:46,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,846 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_return_f_61_62_0 given in one single declaration
[2025-05-07 17:28:46,846 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_return_f_61_62_0
[2025-05-07 17:28:46,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_return_f_61_62_0
[2025-05-07 17:28:46,846 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_return_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,846 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_return_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_return_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,846 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,846 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,846 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_function_f__33_62_0
[2025-05-07 17:28:46,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_function_f__33_62_0
[2025-05-07 17:28:46,847 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_function_f__33_62_0 given in one single declaration
[2025-05-07 17:28:46,847 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_function_f__33_62_0
[2025-05-07 17:28:46,847 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_function_f__33_62_0
[2025-05-07 17:28:46,847 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_10_C_62_0 given in one single declaration
[2025-05-07 17:28:46,847 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_10_C_62_0
[2025-05-07 17:28:46,847 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_10_C_62_0
[2025-05-07 17:28:46,847 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_12_C_62_0 given in one single declaration
[2025-05-07 17:28:46,847 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_12_C_62_0
[2025-05-07 17:28:46,847 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_12_C_62_0
[2025-05-07 17:28:46,847 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_63_C_62_0 given in one single declaration
[2025-05-07 17:28:46,847 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_63_C_62_0
[2025-05-07 17:28:46,847 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_63_C_62_0
[2025-05-07 17:28:46,847 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_60_A_38_0 given in one single declaration
[2025-05-07 17:28:46,847 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_60_A_38_0
[2025-05-07 17:28:46,847 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_60_A_38_0
[2025-05-07 17:28:46,847 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_62_A_38_0 given in one single declaration
[2025-05-07 17:28:46,847 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_62_A_38_0
[2025-05-07 17:28:46,848 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_62_A_38_0
[2025-05-07 17:28:46,848 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_61_A_38_0 given in one single declaration
[2025-05-07 17:28:46,848 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_61_A_38_0
[2025-05-07 17:28:46,848 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_61_A_38_0
[2025-05-07 17:28:46,848 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_57_C_62_0 given in one single declaration
[2025-05-07 17:28:46,848 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_57_C_62_0
[2025-05-07 17:28:46,848 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_57_C_62_0
[2025-05-07 17:28:46,848 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_59_C_62_0 given in one single declaration
[2025-05-07 17:28:46,848 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_59_C_62_0
[2025-05-07 17:28:46,848 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_59_C_62_0
[2025-05-07 17:28:46,848 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_58_C_62_0 given in one single declaration
[2025-05-07 17:28:46,848 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_58_C_62_0
[2025-05-07 17:28:46,848 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_58_C_62_0
[2025-05-07 17:28:46,848 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_5_B_50_0 given in one single declaration
[2025-05-07 17:28:46,848 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_5_B_50_0
[2025-05-07 17:28:46,848 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_5_B_50_0
[2025-05-07 17:28:46,848 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_7_B_50_0 given in one single declaration
[2025-05-07 17:28:46,849 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_7_B_50_0
[2025-05-07 17:28:46,849 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_7_B_50_0
[2025-05-07 17:28:46,849 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_44_A_38_0 given in one single declaration
[2025-05-07 17:28:46,849 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_44_A_38_0
[2025-05-07 17:28:46,849 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_44_A_38_0
[2025-05-07 17:28:46,849 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_46_A_38_0 given in one single declaration
[2025-05-07 17:28:46,849 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_46_A_38_0
[2025-05-07 17:28:46,849 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_46_A_38_0
[2025-05-07 17:28:46,849 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_45_A_38_0 given in one single declaration
[2025-05-07 17:28:46,849 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_45_A_38_0
[2025-05-07 17:28:46,849 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_45_A_38_0
[2025-05-07 17:28:46,849 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_47_B_50_0 given in one single declaration
[2025-05-07 17:28:46,849 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_47_B_50_0
[2025-05-07 17:28:46,849 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_47_B_50_0
[2025-05-07 17:28:46,849 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_41_B_50_0 given in one single declaration
[2025-05-07 17:28:46,849 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_41_B_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_41_B_50_0
[2025-05-07 17:28:46,850 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_43_B_50_0 given in one single declaration
[2025-05-07 17:28:46,850 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_43_B_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_43_B_50_0
[2025-05-07 17:28:46,850 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_42_B_50_0 given in one single declaration
[2025-05-07 17:28:46,850 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_42_B_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_42_B_50_0
[2025-05-07 17:28:46,850 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,850 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,850 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_8_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,850 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_8_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_8_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,850 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_function_f__33_50_0
[2025-05-07 17:28:46,850 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_33_f_32_50_0 given in one single declaration
[2025-05-07 17:28:46,851 INFO  L130     BoogieDeclarations]: Found specification of procedure block_33_f_32_50_0
[2025-05-07 17:28:46,851 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_33_f_32_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,851 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,851 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,851 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_34_return_f_49_50_0 given in one single declaration
[2025-05-07 17:28:46,851 INFO  L130     BoogieDeclarations]: Found specification of procedure block_34_return_f_49_50_0
[2025-05-07 17:28:46,851 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_34_return_f_49_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_return_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,851 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_return_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_return_function_f__33_50_0
[2025-05-07 17:28:46,851 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_function_f__33_50_0 given in one single declaration
[2025-05-07 17:28:46,852 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_function_f__33_50_0
[2025-05-07 17:28:46,852 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_function_f__33_50_0
[2025-05-07 17:28:46,852 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:46,852 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:46,852 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:47,148 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:47,151 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:47,695 INFO  L?                        ?]: Removed 628 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:47,695 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:47,713 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:47,714 INFO  L312             CfgBuilder]: Removed 38 assume(true) statements.
[2025-05-07 17:28:47,714 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:47 BoogieIcfgContainer
[2025-05-07 17:28:47,714 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:47,717 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:47,717 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:47,721 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:47,721 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:46" (1/3) ...
[2025-05-07 17:28:47,721 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@202174f5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:47, skipping insertion in model container
[2025-05-07 17:28:47,721 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:46" (2/3) ...
[2025-05-07 17:28:47,722 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@202174f5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:47, skipping insertion in model container
[2025-05-07 17:28:47,722 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:47" (3/3) ...
[2025-05-07 17:28:47,723 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:47,738 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:47,740 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 69 procedures, 280 locations, 456 edges, 69 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:47,776 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:47,785 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;@a55bec8, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:47,785 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:47,789 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 280 states, 112 states have (on average 1.125) internal successors, (126), 126 states have internal predecessors, (126), 98 states have call successors, (110), 68 states have call predecessors, (110), 68 states have return successors, (110), 85 states have call predecessors, (110), 98 states have call successors, (110)
[2025-05-07 17:28:47,800 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-05-07 17:28:47,800 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:47,801 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]
[2025-05-07 17:28:47,801 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:47,804 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:47,805 INFO  L85        PathProgramCache]: Analyzing trace with hash 1875683095, now seen corresponding path program 1 times
[2025-05-07 17:28:47,810 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:47,810 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [904654022]
[2025-05-07 17:28:47,811 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:47,811 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:47,859 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-05-07 17:28:47,889 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-05-07 17:28:47,889 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:47,889 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:47,956 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:47,956 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:47,956 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [904654022]
[2025-05-07 17:28:47,956 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [904654022] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:47,956 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:47,958 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-05-07 17:28:47,959 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [584252152]
[2025-05-07 17:28:47,960 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:47,962 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-05-07 17:28:47,963 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:47,987 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-05-07 17:28:47,988 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:28:47,991 INFO  L87              Difference]: Start difference. First operand  has 280 states, 112 states have (on average 1.125) internal successors, (126), 126 states have internal predecessors, (126), 98 states have call successors, (110), 68 states have call predecessors, (110), 68 states have return successors, (110), 85 states have call predecessors, (110), 98 states have call successors, (110) Second operand  has 2 states, 2 states have (on average 12.0) internal successors, (24), 2 states have internal predecessors, (24), 2 states have call successors, (14), 1 states have call predecessors, (14), 2 states have return successors, (14), 2 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:28:48,033 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,033 INFO  L93              Difference]: Finished difference Result 251 states and 299 transitions.
[2025-05-07 17:28:48,034 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-05-07 17:28:48,036 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 12.0) internal successors, (24), 2 states have internal predecessors, (24), 2 states have call successors, (14), 1 states have call predecessors, (14), 2 states have return successors, (14), 2 states have call predecessors, (14), 2 states have call successors, (14) Word has length 52
[2025-05-07 17:28:48,036 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,045 INFO  L225             Difference]: With dead ends: 251
[2025-05-07 17:28:48,045 INFO  L226             Difference]: Without dead ends: 242
[2025-05-07 17:28:48,047 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:28:48,050 INFO  L437           NwaCegarLoop]: 299 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 299 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:48,051 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 299 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:48,062 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 242 states.
[2025-05-07 17:28:48,086 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 242 to 242.
[2025-05-07 17:28:48,088 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 242 states, 93 states have (on average 1.1397849462365592) internal successors, (106), 106 states have internal predecessors, (106), 89 states have call successors, (92), 59 states have call predecessors, (92), 59 states have return successors, (92), 76 states have call predecessors, (92), 89 states have call successors, (92)
[2025-05-07 17:28:48,094 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 242 states to 242 states and 290 transitions.
[2025-05-07 17:28:48,095 INFO  L79                 Accepts]: Start accepts. Automaton has 242 states and 290 transitions. Word has length 52
[2025-05-07 17:28:48,096 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:48,096 INFO  L485      AbstractCegarLoop]: Abstraction has 242 states and 290 transitions.
[2025-05-07 17:28:48,096 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 12.0) internal successors, (24), 2 states have internal predecessors, (24), 2 states have call successors, (14), 1 states have call predecessors, (14), 2 states have return successors, (14), 2 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:28:48,096 INFO  L278                IsEmpty]: Start isEmpty. Operand 242 states and 290 transitions.
[2025-05-07 17:28:48,099 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-05-07 17:28:48,100 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:48,100 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]
[2025-05-07 17:28:48,100 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:48,100 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:48,101 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:48,101 INFO  L85        PathProgramCache]: Analyzing trace with hash 1457639395, now seen corresponding path program 1 times
[2025-05-07 17:28:48,101 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:48,101 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1089215418]
[2025-05-07 17:28:48,101 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:48,101 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:48,128 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-05-07 17:28:48,154 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-05-07 17:28:48,154 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:48,154 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:48,275 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:48,276 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:48,276 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1089215418]
[2025-05-07 17:28:48,276 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1089215418] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:48,276 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:48,276 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:48,276 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1188943394]
[2025-05-07 17:28:48,276 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:48,277 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:48,277 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:48,278 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:48,278 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:48,278 INFO  L87              Difference]: Start difference. First operand 242 states and 290 transitions. Second operand  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 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:48,308 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,308 INFO  L93              Difference]: Finished difference Result 246 states and 294 transitions.
[2025-05-07 17:28:48,308 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:48,308 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 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 52
[2025-05-07 17:28:48,309 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,310 INFO  L225             Difference]: With dead ends: 246
[2025-05-07 17:28:48,310 INFO  L226             Difference]: Without dead ends: 230
[2025-05-07 17:28:48,310 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:48,311 INFO  L437           NwaCegarLoop]: 290 mSDtfsCounter, 1 mSDsluCounter, 558 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 848 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:48,311 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 848 Invalid, 5 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:48,312 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 230 states.
[2025-05-07 17:28:48,321 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 230 to 228.
[2025-05-07 17:28:48,321 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 228 states, 93 states have (on average 1.096774193548387) internal successors, (102), 102 states have internal predecessors, (102), 75 states have call successors, (78), 59 states have call predecessors, (78), 59 states have return successors, (78), 66 states have call predecessors, (78), 75 states have call successors, (78)
[2025-05-07 17:28:48,323 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 228 states to 228 states and 258 transitions.
[2025-05-07 17:28:48,323 INFO  L79                 Accepts]: Start accepts. Automaton has 228 states and 258 transitions. Word has length 52
[2025-05-07 17:28:48,323 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:48,323 INFO  L485      AbstractCegarLoop]: Abstraction has 228 states and 258 transitions.
[2025-05-07 17:28:48,323 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 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:48,323 INFO  L278                IsEmpty]: Start isEmpty. Operand 228 states and 258 transitions.
[2025-05-07 17:28:48,324 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-05-07 17:28:48,324 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:48,325 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]
[2025-05-07 17:28:48,325 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:48,325 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:48,325 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:48,325 INFO  L85        PathProgramCache]: Analyzing trace with hash 1667833383, now seen corresponding path program 1 times
[2025-05-07 17:28:48,325 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:48,325 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1513604530]
[2025-05-07 17:28:48,325 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:48,326 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:48,349 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-05-07 17:28:48,361 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-05-07 17:28:48,361 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:48,361 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:48,471 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:48,471 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:48,471 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1513604530]
[2025-05-07 17:28:48,471 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1513604530] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:48,471 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:48,471 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:48,471 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1176605082]
[2025-05-07 17:28:48,471 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:48,472 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:48,472 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:48,472 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:48,472 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:48,473 INFO  L87              Difference]: Start difference. First operand 228 states and 258 transitions. Second operand  has 5 states, 4 states have (on average 6.0) internal successors, (24), 5 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 4 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:48,508 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,508 INFO  L93              Difference]: Finished difference Result 232 states and 262 transitions.
[2025-05-07 17:28:48,509 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:48,509 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.0) internal successors, (24), 5 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 4 states have call predecessors, (14), 4 states have call successors, (14) Word has length 52
[2025-05-07 17:28:48,509 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,511 INFO  L225             Difference]: With dead ends: 232
[2025-05-07 17:28:48,511 INFO  L226             Difference]: Without dead ends: 225
[2025-05-07 17:28:48,511 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:48,512 INFO  L437           NwaCegarLoop]: 256 mSDtfsCounter, 1 mSDsluCounter, 751 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1007 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:48,512 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1007 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:48,513 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 225 states.
[2025-05-07 17:28:48,524 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 225 to 223.
[2025-05-07 17:28:48,524 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 223 states, 93 states have (on average 1.075268817204301) internal successors, (100), 100 states have internal predecessors, (100), 70 states have call successors, (73), 59 states have call predecessors, (73), 59 states have return successors, (73), 63 states have call predecessors, (73), 70 states have call successors, (73)
[2025-05-07 17:28:48,526 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 223 states to 223 states and 246 transitions.
[2025-05-07 17:28:48,526 INFO  L79                 Accepts]: Start accepts. Automaton has 223 states and 246 transitions. Word has length 52
[2025-05-07 17:28:48,526 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:48,526 INFO  L485      AbstractCegarLoop]: Abstraction has 223 states and 246 transitions.
[2025-05-07 17:28:48,526 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.0) internal successors, (24), 5 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 4 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:48,527 INFO  L278                IsEmpty]: Start isEmpty. Operand 223 states and 246 transitions.
[2025-05-07 17:28:48,528 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-05-07 17:28:48,528 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:48,528 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]
[2025-05-07 17:28:48,529 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:48,529 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:48,529 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:48,529 INFO  L85        PathProgramCache]: Analyzing trace with hash -97460717, now seen corresponding path program 1 times
[2025-05-07 17:28:48,529 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:48,529 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [798608921]
[2025-05-07 17:28:48,529 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:48,529 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:48,558 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-05-07 17:28:48,561 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-05-07 17:28:48,561 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:48,561 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:48,630 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:48,631 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:48,631 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [798608921]
[2025-05-07 17:28:48,631 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [798608921] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:48,631 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:48,631 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:48,631 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1494143421]
[2025-05-07 17:28:48,631 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:48,631 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:48,631 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:48,632 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:48,632 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:48,632 INFO  L87              Difference]: Start difference. First operand 223 states and 246 transitions. Second operand  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:48,646 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,647 INFO  L93              Difference]: Finished difference Result 227 states and 250 transitions.
[2025-05-07 17:28:48,647 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:48,647 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14) Word has length 52
[2025-05-07 17:28:48,647 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,648 INFO  L225             Difference]: With dead ends: 227
[2025-05-07 17:28:48,648 INFO  L226             Difference]: Without dead ends: 220
[2025-05-07 17:28:48,648 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:48,649 INFO  L437           NwaCegarLoop]: 246 mSDtfsCounter, 1 mSDsluCounter, 481 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 727 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:48,649 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 727 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:48,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 220 states.
[2025-05-07 17:28:48,654 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 220 to 218.
[2025-05-07 17:28:48,654 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 93 states have (on average 1.053763440860215) internal successors, (98), 98 states have internal predecessors, (98), 65 states have call successors, (68), 59 states have call predecessors, (68), 59 states have return successors, (68), 60 states have call predecessors, (68), 65 states have call successors, (68)
[2025-05-07 17:28:48,655 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 234 transitions.
[2025-05-07 17:28:48,656 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 234 transitions. Word has length 52
[2025-05-07 17:28:48,656 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:48,656 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 234 transitions.
[2025-05-07 17:28:48,656 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:48,656 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 234 transitions.
[2025-05-07 17:28:48,657 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-05-07 17:28:48,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:48,657 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]
[2025-05-07 17:28:48,657 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:48,657 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:48,657 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:48,657 INFO  L85        PathProgramCache]: Analyzing trace with hash 2039998626, now seen corresponding path program 1 times
[2025-05-07 17:28:48,657 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:48,657 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [952074359]
[2025-05-07 17:28:48,657 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:48,657 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:48,682 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-05-07 17:28:48,693 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-05-07 17:28:48,693 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:48,694 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:48,771 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:48,771 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:48,771 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [952074359]
[2025-05-07 17:28:48,771 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [952074359] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:48,771 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:48,771 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:48,771 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1311639066]
[2025-05-07 17:28:48,771 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:48,772 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:48,772 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:48,772 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:48,772 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:48,773 INFO  L87              Difference]: Start difference. First operand 218 states and 234 transitions. Second operand  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 5 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 5 states have call successors, (17)
[2025-05-07 17:28:48,811 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,811 INFO  L93              Difference]: Finished difference Result 223 states and 240 transitions.
[2025-05-07 17:28:48,812 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:48,812 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 5 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 5 states have call successors, (17) Word has length 62
[2025-05-07 17:28:48,812 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,814 INFO  L225             Difference]: With dead ends: 223
[2025-05-07 17:28:48,814 INFO  L226             Difference]: Without dead ends: 223
[2025-05-07 17:28:48,814 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:48,814 INFO  L437           NwaCegarLoop]: 231 mSDtfsCounter, 1 mSDsluCounter, 908 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1139 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:48,815 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1139 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:48,815 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 223 states.
[2025-05-07 17:28:48,820 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 223 to 223.
[2025-05-07 17:28:48,820 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 223 states, 95 states have (on average 1.0526315789473684) internal successors, (100), 100 states have internal predecessors, (100), 66 states have call successors, (69), 59 states have call predecessors, (69), 61 states have return successors, (71), 63 states have call predecessors, (71), 66 states have call successors, (71)
[2025-05-07 17:28:48,821 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 223 states to 223 states and 240 transitions.
[2025-05-07 17:28:48,821 INFO  L79                 Accepts]: Start accepts. Automaton has 223 states and 240 transitions. Word has length 62
[2025-05-07 17:28:48,821 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:48,821 INFO  L485      AbstractCegarLoop]: Abstraction has 223 states and 240 transitions.
[2025-05-07 17:28:48,821 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 5 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 5 states have call successors, (17)
[2025-05-07 17:28:48,821 INFO  L278                IsEmpty]: Start isEmpty. Operand 223 states and 240 transitions.
[2025-05-07 17:28:48,822 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-05-07 17:28:48,822 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:48,822 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]
[2025-05-07 17:28:48,823 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:48,823 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:48,823 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:48,823 INFO  L85        PathProgramCache]: Analyzing trace with hash -109246365, now seen corresponding path program 1 times
[2025-05-07 17:28:48,823 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:48,823 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1157083789]
[2025-05-07 17:28:48,823 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:48,823 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:48,846 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-05-07 17:28:48,857 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-05-07 17:28:48,857 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:48,857 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:48,944 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:48,944 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:48,944 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1157083789]
[2025-05-07 17:28:48,944 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1157083789] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:48,944 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:48,944 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:48,944 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1672317884]
[2025-05-07 17:28:48,944 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:48,945 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:48,945 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:48,945 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:48,945 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:48,945 INFO  L87              Difference]: Start difference. First operand 223 states and 240 transitions. Second operand  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 6 states have call predecessors, (17), 3 states have call successors, (17)
[2025-05-07 17:28:48,987 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,987 INFO  L93              Difference]: Finished difference Result 227 states and 244 transitions.
[2025-05-07 17:28:48,987 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:48,988 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 6 states have call predecessors, (17), 3 states have call successors, (17) Word has length 62
[2025-05-07 17:28:48,988 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,989 INFO  L225             Difference]: With dead ends: 227
[2025-05-07 17:28:48,989 INFO  L226             Difference]: Without dead ends: 227
[2025-05-07 17:28:48,989 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:48,990 INFO  L437           NwaCegarLoop]: 232 mSDtfsCounter, 1 mSDsluCounter, 912 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1144 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:48,990 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1144 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:48,991 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 227 states.
[2025-05-07 17:28:48,997 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 227 to 227.
[2025-05-07 17:28:48,998 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 227 states, 97 states have (on average 1.0515463917525774) internal successors, (102), 102 states have internal predecessors, (102), 66 states have call successors, (69), 59 states have call predecessors, (69), 63 states have return successors, (73), 65 states have call predecessors, (73), 66 states have call successors, (73)
[2025-05-07 17:28:49,000 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 227 states to 227 states and 244 transitions.
[2025-05-07 17:28:49,000 INFO  L79                 Accepts]: Start accepts. Automaton has 227 states and 244 transitions. Word has length 62
[2025-05-07 17:28:49,000 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:49,000 INFO  L485      AbstractCegarLoop]: Abstraction has 227 states and 244 transitions.
[2025-05-07 17:28:49,000 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 6 states have call predecessors, (17), 3 states have call successors, (17)
[2025-05-07 17:28:49,000 INFO  L278                IsEmpty]: Start isEmpty. Operand 227 states and 244 transitions.
[2025-05-07 17:28:49,001 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:28:49,001 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:49,002 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:49,002 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:49,002 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:49,002 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:49,002 INFO  L85        PathProgramCache]: Analyzing trace with hash 1055943625, now seen corresponding path program 1 times
[2025-05-07 17:28:49,002 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:49,002 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1443334026]
[2025-05-07 17:28:49,002 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:49,003 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:49,028 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:28:49,039 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:28:49,039 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:49,039 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:49,183 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:49,183 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:49,183 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1443334026]
[2025-05-07 17:28:49,183 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1443334026] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:49,183 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:49,183 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:28:49,183 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2079163651]
[2025-05-07 17:28:49,183 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:49,184 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:28:49,184 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:49,184 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:28:49,184 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:49,184 INFO  L87              Difference]: Start difference. First operand 227 states and 244 transitions. Second operand  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 6 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 7 states have call predecessors, (18), 6 states have call successors, (18)
[2025-05-07 17:28:49,256 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:49,257 INFO  L93              Difference]: Finished difference Result 192 states and 204 transitions.
[2025-05-07 17:28:49,257 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:28:49,257 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 6 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 7 states have call predecessors, (18), 6 states have call successors, (18) Word has length 65
[2025-05-07 17:28:49,257 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:49,258 INFO  L225             Difference]: With dead ends: 192
[2025-05-07 17:28:49,258 INFO  L226             Difference]: Without dead ends: 159
[2025-05-07 17:28:49,258 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:49,258 INFO  L437           NwaCegarLoop]: 195 mSDtfsCounter, 2 mSDsluCounter, 1339 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1534 SdHoareTripleChecker+Invalid, 45 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:49,258 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1534 Invalid, 45 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:49,259 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 159 states.
[2025-05-07 17:28:49,262 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 159 to 159.
[2025-05-07 17:28:49,262 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 68 states have (on average 1.0441176470588236) internal successors, (71), 71 states have internal predecessors, (71), 46 states have call successors, (48), 42 states have call predecessors, (48), 44 states have return successors, (50), 45 states have call predecessors, (50), 46 states have call successors, (50)
[2025-05-07 17:28:49,263 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 169 transitions.
[2025-05-07 17:28:49,263 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 169 transitions. Word has length 65
[2025-05-07 17:28:49,263 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:49,263 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 169 transitions.
[2025-05-07 17:28:49,263 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 6 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 7 states have call predecessors, (18), 6 states have call successors, (18)
[2025-05-07 17:28:49,263 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 169 transitions.
[2025-05-07 17:28:49,264 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-05-07 17:28:49,264 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:49,264 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:49,264 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:49,264 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:49,264 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:49,264 INFO  L85        PathProgramCache]: Analyzing trace with hash -2056447711, now seen corresponding path program 1 times
[2025-05-07 17:28:49,264 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:49,264 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [325136259]
[2025-05-07 17:28:49,264 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:49,264 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:49,283 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-05-07 17:28:49,293 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-05-07 17:28:49,293 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:49,293 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:49,430 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:49,430 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:49,430 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [325136259]
[2025-05-07 17:28:49,430 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [325136259] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:49,430 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:49,431 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:28:49,431 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1885624827]
[2025-05-07 17:28:49,431 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:49,431 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:28:49,431 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:49,431 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:28:49,431 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:49,432 INFO  L87              Difference]: Start difference. First operand 159 states and 169 transitions. Second operand  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 8 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:49,505 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:49,505 INFO  L93              Difference]: Finished difference Result 159 states and 168 transitions.
[2025-05-07 17:28:49,506 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:28:49,506 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 8 states have call predecessors, (18), 4 states have call successors, (18) Word has length 65
[2025-05-07 17:28:49,506 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:49,507 INFO  L225             Difference]: With dead ends: 159
[2025-05-07 17:28:49,507 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:28:49,507 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:49,508 INFO  L437           NwaCegarLoop]: 162 mSDtfsCounter, 1 mSDsluCounter, 1110 mSDsCounter, 0 mSdLazyCounter, 52 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1272 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 52 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:49,508 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1272 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 52 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:49,508 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:28:49,511 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-05-07 17:28:49,512 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 39 states have (on average 1.0256410256410255) internal successors, (40), 40 states have internal predecessors, (40), 27 states have call successors, (28), 25 states have call predecessors, (28), 25 states have return successors, (28), 26 states have call predecessors, (28), 27 states have call successors, (28)
[2025-05-07 17:28:49,512 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 96 transitions.
[2025-05-07 17:28:49,512 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 96 transitions. Word has length 65
[2025-05-07 17:28:49,513 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:49,513 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 96 transitions.
[2025-05-07 17:28:49,513 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 8 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:49,513 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 96 transitions.
[2025-05-07 17:28:49,514 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 83
[2025-05-07 17:28:49,514 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:49,514 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:49,514 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:49,514 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:49,514 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:49,514 INFO  L85        PathProgramCache]: Analyzing trace with hash 534772128, now seen corresponding path program 1 times
[2025-05-07 17:28:49,515 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:49,515 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2045996854]
[2025-05-07 17:28:49,515 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:49,515 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:49,546 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 82 statements into 1 equivalence classes.
[2025-05-07 17:28:49,562 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 82 of 82 statements.
[2025-05-07 17:28:49,563 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:49,563 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:49,650 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:49,650 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:49,650 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2045996854]
[2025-05-07 17:28:49,650 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2045996854] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:49,650 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:49,650 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:49,650 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1486482697]
[2025-05-07 17:28:49,650 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:49,650 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:49,650 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:49,651 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:49,651 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:49,651 INFO  L87              Difference]: Start difference. First operand 92 states and 96 transitions. Second operand  has 6 states, 5 states have (on average 7.2) internal successors, (36), 6 states have internal predecessors, (36), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:49,677 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:49,677 INFO  L93              Difference]: Finished difference Result 96 states and 100 transitions.
[2025-05-07 17:28:49,677 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:49,678 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.2) internal successors, (36), 6 states have internal predecessors, (36), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23) Word has length 82
[2025-05-07 17:28:49,678 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:49,678 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:28:49,678 INFO  L226             Difference]: Without dead ends: 96
[2025-05-07 17:28:49,679 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:49,679 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 1 mSDsluCounter, 362 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 455 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:49,679 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 455 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:49,679 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-05-07 17:28:49,681 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 96.
[2025-05-07 17:28:49,681 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 96 states, 41 states have (on average 1.024390243902439) internal successors, (42), 42 states have internal predecessors, (42), 27 states have call successors, (28), 25 states have call predecessors, (28), 27 states have return successors, (30), 28 states have call predecessors, (30), 27 states have call successors, (30)
[2025-05-07 17:28:49,682 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 96 states to 96 states and 100 transitions.
[2025-05-07 17:28:49,682 INFO  L79                 Accepts]: Start accepts. Automaton has 96 states and 100 transitions. Word has length 82
[2025-05-07 17:28:49,682 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:49,682 INFO  L485      AbstractCegarLoop]: Abstraction has 96 states and 100 transitions.
[2025-05-07 17:28:49,682 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.2) internal successors, (36), 6 states have internal predecessors, (36), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:49,682 INFO  L278                IsEmpty]: Start isEmpty. Operand 96 states and 100 transitions.
[2025-05-07 17:28:49,683 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 86
[2025-05-07 17:28:49,683 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:49,683 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:49,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:49,683 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:49,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:49,683 INFO  L85        PathProgramCache]: Analyzing trace with hash -1378899680, now seen corresponding path program 1 times
[2025-05-07 17:28:49,683 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:49,683 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2094066171]
[2025-05-07 17:28:49,683 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:49,683 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:49,706 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 85 statements into 1 equivalence classes.
[2025-05-07 17:28:49,717 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 85 of 85 statements.
[2025-05-07 17:28:49,717 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:49,717 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:49,868 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:49,869 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:49,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2094066171]
[2025-05-07 17:28:49,869 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2094066171] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:49,869 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:49,869 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:28:49,869 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [314494582]
[2025-05-07 17:28:49,869 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:49,869 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:28:49,869 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:49,870 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:28:49,870 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:49,870 INFO  L87              Difference]: Start difference. First operand 96 states and 100 transitions. Second operand  has 9 states, 7 states have (on average 5.285714285714286) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 7 states have return successors, (24), 7 states have call predecessors, (24), 5 states have call successors, (24)
[2025-05-07 17:28:49,921 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:49,921 INFO  L93              Difference]: Finished difference Result 35 states and 35 transitions.
[2025-05-07 17:28:49,922 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:28:49,922 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 5.285714285714286) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 7 states have return successors, (24), 7 states have call predecessors, (24), 5 states have call successors, (24) Word has length 85
[2025-05-07 17:28:49,922 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:49,922 INFO  L225             Difference]: With dead ends: 35
[2025-05-07 17:28:49,922 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:49,923 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:49,923 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 0 mSDsluCounter, 192 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 222 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:49,923 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 222 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:49,924 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:49,924 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:49,924 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:49,924 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:49,924 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 85
[2025-05-07 17:28:49,924 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:49,924 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:49,924 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 5.285714285714286) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 7 states have return successors, (24), 7 states have call predecessors, (24), 5 states have call successors, (24)
[2025-05-07 17:28:49,924 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:49,925 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:49,927 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:49,927 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:49,930 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:49,932 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:49,935 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:49 BoogieIcfgContainer
[2025-05-07 17:28:49,935 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:49,935 INFO  L158              Benchmark]: Toolchain (without parser) took 3249.24ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 271.1MB in the beginning and 178.7MB in the end (delta: 92.3MB). Peak memory consumption was 52.6MB. Max. memory is 33.6GB.
[2025-05-07 17:28:49,935 INFO  L158              Benchmark]: SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 173.1MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:49,936 INFO  L158              Benchmark]: ChcToBoogie took 44.89ms. Allocated memory is still 318.8MB. Free memory was 271.1MB in the beginning and 263.9MB in the end (delta: 7.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:49,936 INFO  L158              Benchmark]: Boogie Preprocessor took 73.31ms. Allocated memory is still 318.8MB. Free memory was 263.9MB in the beginning and 258.4MB in the end (delta: 5.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:49,936 INFO  L158              Benchmark]: RCFGBuilder took 908.58ms. Allocated memory is still 318.8MB. Free memory was 258.4MB in the beginning and 264.7MB in the end (delta: -6.3MB). Peak memory consumption was 112.7MB. Max. memory is 33.6GB.
[2025-05-07 17:28:49,936 INFO  L158              Benchmark]: TraceAbstraction took 2218.03ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 264.7MB in the beginning and 178.7MB in the end (delta: 86.0MB). Peak memory consumption was 40.5MB. Max. memory is 33.6GB.
[2025-05-07 17:28:49,937 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.18ms. Allocated memory is still 234.9MB. Free memory is still 173.1MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 44.89ms. Allocated memory is still 318.8MB. Free memory was 271.1MB in the beginning and 263.9MB in the end (delta: 7.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 73.31ms. Allocated memory is still 318.8MB. Free memory was 263.9MB in the beginning and 258.4MB in the end (delta: 5.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 908.58ms. Allocated memory is still 318.8MB. Free memory was 258.4MB in the beginning and 264.7MB in the end (delta: -6.3MB). Peak memory consumption was 112.7MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2218.03ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 264.7MB in the beginning and 178.7MB in the end (delta: 86.0MB). Peak memory consumption was 40.5MB. 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 69 procedures, 280 locations, 456 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.2s, OverallIterations: 10, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 50 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 9 mSDsluCounter, 8647 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 6613 mSDsCounter, 12 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 205 IncrementalHoareTripleChecker+Invalid, 217 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 12 mSolverCounterUnsat, 2034 mSDtfsCounter, 205 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 63 GetRequests, 22 SyntacticMatches, 0 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=280occurred in iteration=0, InterpolantAutomatonStates: 60, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 10 MinimizatonAttempts, 6 StatesRemovedByMinimization, 3 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.0s InterpolantComputationTime, 629 NumberOfCodeBlocks, 629 NumberOfCodeBlocksAsserted, 10 NumberOfCheckSat, 619 ConstructedInterpolants, 0 QuantifiedInterpolants, 805 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 10 InterpolantComputations, 10 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:28:49,950 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
