./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_2_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:47,208 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:47,245 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df2a7c0-0a51-411a-9b00-402848c2d7bd/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:47,248 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:47,249 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:47,261 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:47,262 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:47,262 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:47,262 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:47,262 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:47,262 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:47,262 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:47,262 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:47,263 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:47,263 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:47,263 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:47,263 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:47,263 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:47,263 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:47,263 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:47,264 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:47,264 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:47,264 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:47,264 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:47,264 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:47,264 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:47,264 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:47,445 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:47,451 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:47,453 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:47,454 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:47,454 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:47,455 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df2a7c0-0a51-411a-9b00-402848c2d7bd/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_2_no_adts_000.smt2
[2025-05-07 17:26:47,456 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:47,459 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:47,748 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df2a7c0-0a51-411a-9b00-402848c2d7bd/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_2_no_adts_000.smt2
[2025-05-07 17:26:47,750 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:47,751 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:47,751 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:47,751 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:47,752 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:47,754 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,795 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47 Unit
[2025-05-07 17:26:47,795 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:47,796 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:47,796 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:47,796 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:47,807 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,807 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,836 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,836 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,842 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,842 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,844 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,846 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,847 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,857 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:47,858 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:47,858 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:47,858 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:47,859 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (1/1) ...
[2025-05-07 17:26:47,860 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:47,869 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:47,877 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:26:47,879 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:26:47,886 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:47,886 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:47,886 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:47,886 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_14_0 given in one single declaration
[2025-05-07 17:26:47,886 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_14_0
[2025-05-07 17:26:47,887 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_14_0
[2025-05-07 17:26:47,887 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_23_function_g__64_74_0 given in one single declaration
[2025-05-07 17:26:47,887 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_23_function_g__64_74_0
[2025-05-07 17:26:47,887 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_23_function_g__64_74_0
[2025-05-07 17:26:47,887 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_function_g__64_74_0 given in one single declaration
[2025-05-07 17:26:47,887 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_function_g__64_74_0
[2025-05-07 17:26:47,887 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_function_g__64_74_0
[2025-05-07 17:26:47,887 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_86_g_63_74_0 given in one single declaration
[2025-05-07 17:26:47,887 INFO  L130     BoogieDeclarations]: Found specification of procedure block_86_g_63_74_0
[2025-05-07 17:26:47,887 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_86_g_63_74_0
[2025-05-07 17:26:47,887 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_85_function_g__64_74_0 given in one single declaration
[2025-05-07 17:26:47,887 INFO  L130     BoogieDeclarations]: Found specification of procedure block_85_function_g__64_74_0
[2025-05-07 17:26:47,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_85_function_g__64_74_0
[2025-05-07 17:26:47,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_88_function_f__49_74_0 given in one single declaration
[2025-05-07 17:26:47,888 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_88_function_f__49_74_0
[2025-05-07 17:26:47,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_88_function_f__49_74_0
[2025-05-07 17:26:47,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_function_f__49_74_0 given in one single declaration
[2025-05-07 17:26:47,888 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_function_f__49_74_0
[2025-05-07 17:26:47,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_function_f__49_74_0
[2025-05-07 17:26:47,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_82_f_48_74_0 given in one single declaration
[2025-05-07 17:26:47,888 INFO  L130     BoogieDeclarations]: Found specification of procedure block_82_f_48_74_0
[2025-05-07 17:26:47,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_82_f_48_74_0
[2025-05-07 17:26:47,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_81_function_f__49_74_0 given in one single declaration
[2025-05-07 17:26:47,889 INFO  L130     BoogieDeclarations]: Found specification of procedure block_81_function_f__49_74_0
[2025-05-07 17:26:47,889 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_81_function_f__49_74_0
[2025-05-07 17:26:47,889 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_84_function_f__15_74_0 given in one single declaration
[2025-05-07 17:26:47,889 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_84_function_f__15_74_0
[2025-05-07 17:26:47,889 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_84_function_f__15_74_0
[2025-05-07 17:26:47,889 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_f__15_74_0 given in one single declaration
[2025-05-07 17:26:47,889 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_f__15_74_0
[2025-05-07 17:26:47,889 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_f__15_74_0
[2025-05-07 17:26:47,889 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_return_function_f__15_74_0 given in one single declaration
[2025-05-07 17:26:47,889 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_return_function_f__15_74_0
[2025-05-07 17:26:47,889 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_return_function_f__15_74_0
[2025-05-07 17:26:47,889 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_f_14_74_0 given in one single declaration
[2025-05-07 17:26:47,890 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_f_14_74_0
[2025-05-07 17:26:47,890 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_f_14_74_0
[2025-05-07 17:26:47,890 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_function_f__15_74_0 given in one single declaration
[2025-05-07 17:26:47,890 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_function_f__15_74_0
[2025-05-07 17:26:47,890 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_function_f__15_74_0
[2025-05-07 17:26:47,890 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_71_function_v__73_74_0 given in one single declaration
[2025-05-07 17:26:47,890 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_71_function_v__73_74_0
[2025-05-07 17:26:47,890 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_71_function_v__73_74_0
[2025-05-07 17:26:47,890 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_24_function_v__73_74_0 given in one single declaration
[2025-05-07 17:26:47,890 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_24_function_v__73_74_0
[2025-05-07 17:26:47,890 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_24_function_v__73_74_0
[2025-05-07 17:26:47,890 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_92_return_function_v__73_74_0 given in one single declaration
[2025-05-07 17:26:47,891 INFO  L130     BoogieDeclarations]: Found specification of procedure block_92_return_function_v__73_74_0
[2025-05-07 17:26:47,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_92_return_function_v__73_74_0
[2025-05-07 17:26:47,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_91_v_72_74_0 given in one single declaration
[2025-05-07 17:26:47,891 INFO  L130     BoogieDeclarations]: Found specification of procedure block_91_v_72_74_0
[2025-05-07 17:26:47,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_91_v_72_74_0
[2025-05-07 17:26:47,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_90_function_v__73_74_0 given in one single declaration
[2025-05-07 17:26:47,891 INFO  L130     BoogieDeclarations]: Found specification of procedure block_90_function_v__73_74_0
[2025-05-07 17:26:47,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_90_function_v__73_74_0
[2025-05-07 17:26:47,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_72_function_f__15_74_0 given in one single declaration
[2025-05-07 17:26:47,891 INFO  L130     BoogieDeclarations]: Found specification of procedure block_72_function_f__15_74_0
[2025-05-07 17:26:47,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_72_function_f__15_74_0
[2025-05-07 17:26:47,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_83_return_function_f__49_74_0 given in one single declaration
[2025-05-07 17:26:47,892 INFO  L130     BoogieDeclarations]: Found specification of procedure block_83_return_function_f__49_74_0
[2025-05-07 17:26:47,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_83_return_function_f__49_74_0
[2025-05-07 17:26:47,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_87_return_function_g__64_74_0 given in one single declaration
[2025-05-07 17:26:47,892 INFO  L130     BoogieDeclarations]: Found specification of procedure block_87_return_function_g__64_74_0
[2025-05-07 17:26:47,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_87_return_function_g__64_74_0
[2025-05-07 17:26:47,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_89_function_g__64_74_0 given in one single declaration
[2025-05-07 17:26:47,892 INFO  L130     BoogieDeclarations]: Found specification of procedure block_89_function_g__64_74_0
[2025-05-07 17:26:47,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_89_function_g__64_74_0
[2025-05-07 17:26:47,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_15_C_74_0 given in one single declaration
[2025-05-07 17:26:47,892 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_15_C_74_0
[2025-05-07 17:26:47,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_15_C_74_0
[2025-05-07 17:26:47,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_C_74_0 given in one single declaration
[2025-05-07 17:26:47,892 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_C_74_0
[2025-05-07 17:26:47,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_C_74_0
[2025-05-07 17:26:47,893 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_96_B_50_0 given in one single declaration
[2025-05-07 17:26:47,893 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_96_B_50_0
[2025-05-07 17:26:47,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_96_B_50_0
[2025-05-07 17:26:47,893 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_98_B_50_0 given in one single declaration
[2025-05-07 17:26:47,893 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_98_B_50_0
[2025-05-07 17:26:47,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_98_B_50_0
[2025-05-07 17:26:47,893 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_97_B_50_0 given in one single declaration
[2025-05-07 17:26:47,893 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_97_B_50_0
[2025-05-07 17:26:47,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_97_B_50_0
[2025-05-07 17:26:47,893 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_93_C_74_0 given in one single declaration
[2025-05-07 17:26:47,893 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_93_C_74_0
[2025-05-07 17:26:47,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_93_C_74_0
[2025-05-07 17:26:47,893 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_95_C_74_0 given in one single declaration
[2025-05-07 17:26:47,894 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_95_C_74_0
[2025-05-07 17:26:47,894 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_95_C_74_0
[2025-05-07 17:26:47,894 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_94_C_74_0 given in one single declaration
[2025-05-07 17:26:47,894 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_94_C_74_0
[2025-05-07 17:26:47,894 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_94_C_74_0
[2025-05-07 17:26:47,894 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_102_C_74_0 given in one single declaration
[2025-05-07 17:26:47,894 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_102_C_74_0
[2025-05-07 17:26:47,894 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_102_C_74_0
[2025-05-07 17:26:47,894 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_99_A_37_0 given in one single declaration
[2025-05-07 17:26:47,894 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_99_A_37_0
[2025-05-07 17:26:47,894 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_99_A_37_0
[2025-05-07 17:26:47,894 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_101_A_37_0 given in one single declaration
[2025-05-07 17:26:47,894 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_101_A_37_0
[2025-05-07 17:26:47,894 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_101_A_37_0
[2025-05-07 17:26:47,895 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_100_A_37_0 given in one single declaration
[2025-05-07 17:26:47,895 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_100_A_37_0
[2025-05-07 17:26:47,895 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_100_A_37_0
[2025-05-07 17:26:47,895 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:47,895 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:47,895 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:26:48,076 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:26:48,078 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:26:48,310 INFO  L?                        ?]: Removed 273 outVars from TransFormulas that were not future-live.
[2025-05-07 17:26:48,310 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:26:48,319 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:26:48,319 INFO  L312             CfgBuilder]: Removed 20 assume(true) statements.
[2025-05-07 17:26:48,319 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:48 BoogieIcfgContainer
[2025-05-07 17:26:48,320 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:26:48,321 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:26:48,321 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:26:48,323 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:26:48,324 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:47" (1/3) ...
[2025-05-07 17:26:48,324 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@51b1f570 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:26:48, skipping insertion in model container
[2025-05-07 17:26:48,324 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:47" (2/3) ...
[2025-05-07 17:26:48,324 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@51b1f570 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:26:48, skipping insertion in model container
[2025-05-07 17:26:48,324 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:48" (3/3) ...
[2025-05-07 17:26:48,325 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:26:48,335 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:26:48,337 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 37 procedures, 147 locations, 228 edges, 37 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:26:48,366 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:26:48,375 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;@141f5be6, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:26:48,375 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:26:48,377 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 147 states, 58 states have (on average 1.0862068965517242) internal successors, (63), 63 states have internal predecessors, (63), 54 states have call successors, (55), 36 states have call predecessors, (55), 36 states have return successors, (55), 47 states have call predecessors, (55), 54 states have call successors, (55)
[2025-05-07 17:26:48,386 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:48,386 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:48,386 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:48,386 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:48,390 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:48,390 INFO  L85        PathProgramCache]: Analyzing trace with hash 1375807667, now seen corresponding path program 1 times
[2025-05-07 17:26:48,395 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:48,396 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [816239315]
[2025-05-07 17:26:48,396 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:48,396 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:48,455 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:48,473 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:48,473 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:48,473 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:48,717 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:26:48,718 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:48,718 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [816239315]
[2025-05-07 17:26:48,719 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [816239315] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:48,719 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:48,721 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:48,723 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [35149512]
[2025-05-07 17:26:48,723 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:48,727 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:48,727 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:48,769 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:48,770 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:48,772 INFO  L87              Difference]: Start difference. First operand  has 147 states, 58 states have (on average 1.0862068965517242) internal successors, (63), 63 states have internal predecessors, (63), 54 states have call successors, (55), 36 states have call predecessors, (55), 36 states have return successors, (55), 47 states have call predecessors, (55), 54 states have call successors, (55) Second operand  has 4 states, 3 states have (on average 14.0) internal successors, (42), 4 states have internal predecessors, (42), 4 states have call successors, (27), 1 states have call predecessors, (27), 3 states have return successors, (27), 3 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:26:48,825 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:48,825 INFO  L93              Difference]: Finished difference Result 149 states and 175 transitions.
[2025-05-07 17:26:48,826 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:48,828 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 14.0) internal successors, (42), 4 states have internal predecessors, (42), 4 states have call successors, (27), 1 states have call predecessors, (27), 3 states have return successors, (27), 3 states have call predecessors, (27), 4 states have call successors, (27) Word has length 96
[2025-05-07 17:26:48,828 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:48,834 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:26:48,834 INFO  L226             Difference]: Without dead ends: 138
[2025-05-07 17:26:48,836 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:26:48,839 INFO  L437           NwaCegarLoop]: 171 mSDtfsCounter, 1 mSDsluCounter, 326 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 497 SdHoareTripleChecker+Invalid, 4 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:48,840 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 497 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:48,854 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-05-07 17:26:48,877 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 136.
[2025-05-07 17:26:48,879 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 136 states, 57 states have (on average 1.0175438596491229) internal successors, (58), 58 states have internal predecessors, (58), 45 states have call successors, (46), 36 states have call predecessors, (46), 36 states have return successors, (46), 41 states have call predecessors, (46), 45 states have call successors, (46)
[2025-05-07 17:26:48,884 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 136 states to 136 states and 150 transitions.
[2025-05-07 17:26:48,885 INFO  L79                 Accepts]: Start accepts. Automaton has 136 states and 150 transitions. Word has length 96
[2025-05-07 17:26:48,886 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:48,886 INFO  L485      AbstractCegarLoop]: Abstraction has 136 states and 150 transitions.
[2025-05-07 17:26:48,886 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 14.0) internal successors, (42), 4 states have internal predecessors, (42), 4 states have call successors, (27), 1 states have call predecessors, (27), 3 states have return successors, (27), 3 states have call predecessors, (27), 4 states have call successors, (27)
[2025-05-07 17:26:48,886 INFO  L278                IsEmpty]: Start isEmpty. Operand 136 states and 150 transitions.
[2025-05-07 17:26:48,891 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:26:48,891 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:48,891 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, 1, 1, 1, 1, 1, 1, 1, 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:26:48,891 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:26:48,891 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:48,892 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:48,892 INFO  L85        PathProgramCache]: Analyzing trace with hash 610656920, now seen corresponding path program 1 times
[2025-05-07 17:26:48,892 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:48,892 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1585647283]
[2025-05-07 17:26:48,893 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:48,893 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:48,960 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:26:48,995 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:26:48,995 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:48,995 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:49,281 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:26:49,282 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:49,282 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1585647283]
[2025-05-07 17:26:49,282 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1585647283] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:49,282 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:49,282 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:49,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1085289693]
[2025-05-07 17:26:49,282 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:49,283 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:49,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:49,284 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:49,284 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:49,284 INFO  L87              Difference]: Start difference. First operand 136 states and 150 transitions. Second operand  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:49,338 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:49,338 INFO  L93              Difference]: Finished difference Result 134 states and 147 transitions.
[2025-05-07 17:26:49,339 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:49,339 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33) Word has length 116
[2025-05-07 17:26:49,340 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:49,340 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:26:49,340 INFO  L226             Difference]: Without dead ends: 131
[2025-05-07 17:26:49,341 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:26:49,341 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 0 mSDsluCounter, 559 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 702 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:49,341 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 702 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:49,342 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 131 states.
[2025-05-07 17:26:49,347 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 131 to 131.
[2025-05-07 17:26:49,347 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 131 states, 55 states have (on average 1.018181818181818) internal successors, (56), 56 states have internal predecessors, (56), 43 states have call successors, (43), 35 states have call predecessors, (43), 35 states have return successors, (43), 39 states have call predecessors, (43), 43 states have call successors, (43)
[2025-05-07 17:26:49,348 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 131 states to 131 states and 142 transitions.
[2025-05-07 17:26:49,348 INFO  L79                 Accepts]: Start accepts. Automaton has 131 states and 142 transitions. Word has length 116
[2025-05-07 17:26:49,349 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:49,349 INFO  L485      AbstractCegarLoop]: Abstraction has 131 states and 142 transitions.
[2025-05-07 17:26:49,349 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:49,349 INFO  L278                IsEmpty]: Start isEmpty. Operand 131 states and 142 transitions.
[2025-05-07 17:26:49,350 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:26:49,350 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:49,350 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, 1, 1, 1, 1, 1, 1, 1, 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:26:49,350 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:26:49,350 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:49,351 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:49,351 INFO  L85        PathProgramCache]: Analyzing trace with hash 724796920, now seen corresponding path program 1 times
[2025-05-07 17:26:49,351 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:49,351 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1609554144]
[2025-05-07 17:26:49,351 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:49,351 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:49,393 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:26:49,412 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:26:49,412 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:49,412 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:49,552 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:26:49,552 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:49,552 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1609554144]
[2025-05-07 17:26:49,552 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1609554144] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:49,552 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:49,552 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:49,552 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1701201422]
[2025-05-07 17:26:49,552 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:49,553 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:49,553 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:49,553 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:49,553 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:49,554 INFO  L87              Difference]: Start difference. First operand 131 states and 142 transitions. Second operand  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:49,602 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:49,602 INFO  L93              Difference]: Finished difference Result 137 states and 148 transitions.
[2025-05-07 17:26:49,602 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:49,603 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33) Word has length 116
[2025-05-07 17:26:49,603 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:49,604 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:26:49,605 INFO  L226             Difference]: Without dead ends: 137
[2025-05-07 17:26:49,605 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:26:49,605 INFO  L437           NwaCegarLoop]: 140 mSDtfsCounter, 1 mSDsluCounter, 547 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 687 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:49,606 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 687 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:49,606 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-05-07 17:26:49,615 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 135.
[2025-05-07 17:26:49,615 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 135 states, 57 states have (on average 1.0175438596491229) internal successors, (58), 58 states have internal predecessors, (58), 43 states have call successors, (43), 35 states have call predecessors, (43), 37 states have return successors, (45), 41 states have call predecessors, (45), 43 states have call successors, (45)
[2025-05-07 17:26:49,617 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 135 states to 135 states and 146 transitions.
[2025-05-07 17:26:49,617 INFO  L79                 Accepts]: Start accepts. Automaton has 135 states and 146 transitions. Word has length 116
[2025-05-07 17:26:49,617 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:49,618 INFO  L485      AbstractCegarLoop]: Abstraction has 135 states and 146 transitions.
[2025-05-07 17:26:49,618 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.0) internal successors, (50), 6 states have internal predecessors, (50), 4 states have call successors, (33), 1 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:26:49,618 INFO  L278                IsEmpty]: Start isEmpty. Operand 135 states and 146 transitions.
[2025-05-07 17:26:49,619 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 114
[2025-05-07 17:26:49,620 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:49,620 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, 1, 1, 1, 1, 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:26:49,620 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:26:49,620 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:49,620 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:49,621 INFO  L85        PathProgramCache]: Analyzing trace with hash -219201676, now seen corresponding path program 1 times
[2025-05-07 17:26:49,621 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:49,621 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1849499680]
[2025-05-07 17:26:49,621 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:49,621 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:49,670 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 113 statements into 1 equivalence classes.
[2025-05-07 17:26:49,686 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 113 of 113 statements.
[2025-05-07 17:26:49,686 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:49,687 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:49,801 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:26:49,801 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:49,801 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1849499680]
[2025-05-07 17:26:49,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1849499680] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:49,801 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:49,801 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:26:49,801 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [888662463]
[2025-05-07 17:26:49,801 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:49,802 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:26:49,802 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:49,803 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:26:49,803 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:49,803 INFO  L87              Difference]: Start difference. First operand 135 states and 146 transitions. Second operand  has 7 states, 6 states have (on average 8.166666666666666) internal successors, (49), 7 states have internal predecessors, (49), 4 states have call successors, (32), 1 states have call predecessors, (32), 6 states have return successors, (32), 6 states have call predecessors, (32), 4 states have call successors, (32)
[2025-05-07 17:26:49,846 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:49,846 INFO  L93              Difference]: Finished difference Result 129 states and 136 transitions.
[2025-05-07 17:26:49,847 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:26:49,847 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 8.166666666666666) internal successors, (49), 7 states have internal predecessors, (49), 4 states have call successors, (32), 1 states have call predecessors, (32), 6 states have return successors, (32), 6 states have call predecessors, (32), 4 states have call successors, (32) Word has length 113
[2025-05-07 17:26:49,847 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:49,848 INFO  L225             Difference]: With dead ends: 129
[2025-05-07 17:26:49,848 INFO  L226             Difference]: Without dead ends: 127
[2025-05-07 17:26:49,849 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:49,849 INFO  L437           NwaCegarLoop]: 132 mSDtfsCounter, 0 mSDsluCounter, 647 mSDsCounter, 0 mSdLazyCounter, 27 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 779 SdHoareTripleChecker+Invalid, 27 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 27 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:49,850 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 779 Invalid, 27 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 27 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:49,850 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-05-07 17:26:49,856 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 127.
[2025-05-07 17:26:49,856 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 127 states, 53 states have (on average 1.0188679245283019) internal successors, (54), 54 states have internal predecessors, (54), 39 states have call successors, (39), 35 states have call predecessors, (39), 35 states have return successors, (39), 37 states have call predecessors, (39), 39 states have call successors, (39)
[2025-05-07 17:26:49,857 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 132 transitions.
[2025-05-07 17:26:49,857 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 132 transitions. Word has length 113
[2025-05-07 17:26:49,857 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:49,858 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 132 transitions.
[2025-05-07 17:26:49,858 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 8.166666666666666) internal successors, (49), 7 states have internal predecessors, (49), 4 states have call successors, (32), 1 states have call predecessors, (32), 6 states have return successors, (32), 6 states have call predecessors, (32), 4 states have call successors, (32)
[2025-05-07 17:26:49,858 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 132 transitions.
[2025-05-07 17:26:49,859 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 120
[2025-05-07 17:26:49,859 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:49,860 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:49,860 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:26:49,860 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:49,860 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:49,860 INFO  L85        PathProgramCache]: Analyzing trace with hash 664610630, now seen corresponding path program 1 times
[2025-05-07 17:26:49,860 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:49,860 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1885930845]
[2025-05-07 17:26:49,861 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:49,861 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:49,908 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:26:49,922 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:26:49,922 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:49,922 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:50,033 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:26:50,033 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:50,033 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1885930845]
[2025-05-07 17:26:50,033 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1885930845] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:50,033 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:50,033 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:50,033 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [383683282]
[2025-05-07 17:26:50,033 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:50,034 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:50,034 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:50,034 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:50,034 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:50,035 INFO  L87              Difference]: Start difference. First operand 127 states and 132 transitions. Second operand  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 5 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:26:50,071 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:50,071 INFO  L93              Difference]: Finished difference Result 126 states and 129 transitions.
[2025-05-07 17:26:50,072 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:50,072 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 5 states have call predecessors, (34), 4 states have call successors, (34) Word has length 119
[2025-05-07 17:26:50,073 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:50,074 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:26:50,074 INFO  L226             Difference]: Without dead ends: 125
[2025-05-07 17:26:50,074 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:26:50,075 INFO  L437           NwaCegarLoop]: 126 mSDtfsCounter, 0 mSDsluCounter, 492 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 618 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:50,075 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 618 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:50,075 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-05-07 17:26:50,078 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 125.
[2025-05-07 17:26:50,078 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 52 states have (on average 1.0192307692307692) internal successors, (53), 53 states have internal predecessors, (53), 37 states have call successors, (37), 35 states have call predecessors, (37), 35 states have return successors, (37), 36 states have call predecessors, (37), 37 states have call successors, (37)
[2025-05-07 17:26:50,079 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 127 transitions.
[2025-05-07 17:26:50,079 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 127 transitions. Word has length 119
[2025-05-07 17:26:50,079 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:50,079 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 127 transitions.
[2025-05-07 17:26:50,079 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (34), 1 states have call predecessors, (34), 5 states have return successors, (34), 5 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:26:50,079 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 127 transitions.
[2025-05-07 17:26:50,080 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:26:50,080 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:50,080 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:50,080 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:26:50,080 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:50,080 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:50,080 INFO  L85        PathProgramCache]: Analyzing trace with hash -1985091013, now seen corresponding path program 1 times
[2025-05-07 17:26:50,080 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:50,081 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [925376698]
[2025-05-07 17:26:50,081 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:50,081 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:50,125 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:26:50,141 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:26:50,141 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:50,141 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:50,228 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:26:50,228 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:50,228 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [925376698]
[2025-05-07 17:26:50,228 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [925376698] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:50,228 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:50,229 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:50,229 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [523565040]
[2025-05-07 17:26:50,229 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:50,229 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:50,229 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:50,230 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:50,230 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:50,230 INFO  L87              Difference]: Start difference. First operand 125 states and 127 transitions. Second operand  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 3 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 6 states have call predecessors, (35), 3 states have call successors, (35)
[2025-05-07 17:26:50,260 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:50,260 INFO  L93              Difference]: Finished difference Result 119 states and 121 transitions.
[2025-05-07 17:26:50,261 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:50,261 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 3 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 6 states have call predecessors, (35), 3 states have call successors, (35) Word has length 122
[2025-05-07 17:26:50,262 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:50,262 INFO  L225             Difference]: With dead ends: 119
[2025-05-07 17:26:50,262 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:26:50,262 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:26:50,262 INFO  L437           NwaCegarLoop]: 118 mSDtfsCounter, 0 mSDsluCounter, 460 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 578 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:26:50,263 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 578 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:50,263 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:26:50,263 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:26:50,263 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:26:50,263 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:26:50,263 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 122
[2025-05-07 17:26:50,263 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:50,263 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:26:50,264 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 3 states have call successors, (35), 1 states have call predecessors, (35), 5 states have return successors, (35), 6 states have call predecessors, (35), 3 states have call successors, (35)
[2025-05-07 17:26:50,264 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:26:50,264 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:26:50,266 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:26:50,266 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:26:50,269 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:50,270 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:26:50,273 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:26:50 BoogieIcfgContainer
[2025-05-07 17:26:50,273 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:26:50,273 INFO  L158              Benchmark]: Toolchain (without parser) took 2522.63ms. Allocated memory is still 234.9MB. Free memory was 143.5MB in the beginning and 91.7MB in the end (delta: 51.8MB). Peak memory consumption was 66.0MB. Max. memory is 33.6GB.
[2025-05-07 17:26:50,274 INFO  L158              Benchmark]: SmtParser took 0.24ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:50,274 INFO  L158              Benchmark]: ChcToBoogie took 43.74ms. Allocated memory is still 234.9MB. Free memory was 143.5MB in the beginning and 140.2MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:50,274 INFO  L158              Benchmark]: Boogie Preprocessor took 61.96ms. Allocated memory is still 234.9MB. Free memory was 140.2MB in the beginning and 136.6MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:50,274 INFO  L158              Benchmark]: RCFGBuilder took 461.55ms. Allocated memory is still 234.9MB. Free memory was 136.5MB in the beginning and 162.5MB in the end (delta: -26.0MB). Peak memory consumption was 42.9MB. Max. memory is 33.6GB.
[2025-05-07 17:26:50,274 INFO  L158              Benchmark]: TraceAbstraction took 1951.85ms. Allocated memory is still 234.9MB. Free memory was 162.1MB in the beginning and 91.7MB in the end (delta: 70.4MB). Peak memory consumption was 73.4MB. Max. memory is 33.6GB.
[2025-05-07 17:26:50,275 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.24ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 43.74ms. Allocated memory is still 234.9MB. Free memory was 143.5MB in the beginning and 140.2MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 61.96ms. Allocated memory is still 234.9MB. Free memory was 140.2MB in the beginning and 136.6MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 461.55ms. Allocated memory is still 234.9MB. Free memory was 136.5MB in the beginning and 162.5MB in the end (delta: -26.0MB). Peak memory consumption was 42.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 1951.85ms. Allocated memory is still 234.9MB. Free memory was 162.1MB in the beginning and 91.7MB in the end (delta: 70.4MB). Peak memory consumption was 73.4MB. 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 37 procedures, 147 locations, 228 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 1.9s, OverallIterations: 6, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.3s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 12 SdHoareTripleChecker+Valid, 0.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 2 mSDsluCounter, 3861 SdHoareTripleChecker+Invalid, 0.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 3031 mSDsCounter, 2 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 112 IncrementalHoareTripleChecker+Invalid, 114 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 2 mSolverCounterUnsat, 830 mSDtfsCounter, 112 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 35 GetRequests, 12 SyntacticMatches, 0 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=147occurred in iteration=0, InterpolantAutomatonStates: 35, 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, 6 MinimizatonAttempts, 4 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 1.0s InterpolantComputationTime, 682 NumberOfCodeBlocks, 682 NumberOfCodeBlocksAsserted, 6 NumberOfCheckSat, 676 ConstructedInterpolants, 0 QuantifiedInterpolants, 782 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 6 InterpolantComputations, 6 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:26:50,286 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
