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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:53,228 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:53,277 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30cbbf56-0e05-4d78-be6b-ebcc3c703c25/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:53,281 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:53,281 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:53,299 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:53,299 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:53,299 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:53,300 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:53,300 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:53,300 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:53,300 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:53,300 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:53,301 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:53,301 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:53,301 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:53,301 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:53,302 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:53,302 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:53,302 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:53,302 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:53,490 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:53,498 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:53,500 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:53,501 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:53,501 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:53,502 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30cbbf56-0e05-4d78-be6b-ebcc3c703c25/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_5_no_adts_000.smt2
[2025-05-07 17:27:53,503 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:53,506 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:53,753 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30cbbf56-0e05-4d78-be6b-ebcc3c703c25/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/base_contract_assertion_fail_6.sol_5_no_adts_000.smt2
[2025-05-07 17:27:53,755 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:53,756 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:53,757 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:53,757 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:53,757 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:53,759 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,789 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53 Unit
[2025-05-07 17:27:53,789 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:53,789 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:53,790 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:53,790 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:53,801 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,801 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,822 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,823 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,827 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,828 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,829 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,831 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,833 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,843 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:53,844 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:53,844 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:53,844 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:53,845 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (1/1) ...
[2025-05-07 17:27:53,846 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:53,855 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:53,863 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:27:53,866 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:27:53,873 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:53,873 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:53,873 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:53,873 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_10_0 given in one single declaration
[2025-05-07 17:27:53,873 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_10_0
[2025-05-07 17:27:53,873 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_10_0
[2025-05-07 17:27:53,873 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_23_function_g__64_74_0 given in one single declaration
[2025-05-07 17:27:53,873 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_23_function_g__64_74_0
[2025-05-07 17:27:53,873 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_23_function_g__64_74_0
[2025-05-07 17:27:53,873 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_function_g__64_74_0 given in one single declaration
[2025-05-07 17:27:53,874 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_function_g__64_74_0
[2025-05-07 17:27:53,874 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_function_g__64_74_0
[2025-05-07 17:27:53,874 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_86_g_63_74_0 given in one single declaration
[2025-05-07 17:27:53,874 INFO  L130     BoogieDeclarations]: Found specification of procedure block_86_g_63_74_0
[2025-05-07 17:27:53,874 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_86_g_63_74_0
[2025-05-07 17:27:53,874 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_85_function_g__64_74_0 given in one single declaration
[2025-05-07 17:27:53,874 INFO  L130     BoogieDeclarations]: Found specification of procedure block_85_function_g__64_74_0
[2025-05-07 17:27:53,874 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_85_function_g__64_74_0
[2025-05-07 17:27:53,874 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_88_function_f__49_74_0 given in one single declaration
[2025-05-07 17:27:53,874 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_88_function_f__49_74_0
[2025-05-07 17:27:53,874 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_88_function_f__49_74_0
[2025-05-07 17:27:53,874 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_function_f__49_74_0 given in one single declaration
[2025-05-07 17:27:53,874 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_function_f__49_74_0
[2025-05-07 17:27:53,874 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_function_f__49_74_0
[2025-05-07 17:27:53,875 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_82_f_48_74_0 given in one single declaration
[2025-05-07 17:27:53,875 INFO  L130     BoogieDeclarations]: Found specification of procedure block_82_f_48_74_0
[2025-05-07 17:27:53,875 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_82_f_48_74_0
[2025-05-07 17:27:53,875 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_81_function_f__49_74_0 given in one single declaration
[2025-05-07 17:27:53,875 INFO  L130     BoogieDeclarations]: Found specification of procedure block_81_function_f__49_74_0
[2025-05-07 17:27:53,875 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_81_function_f__49_74_0
[2025-05-07 17:27:53,875 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_84_function_f__15_74_0 given in one single declaration
[2025-05-07 17:27:53,875 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_84_function_f__15_74_0
[2025-05-07 17:27:53,875 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_84_function_f__15_74_0
[2025-05-07 17:27:53,875 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_f__15_74_0 given in one single declaration
[2025-05-07 17:27:53,875 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_f__15_74_0
[2025-05-07 17:27:53,875 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_f__15_74_0
[2025-05-07 17:27:53,875 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:27:53,875 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_return_function_f__15_74_0
[2025-05-07 17:27:53,875 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_return_function_f__15_74_0
[2025-05-07 17:27:53,875 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_f_14_74_0 given in one single declaration
[2025-05-07 17:27:53,875 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_f_14_74_0
[2025-05-07 17:27:53,875 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_f_14_74_0
[2025-05-07 17:27:53,876 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_function_f__15_74_0 given in one single declaration
[2025-05-07 17:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_function_f__15_74_0
[2025-05-07 17:27:53,876 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_function_f__15_74_0
[2025-05-07 17:27:53,876 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_71_function_v__73_74_0 given in one single declaration
[2025-05-07 17:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_71_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_71_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_24_function_v__73_74_0 given in one single declaration
[2025-05-07 17:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_24_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_24_function_v__73_74_0
[2025-05-07 17:27:53,876 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:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure block_92_return_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_92_return_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_91_v_72_74_0 given in one single declaration
[2025-05-07 17:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure block_91_v_72_74_0
[2025-05-07 17:27:53,876 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_91_v_72_74_0
[2025-05-07 17:27:53,876 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_90_function_v__73_74_0 given in one single declaration
[2025-05-07 17:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure block_90_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_90_function_v__73_74_0
[2025-05-07 17:27:53,876 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_72_function_f__15_74_0 given in one single declaration
[2025-05-07 17:27:53,876 INFO  L130     BoogieDeclarations]: Found specification of procedure block_72_function_f__15_74_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_72_function_f__15_74_0
[2025-05-07 17:27:53,877 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:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure block_83_return_function_f__49_74_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_83_return_function_f__49_74_0
[2025-05-07 17:27:53,877 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:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure block_87_return_function_g__64_74_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_87_return_function_g__64_74_0
[2025-05-07 17:27:53,877 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_89_function_g__64_74_0 given in one single declaration
[2025-05-07 17:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure block_89_function_g__64_74_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_89_function_g__64_74_0
[2025-05-07 17:27:53,877 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_15_C_74_0 given in one single declaration
[2025-05-07 17:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_15_C_74_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_15_C_74_0
[2025-05-07 17:27:53,877 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_C_74_0 given in one single declaration
[2025-05-07 17:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_C_74_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_C_74_0
[2025-05-07 17:27:53,877 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_96_B_50_0 given in one single declaration
[2025-05-07 17:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_96_B_50_0
[2025-05-07 17:27:53,877 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_96_B_50_0
[2025-05-07 17:27:53,877 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:27:53,877 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_98_B_50_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_98_B_50_0
[2025-05-07 17:27:53,878 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_97_B_50_0 given in one single declaration
[2025-05-07 17:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_97_B_50_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_97_B_50_0
[2025-05-07 17:27:53,878 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_93_C_74_0 given in one single declaration
[2025-05-07 17:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_93_C_74_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_93_C_74_0
[2025-05-07 17:27:53,878 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:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_95_C_74_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_95_C_74_0
[2025-05-07 17:27:53,878 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_94_C_74_0 given in one single declaration
[2025-05-07 17:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_94_C_74_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_94_C_74_0
[2025-05-07 17:27:53,878 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_102_C_74_0 given in one single declaration
[2025-05-07 17:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_102_C_74_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_102_C_74_0
[2025-05-07 17:27:53,878 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_99_A_37_0 given in one single declaration
[2025-05-07 17:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_99_A_37_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_99_A_37_0
[2025-05-07 17:27:53,878 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:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_101_A_37_0
[2025-05-07 17:27:53,878 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_101_A_37_0
[2025-05-07 17:27:53,878 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_100_A_37_0 given in one single declaration
[2025-05-07 17:27:53,878 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_100_A_37_0
[2025-05-07 17:27:53,879 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_100_A_37_0
[2025-05-07 17:27:53,879 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:53,879 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:53,879 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:54,054 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:54,055 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:54,280 INFO  L?                        ?]: Removed 273 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:54,280 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:54,289 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:54,289 INFO  L312             CfgBuilder]: Removed 20 assume(true) statements.
[2025-05-07 17:27:54,290 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:54 BoogieIcfgContainer
[2025-05-07 17:27:54,290 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:54,291 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:54,291 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:54,294 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:54,294 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:53" (1/3) ...
[2025-05-07 17:27:54,294 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@203dff48 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:54, skipping insertion in model container
[2025-05-07 17:27:54,294 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:53" (2/3) ...
[2025-05-07 17:27:54,294 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@203dff48 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:54, skipping insertion in model container
[2025-05-07 17:27:54,294 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:54" (3/3) ...
[2025-05-07 17:27:54,295 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:54,305 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:54,307 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:27:54,335 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:54,343 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;@6d9bd6c0, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:54,343 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:54,346 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:27:54,353 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:27:54,354 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:54,354 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:27:54,354 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:54,357 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:54,358 INFO  L85        PathProgramCache]: Analyzing trace with hash -1394290445, now seen corresponding path program 1 times
[2025-05-07 17:27:54,362 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:54,363 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1854008414]
[2025-05-07 17:27:54,363 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:54,363 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:54,412 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:27:54,430 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:27:54,431 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:54,431 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:54,640 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:27:54,640 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:54,640 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1854008414]
[2025-05-07 17:27:54,641 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1854008414] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:54,641 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:54,642 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:54,643 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [636500494]
[2025-05-07 17:27:54,644 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:54,647 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:54,647 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:54,684 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:54,684 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:54,690 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:27:54,749 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:54,750 INFO  L93              Difference]: Finished difference Result 149 states and 175 transitions.
[2025-05-07 17:27:54,751 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:54,753 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:27:54,753 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:54,761 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:27:54,761 INFO  L226             Difference]: Without dead ends: 138
[2025-05-07 17:27:54,763 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:27:54,766 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:27:54,767 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:27:54,782 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-05-07 17:27:54,809 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 136.
[2025-05-07 17:27:54,810 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:27:54,815 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 136 states to 136 states and 150 transitions.
[2025-05-07 17:27:54,816 INFO  L79                 Accepts]: Start accepts. Automaton has 136 states and 150 transitions. Word has length 96
[2025-05-07 17:27:54,817 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:54,817 INFO  L485      AbstractCegarLoop]: Abstraction has 136 states and 150 transitions.
[2025-05-07 17:27:54,817 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:27:54,817 INFO  L278                IsEmpty]: Start isEmpty. Operand 136 states and 150 transitions.
[2025-05-07 17:27:54,821 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:27:54,821 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:54,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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27:54,822 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:54,822 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:54,823 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:54,823 INFO  L85        PathProgramCache]: Analyzing trace with hash -135815208, now seen corresponding path program 1 times
[2025-05-07 17:27:54,823 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:54,823 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1484547451]
[2025-05-07 17:27:54,823 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:54,823 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:54,880 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:27:54,918 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:27:54,918 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:54,918 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:55,193 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:27:55,193 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:55,193 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1484547451]
[2025-05-07 17:27:55,193 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1484547451] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:55,193 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:55,193 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:55,193 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [511597696]
[2025-05-07 17:27:55,193 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:55,195 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:55,195 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,195 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:55,195 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:55,195 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:27:55,246 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,246 INFO  L93              Difference]: Finished difference Result 134 states and 147 transitions.
[2025-05-07 17:27:55,247 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:55,247 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:27:55,247 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,248 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:27:55,248 INFO  L226             Difference]: Without dead ends: 131
[2025-05-07 17:27:55,248 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:27:55,249 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:27:55,249 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:27:55,250 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 131 states.
[2025-05-07 17:27:55,255 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 131 to 131.
[2025-05-07 17:27:55,255 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:27:55,256 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 131 states to 131 states and 142 transitions.
[2025-05-07 17:27:55,256 INFO  L79                 Accepts]: Start accepts. Automaton has 131 states and 142 transitions. Word has length 116
[2025-05-07 17:27:55,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,256 INFO  L485      AbstractCegarLoop]: Abstraction has 131 states and 142 transitions.
[2025-05-07 17:27:55,256 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:27:55,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 131 states and 142 transitions.
[2025-05-07 17:27:55,258 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-05-07 17:27:55,258 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,258 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:27:55,258 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:55,258 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,258 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,258 INFO  L85        PathProgramCache]: Analyzing trace with hash 1946137272, now seen corresponding path program 1 times
[2025-05-07 17:27:55,259 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,259 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [360198110]
[2025-05-07 17:27:55,259 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,259 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,302 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-05-07 17:27:55,322 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-05-07 17:27:55,322 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,322 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:55,482 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:27:55,482 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:55,482 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [360198110]
[2025-05-07 17:27:55,482 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [360198110] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:55,482 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:55,482 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:55,482 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1455212808]
[2025-05-07 17:27:55,482 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:55,483 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:55,483 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,484 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:55,484 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:55,484 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:27:55,525 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,525 INFO  L93              Difference]: Finished difference Result 137 states and 148 transitions.
[2025-05-07 17:27:55,526 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:55,526 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:27:55,527 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,528 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:27:55,528 INFO  L226             Difference]: Without dead ends: 137
[2025-05-07 17:27:55,528 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:27:55,528 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:27:55,529 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:27:55,529 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-05-07 17:27:55,534 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 135.
[2025-05-07 17:27:55,535 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:27:55,536 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 135 states to 135 states and 146 transitions.
[2025-05-07 17:27:55,536 INFO  L79                 Accepts]: Start accepts. Automaton has 135 states and 146 transitions. Word has length 116
[2025-05-07 17:27:55,536 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,536 INFO  L485      AbstractCegarLoop]: Abstraction has 135 states and 146 transitions.
[2025-05-07 17:27:55,537 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:27:55,537 INFO  L278                IsEmpty]: Start isEmpty. Operand 135 states and 146 transitions.
[2025-05-07 17:27:55,537 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 114
[2025-05-07 17:27:55,538 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,538 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:27:55,538 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:55,538 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,538 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,538 INFO  L85        PathProgramCache]: Analyzing trace with hash -1575441928, now seen corresponding path program 1 times
[2025-05-07 17:27:55,538 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,539 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1087893598]
[2025-05-07 17:27:55,539 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,539 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,574 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 113 statements into 1 equivalence classes.
[2025-05-07 17:27:55,599 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 113 of 113 statements.
[2025-05-07 17:27:55,599 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,599 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:55,707 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:27:55,708 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:55,708 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1087893598]
[2025-05-07 17:27:55,708 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1087893598] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:55,708 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:55,708 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:55,708 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1319746808]
[2025-05-07 17:27:55,708 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:55,709 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:55,709 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,709 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:55,709 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:55,709 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:27:55,748 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,748 INFO  L93              Difference]: Finished difference Result 129 states and 136 transitions.
[2025-05-07 17:27:55,748 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:55,749 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:27:55,749 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,750 INFO  L225             Difference]: With dead ends: 129
[2025-05-07 17:27:55,750 INFO  L226             Difference]: Without dead ends: 127
[2025-05-07 17:27:55,750 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:27:55,750 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:27:55,751 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:27:55,751 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-05-07 17:27:55,755 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 127.
[2025-05-07 17:27:55,756 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:27:55,756 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 132 transitions.
[2025-05-07 17:27:55,756 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 132 transitions. Word has length 113
[2025-05-07 17:27:55,756 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,757 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 132 transitions.
[2025-05-07 17:27:55,757 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:27:55,757 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 132 transitions.
[2025-05-07 17:27:55,758 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 120
[2025-05-07 17:27:55,758 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,758 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:27:55,758 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:55,758 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,758 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,758 INFO  L85        PathProgramCache]: Analyzing trace with hash -909158454, now seen corresponding path program 1 times
[2025-05-07 17:27:55,758 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,759 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [549170167]
[2025-05-07 17:27:55,759 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,759 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,790 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:27:55,806 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:27:55,806 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:55,806 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:55,908 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:27:55,908 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:55,908 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [549170167]
[2025-05-07 17:27:55,908 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [549170167] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:55,908 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:55,908 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:55,908 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [731481516]
[2025-05-07 17:27:55,908 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:55,909 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:55,909 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:55,910 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:55,910 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:55,910 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:27:55,946 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:55,946 INFO  L93              Difference]: Finished difference Result 126 states and 129 transitions.
[2025-05-07 17:27:55,946 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:55,946 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:27:55,947 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:55,947 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:27:55,947 INFO  L226             Difference]: Without dead ends: 125
[2025-05-07 17:27:55,948 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:27:55,948 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:27:55,948 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:27:55,949 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-05-07 17:27:55,952 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 125.
[2025-05-07 17:27:55,952 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:27:55,953 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 127 transitions.
[2025-05-07 17:27:55,953 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 127 transitions. Word has length 119
[2025-05-07 17:27:55,953 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:55,953 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 127 transitions.
[2025-05-07 17:27:55,953 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:27:55,954 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 127 transitions.
[2025-05-07 17:27:55,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:27:55,954 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:55,954 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:27:55,955 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:55,955 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:55,955 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:55,955 INFO  L85        PathProgramCache]: Analyzing trace with hash -580874117, now seen corresponding path program 1 times
[2025-05-07 17:27:55,955 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:55,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [756985230]
[2025-05-07 17:27:55,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:55,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:55,996 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:27:56,011 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:27:56,011 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:56,011 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:56,098 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:27:56,099 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:56,099 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [756985230]
[2025-05-07 17:27:56,099 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [756985230] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:56,099 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:56,099 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:56,099 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [902557092]
[2025-05-07 17:27:56,099 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:56,099 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:56,100 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:56,100 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:56,100 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:56,100 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:27:56,129 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:56,129 INFO  L93              Difference]: Finished difference Result 119 states and 121 transitions.
[2025-05-07 17:27:56,129 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:56,129 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:27:56,130 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:56,130 INFO  L225             Difference]: With dead ends: 119
[2025-05-07 17:27:56,130 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:56,130 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:27:56,130 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:27:56,131 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:27:56,131 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:56,131 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:56,131 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:27:56,131 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:56,131 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 122
[2025-05-07 17:27:56,131 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:56,131 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:56,131 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:27:56,131 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:56,132 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:56,134 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:56,134 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:56,136 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:56,138 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:56,140 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:56 BoogieIcfgContainer
[2025-05-07 17:27:56,140 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:56,141 INFO  L158              Benchmark]: Toolchain (without parser) took 2384.44ms. Allocated memory is still 234.9MB. Free memory was 146.2MB in the beginning and 99.5MB in the end (delta: 46.8MB). Peak memory consumption was 67.5MB. Max. memory is 33.6GB.
[2025-05-07 17:27:56,141 INFO  L158              Benchmark]: SmtParser took 0.29ms. Allocated memory is still 234.9MB. Free memory is still 174.3MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:56,141 INFO  L158              Benchmark]: ChcToBoogie took 32.29ms. Allocated memory is still 234.9MB. Free memory was 146.2MB in the beginning and 143.1MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:56,141 INFO  L158              Benchmark]: Boogie Preprocessor took 53.83ms. Allocated memory is still 234.9MB. Free memory was 143.0MB in the beginning and 139.4MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:56,141 INFO  L158              Benchmark]: RCFGBuilder took 445.96ms. Allocated memory is still 234.9MB. Free memory was 139.3MB in the beginning and 164.7MB in the end (delta: -25.4MB). Peak memory consumption was 43.9MB. Max. memory is 33.6GB.
[2025-05-07 17:27:56,141 INFO  L158              Benchmark]: TraceAbstraction took 1849.10ms. Allocated memory is still 234.9MB. Free memory was 164.1MB in the beginning and 99.5MB in the end (delta: 64.6MB). Peak memory consumption was 74.0MB. Max. memory is 33.6GB.
[2025-05-07 17:27:56,142 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.29ms. Allocated memory is still 234.9MB. Free memory is still 174.3MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 32.29ms. Allocated memory is still 234.9MB. Free memory was 146.2MB in the beginning and 143.1MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 53.83ms. Allocated memory is still 234.9MB. Free memory was 143.0MB in the beginning and 139.4MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 445.96ms. Allocated memory is still 234.9MB. Free memory was 139.3MB in the beginning and 164.7MB in the end (delta: -25.4MB). Peak memory consumption was 43.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 1849.10ms. Allocated memory is still 234.9MB. Free memory was 164.1MB in the beginning and 99.5MB in the end (delta: 64.6MB). Peak memory consumption was 74.0MB. 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.8s, 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, 0.9s 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:27:56,153 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
