./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/loops/for_1_continue.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:14,882 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:14,932 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4340851f-5ec2-4208-8d33-fe9ee708aa3b/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:14,935 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:14,935 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:14,952 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:14,953 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:14,953 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:14,953 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:14,953 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:14,954 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:14,954 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:14,954 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:14,954 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:14,954 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:14,954 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:14,954 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:14,954 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:14,954 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:14,955 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:14,955 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:14,955 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:14,955 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:14,955 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:14,955 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:14,956 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:14,956 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:15,150 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:15,158 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:15,160 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:15,161 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:15,161 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:15,162 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4340851f-5ec2-4208-8d33-fe9ee708aa3b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/loops/for_1_continue.sol_0_no_adts_000.smt2
[2025-05-07 17:26:15,164 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:15,166 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:15,405 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4340851f-5ec2-4208-8d33-fe9ee708aa3b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/loops/for_1_continue.sol_0_no_adts_000.smt2
[2025-05-07 17:26:15,408 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:15,409 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:15,409 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:15,409 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:15,409 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:15,411 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,442 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15 Unit
[2025-05-07 17:26:15,442 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:15,443 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:15,443 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:15,443 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:15,459 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,459 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,481 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,481 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,484 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,485 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,486 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,488 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,489 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,498 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:15,498 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:15,499 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:15,499 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:15,499 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (1/1) ...
[2025-05-07 17:26:15,501 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:15,510 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:15,518 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:26:15,520 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:26:15,527 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:15,528 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:15,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:15,528 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_3_0 given in one single declaration
[2025-05-07 17:26:15,528 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_3_0
[2025-05-07 17:26:15,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_3_0
[2025-05-07 17:26:15,528 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__36_37_0 given in one single declaration
[2025-05-07 17:26:15,528 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__36_37_0
[2025-05-07 17:26:15,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__36_37_0
[2025-05-07 17:26:15,528 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__36_37_0 given in one single declaration
[2025-05-07 17:26:15,528 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__36_37_0
[2025-05-07 17:26:15,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__36_37_0
[2025-05-07 17:26:15,528 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_f__36_37_0 given in one single declaration
[2025-05-07 17:26:15,528 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_f__36_37_0
[2025-05-07 17:26:15,528 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_f__36_37_0
[2025-05-07 17:26:15,528 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_f_35_37_0 given in one single declaration
[2025-05-07 17:26:15,528 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_f_35_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_f_35_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_for_header_f_28_37_0 given in one single declaration
[2025-05-07 17:26:15,529 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_for_header_f_28_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_for_header_f_28_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_for_post_f_18_37_0 given in one single declaration
[2025-05-07 17:26:15,529 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_for_post_f_18_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_for_post_f_18_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_if_true_f_25_37_0 given in one single declaration
[2025-05-07 17:26:15,529 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_if_true_f_25_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_if_true_f_25_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_if_header_f_26_37_0 given in one single declaration
[2025-05-07 17:26:15,529 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_if_header_f_26_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_if_header_f_26_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_for_body_f_27_37_0 given in one single declaration
[2025-05-07 17:26:15,529 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_for_body_f_27_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_for_body_f_27_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_f_35_37_0 given in one single declaration
[2025-05-07 17:26:15,529 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_f_35_37_0
[2025-05-07 17:26:15,529 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_f_35_37_0
[2025-05-07 17:26:15,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_f_35_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_f_35_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_f_35_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_5_function_f__36_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure block_5_function_f__36_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_5_function_f__36_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_return_function_f__36_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_return_function_f__36_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_return_function_f__36_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_f__36_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_f__36_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_f__36_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_21_C_37_0 given in one single declaration
[2025-05-07 17:26:15,530 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_21_C_37_0
[2025-05-07 17:26:15,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_21_C_37_0
[2025-05-07 17:26:15,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_18_C_37_0 given in one single declaration
[2025-05-07 17:26:15,531 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_18_C_37_0
[2025-05-07 17:26:15,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_18_C_37_0
[2025-05-07 17:26:15,531 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_20_C_37_0 given in one single declaration
[2025-05-07 17:26:15,531 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_20_C_37_0
[2025-05-07 17:26:15,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_20_C_37_0
[2025-05-07 17:26:15,531 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_19_C_37_0 given in one single declaration
[2025-05-07 17:26:15,531 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_19_C_37_0
[2025-05-07 17:26:15,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_19_C_37_0
[2025-05-07 17:26:15,531 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:15,531 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:15,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:26:15,652 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:26:15,654 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:26:15,814 INFO  L?                        ?]: Removed 133 outVars from TransFormulas that were not future-live.
[2025-05-07 17:26:15,814 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:26:15,822 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:26:15,822 INFO  L312             CfgBuilder]: Removed 9 assume(true) statements.
[2025-05-07 17:26:15,823 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:15 BoogieIcfgContainer
[2025-05-07 17:26:15,823 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:26:15,824 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:26:15,824 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:26:15,826 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:26:15,827 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:15" (1/3) ...
[2025-05-07 17:26:15,827 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3615d074 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:26:15, skipping insertion in model container
[2025-05-07 17:26:15,827 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:15" (2/3) ...
[2025-05-07 17:26:15,827 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3615d074 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:26:15, skipping insertion in model container
[2025-05-07 17:26:15,827 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:15" (3/3) ...
[2025-05-07 17:26:15,828 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:26:15,838 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:26:15,839 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 23 procedures, 90 locations, 130 edges, 23 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:26:15,867 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:26:15,875 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;@3a090d46, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:26:15,875 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:26:15,878 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 90 states, 39 states have (on average 1.1025641025641026) internal successors, (43), 43 states have internal predecessors, (43), 28 states have call successors, (29), 22 states have call predecessors, (29), 22 states have return successors, (29), 24 states have call predecessors, (29), 28 states have call successors, (29)
[2025-05-07 17:26:15,885 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:26:15,885 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:15,885 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:26:15,885 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:15,889 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:15,889 INFO  L85        PathProgramCache]: Analyzing trace with hash 51644629, now seen corresponding path program 1 times
[2025-05-07 17:26:15,894 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:15,895 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1119650461]
[2025-05-07 17:26:15,895 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:15,895 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:15,934 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:26:15,951 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:26:15,952 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:15,952 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:16,118 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:16,118 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:16,118 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1119650461]
[2025-05-07 17:26:16,118 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1119650461] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:16,119 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:16,120 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:16,122 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1128990128]
[2025-05-07 17:26:16,122 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:16,125 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:16,125 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:16,142 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:16,143 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:16,144 INFO  L87              Difference]: Start difference. First operand  has 90 states, 39 states have (on average 1.1025641025641026) internal successors, (43), 43 states have internal predecessors, (43), 28 states have call successors, (29), 22 states have call predecessors, (29), 22 states have return successors, (29), 24 states have call predecessors, (29), 28 states have call successors, (29) Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:26:16,196 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:16,197 INFO  L93              Difference]: Finished difference Result 92 states and 103 transitions.
[2025-05-07 17:26:16,197 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:16,199 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), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16) Word has length 59
[2025-05-07 17:26:16,199 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:16,211 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:26:16,211 INFO  L226             Difference]: Without dead ends: 88
[2025-05-07 17:26:16,213 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:16,215 INFO  L437           NwaCegarLoop]: 99 mSDtfsCounter, 1 mSDsluCounter, 191 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 290 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:26:16,216 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 290 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:16,227 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 88 states.
[2025-05-07 17:26:16,244 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 88 to 86.
[2025-05-07 17:26:16,245 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 38 states have (on average 1.0526315789473684) internal successors, (40), 40 states have internal predecessors, (40), 26 states have call successors, (27), 22 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 26 states have call successors, (27)
[2025-05-07 17:26:16,249 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 94 transitions.
[2025-05-07 17:26:16,250 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 94 transitions. Word has length 59
[2025-05-07 17:26:16,250 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:16,250 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 94 transitions.
[2025-05-07 17:26:16,250 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), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:26:16,250 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 94 transitions.
[2025-05-07 17:26:16,252 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:26:16,252 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:16,252 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:26:16,253 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:26:16,253 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:16,253 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:16,253 INFO  L85        PathProgramCache]: Analyzing trace with hash -1856196163, now seen corresponding path program 1 times
[2025-05-07 17:26:16,253 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:16,253 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1450425835]
[2025-05-07 17:26:16,254 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:16,254 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:16,291 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:26:16,323 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:26:16,323 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:16,323 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:16,529 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:16,529 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:16,529 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1450425835]
[2025-05-07 17:26:16,529 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1450425835] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:16,529 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:16,529 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:16,530 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [740130117]
[2025-05-07 17:26:16,530 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:16,531 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:16,531 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:16,532 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:16,532 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:16,532 INFO  L87              Difference]: Start difference. First operand 86 states and 94 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:26:16,555 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:16,555 INFO  L93              Difference]: Finished difference Result 84 states and 91 transitions.
[2025-05-07 17:26:16,556 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:16,556 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:26:16,556 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:16,557 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:26:16,558 INFO  L226             Difference]: Without dead ends: 82
[2025-05-07 17:26:16,558 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:16,558 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 0 mSDsluCounter, 173 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 263 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:16,559 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 263 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:16,560 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-05-07 17:26:16,565 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 82.
[2025-05-07 17:26:16,566 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 36 states have (on average 1.0555555555555556) internal successors, (38), 38 states have internal predecessors, (38), 25 states have call successors, (25), 21 states have call predecessors, (25), 21 states have return successors, (25), 22 states have call predecessors, (25), 25 states have call successors, (25)
[2025-05-07 17:26:16,567 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 88 transitions.
[2025-05-07 17:26:16,567 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 88 transitions. Word has length 59
[2025-05-07 17:26:16,568 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:16,568 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 88 transitions.
[2025-05-07 17:26:16,568 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:26:16,568 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 88 transitions.
[2025-05-07 17:26:16,569 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:26:16,569 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:16,569 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:26:16,570 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:26:16,570 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:16,570 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:16,570 INFO  L85        PathProgramCache]: Analyzing trace with hash 1076391121, now seen corresponding path program 1 times
[2025-05-07 17:26:16,570 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:16,570 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1528950458]
[2025-05-07 17:26:16,571 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:16,571 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:16,596 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:26:16,611 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:26:16,611 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:16,611 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:16,811 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:16,812 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:16,812 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1528950458]
[2025-05-07 17:26:16,812 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1528950458] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:16,812 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:16,812 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-05-07 17:26:16,812 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1110745737]
[2025-05-07 17:26:16,812 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:16,813 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-05-07 17:26:16,813 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:16,813 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-05-07 17:26:16,814 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:26:16,814 INFO  L87              Difference]: Start difference. First operand 82 states and 88 transitions. Second operand  has 10 states, 8 states have (on average 3.375) internal successors, (27), 10 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 8 states have return successors, (16), 9 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:26:16,941 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:16,941 INFO  L93              Difference]: Finished difference Result 92 states and 99 transitions.
[2025-05-07 17:26:16,941 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:26:16,942 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 3.375) internal successors, (27), 10 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 8 states have return successors, (16), 9 states have call predecessors, (16), 4 states have call successors, (16) Word has length 59
[2025-05-07 17:26:16,942 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:16,943 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:26:16,943 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:26:16,943 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:26:16,944 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 3 mSDsluCounter, 631 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 712 SdHoareTripleChecker+Invalid, 69 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:16,945 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 712 Invalid, 69 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:16,945 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:26:16,951 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-05-07 17:26:16,952 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 25 states have call successors, (25), 21 states have call predecessors, (25), 26 states have return successors, (31), 27 states have call predecessors, (31), 25 states have call successors, (31)
[2025-05-07 17:26:16,953 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 99 transitions.
[2025-05-07 17:26:16,953 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 99 transitions. Word has length 59
[2025-05-07 17:26:16,954 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:16,954 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 99 transitions.
[2025-05-07 17:26:16,954 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 3.375) internal successors, (27), 10 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 8 states have return successors, (16), 9 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:26:16,954 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 99 transitions.
[2025-05-07 17:26:16,956 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 78
[2025-05-07 17:26:16,956 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:16,956 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:16,956 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:26:16,956 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:16,957 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:16,957 INFO  L85        PathProgramCache]: Analyzing trace with hash 1912192662, now seen corresponding path program 1 times
[2025-05-07 17:26:16,957 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:16,957 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1875240439]
[2025-05-07 17:26:16,957 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:16,957 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:16,983 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 77 statements into 1 equivalence classes.
[2025-05-07 17:26:17,002 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 77 of 77 statements.
[2025-05-07 17:26:17,003 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:17,003 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:17,251 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:17,251 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:17,251 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1875240439]
[2025-05-07 17:26:17,252 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1875240439] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:17,252 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:17,252 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [14] imperfect sequences [] total 14
[2025-05-07 17:26:17,252 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [303575524]
[2025-05-07 17:26:17,252 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:17,252 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-05-07 17:26:17,252 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:17,253 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-05-07 17:26:17,253 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=157, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:26:17,253 INFO  L87              Difference]: Start difference. First operand 92 states and 99 transitions. Second operand  has 14 states, 12 states have (on average 2.8333333333333335) internal successors, (34), 14 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 13 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:26:17,419 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:17,420 INFO  L93              Difference]: Finished difference Result 110 states and 119 transitions.
[2025-05-07 17:26:17,420 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:26:17,420 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 12 states have (on average 2.8333333333333335) internal successors, (34), 14 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 13 states have call predecessors, (21), 4 states have call successors, (21) Word has length 77
[2025-05-07 17:26:17,421 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:17,422 INFO  L225             Difference]: With dead ends: 110
[2025-05-07 17:26:17,422 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:26:17,422 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 16 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=29, Invalid=181, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:26:17,423 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 3 mSDsluCounter, 917 mSDsCounter, 0 mSdLazyCounter, 162 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 995 SdHoareTripleChecker+Invalid, 162 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 162 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:17,423 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 995 Invalid, 162 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 162 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:17,424 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:26:17,441 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 100.
[2025-05-07 17:26:17,441 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 100 states, 45 states have (on average 1.0444444444444445) internal successors, (47), 47 states have internal predecessors, (47), 25 states have call successors, (25), 21 states have call predecessors, (25), 30 states have return successors, (36), 31 states have call predecessors, (36), 25 states have call successors, (36)
[2025-05-07 17:26:17,442 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 100 states to 100 states and 108 transitions.
[2025-05-07 17:26:17,442 INFO  L79                 Accepts]: Start accepts. Automaton has 100 states and 108 transitions. Word has length 77
[2025-05-07 17:26:17,442 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:17,442 INFO  L485      AbstractCegarLoop]: Abstraction has 100 states and 108 transitions.
[2025-05-07 17:26:17,442 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 12 states have (on average 2.8333333333333335) internal successors, (34), 14 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 13 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:26:17,442 INFO  L278                IsEmpty]: Start isEmpty. Operand 100 states and 108 transitions.
[2025-05-07 17:26:17,443 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 79
[2025-05-07 17:26:17,443 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:17,443 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:17,444 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:26:17,444 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:17,444 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:17,444 INFO  L85        PathProgramCache]: Analyzing trace with hash -1983541630, now seen corresponding path program 1 times
[2025-05-07 17:26:17,444 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:17,444 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [380361721]
[2025-05-07 17:26:17,445 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:17,445 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:17,475 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 78 statements into 1 equivalence classes.
[2025-05-07 17:26:17,493 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 78 of 78 statements.
[2025-05-07 17:26:17,494 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:17,494 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:17,733 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:17,733 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:17,734 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [380361721]
[2025-05-07 17:26:17,734 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [380361721] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:17,734 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:17,734 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [14] imperfect sequences [] total 14
[2025-05-07 17:26:17,734 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [807392796]
[2025-05-07 17:26:17,734 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:17,734 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-05-07 17:26:17,735 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:17,735 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-05-07 17:26:17,735 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=157, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:26:17,736 INFO  L87              Difference]: Start difference. First operand 100 states and 108 transitions. Second operand  has 14 states, 12 states have (on average 2.9166666666666665) internal successors, (35), 14 states have internal predecessors, (35), 4 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 13 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:26:17,915 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:17,915 INFO  L93              Difference]: Finished difference Result 132 states and 144 transitions.
[2025-05-07 17:26:17,916 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:26:17,916 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 12 states have (on average 2.9166666666666665) internal successors, (35), 14 states have internal predecessors, (35), 4 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 13 states have call predecessors, (21), 4 states have call successors, (21) Word has length 78
[2025-05-07 17:26:17,916 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:17,918 INFO  L225             Difference]: With dead ends: 132
[2025-05-07 17:26:17,918 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:26:17,918 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 16 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=29, Invalid=181, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:26:17,919 INFO  L437           NwaCegarLoop]: 77 mSDtfsCounter, 3 mSDsluCounter, 907 mSDsCounter, 0 mSdLazyCounter, 162 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 984 SdHoareTripleChecker+Invalid, 162 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 162 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:17,919 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 984 Invalid, 162 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 162 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:26:17,920 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:26:17,929 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 116.
[2025-05-07 17:26:17,929 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 116 states, 53 states have (on average 1.0377358490566038) internal successors, (55), 55 states have internal predecessors, (55), 25 states have call successors, (25), 21 states have call predecessors, (25), 38 states have return successors, (48), 39 states have call predecessors, (48), 25 states have call successors, (48)
[2025-05-07 17:26:17,930 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 128 transitions.
[2025-05-07 17:26:17,930 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 128 transitions. Word has length 78
[2025-05-07 17:26:17,931 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:17,931 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 128 transitions.
[2025-05-07 17:26:17,931 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 12 states have (on average 2.9166666666666665) internal successors, (35), 14 states have internal predecessors, (35), 4 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 13 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:26:17,931 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 128 transitions.
[2025-05-07 17:26:17,932 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:17,932 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:17,932 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:17,933 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:26:17,933 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:17,933 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:17,933 INFO  L85        PathProgramCache]: Analyzing trace with hash 678788935, now seen corresponding path program 1 times
[2025-05-07 17:26:17,933 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:17,933 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1418895947]
[2025-05-07 17:26:17,933 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:17,933 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:17,972 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:17,992 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:17,993 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:17,993 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:18,281 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 12 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:26:18,281 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:18,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1418895947]
[2025-05-07 17:26:18,281 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1418895947] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:18,281 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:18,281 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:26:18,281 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [315275663]
[2025-05-07 17:26:18,281 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:18,282 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:26:18,282 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:18,282 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:26:18,283 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:18,283 INFO  L87              Difference]: Start difference. First operand 116 states and 128 transitions. Second operand  has 8 states, 7 states have (on average 6.0) internal successors, (42), 8 states have internal predecessors, (42), 3 states have call successors, (23), 1 states have call predecessors, (23), 7 states have return successors, (26), 7 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:26:18,368 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:18,368 INFO  L93              Difference]: Finished difference Result 105 states and 119 transitions.
[2025-05-07 17:26:18,368 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:26:18,369 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 6.0) internal successors, (42), 8 states have internal predecessors, (42), 3 states have call successors, (23), 1 states have call predecessors, (23), 7 states have return successors, (26), 7 states have call predecessors, (26), 3 states have call successors, (26) Word has length 96
[2025-05-07 17:26:18,369 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:18,369 INFO  L225             Difference]: With dead ends: 105
[2025-05-07 17:26:18,369 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:26:18,369 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:18,370 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 5 mSDsluCounter, 522 mSDsCounter, 0 mSdLazyCounter, 70 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 613 SdHoareTripleChecker+Invalid, 76 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 70 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:18,370 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 613 Invalid, 76 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 70 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:18,370 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:26:18,370 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:26:18,370 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:26:18,370 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:26:18,370 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 96
[2025-05-07 17:26:18,370 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:18,370 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:26:18,371 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 6.0) internal successors, (42), 8 states have internal predecessors, (42), 3 states have call successors, (23), 1 states have call predecessors, (23), 7 states have return successors, (26), 7 states have call predecessors, (26), 3 states have call successors, (26)
[2025-05-07 17:26:18,371 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:26:18,371 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:26:18,372 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:26:18,373 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:26:18,375 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:18,377 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:26:18,379 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:26:18 BoogieIcfgContainer
[2025-05-07 17:26:18,379 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:26:18,380 INFO  L158              Benchmark]: Toolchain (without parser) took 2971.00ms. Allocated memory is still 234.9MB. Free memory was 147.5MB in the beginning and 170.0MB in the end (delta: -22.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:18,380 INFO  L158              Benchmark]: SmtParser took 0.28ms. Allocated memory is still 234.9MB. Free memory is still 167.5MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:18,380 INFO  L158              Benchmark]: ChcToBoogie took 33.39ms. Allocated memory is still 234.9MB. Free memory was 147.5MB in the beginning and 145.0MB in the end (delta: 2.5MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:26:18,380 INFO  L158              Benchmark]: Boogie Preprocessor took 55.00ms. Allocated memory is still 234.9MB. Free memory was 145.0MB in the beginning and 141.9MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:18,380 INFO  L158              Benchmark]: RCFGBuilder took 324.15ms. Allocated memory is still 234.9MB. Free memory was 141.9MB in the beginning and 169.1MB in the end (delta: -27.2MB). Peak memory consumption was 25.9MB. Max. memory is 33.6GB.
[2025-05-07 17:26:18,381 INFO  L158              Benchmark]: TraceAbstraction took 2555.26ms. Allocated memory is still 234.9MB. Free memory was 168.3MB in the beginning and 170.0MB in the end (delta: -1.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:18,381 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.28ms. Allocated memory is still 234.9MB. Free memory is still 167.5MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 33.39ms. Allocated memory is still 234.9MB. Free memory was 147.5MB in the beginning and 145.0MB in the end (delta: 2.5MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 55.00ms. Allocated memory is still 234.9MB. Free memory was 145.0MB in the beginning and 141.9MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 324.15ms. Allocated memory is still 234.9MB. Free memory was 141.9MB in the beginning and 169.1MB in the end (delta: -27.2MB). Peak memory consumption was 25.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2555.26ms. Allocated memory is still 234.9MB. Free memory was 168.3MB in the beginning and 170.0MB in the end (delta: -1.8MB). There was no memory consumed. 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 23 procedures, 90 locations, 130 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.5s, OverallIterations: 6, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.7s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 27 SdHoareTripleChecker+Valid, 0.5s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 15 mSDsluCounter, 3857 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 3341 mSDsCounter, 6 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 471 IncrementalHoareTripleChecker+Invalid, 477 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 6 mSolverCounterUnsat, 516 mSDtfsCounter, 471 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 59 GetRequests, 14 SyntacticMatches, 0 SemanticMatches, 45 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=116occurred in iteration=5, InterpolantAutomatonStates: 54, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 6 MinimizatonAttempts, 28 StatesRemovedByMinimization, 3 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 1.3s InterpolantComputationTime, 428 NumberOfCodeBlocks, 428 NumberOfCodeBlocksAsserted, 6 NumberOfCheckSat, 422 ConstructedInterpolants, 0 QuantifiedInterpolants, 587 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 6 InterpolantComputations, 6 PerfectInterpolantSequences, 26/26 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:26:18,391 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
