./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/virtual_function_called_by_constructor.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:29:20,526 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:29:20,578 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_19069bbb-c307-441c-9301-ba2a442dc7d0/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:29:20,581 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:29:20,581 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:29:20,597 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:29:20,598 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:29:20,598 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:29:20,598 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:29:20,598 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:29:20,599 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:29:20,599 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:29:20,599 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:29:20,599 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:29:20,599 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:29:20,599 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:29:20,599 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:29:20,599 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:29:20,599 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:20,600 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:29:20,600 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:29:20,600 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:29:20,600 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:29:20,600 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:29:20,600 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:29:20,601 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:29:20,601 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:29:20,784 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:29:20,790 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:29:20,792 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:29:20,793 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:29:20,793 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:29:20,794 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_19069bbb-c307-441c-9301-ba2a442dc7d0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/virtual_function_called_by_constructor.sol_0_no_adts_000.smt2
[2025-05-07 17:29:20,795 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:29:20,797 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:29:21,006 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_19069bbb-c307-441c-9301-ba2a442dc7d0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/virtual_function_called_by_constructor.sol_0_no_adts_000.smt2
[2025-05-07 17:29:21,008 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:29:21,009 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:29:21,009 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:29:21,009 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:29:21,009 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:29:21,011 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,037 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21 Unit
[2025-05-07 17:29:21,037 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:29:21,038 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:29:21,038 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:29:21,038 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:29:21,050 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,050 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,071 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,071 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,076 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,076 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,078 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,080 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,081 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,091 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:29:21,091 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:29:21,091 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:29:21,092 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:29:21,092 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (1/1) ...
[2025-05-07 17:29:21,094 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:21,103 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:21,111 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:29:21,114 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:29:21,123 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:29:21,123 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:29:21,123 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:29:21,123 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_13_0 given in one single declaration
[2025-05-07 17:29:21,123 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_13_0
[2025-05-07 17:29:21,123 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_13_0
[2025-05-07 17:29:21,123 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_7_C_63_0 given in one single declaration
[2025-05-07 17:29:21,123 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_7_C_63_0
[2025-05-07 17:29:21,123 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_7_C_63_0
[2025-05-07 17:29:21,123 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_9_C_63_0 given in one single declaration
[2025-05-07 17:29:21,123 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_9_C_63_0
[2025-05-07 17:29:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_9_C_63_0
[2025-05-07 17:29:21,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_50_C_63_0 given in one single declaration
[2025-05-07 17:29:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_50_C_63_0
[2025-05-07 17:29:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_50_C_63_0
[2025-05-07 17:29:21,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_52_C_63_0 given in one single declaration
[2025-05-07 17:29:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_52_C_63_0
[2025-05-07 17:29:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_52_C_63_0
[2025-05-07 17:29:21,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_51_C_63_0 given in one single declaration
[2025-05-07 17:29:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_51_C_63_0
[2025-05-07 17:29:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_51_C_63_0
[2025-05-07 17:29:21,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_60_C_63_0 given in one single declaration
[2025-05-07 17:29:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_60_C_63_0
[2025-05-07 17:29:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_60_C_63_0
[2025-05-07 17:29:21,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_57_A_34_0 given in one single declaration
[2025-05-07 17:29:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_57_A_34_0
[2025-05-07 17:29:21,124 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_57_A_34_0
[2025-05-07 17:29:21,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_constructor_17_63_0 given in one single declaration
[2025-05-07 17:29:21,124 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_constructor_17_63_0
[2025-05-07 17:29:21,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_constructor_17_63_0
[2025-05-07 17:29:21,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_return_constructor_17_63_0 given in one single declaration
[2025-05-07 17:29:21,125 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_return_constructor_17_63_0
[2025-05-07 17:29:21,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_return_constructor_17_63_0
[2025-05-07 17:29:21,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54__16_63_0 given in one single declaration
[2025-05-07 17:29:21,125 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54__16_63_0
[2025-05-07 17:29:21,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54__16_63_0
[2025-05-07 17:29:21,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_constructor_17_63_0 given in one single declaration
[2025-05-07 17:29:21,125 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_constructor_17_63_0
[2025-05-07 17:29:21,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_constructor_17_63_0
[2025-05-07 17:29:21,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_56_function_v__45_63_0 given in one single declaration
[2025-05-07 17:29:21,125 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_56_function_v__45_63_0
[2025-05-07 17:29:21,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_56_function_v__45_63_0
[2025-05-07 17:29:21,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_v__45_63_0 given in one single declaration
[2025-05-07 17:29:21,125 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_v__45_63_0
[2025-05-07 17:29:21,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_v__45_63_0
[2025-05-07 17:29:21,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_return_function_v__45_63_0 given in one single declaration
[2025-05-07 17:29:21,125 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_return_function_v__45_63_0
[2025-05-07 17:29:21,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_return_function_v__45_63_0
[2025-05-07 17:29:21,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_v_44_63_0 given in one single declaration
[2025-05-07 17:29:21,126 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_v_44_63_0
[2025-05-07 17:29:21,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_v_44_63_0
[2025-05-07 17:29:21,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_function_v__45_63_0 given in one single declaration
[2025-05-07 17:29:21,126 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_function_v__45_63_0
[2025-05-07 17:29:21,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_function_v__45_63_0
[2025-05-07 17:29:21,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_59_A_34_0 given in one single declaration
[2025-05-07 17:29:21,126 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_59_A_34_0
[2025-05-07 17:29:21,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_59_A_34_0
[2025-05-07 17:29:21,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_58_A_34_0 given in one single declaration
[2025-05-07 17:29:21,126 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_58_A_34_0
[2025-05-07 17:29:21,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_58_A_34_0
[2025-05-07 17:29:21,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_15_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,126 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_15_function_i__62_63_0
[2025-05-07 17:29:21,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_15_function_i__62_63_0
[2025-05-07 17:29:21,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,126 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_function_i__62_63_0
[2025-05-07 17:29:21,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_function_i__62_63_0
[2025-05-07 17:29:21,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_14_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,127 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_14_function_i__62_63_0
[2025-05-07 17:29:21,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_14_function_i__62_63_0
[2025-05-07 17:29:21,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,127 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_function_i__62_63_0
[2025-05-07 17:29:21,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_function_i__62_63_0
[2025-05-07 17:29:21,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_i_61_63_0 given in one single declaration
[2025-05-07 17:29:21,127 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_i_61_63_0
[2025-05-07 17:29:21,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_i_61_63_0
[2025-05-07 17:29:21,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,128 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_function_i__62_63_0
[2025-05-07 17:29:21,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_function_i__62_63_0
[2025-05-07 17:29:21,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_return_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,128 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_return_function_i__62_63_0
[2025-05-07 17:29:21,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_return_function_i__62_63_0
[2025-05-07 17:29:21,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_function_i__62_63_0 given in one single declaration
[2025-05-07 17:29:21,128 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_function_i__62_63_0
[2025-05-07 17:29:21,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_function_i__62_63_0
[2025-05-07 17:29:21,128 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:29:21,128 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:29:21,128 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:29:21,261 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:29:21,262 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:29:21,495 INFO  L?                        ?]: Removed 215 outVars from TransFormulas that were not future-live.
[2025-05-07 17:29:21,495 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:29:21,505 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:29:21,505 INFO  L312             CfgBuilder]: Removed 14 assume(true) statements.
[2025-05-07 17:29:21,506 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:21 BoogieIcfgContainer
[2025-05-07 17:29:21,506 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:29:21,508 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:29:21,508 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:29:21,511 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:29:21,511 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:21" (1/3) ...
[2025-05-07 17:29:21,511 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3aa023b9 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:29:21, skipping insertion in model container
[2025-05-07 17:29:21,512 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:21" (2/3) ...
[2025-05-07 17:29:21,512 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3aa023b9 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:29:21, skipping insertion in model container
[2025-05-07 17:29:21,512 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:21" (3/3) ...
[2025-05-07 17:29:21,513 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:29:21,524 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:29:21,526 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 29 procedures, 115 locations, 175 edges, 29 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:29:21,561 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:29:21,572 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;@d66eb09, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:29:21,572 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:29:21,575 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 115 states, 47 states have (on average 1.1063829787234043) internal successors, (52), 52 states have internal predecessors, (52), 39 states have call successors, (41), 28 states have call predecessors, (41), 28 states have return successors, (41), 34 states have call predecessors, (41), 39 states have call successors, (41)
[2025-05-07 17:29:21,583 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:29:21,583 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:21,584 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:21,584 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:21,587 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:21,587 INFO  L85        PathProgramCache]: Analyzing trace with hash -312467861, now seen corresponding path program 1 times
[2025-05-07 17:29:21,593 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:21,593 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1078718660]
[2025-05-07 17:29:21,593 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:21,593 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:21,647 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:29:21,717 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:29:21,718 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:21,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:22,026 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:29:22,026 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:22,027 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1078718660]
[2025-05-07 17:29:22,027 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1078718660] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:22,027 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:22,041 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:22,043 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1499690011]
[2025-05-07 17:29:22,043 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:22,046 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:22,046 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:22,068 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:22,068 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:22,070 INFO  L87              Difference]: Start difference. First operand  has 115 states, 47 states have (on average 1.1063829787234043) internal successors, (52), 52 states have internal predecessors, (52), 39 states have call successors, (41), 28 states have call predecessors, (41), 28 states have return successors, (41), 34 states have call predecessors, (41), 39 states have call successors, (41) Second operand  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 3 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 3 states have call successors, (22)
[2025-05-07 17:29:22,114 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:22,115 INFO  L93              Difference]: Finished difference Result 117 states and 136 transitions.
[2025-05-07 17:29:22,116 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:22,117 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 3 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 3 states have call successors, (22) Word has length 80
[2025-05-07 17:29:22,118 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:22,123 INFO  L225             Difference]: With dead ends: 117
[2025-05-07 17:29:22,124 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:29:22,125 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:29:22,127 INFO  L437           NwaCegarLoop]: 132 mSDtfsCounter, 1 mSDsluCounter, 253 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 385 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:22,128 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 385 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:22,138 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:29:22,160 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 108.
[2025-05-07 17:29:22,161 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 108 states, 46 states have (on average 1.0434782608695652) internal successors, (48), 48 states have internal predecessors, (48), 34 states have call successors, (36), 28 states have call predecessors, (36), 28 states have return successors, (36), 31 states have call predecessors, (36), 34 states have call successors, (36)
[2025-05-07 17:29:22,164 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 108 states to 108 states and 120 transitions.
[2025-05-07 17:29:22,165 INFO  L79                 Accepts]: Start accepts. Automaton has 108 states and 120 transitions. Word has length 80
[2025-05-07 17:29:22,166 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:22,166 INFO  L485      AbstractCegarLoop]: Abstraction has 108 states and 120 transitions.
[2025-05-07 17:29:22,166 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 3 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 3 states have call successors, (22)
[2025-05-07 17:29:22,166 INFO  L278                IsEmpty]: Start isEmpty. Operand 108 states and 120 transitions.
[2025-05-07 17:29:22,168 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:29:22,168 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:22,168 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]
[2025-05-07 17:29:22,169 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:29:22,169 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:22,169 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:22,169 INFO  L85        PathProgramCache]: Analyzing trace with hash -1548047316, now seen corresponding path program 1 times
[2025-05-07 17:29:22,169 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:22,169 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1220399227]
[2025-05-07 17:29:22,169 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:22,170 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:22,212 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:29:22,226 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:29:22,227 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:22,227 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:22,334 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:29:22,335 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:22,335 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1220399227]
[2025-05-07 17:29:22,335 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1220399227] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:22,335 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:22,335 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:22,335 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1060323961]
[2025-05-07 17:29:22,335 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:22,336 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:22,336 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:22,337 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:22,337 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:22,337 INFO  L87              Difference]: Start difference. First operand 108 states and 120 transitions. Second operand  has 4 states, 3 states have (on average 13.333333333333334) internal successors, (40), 4 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 3 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:29:22,348 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:22,348 INFO  L93              Difference]: Finished difference Result 110 states and 121 transitions.
[2025-05-07 17:29:22,348 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:22,349 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 13.333333333333334) internal successors, (40), 4 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 3 states have call predecessors, (25), 4 states have call successors, (25) Word has length 90
[2025-05-07 17:29:22,349 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:22,349 INFO  L225             Difference]: With dead ends: 110
[2025-05-07 17:29:22,350 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:29:22,350 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:29:22,350 INFO  L437           NwaCegarLoop]: 120 mSDtfsCounter, 1 mSDsluCounter, 230 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 350 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:22,350 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 350 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:22,351 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:29:22,355 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:29:22,355 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 46 states have (on average 1.0217391304347827) internal successors, (47), 47 states have internal predecessors, (47), 32 states have call successors, (34), 28 states have call predecessors, (34), 28 states have return successors, (34), 30 states have call predecessors, (34), 32 states have call successors, (34)
[2025-05-07 17:29:22,356 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 115 transitions.
[2025-05-07 17:29:22,356 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 115 transitions. Word has length 90
[2025-05-07 17:29:22,357 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:22,357 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 115 transitions.
[2025-05-07 17:29:22,357 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 13.333333333333334) internal successors, (40), 4 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 3 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:29:22,357 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 115 transitions.
[2025-05-07 17:29:22,358 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:29:22,358 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:22,358 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]
[2025-05-07 17:29:22,358 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:22,358 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:22,359 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:22,359 INFO  L85        PathProgramCache]: Analyzing trace with hash -936538806, now seen corresponding path program 1 times
[2025-05-07 17:29:22,359 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:22,359 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [314017294]
[2025-05-07 17:29:22,359 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:22,359 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:22,391 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:29:22,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:29:22,407 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:22,407 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:22,515 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:29:22,515 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:22,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [314017294]
[2025-05-07 17:29:22,515 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [314017294] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:22,515 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:22,515 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:29:22,516 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1496756626]
[2025-05-07 17:29:22,516 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:22,516 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:29:22,516 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:22,517 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:29:22,517 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:29:22,517 INFO  L87              Difference]: Start difference. First operand 106 states and 115 transitions. Second operand  has 5 states, 4 states have (on average 10.0) internal successors, (40), 5 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 4 states have return successors, (25), 4 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:29:22,537 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:22,538 INFO  L93              Difference]: Finished difference Result 110 states and 118 transitions.
[2025-05-07 17:29:22,538 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:29:22,538 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 10.0) internal successors, (40), 5 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 4 states have return successors, (25), 4 states have call predecessors, (25), 4 states have call successors, (25) Word has length 90
[2025-05-07 17:29:22,539 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:22,539 INFO  L225             Difference]: With dead ends: 110
[2025-05-07 17:29:22,539 INFO  L226             Difference]: Without dead ends: 104
[2025-05-07 17:29:22,539 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:29:22,540 INFO  L437           NwaCegarLoop]: 114 mSDtfsCounter, 1 mSDsluCounter, 332 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 446 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:22,540 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 446 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:22,541 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 104 states.
[2025-05-07 17:29:22,545 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 104 to 104.
[2025-05-07 17:29:22,545 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 104 states, 45 states have (on average 1.0222222222222221) internal successors, (46), 46 states have internal predecessors, (46), 30 states have call successors, (32), 28 states have call predecessors, (32), 28 states have return successors, (32), 29 states have call predecessors, (32), 30 states have call successors, (32)
[2025-05-07 17:29:22,546 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 104 states to 104 states and 110 transitions.
[2025-05-07 17:29:22,546 INFO  L79                 Accepts]: Start accepts. Automaton has 104 states and 110 transitions. Word has length 90
[2025-05-07 17:29:22,546 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:22,546 INFO  L485      AbstractCegarLoop]: Abstraction has 104 states and 110 transitions.
[2025-05-07 17:29:22,546 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 10.0) internal successors, (40), 5 states have internal predecessors, (40), 4 states have call successors, (25), 1 states have call predecessors, (25), 4 states have return successors, (25), 4 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:29:22,547 INFO  L278                IsEmpty]: Start isEmpty. Operand 104 states and 110 transitions.
[2025-05-07 17:29:22,548 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:29:22,548 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:22,548 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]
[2025-05-07 17:29:22,548 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:22,548 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:22,549 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:22,549 INFO  L85        PathProgramCache]: Analyzing trace with hash 1316498625, now seen corresponding path program 1 times
[2025-05-07 17:29:22,549 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:22,549 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [328701512]
[2025-05-07 17:29:22,549 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:22,549 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:22,576 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:29:22,591 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:29:22,591 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:22,591 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:23,252 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:29:23,252 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:23,252 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [328701512]
[2025-05-07 17:29:23,252 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [328701512] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:23,252 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:23,252 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [21] imperfect sequences [] total 21
[2025-05-07 17:29:23,252 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1842766371]
[2025-05-07 17:29:23,253 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:23,253 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-05-07 17:29:23,253 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:23,254 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-05-07 17:29:23,254 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=381, Unknown=0, NotChecked=0, Total=420
[2025-05-07 17:29:23,254 INFO  L87              Difference]: Start difference. First operand 104 states and 110 transitions. Second operand  has 21 states, 17 states have (on average 2.411764705882353) internal successors, (41), 19 states have internal predecessors, (41), 9 states have call successors, (26), 1 states have call predecessors, (26), 17 states have return successors, (26), 18 states have call predecessors, (26), 9 states have call successors, (26)
[2025-05-07 17:29:23,610 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:23,610 INFO  L93              Difference]: Finished difference Result 114 states and 124 transitions.
[2025-05-07 17:29:23,611 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-05-07 17:29:23,611 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 17 states have (on average 2.411764705882353) internal successors, (41), 19 states have internal predecessors, (41), 9 states have call successors, (26), 1 states have call predecessors, (26), 17 states have return successors, (26), 18 states have call predecessors, (26), 9 states have call successors, (26) Word has length 93
[2025-05-07 17:29:23,611 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:23,613 INFO  L225             Difference]: With dead ends: 114
[2025-05-07 17:29:23,613 INFO  L226             Difference]: Without dead ends: 114
[2025-05-07 17:29:23,613 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 24 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=51, Invalid=501, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:29:23,614 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 5 mSDsluCounter, 1789 mSDsCounter, 0 mSdLazyCounter, 389 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1886 SdHoareTripleChecker+Invalid, 390 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 389 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:23,614 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1886 Invalid, 390 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 389 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:29:23,615 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-05-07 17:29:23,625 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 112.
[2025-05-07 17:29:23,626 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 112 states, 48 states have (on average 1.0208333333333333) internal successors, (49), 49 states have internal predecessors, (49), 32 states have call successors, (34), 28 states have call predecessors, (34), 31 states have return successors, (39), 34 states have call predecessors, (39), 32 states have call successors, (39)
[2025-05-07 17:29:23,627 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 112 states to 112 states and 122 transitions.
[2025-05-07 17:29:23,627 INFO  L79                 Accepts]: Start accepts. Automaton has 112 states and 122 transitions. Word has length 93
[2025-05-07 17:29:23,628 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:23,628 INFO  L485      AbstractCegarLoop]: Abstraction has 112 states and 122 transitions.
[2025-05-07 17:29:23,628 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 17 states have (on average 2.411764705882353) internal successors, (41), 19 states have internal predecessors, (41), 9 states have call successors, (26), 1 states have call predecessors, (26), 17 states have return successors, (26), 18 states have call predecessors, (26), 9 states have call successors, (26)
[2025-05-07 17:29:23,628 INFO  L278                IsEmpty]: Start isEmpty. Operand 112 states and 122 transitions.
[2025-05-07 17:29:23,630 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:29:23,630 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:23,630 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]
[2025-05-07 17:29:23,630 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:29:23,630 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:23,631 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:23,631 INFO  L85        PathProgramCache]: Analyzing trace with hash 1998068929, now seen corresponding path program 1 times
[2025-05-07 17:29:23,631 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:23,631 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [205658590]
[2025-05-07 17:29:23,631 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:23,631 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:23,673 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:29:23,692 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:29:23,693 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:23,693 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:23,822 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:29:23,822 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:23,822 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [205658590]
[2025-05-07 17:29:23,822 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [205658590] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:23,823 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:23,823 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:29:23,823 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1375983749]
[2025-05-07 17:29:23,823 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:23,823 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:29:23,824 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:23,824 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:29:23,824 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:29:23,824 INFO  L87              Difference]: Start difference. First operand 112 states and 122 transitions. Second operand  has 8 states, 6 states have (on average 6.833333333333333) internal successors, (41), 8 states have internal predecessors, (41), 6 states have call successors, (26), 1 states have call predecessors, (26), 6 states have return successors, (26), 6 states have call predecessors, (26), 6 states have call successors, (26)
[2025-05-07 17:29:23,885 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:23,885 INFO  L93              Difference]: Finished difference Result 117 states and 128 transitions.
[2025-05-07 17:29:23,886 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:29:23,886 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 6.833333333333333) internal successors, (41), 8 states have internal predecessors, (41), 6 states have call successors, (26), 1 states have call predecessors, (26), 6 states have return successors, (26), 6 states have call predecessors, (26), 6 states have call successors, (26) Word has length 93
[2025-05-07 17:29:23,886 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:23,886 INFO  L225             Difference]: With dead ends: 117
[2025-05-07 17:29:23,887 INFO  L226             Difference]: Without dead ends: 117
[2025-05-07 17:29:23,887 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:29:23,887 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 2 mSDsluCounter, 638 mSDsCounter, 0 mSdLazyCounter, 47 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 748 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 47 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:23,887 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 748 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 47 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:23,888 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-05-07 17:29:23,892 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 117.
[2025-05-07 17:29:23,893 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 50 states have (on average 1.02) internal successors, (51), 51 states have internal predecessors, (51), 33 states have call successors, (35), 28 states have call predecessors, (35), 33 states have return successors, (42), 37 states have call predecessors, (42), 33 states have call successors, (42)
[2025-05-07 17:29:23,893 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 128 transitions.
[2025-05-07 17:29:23,893 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 128 transitions. Word has length 93
[2025-05-07 17:29:23,893 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:23,893 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 128 transitions.
[2025-05-07 17:29:23,893 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 6.833333333333333) internal successors, (41), 8 states have internal predecessors, (41), 6 states have call successors, (26), 1 states have call predecessors, (26), 6 states have return successors, (26), 6 states have call predecessors, (26), 6 states have call successors, (26)
[2025-05-07 17:29:23,894 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 128 transitions.
[2025-05-07 17:29:23,894 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-05-07 17:29:23,894 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:23,894 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]
[2025-05-07 17:29:23,894 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:29:23,895 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:23,895 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:23,895 INFO  L85        PathProgramCache]: Analyzing trace with hash -621794081, now seen corresponding path program 1 times
[2025-05-07 17:29:23,895 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:23,895 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1831613914]
[2025-05-07 17:29:23,895 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:23,895 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:23,923 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 93 statements into 1 equivalence classes.
[2025-05-07 17:29:23,934 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 93 of 93 statements.
[2025-05-07 17:29:23,934 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:23,934 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:24,010 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:29:24,010 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:24,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1831613914]
[2025-05-07 17:29:24,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1831613914] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:24,010 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:24,010 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:24,010 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [261702344]
[2025-05-07 17:29:24,010 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:24,011 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:24,011 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:24,011 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:24,011 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:24,011 INFO  L87              Difference]: Start difference. First operand 117 states and 128 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 5 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 5 states have call successors, (26)
[2025-05-07 17:29:24,038 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:24,038 INFO  L93              Difference]: Finished difference Result 116 states and 124 transitions.
[2025-05-07 17:29:24,038 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:24,039 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 5 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 5 states have call successors, (26) Word has length 93
[2025-05-07 17:29:24,039 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:24,040 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:29:24,040 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:29:24,040 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:29:24,041 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 428 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 538 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:29:24,041 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 538 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:24,042 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:29:24,045 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 111.
[2025-05-07 17:29:24,046 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 111 states, 48 states have (on average 1.0208333333333333) internal successors, (49), 49 states have internal predecessors, (49), 31 states have call successors, (33), 28 states have call predecessors, (33), 31 states have return successors, (36), 33 states have call predecessors, (36), 31 states have call successors, (36)
[2025-05-07 17:29:24,046 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 118 transitions.
[2025-05-07 17:29:24,046 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 118 transitions. Word has length 93
[2025-05-07 17:29:24,047 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:24,047 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 118 transitions.
[2025-05-07 17:29:24,047 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 5 states have call successors, (26), 1 states have call predecessors, (26), 5 states have return successors, (26), 5 states have call predecessors, (26), 5 states have call successors, (26)
[2025-05-07 17:29:24,047 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 118 transitions.
[2025-05-07 17:29:24,047 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 119
[2025-05-07 17:29:24,048 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:24,048 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:29:24,048 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:29:24,048 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:24,048 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:24,048 INFO  L85        PathProgramCache]: Analyzing trace with hash -471144788, now seen corresponding path program 1 times
[2025-05-07 17:29:24,048 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:24,048 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1108018743]
[2025-05-07 17:29:24,048 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:24,048 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:24,083 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 118 statements into 1 equivalence classes.
[2025-05-07 17:29:24,088 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 118 of 118 statements.
[2025-05-07 17:29:24,088 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:24,088 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:24,178 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:29:24,178 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:24,178 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1108018743]
[2025-05-07 17:29:24,178 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1108018743] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:24,178 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:24,179 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:24,179 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1738460662]
[2025-05-07 17:29:24,179 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:24,179 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:24,179 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:24,179 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:24,179 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:24,179 INFO  L87              Difference]: Start difference. First operand 111 states and 118 transitions. Second operand  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (32), 5 states have call predecessors, (32), 5 states have call successors, (32)
[2025-05-07 17:29:24,208 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:24,208 INFO  L93              Difference]: Finished difference Result 111 states and 117 transitions.
[2025-05-07 17:29:24,209 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:24,209 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (32), 5 states have call predecessors, (32), 5 states have call successors, (32) Word has length 118
[2025-05-07 17:29:24,209 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:24,210 INFO  L225             Difference]: With dead ends: 111
[2025-05-07 17:29:24,210 INFO  L226             Difference]: Without dead ends: 111
[2025-05-07 17:29:24,210 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:29:24,210 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 424 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 533 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:29:24,210 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 533 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:24,211 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 111 states.
[2025-05-07 17:29:24,213 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 111 to 111.
[2025-05-07 17:29:24,213 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 111 states, 48 states have (on average 1.0208333333333333) internal successors, (49), 49 states have internal predecessors, (49), 31 states have call successors, (33), 28 states have call predecessors, (33), 31 states have return successors, (35), 33 states have call predecessors, (35), 31 states have call successors, (35)
[2025-05-07 17:29:24,214 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 117 transitions.
[2025-05-07 17:29:24,214 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 117 transitions. Word has length 118
[2025-05-07 17:29:24,214 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:24,214 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 117 transitions.
[2025-05-07 17:29:24,214 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (32), 5 states have call predecessors, (32), 5 states have call successors, (32)
[2025-05-07 17:29:24,215 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 117 transitions.
[2025-05-07 17:29:24,215 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 119
[2025-05-07 17:29:24,215 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:24,215 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:24,215 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:29:24,216 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:24,216 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:24,216 INFO  L85        PathProgramCache]: Analyzing trace with hash 845371210, now seen corresponding path program 1 times
[2025-05-07 17:29:24,216 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:24,216 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [548256693]
[2025-05-07 17:29:24,216 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:24,216 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:24,254 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 118 statements into 1 equivalence classes.
[2025-05-07 17:29:24,262 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 118 of 118 statements.
[2025-05-07 17:29:24,262 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:24,262 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:24,369 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:29:24,370 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:24,370 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [548256693]
[2025-05-07 17:29:24,370 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [548256693] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:24,370 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:24,370 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:24,370 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1130746920]
[2025-05-07 17:29:24,370 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:24,370 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:24,370 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:24,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:24,371 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:24,371 INFO  L87              Difference]: Start difference. First operand 111 states and 117 transitions. Second operand  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (32), 5 states have call predecessors, (32), 5 states have call successors, (32)
[2025-05-07 17:29:24,398 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:24,398 INFO  L93              Difference]: Finished difference Result 116 states and 122 transitions.
[2025-05-07 17:29:24,398 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:24,398 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (32), 5 states have call predecessors, (32), 5 states have call successors, (32) Word has length 118
[2025-05-07 17:29:24,399 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:24,399 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:29:24,399 INFO  L226             Difference]: Without dead ends: 107
[2025-05-07 17:29:24,400 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:29:24,400 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 1 mSDsluCounter, 444 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 559 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:24,401 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 559 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:24,401 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-05-07 17:29:24,405 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 107.
[2025-05-07 17:29:24,405 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 46 states have (on average 1.0217391304347827) internal successors, (47), 47 states have internal predecessors, (47), 30 states have call successors, (31), 27 states have call predecessors, (31), 30 states have return successors, (33), 32 states have call predecessors, (33), 30 states have call successors, (33)
[2025-05-07 17:29:24,406 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 111 transitions.
[2025-05-07 17:29:24,406 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 111 transitions. Word has length 118
[2025-05-07 17:29:24,407 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:24,407 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 111 transitions.
[2025-05-07 17:29:24,407 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.4) internal successors, (47), 6 states have internal predecessors, (47), 5 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (32), 5 states have call predecessors, (32), 5 states have call successors, (32)
[2025-05-07 17:29:24,407 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 111 transitions.
[2025-05-07 17:29:24,408 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 119
[2025-05-07 17:29:24,408 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:24,408 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:24,409 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:29:24,409 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:24,409 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:24,409 INFO  L85        PathProgramCache]: Analyzing trace with hash 1682888364, now seen corresponding path program 1 times
[2025-05-07 17:29:24,409 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:24,409 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1019786695]
[2025-05-07 17:29:24,409 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:24,410 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:24,450 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 118 statements into 1 equivalence classes.
[2025-05-07 17:29:24,464 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 118 of 118 statements.
[2025-05-07 17:29:24,464 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:24,464 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,229 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:29:25,230 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,230 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1019786695]
[2025-05-07 17:29:25,230 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1019786695] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:25,230 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [796455934]
[2025-05-07 17:29:25,230 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,230 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:25,233 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:25,235 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:25,236 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:29:25,561 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 118 statements into 1 equivalence classes.
[2025-05-07 17:29:25,749 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 118 of 118 statements.
[2025-05-07 17:29:25,749 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,749 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,756 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1581 conjuncts, 78 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:25,771 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:25,906 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:29:25,906 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:27,779 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 3 proven. 6 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:29:27,779 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [796455934] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:27,779 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:27,779 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [25, 25, 27] total 38
[2025-05-07 17:29:27,779 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1856189305]
[2025-05-07 17:29:27,779 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,780 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 38 states
[2025-05-07 17:29:27,780 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,781 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 38 interpolants.
[2025-05-07 17:29:27,781 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=96, Invalid=1310, Unknown=0, NotChecked=0, Total=1406
[2025-05-07 17:29:27,782 INFO  L87              Difference]: Start difference. First operand 107 states and 111 transitions. Second operand  has 38 states, 28 states have (on average 2.142857142857143) internal successors, (60), 33 states have internal predecessors, (60), 19 states have call successors, (40), 1 states have call predecessors, (40), 28 states have return successors, (47), 31 states have call predecessors, (47), 19 states have call successors, (47)
[2025-05-07 17:29:28,264 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,264 INFO  L93              Difference]: Finished difference Result 101 states and 105 transitions.
[2025-05-07 17:29:28,265 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 26 states. 
[2025-05-07 17:29:28,265 INFO  L79                 Accepts]: Start accepts. Automaton has  has 38 states, 28 states have (on average 2.142857142857143) internal successors, (60), 33 states have internal predecessors, (60), 19 states have call successors, (40), 1 states have call predecessors, (40), 28 states have return successors, (47), 31 states have call predecessors, (47), 19 states have call successors, (47) Word has length 118
[2025-05-07 17:29:28,265 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,265 INFO  L225             Difference]: With dead ends: 101
[2025-05-07 17:29:28,266 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:29:28,266 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 268 GetRequests, 227 SyntacticMatches, 0 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 91 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=125, Invalid=1681, Unknown=0, NotChecked=0, Total=1806
[2025-05-07 17:29:28,267 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 6 mSDsluCounter, 2351 mSDsCounter, 0 mSdLazyCounter, 634 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 2436 SdHoareTripleChecker+Invalid, 638 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 634 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,267 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 2436 Invalid, 638 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 634 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:29:28,267 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:29:28,267 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:29:28,267 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:29:28,267 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:29:28,267 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 118
[2025-05-07 17:29:28,267 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,267 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:29:28,268 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 38 states, 28 states have (on average 2.142857142857143) internal successors, (60), 33 states have internal predecessors, (60), 19 states have call successors, (40), 1 states have call predecessors, (40), 28 states have return successors, (47), 31 states have call predecessors, (47), 19 states have call successors, (47)
[2025-05-07 17:29:28,268 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:29:28,268 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:29:28,270 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:29:28,276 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:29:28,471 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-05-07 17:29:28,478 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,480 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:29:28,482 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:29:28 BoogieIcfgContainer
[2025-05-07 17:29:28,482 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:29:28,483 INFO  L158              Benchmark]: Toolchain (without parser) took 7474.20ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 150.9MB in the beginning and 169.0MB in the end (delta: -18.1MB). Peak memory consumption was 102.8MB. Max. memory is 33.6GB.
[2025-05-07 17:29:28,483 INFO  L158              Benchmark]: SmtParser took 0.26ms. Allocated memory is still 234.9MB. Free memory is still 173.5MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:28,483 INFO  L158              Benchmark]: ChcToBoogie took 28.55ms. Allocated memory is still 234.9MB. Free memory was 150.8MB in the beginning and 147.5MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:28,484 INFO  L158              Benchmark]: Boogie Preprocessor took 52.80ms. Allocated memory is still 234.9MB. Free memory was 147.3MB in the beginning and 144.0MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:28,484 INFO  L158              Benchmark]: RCFGBuilder took 414.59ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 144.0MB in the beginning and 263.0MB in the end (delta: -119.0MB). Peak memory consumption was 43.0MB. Max. memory is 33.6GB.
[2025-05-07 17:29:28,484 INFO  L158              Benchmark]: TraceAbstraction took 6974.41ms. Allocated memory was 318.8MB in the beginning and 352.3MB in the end (delta: 33.6MB). Free memory was 262.4MB in the beginning and 169.0MB in the end (delta: 93.4MB). Peak memory consumption was 126.9MB. Max. memory is 33.6GB.
[2025-05-07 17:29:28,485 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.26ms. Allocated memory is still 234.9MB. Free memory is still 173.5MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 28.55ms. Allocated memory is still 234.9MB. Free memory was 150.8MB in the beginning and 147.5MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 52.80ms. Allocated memory is still 234.9MB. Free memory was 147.3MB in the beginning and 144.0MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 414.59ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 144.0MB in the beginning and 263.0MB in the end (delta: -119.0MB). Peak memory consumption was 43.0MB. Max. memory is 33.6GB.
 * TraceAbstraction took 6974.41ms. Allocated memory was 318.8MB in the beginning and 352.3MB in the end (delta: 33.6MB). Free memory was 262.4MB in the beginning and 169.0MB in the end (delta: 93.4MB). Peak memory consumption was 126.9MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 29 procedures, 115 locations, 175 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 6.9s, OverallIterations: 9, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 48 SdHoareTripleChecker+Valid, 0.8s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 19 mSDsluCounter, 7881 SdHoareTripleChecker+Invalid, 0.7s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 6889 mSDsCounter, 6 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1128 IncrementalHoareTripleChecker+Invalid, 1134 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 6 mSolverCounterUnsat, 992 mSDtfsCounter, 1128 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 332 GetRequests, 243 SyntacticMatches, 0 SemanticMatches, 89 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 94 ImplicationChecksByTransitivity, 0.9s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=117occurred in iteration=5, InterpolantAutomatonStates: 86, 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, 9 MinimizatonAttempts, 9 StatesRemovedByMinimization, 3 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.2s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 4.4s InterpolantComputationTime, 1011 NumberOfCodeBlocks, 1011 NumberOfCodeBlocksAsserted, 10 NumberOfCheckSat, 1118 ConstructedInterpolants, 0 QuantifiedInterpolants, 1792 SizeOfPredicates, 5 NumberOfNonLiveVariables, 1581 ConjunctsInSsa, 78 ConjunctsInUnsatCore, 11 InterpolantComputations, 8 PerfectInterpolantSequences, 83/99 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:29:28,496 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
