./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/types/array_branches_1d.sol_4_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:19,850 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:19,898 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4437d5bd-3893-461b-b805-e6e9ea12bd10/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:19,901 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:19,901 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:19,914 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:19,914 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:19,914 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:19,915 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:19,915 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:19,915 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:19,915 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:19,915 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:19,915 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:19,915 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:19,916 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:19,916 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:19,916 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:19,917 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:19,917 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:20,111 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:20,118 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:20,120 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:20,121 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:20,121 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:20,122 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4437d5bd-3893-461b-b805-e6e9ea12bd10/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/types/array_branches_1d.sol_4_no_adts_000.smt2
[2025-05-07 17:27:20,123 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:20,126 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:20,396 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4437d5bd-3893-461b-b805-e6e9ea12bd10/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/types/array_branches_1d.sol_4_no_adts_000.smt2
[2025-05-07 17:27:20,399 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:20,401 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:20,401 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:20,401 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:20,401 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:20,404 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,441 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20 Unit
[2025-05-07 17:27:20,442 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:20,442 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:20,443 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:20,443 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:20,457 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,458 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,486 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,486 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,492 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,493 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,495 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,497 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,499 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,511 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:20,512 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:20,512 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:20,512 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:20,513 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (1/1) ...
[2025-05-07 17:27:20,516 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:20,529 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:20,539 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:27:20,542 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:27:20,552 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:20,552 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:20,552 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:20,552 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_9_0 given in one single declaration
[2025-05-07 17:27:20,552 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_9_0
[2025-05-07 17:27:20,553 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_9_0
[2025-05-07 17:27:20,553 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_45_0 given in one single declaration
[2025-05-07 17:27:20,553 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_45_0
[2025-05-07 17:27:20,553 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_45_0
[2025-05-07 17:27:20,553 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_45_0 given in one single declaration
[2025-05-07 17:27:20,553 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_45_0
[2025-05-07 17:27:20,553 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_45_0
[2025-05-07 17:27:20,553 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_18_C_45_0 given in one single declaration
[2025-05-07 17:27:20,553 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_18_C_45_0
[2025-05-07 17:27:20,553 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_18_C_45_0
[2025-05-07 17:27:20,553 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_20_C_45_0 given in one single declaration
[2025-05-07 17:27:20,553 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_20_C_45_0
[2025-05-07 17:27:20,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_20_C_45_0
[2025-05-07 17:27:20,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_19_C_45_0 given in one single declaration
[2025-05-07 17:27:20,554 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_19_C_45_0
[2025-05-07 17:27:20,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_19_C_45_0
[2025-05-07 17:27:20,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_21_C_45_0 given in one single declaration
[2025-05-07 17:27:20,554 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_21_C_45_0
[2025-05-07 17:27:20,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_21_C_45_0
[2025-05-07 17:27:20,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,554 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__44_45_0
[2025-05-07 17:27:20,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__44_45_0
[2025-05-07 17:27:20,554 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,554 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__44_45_0
[2025-05-07 17:27:20,554 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_f_43_45_0 given in one single declaration
[2025-05-07 17:27:20,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_f_43_45_0
[2025-05-07 17:27:20,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_f_43_45_0
[2025-05-07 17:27:20,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_5_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_5_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_5_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,555 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_function_f__44_45_0
[2025-05-07 17:27:20,555 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_if_true_f_27_45_0 given in one single declaration
[2025-05-07 17:27:20,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_if_true_f_27_45_0
[2025-05-07 17:27:20,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_if_true_f_27_45_0
[2025-05-07 17:27:20,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_if_header_f_34_45_0 given in one single declaration
[2025-05-07 17:27:20,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_if_header_f_34_45_0
[2025-05-07 17:27:20,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_if_header_f_34_45_0
[2025-05-07 17:27:20,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__44_45_0
[2025-05-07 17:27:20,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__44_45_0
[2025-05-07 17:27:20,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_f_43_45_0 given in one single declaration
[2025-05-07 17:27:20,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_f_43_45_0
[2025-05-07 17:27:20,556 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_f_43_45_0
[2025-05-07 17:27:20,556 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_if_false_f_33_45_0 given in one single declaration
[2025-05-07 17:27:20,556 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_if_false_f_33_45_0
[2025-05-07 17:27:20,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_if_false_f_33_45_0
[2025-05-07 17:27:20,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_return_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_return_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_return_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_f__44_45_0 given in one single declaration
[2025-05-07 17:27:20,557 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_f__44_45_0
[2025-05-07 17:27:20,557 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_f__44_45_0
[2025-05-07 17:27:20,558 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:20,558 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:20,558 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:20,695 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:20,697 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:20,933 INFO  L?                        ?]: Removed 181 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:20,933 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:20,944 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:20,944 INFO  L312             CfgBuilder]: Removed 11 assume(true) statements.
[2025-05-07 17:27:20,945 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:20 BoogieIcfgContainer
[2025-05-07 17:27:20,945 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:20,947 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:20,947 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:20,950 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:20,951 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:20" (1/3) ...
[2025-05-07 17:27:20,951 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@55e2746a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:20, skipping insertion in model container
[2025-05-07 17:27:20,951 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:20" (2/3) ...
[2025-05-07 17:27:20,951 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@55e2746a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:20, skipping insertion in model container
[2025-05-07 17:27:20,952 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:20" (3/3) ...
[2025-05-07 17:27:20,953 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:20,963 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:20,964 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 24 procedures, 95 locations, 145 edges, 24 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:21,000 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:21,011 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;@4d170ff7, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:21,011 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:21,014 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 95 states, 42 states have (on average 1.0952380952380953) internal successors, (46), 46 states have internal predecessors, (46), 28 states have call successors, (33), 23 states have call predecessors, (33), 23 states have return successors, (33), 25 states have call predecessors, (33), 28 states have call successors, (33)
[2025-05-07 17:27:21,023 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:21,023 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,024 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]
[2025-05-07 17:27:21,024 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,028 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,029 INFO  L85        PathProgramCache]: Analyzing trace with hash 668426948, now seen corresponding path program 1 times
[2025-05-07 17:27:21,036 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,036 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [333155791]
[2025-05-07 17:27:21,036 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,037 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,086 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:21,119 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:21,119 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,119 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:21,229 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:21,229 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:21,229 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [333155791]
[2025-05-07 17:27:21,230 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [333155791] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:21,230 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:21,232 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-05-07 17:27:21,233 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1209157906]
[2025-05-07 17:27:21,234 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:21,237 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-05-07 17:27:21,237 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:21,257 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-05-07 17:27:21,257 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:27:21,259 INFO  L87              Difference]: Start difference. First operand  has 95 states, 42 states have (on average 1.0952380952380953) internal successors, (46), 46 states have internal predecessors, (46), 28 states have call successors, (33), 23 states have call predecessors, (33), 23 states have return successors, (33), 25 states have call predecessors, (33), 28 states have call successors, (33) Second operand  has 2 states, 2 states have (on average 11.5) internal successors, (23), 2 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 2 states have return successors, (14), 2 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:27:21,289 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:21,290 INFO  L93              Difference]: Finished difference Result 90 states and 105 transitions.
[2025-05-07 17:27:21,290 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-05-07 17:27:21,291 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 11.5) internal successors, (23), 2 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 2 states have return successors, (14), 2 states have call predecessors, (14), 2 states have call successors, (14) Word has length 51
[2025-05-07 17:27:21,291 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:21,297 INFO  L225             Difference]: With dead ends: 90
[2025-05-07 17:27:21,298 INFO  L226             Difference]: Without dead ends: 89
[2025-05-07 17:27:21,299 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:27:21,302 INFO  L437           NwaCegarLoop]: 105 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 105 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:21,302 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 105 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:21,316 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-05-07 17:27:21,331 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 89.
[2025-05-07 17:27:21,332 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 89 states, 39 states have (on average 1.0769230769230769) internal successors, (42), 42 states have internal predecessors, (42), 27 states have call successors, (31), 22 states have call predecessors, (31), 22 states have return successors, (31), 24 states have call predecessors, (31), 27 states have call successors, (31)
[2025-05-07 17:27:21,336 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 89 states to 89 states and 104 transitions.
[2025-05-07 17:27:21,336 INFO  L79                 Accepts]: Start accepts. Automaton has 89 states and 104 transitions. Word has length 51
[2025-05-07 17:27:21,337 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:21,337 INFO  L485      AbstractCegarLoop]: Abstraction has 89 states and 104 transitions.
[2025-05-07 17:27:21,337 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 11.5) internal successors, (23), 2 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 2 states have return successors, (14), 2 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:27:21,337 INFO  L278                IsEmpty]: Start isEmpty. Operand 89 states and 104 transitions.
[2025-05-07 17:27:21,339 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:27:21,339 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,339 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]
[2025-05-07 17:27:21,339 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:21,340 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,340 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,340 INFO  L85        PathProgramCache]: Analyzing trace with hash 2101094228, now seen corresponding path program 1 times
[2025-05-07 17:27:21,340 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,340 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [692334837]
[2025-05-07 17:27:21,340 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,341 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,383 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:27:21,423 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:27:21,423 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,423 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:21,593 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:21,593 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:21,593 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [692334837]
[2025-05-07 17:27:21,593 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [692334837] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:21,594 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:21,594 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:21,594 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1462478009]
[2025-05-07 17:27:21,594 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:21,595 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:21,595 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:21,596 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:21,596 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:21,596 INFO  L87              Difference]: Start difference. First operand 89 states and 104 transitions. Second operand  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:27:21,653 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:21,653 INFO  L93              Difference]: Finished difference Result 93 states and 108 transitions.
[2025-05-07 17:27:21,653 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:21,654 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16) Word has length 59
[2025-05-07 17:27:21,654 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:21,655 INFO  L225             Difference]: With dead ends: 93
[2025-05-07 17:27:21,655 INFO  L226             Difference]: Without dead ends: 93
[2025-05-07 17:27:21,656 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:21,656 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 1 mSDsluCounter, 398 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 500 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:21,656 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 500 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:21,657 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-05-07 17:27:21,663 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 93.
[2025-05-07 17:27:21,663 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 41 states have (on average 1.0731707317073171) internal successors, (44), 44 states have internal predecessors, (44), 27 states have call successors, (31), 22 states have call predecessors, (31), 24 states have return successors, (33), 26 states have call predecessors, (33), 27 states have call successors, (33)
[2025-05-07 17:27:21,664 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 108 transitions.
[2025-05-07 17:27:21,664 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 108 transitions. Word has length 59
[2025-05-07 17:27:21,664 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:21,664 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 108 transitions.
[2025-05-07 17:27:21,665 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:27:21,665 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 108 transitions.
[2025-05-07 17:27:21,666 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:27:21,666 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,666 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]
[2025-05-07 17:27:21,666 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:21,666 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,667 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,667 INFO  L85        PathProgramCache]: Analyzing trace with hash -556615420, now seen corresponding path program 1 times
[2025-05-07 17:27:21,667 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,667 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [739612670]
[2025-05-07 17:27:21,667 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,667 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,697 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:27:21,714 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:27:21,714 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,714 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:21,809 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:21,809 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:21,809 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [739612670]
[2025-05-07 17:27:21,809 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [739612670] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:21,810 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:21,810 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:21,810 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [961879481]
[2025-05-07 17:27:21,810 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:21,810 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:21,810 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:21,811 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:21,811 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:21,811 INFO  L87              Difference]: Start difference. First operand 93 states and 108 transitions. Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:27:21,822 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:21,822 INFO  L93              Difference]: Finished difference Result 97 states and 112 transitions.
[2025-05-07 17:27:21,822 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:21,822 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16) Word has length 59
[2025-05-07 17:27:21,823 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:21,824 INFO  L225             Difference]: With dead ends: 97
[2025-05-07 17:27:21,824 INFO  L226             Difference]: Without dead ends: 93
[2025-05-07 17:27:21,824 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:21,825 INFO  L437           NwaCegarLoop]: 105 mSDtfsCounter, 1 mSDsluCounter, 202 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 307 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:27:21,825 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 307 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:21,825 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-05-07 17:27:21,829 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 91.
[2025-05-07 17:27:21,830 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 25 states have call successors, (29), 22 states have call predecessors, (29), 24 states have return successors, (31), 25 states have call predecessors, (31), 25 states have call successors, (31)
[2025-05-07 17:27:21,830 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 103 transitions.
[2025-05-07 17:27:21,831 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 103 transitions. Word has length 59
[2025-05-07 17:27:21,831 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:21,831 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 103 transitions.
[2025-05-07 17:27:21,831 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:27:21,831 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 103 transitions.
[2025-05-07 17:27:21,832 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:27:21,832 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,832 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]
[2025-05-07 17:27:21,832 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:21,832 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,833 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,833 INFO  L85        PathProgramCache]: Analyzing trace with hash 531592072, now seen corresponding path program 1 times
[2025-05-07 17:27:21,833 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,833 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [269244617]
[2025-05-07 17:27:21,833 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,833 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,859 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:27:21,873 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:27:21,873 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,107 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:22,108 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,108 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [269244617]
[2025-05-07 17:27:22,108 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [269244617] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,108 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,108 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:22,108 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1628627418]
[2025-05-07 17:27:22,108 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,109 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:22,109 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,109 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:22,109 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,109 INFO  L87              Difference]: Start difference. First operand 91 states and 103 transitions. Second operand  has 6 states, 4 states have (on average 6.75) internal successors, (27), 6 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 4 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:27:22,159 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,159 INFO  L93              Difference]: Finished difference Result 89 states and 100 transitions.
[2025-05-07 17:27:22,159 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:22,160 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 6.75) internal successors, (27), 6 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 4 states have call predecessors, (16), 4 states have call successors, (16) Word has length 59
[2025-05-07 17:27:22,160 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,161 INFO  L225             Difference]: With dead ends: 89
[2025-05-07 17:27:22,161 INFO  L226             Difference]: Without dead ends: 87
[2025-05-07 17:27:22,161 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,161 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 1 mSDsluCounter, 357 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 450 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:27:22,162 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 450 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:22,162 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 87 states.
[2025-05-07 17:27:22,166 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 87 to 87.
[2025-05-07 17:27:22,166 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 87 states, 39 states have (on average 1.0512820512820513) internal successors, (41), 41 states have internal predecessors, (41), 24 states have call successors, (27), 21 states have call predecessors, (27), 23 states have return successors, (29), 24 states have call predecessors, (29), 24 states have call successors, (29)
[2025-05-07 17:27:22,167 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 87 states to 87 states and 97 transitions.
[2025-05-07 17:27:22,167 INFO  L79                 Accepts]: Start accepts. Automaton has 87 states and 97 transitions. Word has length 59
[2025-05-07 17:27:22,167 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:22,167 INFO  L485      AbstractCegarLoop]: Abstraction has 87 states and 97 transitions.
[2025-05-07 17:27:22,167 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 6.75) internal successors, (27), 6 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 4 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:27:22,167 INFO  L278                IsEmpty]: Start isEmpty. Operand 87 states and 97 transitions.
[2025-05-07 17:27:22,168 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 64
[2025-05-07 17:27:22,168 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:22,168 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:22,168 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:22,168 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:22,169 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:22,169 INFO  L85        PathProgramCache]: Analyzing trace with hash 1768049270, now seen corresponding path program 1 times
[2025-05-07 17:27:22,169 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:22,169 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1406109574]
[2025-05-07 17:27:22,169 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:22,169 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:22,195 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 63 statements into 1 equivalence classes.
[2025-05-07 17:27:22,208 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 63 of 63 statements.
[2025-05-07 17:27:22,208 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:22,208 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,296 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:22,297 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,297 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1406109574]
[2025-05-07 17:27:22,297 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1406109574] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,297 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,297 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:22,297 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [64302601]
[2025-05-07 17:27:22,297 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,298 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:22,298 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,298 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:22,298 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,299 INFO  L87              Difference]: Start difference. First operand 87 states and 97 transitions. Second operand  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 4 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:27:22,342 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,342 INFO  L93              Difference]: Finished difference Result 91 states and 101 transitions.
[2025-05-07 17:27:22,342 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:22,342 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 4 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 4 states have call successors, (17) Word has length 63
[2025-05-07 17:27:22,343 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,343 INFO  L225             Difference]: With dead ends: 91
[2025-05-07 17:27:22,343 INFO  L226             Difference]: Without dead ends: 91
[2025-05-07 17:27:22,343 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,344 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 1 mSDsluCounter, 359 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 452 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:22,344 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 452 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:22,345 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-05-07 17:27:22,348 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 87.
[2025-05-07 17:27:22,348 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 87 states, 39 states have (on average 1.0512820512820513) internal successors, (41), 41 states have internal predecessors, (41), 24 states have call successors, (27), 21 states have call predecessors, (27), 23 states have return successors, (29), 24 states have call predecessors, (29), 24 states have call successors, (29)
[2025-05-07 17:27:22,349 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 87 states to 87 states and 97 transitions.
[2025-05-07 17:27:22,349 INFO  L79                 Accepts]: Start accepts. Automaton has 87 states and 97 transitions. Word has length 63
[2025-05-07 17:27:22,349 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:22,349 INFO  L485      AbstractCegarLoop]: Abstraction has 87 states and 97 transitions.
[2025-05-07 17:27:22,349 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 4 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:27:22,349 INFO  L278                IsEmpty]: Start isEmpty. Operand 87 states and 97 transitions.
[2025-05-07 17:27:22,350 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 64
[2025-05-07 17:27:22,350 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:22,350 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:22,350 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:22,350 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:22,350 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:22,350 INFO  L85        PathProgramCache]: Analyzing trace with hash 893454343, now seen corresponding path program 1 times
[2025-05-07 17:27:22,350 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:22,351 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1261187643]
[2025-05-07 17:27:22,351 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:22,351 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:22,374 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 63 statements into 1 equivalence classes.
[2025-05-07 17:27:22,385 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 63 of 63 statements.
[2025-05-07 17:27:22,385 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:22,385 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,611 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:22,611 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,611 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1261187643]
[2025-05-07 17:27:22,612 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1261187643] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,612 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,612 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:27:22,612 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [740249544]
[2025-05-07 17:27:22,612 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,612 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:27:22,612 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,612 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:27:22,613 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=132, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:27:22,613 INFO  L87              Difference]: Start difference. First operand 87 states and 97 transitions. Second operand  has 13 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 13 states have internal predecessors, (29), 7 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 9 states have call predecessors, (17), 7 states have call successors, (17)
[2025-05-07 17:27:22,806 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,806 INFO  L93              Difference]: Finished difference Result 95 states and 107 transitions.
[2025-05-07 17:27:22,806 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:27:22,807 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 13 states have internal predecessors, (29), 7 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 9 states have call predecessors, (17), 7 states have call successors, (17) Word has length 63
[2025-05-07 17:27:22,807 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,807 INFO  L225             Difference]: With dead ends: 95
[2025-05-07 17:27:22,808 INFO  L226             Difference]: Without dead ends: 95
[2025-05-07 17:27:22,808 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=178, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:27:22,809 INFO  L437           NwaCegarLoop]: 86 mSDtfsCounter, 5 mSDsluCounter, 904 mSDsCounter, 0 mSdLazyCounter, 148 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 990 SdHoareTripleChecker+Invalid, 149 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 148 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:22,809 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 990 Invalid, 149 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 148 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:27:22,810 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 95 states.
[2025-05-07 17:27:22,815 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 95 to 91.
[2025-05-07 17:27:22,815 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 24 states have call successors, (27), 21 states have call predecessors, (27), 25 states have return successors, (33), 26 states have call predecessors, (33), 24 states have call successors, (33)
[2025-05-07 17:27:22,816 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 103 transitions.
[2025-05-07 17:27:22,816 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 103 transitions. Word has length 63
[2025-05-07 17:27:22,817 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:22,817 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 103 transitions.
[2025-05-07 17:27:22,817 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 13 states have internal predecessors, (29), 7 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 9 states have call predecessors, (17), 7 states have call successors, (17)
[2025-05-07 17:27:22,817 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 103 transitions.
[2025-05-07 17:27:22,818 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 64
[2025-05-07 17:27:22,818 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:22,818 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]
[2025-05-07 17:27:22,818 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:22,818 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:22,819 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:22,819 INFO  L85        PathProgramCache]: Analyzing trace with hash -369479169, now seen corresponding path program 1 times
[2025-05-07 17:27:22,819 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:22,819 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2056266017]
[2025-05-07 17:27:22,819 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:22,819 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:22,846 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 63 statements into 1 equivalence classes.
[2025-05-07 17:27:22,857 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 63 of 63 statements.
[2025-05-07 17:27:22,857 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:22,857 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,947 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:22,947 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,947 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2056266017]
[2025-05-07 17:27:22,947 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2056266017] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,948 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,948 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:22,948 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1015204579]
[2025-05-07 17:27:22,948 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,948 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:22,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,949 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:22,949 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,949 INFO  L87              Difference]: Start difference. First operand 91 states and 103 transitions. Second operand  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 4 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:27:22,981 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,981 INFO  L93              Difference]: Finished difference Result 95 states and 107 transitions.
[2025-05-07 17:27:22,982 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:22,982 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 4 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 4 states have call successors, (17) Word has length 63
[2025-05-07 17:27:22,982 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,983 INFO  L225             Difference]: With dead ends: 95
[2025-05-07 17:27:22,983 INFO  L226             Difference]: Without dead ends: 95
[2025-05-07 17:27:22,983 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,983 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 1 mSDsluCounter, 359 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 452 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:22,983 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 452 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:22,984 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 95 states.
[2025-05-07 17:27:22,987 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 95 to 91.
[2025-05-07 17:27:22,987 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 24 states have call successors, (27), 21 states have call predecessors, (27), 25 states have return successors, (33), 26 states have call predecessors, (33), 24 states have call successors, (33)
[2025-05-07 17:27:22,988 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 103 transitions.
[2025-05-07 17:27:22,988 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 103 transitions. Word has length 63
[2025-05-07 17:27:22,988 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:22,988 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 103 transitions.
[2025-05-07 17:27:22,989 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 4 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:27:22,989 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 103 transitions.
[2025-05-07 17:27:22,989 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 64
[2025-05-07 17:27:22,989 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:22,989 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]
[2025-05-07 17:27:22,989 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:22,989 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:22,990 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:22,990 INFO  L85        PathProgramCache]: Analyzing trace with hash -1339960344, now seen corresponding path program 1 times
[2025-05-07 17:27:22,990 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:22,990 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1446535673]
[2025-05-07 17:27:22,990 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:22,990 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,009 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 63 statements into 1 equivalence classes.
[2025-05-07 17:27:23,020 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 63 of 63 statements.
[2025-05-07 17:27:23,020 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,020 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:23,225 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:23,225 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:23,225 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1446535673]
[2025-05-07 17:27:23,225 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1446535673] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:23,225 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:23,225 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:27:23,226 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [560038031]
[2025-05-07 17:27:23,226 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:23,226 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:27:23,226 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:23,227 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:27:23,227 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=132, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:27:23,227 INFO  L87              Difference]: Start difference. First operand 91 states and 103 transitions. Second operand  has 13 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 13 states have internal predecessors, (29), 7 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 9 states have call predecessors, (17), 7 states have call successors, (17)
[2025-05-07 17:27:23,406 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:23,406 INFO  L93              Difference]: Finished difference Result 61 states and 69 transitions.
[2025-05-07 17:27:23,407 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:27:23,407 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 13 states have internal predecessors, (29), 7 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 9 states have call predecessors, (17), 7 states have call successors, (17) Word has length 63
[2025-05-07 17:27:23,407 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:23,407 INFO  L225             Difference]: With dead ends: 61
[2025-05-07 17:27:23,407 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:23,408 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=178, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:27:23,408 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 3 mSDsluCounter, 575 mSDsCounter, 0 mSdLazyCounter, 167 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 631 SdHoareTripleChecker+Invalid, 168 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 167 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:23,408 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 631 Invalid, 168 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 167 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:27:23,408 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:23,409 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:23,409 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:27:23,409 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:23,409 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 63
[2025-05-07 17:27:23,409 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,409 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:23,409 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 13 states have internal predecessors, (29), 7 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 9 states have call predecessors, (17), 7 states have call successors, (17)
[2025-05-07 17:27:23,409 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:23,409 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:23,411 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:23,411 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:23,414 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:23,415 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:23,417 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:23 BoogieIcfgContainer
[2025-05-07 17:27:23,418 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:23,418 INFO  L158              Benchmark]: Toolchain (without parser) took 3017.85ms. Allocated memory is still 234.9MB. Free memory was 148.7MB in the beginning and 77.6MB in the end (delta: 71.2MB). Peak memory consumption was 62.5MB. Max. memory is 33.6GB.
[2025-05-07 17:27:23,418 INFO  L158              Benchmark]: SmtParser took 0.26ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:23,418 INFO  L158              Benchmark]: ChcToBoogie took 40.77ms. Allocated memory is still 234.9MB. Free memory was 148.7MB in the beginning and 145.9MB in the end (delta: 2.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:23,418 INFO  L158              Benchmark]: Boogie Preprocessor took 68.80ms. Allocated memory is still 234.9MB. Free memory was 145.8MB in the beginning and 142.6MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:23,419 INFO  L158              Benchmark]: RCFGBuilder took 432.99ms. Allocated memory was 234.9MB in the beginning and 302.0MB in the end (delta: 67.1MB). Free memory was 142.5MB in the beginning and 247.1MB in the end (delta: -104.6MB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
[2025-05-07 17:27:23,419 INFO  L158              Benchmark]: TraceAbstraction took 2470.65ms. Allocated memory was 302.0MB in the beginning and 234.9MB in the end (delta: -67.1MB). Free memory was 246.7MB in the beginning and 77.6MB in the end (delta: 169.1MB). Peak memory consumption was 104.2MB. Max. memory is 33.6GB.
[2025-05-07 17:27:23,420 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.26ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 40.77ms. Allocated memory is still 234.9MB. Free memory was 148.7MB in the beginning and 145.9MB in the end (delta: 2.8MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 68.80ms. Allocated memory is still 234.9MB. Free memory was 145.8MB in the beginning and 142.6MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 432.99ms. Allocated memory was 234.9MB in the beginning and 302.0MB in the end (delta: 67.1MB). Free memory was 142.5MB in the beginning and 247.1MB in the end (delta: -104.6MB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2470.65ms. Allocated memory was 302.0MB in the beginning and 234.9MB in the end (delta: -67.1MB). Free memory was 246.7MB in the beginning and 77.6MB in the end (delta: 169.1MB). Peak memory consumption was 104.2MB. 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 24 procedures, 95 locations, 145 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.4s, OverallIterations: 8, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.7s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 31 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 13 mSDsluCounter, 3887 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 3154 mSDsCounter, 2 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 389 IncrementalHoareTripleChecker+Invalid, 391 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 2 mSolverCounterUnsat, 733 mSDtfsCounter, 389 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 60 GetRequests, 16 SyntacticMatches, 0 SemanticMatches, 44 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 11 ImplicationChecksByTransitivity, 0.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=95occurred in iteration=0, InterpolantAutomatonStates: 55, 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, 8 MinimizatonAttempts, 14 StatesRemovedByMinimization, 4 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.2s InterpolantComputationTime, 480 NumberOfCodeBlocks, 480 NumberOfCodeBlocksAsserted, 8 NumberOfCheckSat, 472 ConstructedInterpolants, 0 QuantifiedInterpolants, 634 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 8 InterpolantComputations, 8 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:27:23,430 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
