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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:31,010 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:31,046 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6cc1b41e-edae-49a4-9dbc-ade988739f89/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:31,049 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:31,049 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:31,062 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:31,062 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:31,062 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:31,062 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:31,062 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:31,063 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:31,063 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:31,063 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:31,063 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:31,063 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:31,064 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:31,064 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:31,244 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:31,252 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:31,255 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:31,256 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:31,256 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:31,257 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6cc1b41e-edae-49a4-9dbc-ade988739f89/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol_2_no_adts_000.smt2
[2025-05-07 17:28:31,259 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:31,262 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:31,587 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6cc1b41e-edae-49a4-9dbc-ade988739f89/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol_2_no_adts_000.smt2
[2025-05-07 17:28:31,589 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:31,591 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:31,591 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:31,591 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:31,591 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:31,593 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,638 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31 Unit
[2025-05-07 17:28:31,638 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:31,639 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:31,639 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:31,639 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:31,651 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,651 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,684 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,684 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,694 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,696 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,698 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,703 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,705 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,723 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:31,724 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:31,724 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:31,724 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:31,725 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (1/1) ...
[2025-05-07 17:28:31,727 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:31,740 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:31,749 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:28:31,752 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:28:31,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:31,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:31,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_4_0 given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_4_0
[2025-05-07 17:28:31,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_4_0
[2025-05-07 17:28:31,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_C_94_0 given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_C_94_0
[2025-05-07 17:28:31,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_C_94_0
[2025-05-07 17:28:31,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_71_C_94_0 given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_71_C_94_0
[2025-05-07 17:28:31,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_71_C_94_0
[2025-05-07 17:28:31,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_73_C_94_0 given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_73_C_94_0
[2025-05-07 17:28:31,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_73_C_94_0
[2025-05-07 17:28:31,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_72_C_94_0 given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_72_C_94_0
[2025-05-07 17:28:31,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_72_C_94_0
[2025-05-07 17:28:31,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_constructor_93_94_0 given in one single declaration
[2025-05-07 17:28:31,760 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_constructor_93_94_0 given in one single declaration
[2025-05-07 17:28:31,761 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_66__92_94_0 given in one single declaration
[2025-05-07 17:28:31,761 INFO  L130     BoogieDeclarations]: Found specification of procedure block_66__92_94_0
[2025-05-07 17:28:31,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_66__92_94_0
[2025-05-07 17:28:31,761 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_65_constructor_93_94_0 given in one single declaration
[2025-05-07 17:28:31,761 INFO  L130     BoogieDeclarations]: Found specification of procedure block_65_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_65_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_return_constructor_93_94_0 given in one single declaration
[2025-05-07 17:28:31,761 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_return_constructor_93_94_0
[2025-05-07 17:28:31,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_return_constructor_93_94_0
[2025-05-07 17:28:31,771 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_constructor_93_94_0 given in one single declaration
[2025-05-07 17:28:31,771 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_constructor_93_94_0
[2025-05-07 17:28:31,771 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_constructor_93_94_0
[2025-05-07 17:28:31,771 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_constructor_93_94_0 given in one single declaration
[2025-05-07 17:28:31,771 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_constructor_93_94_0
[2025-05-07 17:28:31,771 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_constructor_93_94_0
[2025-05-07 17:28:31,772 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_77_B_42_0 given in one single declaration
[2025-05-07 17:28:31,772 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_77_B_42_0
[2025-05-07 17:28:31,772 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_77_B_42_0
[2025-05-07 17:28:31,772 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_constructor_27_94_0 given in one single declaration
[2025-05-07 17:28:31,772 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_constructor_27_94_0
[2025-05-07 17:28:31,772 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_constructor_27_94_0
[2025-05-07 17:28:31,772 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_76_return_constructor_27_94_0 given in one single declaration
[2025-05-07 17:28:31,772 INFO  L130     BoogieDeclarations]: Found specification of procedure block_76_return_constructor_27_94_0
[2025-05-07 17:28:31,772 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_76_return_constructor_27_94_0
[2025-05-07 17:28:31,772 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_75__26_94_0 given in one single declaration
[2025-05-07 17:28:31,772 INFO  L130     BoogieDeclarations]: Found specification of procedure block_75__26_94_0
[2025-05-07 17:28:31,772 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_75__26_94_0
[2025-05-07 17:28:31,772 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_74_constructor_27_94_0 given in one single declaration
[2025-05-07 17:28:31,772 INFO  L130     BoogieDeclarations]: Found specification of procedure block_74_constructor_27_94_0
[2025-05-07 17:28:31,772 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_74_constructor_27_94_0
[2025-05-07 17:28:31,773 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_79_B_42_0 given in one single declaration
[2025-05-07 17:28:31,773 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_79_B_42_0
[2025-05-07 17:28:31,773 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_79_B_42_0
[2025-05-07 17:28:31,773 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_78_B_42_0 given in one single declaration
[2025-05-07 17:28:31,773 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_78_B_42_0
[2025-05-07 17:28:31,773 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_78_B_42_0
[2025-05-07 17:28:31,773 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_93_function_f__41_94_0 given in one single declaration
[2025-05-07 17:28:31,773 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_93_function_f__41_94_0
[2025-05-07 17:28:31,773 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_93_function_f__41_94_0
[2025-05-07 17:28:31,773 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_f__41_94_0 given in one single declaration
[2025-05-07 17:28:31,773 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_f__41_94_0
[2025-05-07 17:28:31,773 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_f__41_94_0
[2025-05-07 17:28:31,773 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_63_return_function_f__41_94_0 given in one single declaration
[2025-05-07 17:28:31,773 INFO  L130     BoogieDeclarations]: Found specification of procedure block_63_return_function_f__41_94_0
[2025-05-07 17:28:31,774 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_63_return_function_f__41_94_0
[2025-05-07 17:28:31,774 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_62_f_40_94_0 given in one single declaration
[2025-05-07 17:28:31,774 INFO  L130     BoogieDeclarations]: Found specification of procedure block_62_f_40_94_0
[2025-05-07 17:28:31,774 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_62_f_40_94_0
[2025-05-07 17:28:31,774 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_61_function_f__41_94_0 given in one single declaration
[2025-05-07 17:28:31,774 INFO  L130     BoogieDeclarations]: Found specification of procedure block_61_function_f__41_94_0
[2025-05-07 17:28:31,774 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_61_function_f__41_94_0
[2025-05-07 17:28:31,774 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_83_Z_57_0 given in one single declaration
[2025-05-07 17:28:31,774 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_83_Z_57_0
[2025-05-07 17:28:31,774 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_83_Z_57_0
[2025-05-07 17:28:31,774 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_constructor_56_94_0 given in one single declaration
[2025-05-07 17:28:31,774 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_constructor_56_94_0
[2025-05-07 17:28:31,774 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_constructor_56_94_0
[2025-05-07 17:28:31,774 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_82_return_constructor_56_94_0 given in one single declaration
[2025-05-07 17:28:31,774 INFO  L130     BoogieDeclarations]: Found specification of procedure block_82_return_constructor_56_94_0
[2025-05-07 17:28:31,774 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_82_return_constructor_56_94_0
[2025-05-07 17:28:31,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_81__55_94_0 given in one single declaration
[2025-05-07 17:28:31,775 INFO  L130     BoogieDeclarations]: Found specification of procedure block_81__55_94_0
[2025-05-07 17:28:31,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_81__55_94_0
[2025-05-07 17:28:31,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_80_constructor_56_94_0 given in one single declaration
[2025-05-07 17:28:31,775 INFO  L130     BoogieDeclarations]: Found specification of procedure block_80_constructor_56_94_0
[2025-05-07 17:28:31,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_80_constructor_56_94_0
[2025-05-07 17:28:31,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_85_Z_57_0 given in one single declaration
[2025-05-07 17:28:31,775 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_85_Z_57_0
[2025-05-07 17:28:31,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_85_Z_57_0
[2025-05-07 17:28:31,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_84_Z_57_0 given in one single declaration
[2025-05-07 17:28:31,775 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_84_Z_57_0
[2025-05-07 17:28:31,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_84_Z_57_0
[2025-05-07 17:28:31,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_89_A_13_0 given in one single declaration
[2025-05-07 17:28:31,775 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_89_A_13_0
[2025-05-07 17:28:31,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_89_A_13_0
[2025-05-07 17:28:31,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_constructor_12_94_0 given in one single declaration
[2025-05-07 17:28:31,775 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_constructor_12_94_0
[2025-05-07 17:28:31,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_constructor_12_94_0
[2025-05-07 17:28:31,776 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_88_return_constructor_12_94_0 given in one single declaration
[2025-05-07 17:28:31,776 INFO  L130     BoogieDeclarations]: Found specification of procedure block_88_return_constructor_12_94_0
[2025-05-07 17:28:31,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_88_return_constructor_12_94_0
[2025-05-07 17:28:31,776 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_87__11_94_0 given in one single declaration
[2025-05-07 17:28:31,776 INFO  L130     BoogieDeclarations]: Found specification of procedure block_87__11_94_0
[2025-05-07 17:28:31,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_87__11_94_0
[2025-05-07 17:28:31,776 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_86_constructor_12_94_0 given in one single declaration
[2025-05-07 17:28:31,776 INFO  L130     BoogieDeclarations]: Found specification of procedure block_86_constructor_12_94_0
[2025-05-07 17:28:31,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_86_constructor_12_94_0
[2025-05-07 17:28:31,776 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_91_A_13_0 given in one single declaration
[2025-05-07 17:28:31,776 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_91_A_13_0
[2025-05-07 17:28:31,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_91_A_13_0
[2025-05-07 17:28:31,776 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_90_A_13_0 given in one single declaration
[2025-05-07 17:28:31,776 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_90_A_13_0
[2025-05-07 17:28:31,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_90_A_13_0
[2025-05-07 17:28:31,776 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_92_C_94_0 given in one single declaration
[2025-05-07 17:28:31,776 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_92_C_94_0
[2025-05-07 17:28:31,776 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_92_C_94_0
[2025-05-07 17:28:31,777 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:31,777 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:31,777 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:31,960 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:31,962 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:32,261 INFO  L?                        ?]: Removed 417 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:32,261 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:32,270 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:32,271 INFO  L312             CfgBuilder]: Removed 19 assume(true) statements.
[2025-05-07 17:28:32,271 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:32 BoogieIcfgContainer
[2025-05-07 17:28:32,271 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:32,272 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:32,272 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:32,275 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:32,275 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:31" (1/3) ...
[2025-05-07 17:28:32,275 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@69dc226d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:32, skipping insertion in model container
[2025-05-07 17:28:32,275 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:31" (2/3) ...
[2025-05-07 17:28:32,276 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@69dc226d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:32, skipping insertion in model container
[2025-05-07 17:28:32,276 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:32" (3/3) ...
[2025-05-07 17:28:32,276 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:32,286 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:32,288 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 41 procedures, 176 locations, 289 edges, 41 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:32,318 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:32,327 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;@7cce58dd, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:32,327 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:32,330 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 176 states, 66 states have (on average 1.1515151515151516) internal successors, (76), 76 states have internal predecessors, (76), 68 states have call successors, (71), 40 states have call predecessors, (71), 40 states have return successors, (71), 59 states have call predecessors, (71), 68 states have call successors, (71)
[2025-05-07 17:28:32,338 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-05-07 17:28:32,338 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:32,338 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]
[2025-05-07 17:28:32,339 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:32,342 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:32,342 INFO  L85        PathProgramCache]: Analyzing trace with hash 461503987, now seen corresponding path program 1 times
[2025-05-07 17:28:32,348 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:32,348 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1347654080]
[2025-05-07 17:28:32,348 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:32,349 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:32,380 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-05-07 17:28:32,426 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-05-07 17:28:32,426 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:32,426 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:32,647 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:32,647 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:32,647 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1347654080]
[2025-05-07 17:28:32,648 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1347654080] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:32,648 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:32,650 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:32,651 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [767450102]
[2025-05-07 17:28:32,651 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:32,653 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:32,654 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:32,683 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:32,684 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:32,686 INFO  L87              Difference]: Start difference. First operand  has 176 states, 66 states have (on average 1.1515151515151516) internal successors, (76), 76 states have internal predecessors, (76), 68 states have call successors, (71), 40 states have call predecessors, (71), 40 states have return successors, (71), 59 states have call predecessors, (71), 68 states have call successors, (71) Second operand  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-05-07 17:28:32,845 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:32,845 INFO  L93              Difference]: Finished difference Result 176 states and 217 transitions.
[2025-05-07 17:28:32,846 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:32,847 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9) Word has length 33
[2025-05-07 17:28:32,847 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:32,853 INFO  L225             Difference]: With dead ends: 176
[2025-05-07 17:28:32,853 INFO  L226             Difference]: Without dead ends: 174
[2025-05-07 17:28:32,855 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:32,857 INFO  L437           NwaCegarLoop]: 206 mSDtfsCounter, 1 mSDsluCounter, 993 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 1199 SdHoareTripleChecker+Invalid, 62 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:32,857 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 1199 Invalid, 62 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:32,867 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 174 states.
[2025-05-07 17:28:32,886 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 174 to 172.
[2025-05-07 17:28:32,887 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 172 states, 65 states have (on average 1.123076923076923) internal successors, (73), 73 states have internal predecessors, (73), 66 states have call successors, (69), 40 states have call predecessors, (69), 40 states have return successors, (69), 58 states have call predecessors, (69), 66 states have call successors, (69)
[2025-05-07 17:28:32,891 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 172 states to 172 states and 211 transitions.
[2025-05-07 17:28:32,892 INFO  L79                 Accepts]: Start accepts. Automaton has 172 states and 211 transitions. Word has length 33
[2025-05-07 17:28:32,892 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:32,893 INFO  L485      AbstractCegarLoop]: Abstraction has 172 states and 211 transitions.
[2025-05-07 17:28:32,893 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-05-07 17:28:32,893 INFO  L278                IsEmpty]: Start isEmpty. Operand 172 states and 211 transitions.
[2025-05-07 17:28:32,895 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:28:32,895 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:32,895 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]
[2025-05-07 17:28:32,895 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:32,896 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:32,896 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:32,896 INFO  L85        PathProgramCache]: Analyzing trace with hash 1687691504, now seen corresponding path program 1 times
[2025-05-07 17:28:32,896 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:32,896 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1141977462]
[2025-05-07 17:28:32,897 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:32,897 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:32,928 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:28:32,946 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:28:32,946 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:32,946 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:33,019 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:33,019 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:33,019 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1141977462]
[2025-05-07 17:28:33,019 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1141977462] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:33,020 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:33,020 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:33,020 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [839352936]
[2025-05-07 17:28:33,020 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:33,021 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:33,021 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:33,022 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:33,022 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:33,022 INFO  L87              Difference]: Start difference. First operand 172 states and 211 transitions. Second operand  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 4 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:28:33,087 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:33,087 INFO  L93              Difference]: Finished difference Result 176 states and 218 transitions.
[2025-05-07 17:28:33,088 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:33,088 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 4 states have call predecessors, (16), 3 states have call successors, (16) Word has length 58
[2025-05-07 17:28:33,088 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:33,090 INFO  L225             Difference]: With dead ends: 176
[2025-05-07 17:28:33,090 INFO  L226             Difference]: Without dead ends: 176
[2025-05-07 17:28:33,090 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:33,091 INFO  L437           NwaCegarLoop]: 211 mSDtfsCounter, 1 mSDsluCounter, 388 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 599 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:33,091 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 599 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:33,091 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 176 states.
[2025-05-07 17:28:33,100 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 176 to 174.
[2025-05-07 17:28:33,100 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 174 states, 66 states have (on average 1.121212121212121) internal successors, (74), 74 states have internal predecessors, (74), 66 states have call successors, (69), 40 states have call predecessors, (69), 41 states have return successors, (73), 59 states have call predecessors, (73), 66 states have call successors, (73)
[2025-05-07 17:28:33,101 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 174 states to 174 states and 216 transitions.
[2025-05-07 17:28:33,102 INFO  L79                 Accepts]: Start accepts. Automaton has 174 states and 216 transitions. Word has length 58
[2025-05-07 17:28:33,102 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:33,102 INFO  L485      AbstractCegarLoop]: Abstraction has 174 states and 216 transitions.
[2025-05-07 17:28:33,102 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 4 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:28:33,102 INFO  L278                IsEmpty]: Start isEmpty. Operand 174 states and 216 transitions.
[2025-05-07 17:28:33,103 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:28:33,103 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:33,103 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]
[2025-05-07 17:28:33,104 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:33,104 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:33,104 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:33,104 INFO  L85        PathProgramCache]: Analyzing trace with hash 609217652, now seen corresponding path program 1 times
[2025-05-07 17:28:33,104 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:33,104 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1141238031]
[2025-05-07 17:28:33,104 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:33,104 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:33,128 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:28:33,144 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:28:33,144 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:33,145 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:33,233 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:33,233 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:33,233 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1141238031]
[2025-05-07 17:28:33,233 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1141238031] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:33,233 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:33,233 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:33,233 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1360432541]
[2025-05-07 17:28:33,234 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:33,234 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:33,234 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:33,235 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:33,235 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:33,235 INFO  L87              Difference]: Start difference. First operand 174 states and 216 transitions. Second operand  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:28:33,287 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:33,287 INFO  L93              Difference]: Finished difference Result 172 states and 209 transitions.
[2025-05-07 17:28:33,287 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:33,287 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16) Word has length 58
[2025-05-07 17:28:33,288 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:33,289 INFO  L225             Difference]: With dead ends: 172
[2025-05-07 17:28:33,289 INFO  L226             Difference]: Without dead ends: 167
[2025-05-07 17:28:33,289 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:33,289 INFO  L437           NwaCegarLoop]: 206 mSDtfsCounter, 0 mSDsluCounter, 807 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1013 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:33,290 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1013 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:33,291 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 167 states.
[2025-05-07 17:28:33,296 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 167 to 167.
[2025-05-07 17:28:33,297 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 167 states, 65 states have (on average 1.0923076923076922) internal successors, (71), 71 states have internal predecessors, (71), 61 states have call successors, (64), 40 states have call predecessors, (64), 40 states have return successors, (64), 55 states have call predecessors, (64), 61 states have call successors, (64)
[2025-05-07 17:28:33,298 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 167 states to 167 states and 199 transitions.
[2025-05-07 17:28:33,298 INFO  L79                 Accepts]: Start accepts. Automaton has 167 states and 199 transitions. Word has length 58
[2025-05-07 17:28:33,298 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:33,298 INFO  L485      AbstractCegarLoop]: Abstraction has 167 states and 199 transitions.
[2025-05-07 17:28:33,298 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:28:33,298 INFO  L278                IsEmpty]: Start isEmpty. Operand 167 states and 199 transitions.
[2025-05-07 17:28:33,300 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:33,300 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:33,300 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]
[2025-05-07 17:28:33,300 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:33,300 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:33,301 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:33,301 INFO  L85        PathProgramCache]: Analyzing trace with hash -859423122, now seen corresponding path program 1 times
[2025-05-07 17:28:33,301 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:33,301 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [476397354]
[2025-05-07 17:28:33,301 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:33,301 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:33,340 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:33,377 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:33,378 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:33,378 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:33,483 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:33,483 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:33,483 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [476397354]
[2025-05-07 17:28:33,483 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [476397354] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:33,483 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:33,483 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:33,483 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2120672411]
[2025-05-07 17:28:33,483 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:33,484 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:33,484 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:33,484 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:33,485 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:33,485 INFO  L87              Difference]: Start difference. First operand 167 states and 199 transitions. Second operand  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:33,527 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:33,527 INFO  L93              Difference]: Finished difference Result 167 states and 198 transitions.
[2025-05-07 17:28:33,528 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:33,528 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23) Word has length 83
[2025-05-07 17:28:33,528 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:33,530 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:28:33,530 INFO  L226             Difference]: Without dead ends: 165
[2025-05-07 17:28:33,530 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:33,531 INFO  L437           NwaCegarLoop]: 195 mSDtfsCounter, 0 mSDsluCounter, 764 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 959 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:33,531 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 959 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:33,532 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-05-07 17:28:33,540 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 165.
[2025-05-07 17:28:33,540 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 165 states, 65 states have (on average 1.0769230769230769) internal successors, (70), 70 states have internal predecessors, (70), 59 states have call successors, (62), 40 states have call predecessors, (62), 40 states have return successors, (62), 54 states have call predecessors, (62), 59 states have call successors, (62)
[2025-05-07 17:28:33,542 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 165 states to 165 states and 194 transitions.
[2025-05-07 17:28:33,542 INFO  L79                 Accepts]: Start accepts. Automaton has 165 states and 194 transitions. Word has length 83
[2025-05-07 17:28:33,542 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:33,543 INFO  L485      AbstractCegarLoop]: Abstraction has 165 states and 194 transitions.
[2025-05-07 17:28:33,543 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:33,543 INFO  L278                IsEmpty]: Start isEmpty. Operand 165 states and 194 transitions.
[2025-05-07 17:28:33,544 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:33,544 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:33,545 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]
[2025-05-07 17:28:33,545 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:33,545 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:33,545 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:33,545 INFO  L85        PathProgramCache]: Analyzing trace with hash -1686738070, now seen corresponding path program 1 times
[2025-05-07 17:28:33,545 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:33,546 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [200663790]
[2025-05-07 17:28:33,546 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:33,546 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:33,580 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:33,589 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:33,589 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:33,589 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:33,649 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:33,649 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:33,649 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [200663790]
[2025-05-07 17:28:33,649 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [200663790] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:33,649 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:33,649 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:33,649 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [373625965]
[2025-05-07 17:28:33,649 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:33,650 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:33,650 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:33,650 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:33,650 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:33,650 INFO  L87              Difference]: Start difference. First operand 165 states and 194 transitions. Second operand  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:33,688 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:33,689 INFO  L93              Difference]: Finished difference Result 166 states and 193 transitions.
[2025-05-07 17:28:33,689 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:33,689 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 4 states have call successors, (23) Word has length 83
[2025-05-07 17:28:33,689 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:33,690 INFO  L225             Difference]: With dead ends: 166
[2025-05-07 17:28:33,690 INFO  L226             Difference]: Without dead ends: 163
[2025-05-07 17:28:33,690 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:33,690 INFO  L437           NwaCegarLoop]: 187 mSDtfsCounter, 1 mSDsluCounter, 350 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 537 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:33,691 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 537 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:33,691 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 163 states.
[2025-05-07 17:28:33,695 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 163 to 161.
[2025-05-07 17:28:33,695 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 161 states, 65 states have (on average 1.0615384615384615) internal successors, (69), 69 states have internal predecessors, (69), 55 states have call successors, (58), 40 states have call predecessors, (58), 40 states have return successors, (58), 51 states have call predecessors, (58), 55 states have call successors, (58)
[2025-05-07 17:28:33,696 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 185 transitions.
[2025-05-07 17:28:33,696 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 185 transitions. Word has length 83
[2025-05-07 17:28:33,696 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:33,696 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 185 transitions.
[2025-05-07 17:28:33,696 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:28:33,696 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 185 transitions.
[2025-05-07 17:28:33,697 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 109
[2025-05-07 17:28:33,697 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:33,698 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:33,698 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:33,698 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:33,698 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:33,698 INFO  L85        PathProgramCache]: Analyzing trace with hash -470462882, now seen corresponding path program 1 times
[2025-05-07 17:28:33,698 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:33,698 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2113412056]
[2025-05-07 17:28:33,698 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:33,698 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:33,728 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 108 statements into 1 equivalence classes.
[2025-05-07 17:28:33,749 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 108 of 108 statements.
[2025-05-07 17:28:33,749 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:33,749 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:33,854 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:33,854 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:33,855 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2113412056]
[2025-05-07 17:28:33,855 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2113412056] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:33,855 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:33,855 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:33,855 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [509792397]
[2025-05-07 17:28:33,855 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:33,855 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:33,855 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:33,856 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:33,856 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:33,856 INFO  L87              Difference]: Start difference. First operand 161 states and 185 transitions. Second operand  has 6 states, 5 states have (on average 9.6) internal successors, (48), 6 states have internal predecessors, (48), 4 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 4 states have call successors, (30)
[2025-05-07 17:28:33,893 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:33,893 INFO  L93              Difference]: Finished difference Result 161 states and 184 transitions.
[2025-05-07 17:28:33,894 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:33,894 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.6) internal successors, (48), 6 states have internal predecessors, (48), 4 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 4 states have call successors, (30) Word has length 108
[2025-05-07 17:28:33,894 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:33,895 INFO  L225             Difference]: With dead ends: 161
[2025-05-07 17:28:33,895 INFO  L226             Difference]: Without dead ends: 159
[2025-05-07 17:28:33,895 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:33,895 INFO  L437           NwaCegarLoop]: 181 mSDtfsCounter, 0 mSDsluCounter, 709 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 890 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:33,896 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 890 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:33,896 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 159 states.
[2025-05-07 17:28:33,899 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 159 to 159.
[2025-05-07 17:28:33,900 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 65 states have (on average 1.0461538461538462) internal successors, (68), 68 states have internal predecessors, (68), 53 states have call successors, (56), 40 states have call predecessors, (56), 40 states have return successors, (56), 50 states have call predecessors, (56), 53 states have call successors, (56)
[2025-05-07 17:28:33,900 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 180 transitions.
[2025-05-07 17:28:33,900 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 180 transitions. Word has length 108
[2025-05-07 17:28:33,900 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:33,901 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 180 transitions.
[2025-05-07 17:28:33,901 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.6) internal successors, (48), 6 states have internal predecessors, (48), 4 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 4 states have call successors, (30)
[2025-05-07 17:28:33,901 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 180 transitions.
[2025-05-07 17:28:33,901 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 109
[2025-05-07 17:28:33,901 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:33,902 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:33,902 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:33,902 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:33,902 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:33,902 INFO  L85        PathProgramCache]: Analyzing trace with hash 1147653594, now seen corresponding path program 1 times
[2025-05-07 17:28:33,902 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:33,902 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1077774482]
[2025-05-07 17:28:33,902 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:33,902 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:33,941 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 108 statements into 1 equivalence classes.
[2025-05-07 17:28:33,949 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 108 of 108 statements.
[2025-05-07 17:28:33,949 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:33,949 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,012 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:34,012 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,012 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1077774482]
[2025-05-07 17:28:34,012 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1077774482] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,012 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,012 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:34,012 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1191203755]
[2025-05-07 17:28:34,012 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,013 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:34,013 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,013 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:34,013 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,013 INFO  L87              Difference]: Start difference. First operand 159 states and 180 transitions. Second operand  has 4 states, 3 states have (on average 16.0) internal successors, (48), 4 states have internal predecessors, (48), 4 states have call successors, (30), 1 states have call predecessors, (30), 3 states have return successors, (30), 4 states have call predecessors, (30), 4 states have call successors, (30)
[2025-05-07 17:28:34,043 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,043 INFO  L93              Difference]: Finished difference Result 158 states and 175 transitions.
[2025-05-07 17:28:34,044 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:34,044 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 16.0) internal successors, (48), 4 states have internal predecessors, (48), 4 states have call successors, (30), 1 states have call predecessors, (30), 3 states have return successors, (30), 4 states have call predecessors, (30), 4 states have call successors, (30) Word has length 108
[2025-05-07 17:28:34,044 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,045 INFO  L225             Difference]: With dead ends: 158
[2025-05-07 17:28:34,045 INFO  L226             Difference]: Without dead ends: 156
[2025-05-07 17:28:34,045 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,045 INFO  L437           NwaCegarLoop]: 170 mSDtfsCounter, 1 mSDsluCounter, 323 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 493 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:34,045 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 493 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:34,046 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 156 states.
[2025-05-07 17:28:34,049 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 156 to 154.
[2025-05-07 17:28:34,049 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 154 states, 65 states have (on average 1.0307692307692307) internal successors, (67), 67 states have internal predecessors, (67), 48 states have call successors, (51), 40 states have call predecessors, (51), 40 states have return successors, (51), 46 states have call predecessors, (51), 48 states have call successors, (51)
[2025-05-07 17:28:34,050 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 169 transitions.
[2025-05-07 17:28:34,050 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 169 transitions. Word has length 108
[2025-05-07 17:28:34,050 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,050 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 169 transitions.
[2025-05-07 17:28:34,050 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 16.0) internal successors, (48), 4 states have internal predecessors, (48), 4 states have call successors, (30), 1 states have call predecessors, (30), 3 states have return successors, (30), 4 states have call predecessors, (30), 4 states have call successors, (30)
[2025-05-07 17:28:34,050 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 169 transitions.
[2025-05-07 17:28:34,051 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:28:34,051 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,051 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,051 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:34,051 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,051 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,051 INFO  L85        PathProgramCache]: Analyzing trace with hash -759130631, now seen corresponding path program 1 times
[2025-05-07 17:28:34,051 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,051 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [72965884]
[2025-05-07 17:28:34,051 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,052 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,102 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:28:34,123 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:28:34,123 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,123 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,218 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:34,219 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,219 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [72965884]
[2025-05-07 17:28:34,219 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [72965884] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,219 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,219 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:34,219 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [618864689]
[2025-05-07 17:28:34,219 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,219 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:34,220 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,220 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:34,220 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,220 INFO  L87              Difference]: Start difference. First operand 154 states and 169 transitions. Second operand  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 4 states have call predecessors, (37), 3 states have call successors, (37)
[2025-05-07 17:28:34,243 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,243 INFO  L93              Difference]: Finished difference Result 158 states and 173 transitions.
[2025-05-07 17:28:34,244 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:34,244 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 4 states have call predecessors, (37), 3 states have call successors, (37) Word has length 133
[2025-05-07 17:28:34,244 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,245 INFO  L225             Difference]: With dead ends: 158
[2025-05-07 17:28:34,245 INFO  L226             Difference]: Without dead ends: 158
[2025-05-07 17:28:34,245 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,246 INFO  L437           NwaCegarLoop]: 169 mSDtfsCounter, 1 mSDsluCounter, 322 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 491 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:34,246 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 491 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:34,247 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-05-07 17:28:34,252 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 156.
[2025-05-07 17:28:34,252 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 66 states have (on average 1.0303030303030303) internal successors, (68), 68 states have internal predecessors, (68), 48 states have call successors, (51), 40 states have call predecessors, (51), 41 states have return successors, (52), 47 states have call predecessors, (52), 48 states have call successors, (52)
[2025-05-07 17:28:34,254 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 171 transitions.
[2025-05-07 17:28:34,254 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 171 transitions. Word has length 133
[2025-05-07 17:28:34,255 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,255 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 171 transitions.
[2025-05-07 17:28:34,255 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 4 states have call predecessors, (37), 3 states have call successors, (37)
[2025-05-07 17:28:34,255 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 171 transitions.
[2025-05-07 17:28:34,256 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:28:34,256 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,257 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,257 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:34,257 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,257 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,257 INFO  L85        PathProgramCache]: Analyzing trace with hash 843078411, now seen corresponding path program 1 times
[2025-05-07 17:28:34,257 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,257 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [913951304]
[2025-05-07 17:28:34,258 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,258 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,303 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:28:34,306 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:28:34,306 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,306 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,397 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:34,397 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,397 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [913951304]
[2025-05-07 17:28:34,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [913951304] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,398 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,398 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:34,398 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1606463330]
[2025-05-07 17:28:34,398 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,398 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:34,398 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,399 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:34,399 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,399 INFO  L87              Difference]: Start difference. First operand 156 states and 171 transitions. Second operand  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 3 states have call predecessors, (37), 3 states have call successors, (37)
[2025-05-07 17:28:34,407 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,407 INFO  L93              Difference]: Finished difference Result 158 states and 172 transitions.
[2025-05-07 17:28:34,408 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:34,408 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 3 states have call predecessors, (37), 3 states have call successors, (37) Word has length 133
[2025-05-07 17:28:34,408 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,409 INFO  L225             Difference]: With dead ends: 158
[2025-05-07 17:28:34,409 INFO  L226             Difference]: Without dead ends: 146
[2025-05-07 17:28:34,409 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:34,409 INFO  L437           NwaCegarLoop]: 170 mSDtfsCounter, 1 mSDsluCounter, 327 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 497 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:34,409 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 497 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:34,410 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-05-07 17:28:34,412 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 146.
[2025-05-07 17:28:34,412 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 146 states, 65 states have (on average 1.0) internal successors, (65), 65 states have internal predecessors, (65), 40 states have call successors, (43), 40 states have call predecessors, (43), 40 states have return successors, (43), 40 states have call predecessors, (43), 40 states have call successors, (43)
[2025-05-07 17:28:34,413 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 146 states to 146 states and 151 transitions.
[2025-05-07 17:28:34,413 INFO  L79                 Accepts]: Start accepts. Automaton has 146 states and 151 transitions. Word has length 133
[2025-05-07 17:28:34,413 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,413 INFO  L485      AbstractCegarLoop]: Abstraction has 146 states and 151 transitions.
[2025-05-07 17:28:34,413 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 3 states have call predecessors, (37), 3 states have call successors, (37)
[2025-05-07 17:28:34,413 INFO  L278                IsEmpty]: Start isEmpty. Operand 146 states and 151 transitions.
[2025-05-07 17:28:34,414 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:28:34,414 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,414 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,414 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:34,414 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,414 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,415 INFO  L85        PathProgramCache]: Analyzing trace with hash -1866158649, now seen corresponding path program 1 times
[2025-05-07 17:28:34,415 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,415 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1444634133]
[2025-05-07 17:28:34,415 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,415 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,465 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:28:34,489 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:28:34,489 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,489 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,696 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:34,696 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,696 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1444634133]
[2025-05-07 17:28:34,696 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1444634133] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:34,696 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:34,696 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:34,697 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1428050576]
[2025-05-07 17:28:34,697 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:34,697 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:34,697 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:34,698 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:34,698 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:34,698 INFO  L87              Difference]: Start difference. First operand 146 states and 151 transitions. Second operand  has 7 states, 5 states have (on average 11.8) internal successors, (59), 7 states have internal predecessors, (59), 5 states have call successors, (37), 1 states have call predecessors, (37), 5 states have return successors, (37), 5 states have call predecessors, (37), 5 states have call successors, (37)
[2025-05-07 17:28:34,763 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:34,763 INFO  L93              Difference]: Finished difference Result 148 states and 152 transitions.
[2025-05-07 17:28:34,763 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:34,764 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 11.8) internal successors, (59), 7 states have internal predecessors, (59), 5 states have call successors, (37), 1 states have call predecessors, (37), 5 states have return successors, (37), 5 states have call predecessors, (37), 5 states have call successors, (37) Word has length 133
[2025-05-07 17:28:34,764 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:34,764 INFO  L225             Difference]: With dead ends: 148
[2025-05-07 17:28:34,764 INFO  L226             Difference]: Without dead ends: 142
[2025-05-07 17:28:34,765 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:34,765 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 710 mSDsCounter, 0 mSdLazyCounter, 42 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 856 SdHoareTripleChecker+Invalid, 42 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 42 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:34,765 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 856 Invalid, 42 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 42 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:34,766 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-05-07 17:28:34,768 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 142.
[2025-05-07 17:28:34,768 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 63 states have (on average 1.0) internal successors, (63), 63 states have internal predecessors, (63), 39 states have call successors, (41), 39 states have call predecessors, (41), 39 states have return successors, (41), 39 states have call predecessors, (41), 39 states have call successors, (41)
[2025-05-07 17:28:34,768 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 145 transitions.
[2025-05-07 17:28:34,769 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 145 transitions. Word has length 133
[2025-05-07 17:28:34,769 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:34,769 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 145 transitions.
[2025-05-07 17:28:34,769 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 11.8) internal successors, (59), 7 states have internal predecessors, (59), 5 states have call successors, (37), 1 states have call predecessors, (37), 5 states have return successors, (37), 5 states have call predecessors, (37), 5 states have call successors, (37)
[2025-05-07 17:28:34,769 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 145 transitions.
[2025-05-07 17:28:34,770 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:28:34,770 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:34,770 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:34,770 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:34,770 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,770 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,770 INFO  L85        PathProgramCache]: Analyzing trace with hash -1823016209, now seen corresponding path program 1 times
[2025-05-07 17:28:34,770 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,770 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1249024132]
[2025-05-07 17:28:34,770 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:34,771 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,827 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:28:34,860 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:28:34,860 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:34,860 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:35,007 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:35,008 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:35,008 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1249024132]
[2025-05-07 17:28:35,008 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1249024132] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:35,008 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:35,008 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:35,008 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [306295057]
[2025-05-07 17:28:35,008 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:35,008 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:35,008 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:35,009 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:35,009 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:35,009 INFO  L87              Difference]: Start difference. First operand 142 states and 145 transitions. Second operand  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:28:35,047 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:35,047 INFO  L93              Difference]: Finished difference Result 149 states and 152 transitions.
[2025-05-07 17:28:35,047 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:35,047 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37) Word has length 133
[2025-05-07 17:28:35,048 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:35,048 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:28:35,048 INFO  L226             Difference]: Without dead ends: 138
[2025-05-07 17:28:35,049 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:35,049 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 716 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 862 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:35,049 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 862 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:35,049 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-05-07 17:28:35,051 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 138.
[2025-05-07 17:28:35,052 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 61 states have (on average 1.0) internal successors, (61), 61 states have internal predecessors, (61), 38 states have call successors, (39), 38 states have call predecessors, (39), 38 states have return successors, (39), 38 states have call predecessors, (39), 38 states have call successors, (39)
[2025-05-07 17:28:35,052 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 139 transitions.
[2025-05-07 17:28:35,052 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 139 transitions. Word has length 133
[2025-05-07 17:28:35,052 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:35,052 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 139 transitions.
[2025-05-07 17:28:35,052 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:28:35,053 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 139 transitions.
[2025-05-07 17:28:35,053 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:28:35,054 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:35,054 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:35,054 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:35,054 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:35,054 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:35,054 INFO  L85        PathProgramCache]: Analyzing trace with hash -915419027, now seen corresponding path program 1 times
[2025-05-07 17:28:35,054 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:35,054 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1426923150]
[2025-05-07 17:28:35,054 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:35,054 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:35,093 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:28:35,133 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:28:35,133 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:35,133 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:37,699 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:37,699 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:37,699 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1426923150]
[2025-05-07 17:28:37,699 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1426923150] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:37,699 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:37,699 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [44] imperfect sequences [] total 44
[2025-05-07 17:28:37,699 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [4951299]
[2025-05-07 17:28:37,699 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:37,700 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 44 states
[2025-05-07 17:28:37,700 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:37,700 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 44 interpolants.
[2025-05-07 17:28:37,701 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=87, Invalid=1805, Unknown=0, NotChecked=0, Total=1892
[2025-05-07 17:28:37,701 INFO  L87              Difference]: Start difference. First operand 138 states and 139 transitions. Second operand  has 44 states, 31 states have (on average 1.903225806451613) internal successors, (59), 35 states have internal predecessors, (59), 19 states have call successors, (37), 1 states have call predecessors, (37), 31 states have return successors, (37), 34 states have call predecessors, (37), 19 states have call successors, (37)
[2025-05-07 17:28:38,839 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,839 INFO  L93              Difference]: Finished difference Result 143 states and 144 transitions.
[2025-05-07 17:28:38,839 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 44 states. 
[2025-05-07 17:28:38,840 INFO  L79                 Accepts]: Start accepts. Automaton has  has 44 states, 31 states have (on average 1.903225806451613) internal successors, (59), 35 states have internal predecessors, (59), 19 states have call successors, (37), 1 states have call predecessors, (37), 31 states have return successors, (37), 34 states have call predecessors, (37), 19 states have call successors, (37) Word has length 133
[2025-05-07 17:28:38,840 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,841 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:28:38,841 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:28:38,842 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 53 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 118 ImplicationChecksByTransitivity, 1.1s TimeCoverageRelationStatistics Valid=151, Invalid=2819, Unknown=0, NotChecked=0, Total=2970
[2025-05-07 17:28:38,842 INFO  L437           NwaCegarLoop]: 114 mSDtfsCounter, 11 mSDsluCounter, 4565 mSDsCounter, 0 mSdLazyCounter, 1255 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 4679 SdHoareTripleChecker+Invalid, 1270 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 1255 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,842 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 4679 Invalid, 1270 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 1255 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:28:38,843 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:28:38,846 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 134.
[2025-05-07 17:28:38,847 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 59 states have (on average 1.0) internal successors, (59), 59 states have internal predecessors, (59), 37 states have call successors, (37), 37 states have call predecessors, (37), 37 states have return successors, (37), 37 states have call predecessors, (37), 37 states have call successors, (37)
[2025-05-07 17:28:38,847 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 133 transitions.
[2025-05-07 17:28:38,847 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 133 transitions. Word has length 133
[2025-05-07 17:28:38,848 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,848 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 133 transitions.
[2025-05-07 17:28:38,848 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 44 states, 31 states have (on average 1.903225806451613) internal successors, (59), 35 states have internal predecessors, (59), 19 states have call successors, (37), 1 states have call predecessors, (37), 31 states have return successors, (37), 34 states have call predecessors, (37), 19 states have call successors, (37)
[2025-05-07 17:28:38,848 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 133 transitions.
[2025-05-07 17:28:38,849 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:28:38,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,850 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,850 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:28:38,850 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,850 INFO  L85        PathProgramCache]: Analyzing trace with hash -497675651, now seen corresponding path program 1 times
[2025-05-07 17:28:38,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,850 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1765116014]
[2025-05-07 17:28:38,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,908 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:28:38,930 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:28:38,930 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,930 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,072 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,073 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,073 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1765116014]
[2025-05-07 17:28:39,073 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1765116014] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,073 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,073 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:39,073 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2057236039]
[2025-05-07 17:28:39,073 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,073 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:39,074 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,074 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:39,074 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:39,074 INFO  L87              Difference]: Start difference. First operand 134 states and 133 transitions. Second operand  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:28:39,110 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,110 INFO  L93              Difference]: Finished difference Result 128 states and 127 transitions.
[2025-05-07 17:28:39,111 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:39,111 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37) Word has length 133
[2025-05-07 17:28:39,112 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,112 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:28:39,112 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:39,112 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:39,112 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 0 mSDsluCounter, 606 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 730 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,112 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 730 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,113 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:39,113 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:39,113 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:28:39,113 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:39,113 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 133
[2025-05-07 17:28:39,113 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,113 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:39,113 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:28:39,113 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:39,114 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:39,116 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:39,116 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:28:39,119 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,120 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:39,122 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:39 BoogieIcfgContainer
[2025-05-07 17:28:39,123 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:39,123 INFO  L158              Benchmark]: Toolchain (without parser) took 7532.76ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 133.7MB in the beginning and 300.0MB in the end (delta: -166.4MB). Peak memory consumption was 34.4MB. Max. memory is 33.6GB.
[2025-05-07 17:28:39,123 INFO  L158              Benchmark]: SmtParser took 0.30ms. Allocated memory is still 234.9MB. Free memory is still 173.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:39,123 INFO  L158              Benchmark]: ChcToBoogie took 47.58ms. Allocated memory is still 234.9MB. Free memory was 133.7MB in the beginning and 129.5MB in the end (delta: 4.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:39,123 INFO  L158              Benchmark]: Boogie Preprocessor took 83.81ms. Allocated memory is still 234.9MB. Free memory was 129.5MB in the beginning and 124.0MB in the end (delta: 5.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:39,124 INFO  L158              Benchmark]: RCFGBuilder took 547.24ms. Allocated memory is still 234.9MB. Free memory was 124.0MB in the beginning and 129.1MB in the end (delta: -5.0MB). Peak memory consumption was 25.2MB. Max. memory is 33.6GB.
[2025-05-07 17:28:39,124 INFO  L158              Benchmark]: TraceAbstraction took 6850.25ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 128.5MB in the beginning and 300.0MB in the end (delta: -171.5MB). Peak memory consumption was 42.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:39,125 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.30ms. Allocated memory is still 234.9MB. Free memory is still 173.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 47.58ms. Allocated memory is still 234.9MB. Free memory was 133.7MB in the beginning and 129.5MB in the end (delta: 4.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 83.81ms. Allocated memory is still 234.9MB. Free memory was 129.5MB in the beginning and 124.0MB in the end (delta: 5.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 547.24ms. Allocated memory is still 234.9MB. Free memory was 124.0MB in the beginning and 129.1MB in the end (delta: -5.0MB). Peak memory consumption was 25.2MB. Max. memory is 33.6GB.
 * TraceAbstraction took 6850.25ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 128.5MB in the beginning and 300.0MB in the end (delta: -171.5MB). Peak memory consumption was 42.8MB. 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 41 procedures, 176 locations, 289 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 6.8s, OverallIterations: 13, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 82 SdHoareTripleChecker+Valid, 1.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 19 mSDsluCounter, 13805 SdHoareTripleChecker+Invalid, 1.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 11580 mSDsCounter, 25 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1525 IncrementalHoareTripleChecker+Invalid, 1550 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 25 mSolverCounterUnsat, 2225 mSDtfsCounter, 1525 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 121 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 95 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 119 ImplicationChecksByTransitivity, 1.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=176occurred in iteration=0, InterpolantAutomatonStates: 110, 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, 13 MinimizatonAttempts, 10 StatesRemovedByMinimization, 5 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 4.0s InterpolantComputationTime, 1329 NumberOfCodeBlocks, 1329 NumberOfCodeBlocksAsserted, 13 NumberOfCheckSat, 1316 ConstructedInterpolants, 0 QuantifiedInterpolants, 1885 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 13 InterpolantComputations, 13 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:28:39,135 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
