./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/operators/slice.sol_2_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:26,516 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:26,553 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_123293e5-3fbb-4110-a434-6ed3dd3fd39a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:26,556 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:26,556 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:26,570 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:26,570 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:26,570 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:26,570 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:26,570 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:26,571 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:26,571 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:26,571 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:26,571 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:26,571 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:26,572 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:26,572 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:26,572 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:26,764 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:26,772 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:26,774 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:26,775 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:26,775 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:26,776 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_123293e5-3fbb-4110-a434-6ed3dd3fd39a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/operators/slice.sol_2_no_adts_000.smt2
[2025-05-07 17:28:26,777 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:26,779 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:27,091 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_123293e5-3fbb-4110-a434-6ed3dd3fd39a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/operators/slice.sol_2_no_adts_000.smt2
[2025-05-07 17:28:27,093 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:27,095 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:27,095 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:27,095 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:27,095 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:27,098 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,140 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27 Unit
[2025-05-07 17:28:27,141 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:27,142 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:27,142 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:27,142 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:27,154 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,154 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,183 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,183 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,192 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,193 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,195 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,198 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,200 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,214 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:27,214 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:27,214 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:27,214 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:27,215 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (1/1) ...
[2025-05-07 17:28:27,217 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:27,230 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:27,240 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:28:27,243 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:28:27,251 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:27,251 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:27,251 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:27,251 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_11_0 given in one single declaration
[2025-05-07 17:28:27,251 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_11_0
[2025-05-07 17:28:27,251 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_11_0
[2025-05-07 17:28:27,251 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_63_0 given in one single declaration
[2025-05-07 17:28:27,251 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_63_0
[2025-05-07 17:28:27,251 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_63_0
[2025-05-07 17:28:27,251 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_63_0 given in one single declaration
[2025-05-07 17:28:27,251 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_63_0
[2025-05-07 17:28:27,251 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_63_0
[2025-05-07 17:28:27,251 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_15_C_63_0 given in one single declaration
[2025-05-07 17:28:27,251 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_15_C_63_0
[2025-05-07 17:28:27,251 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_15_C_63_0
[2025-05-07 17:28:27,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_17_C_63_0 given in one single declaration
[2025-05-07 17:28:27,252 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_17_C_63_0
[2025-05-07 17:28:27,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_17_C_63_0
[2025-05-07 17:28:27,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_16_C_63_0 given in one single declaration
[2025-05-07 17:28:27,252 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_16_C_63_0
[2025-05-07 17:28:27,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_16_C_63_0
[2025-05-07 17:28:27,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_18_C_63_0 given in one single declaration
[2025-05-07 17:28:27,252 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_18_C_63_0
[2025-05-07 17:28:27,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_18_C_63_0
[2025-05-07 17:28:27,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,252 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__62_63_0
[2025-05-07 17:28:27,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__62_63_0
[2025-05-07 17:28:27,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,252 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__62_63_0
[2025-05-07 17:28:27,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__62_63_0
[2025-05-07 17:28:27,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,252 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__62_63_0
[2025-05-07 17:28:27,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__62_63_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,253 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_f__62_63_0
[2025-05-07 17:28:27,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_f__62_63_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_f_61_63_0 given in one single declaration
[2025-05-07 17:28:27,253 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_f_61_63_0
[2025-05-07 17:28:27,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_f_61_63_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_5_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,253 INFO  L130     BoogieDeclarations]: Found specification of procedure block_5_function_f__62_63_0
[2025-05-07 17:28:27,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_5_function_f__62_63_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure array_slice_bytes_tuple_0 given in one single declaration
[2025-05-07 17:28:27,253 INFO  L130     BoogieDeclarations]: Found specification of procedure array_slice_bytes_tuple_0
[2025-05-07 17:28:27,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure array_slice_bytes_tuple_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure array_slice_header_bytes_tuple_0 given in one single declaration
[2025-05-07 17:28:27,253 INFO  L130     BoogieDeclarations]: Found specification of procedure array_slice_header_bytes_tuple_0
[2025-05-07 17:28:27,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure array_slice_header_bytes_tuple_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure array_slice_loop_bytes_tuple_0 given in one single declaration
[2025-05-07 17:28:27,253 INFO  L130     BoogieDeclarations]: Found specification of procedure array_slice_loop_bytes_tuple_0
[2025-05-07 17:28:27,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure array_slice_loop_bytes_tuple_0
[2025-05-07 17:28:27,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_return_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_return_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_return_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_f__62_63_0 given in one single declaration
[2025-05-07 17:28:27,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_f__62_63_0
[2025-05-07 17:28:27,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_f__62_63_0
[2025-05-07 17:28:27,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:27,255 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:27,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:27,393 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:27,395 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:27,638 INFO  L?                        ?]: Removed 222 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:27,638 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:27,648 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:27,648 INFO  L312             CfgBuilder]: Removed 12 assume(true) statements.
[2025-05-07 17:28:27,649 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:27 BoogieIcfgContainer
[2025-05-07 17:28:27,649 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:27,651 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:27,651 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:27,653 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:27,653 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:27" (1/3) ...
[2025-05-07 17:28:27,654 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35bcbda5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:27, skipping insertion in model container
[2025-05-07 17:28:27,654 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:27" (2/3) ...
[2025-05-07 17:28:27,654 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35bcbda5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:27, skipping insertion in model container
[2025-05-07 17:28:27,654 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:27" (3/3) ...
[2025-05-07 17:28:27,655 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:27,666 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:27,668 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 24 procedures, 108 locations, 187 edges, 24 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:27,705 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:27,715 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;@332198b1, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:27,715 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:27,718 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 108 states, 42 states have (on average 1.0952380952380953) internal successors, (46), 46 states have internal predecessors, (46), 41 states have call successors, (47), 23 states have call predecessors, (47), 23 states have return successors, (47), 39 states have call predecessors, (47), 41 states have call successors, (47)
[2025-05-07 17:28:27,727 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:27,727 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:27,727 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:28:27,727 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:27,731 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:27,731 INFO  L85        PathProgramCache]: Analyzing trace with hash 300977416, now seen corresponding path program 1 times
[2025-05-07 17:28:27,736 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:27,736 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [495667783]
[2025-05-07 17:28:27,736 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:27,737 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:27,782 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:27,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:27,814 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:27,815 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:27,907 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:27,907 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:27,907 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [495667783]
[2025-05-07 17:28:27,908 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [495667783] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:27,908 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:27,911 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-05-07 17:28:27,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [601135099]
[2025-05-07 17:28:27,912 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:27,916 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-05-07 17:28:27,916 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:27,936 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-05-07 17:28:27,937 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:28:27,939 INFO  L87              Difference]: Start difference. First operand  has 108 states, 42 states have (on average 1.0952380952380953) internal successors, (46), 46 states have internal predecessors, (46), 41 states have call successors, (47), 23 states have call predecessors, (47), 23 states have return successors, (47), 39 states have call predecessors, (47), 41 states have call successors, (47) 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:28:27,973 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:27,973 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:28:27,974 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-05-07 17:28:27,975 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:28:27,975 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:27,982 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:28:27,982 INFO  L226             Difference]: Without dead ends: 84
[2025-05-07 17:28:27,984 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:28:27,987 INFO  L437           NwaCegarLoop]: 106 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, 106 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:28:27,988 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 106 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:28,004 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-05-07 17:28:28,030 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 84.
[2025-05-07 17:28:28,032 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 33 states have (on average 1.0909090909090908) internal successors, (36), 36 states have internal predecessors, (36), 31 states have call successors, (33), 19 states have call predecessors, (33), 19 states have return successors, (33), 29 states have call predecessors, (33), 31 states have call successors, (33)
[2025-05-07 17:28:28,037 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 102 transitions.
[2025-05-07 17:28:28,038 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 102 transitions. Word has length 51
[2025-05-07 17:28:28,039 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:28,039 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 102 transitions.
[2025-05-07 17:28:28,040 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:28:28,040 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 102 transitions.
[2025-05-07 17:28:28,042 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-05-07 17:28:28,043 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:28,043 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:28,043 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:28,043 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:28,044 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:28,044 INFO  L85        PathProgramCache]: Analyzing trace with hash -816802854, now seen corresponding path program 1 times
[2025-05-07 17:28:28,045 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:28,045 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1223978441]
[2025-05-07 17:28:28,045 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:28,045 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:28,080 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-05-07 17:28:28,122 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-05-07 17:28:28,122 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:28,122 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:28,366 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-05-07 17:28:28,366 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:28,366 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1223978441]
[2025-05-07 17:28:28,366 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1223978441] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:28,366 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:28,366 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:28,366 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [965922425]
[2025-05-07 17:28:28,366 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:28,367 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:28,367 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:28,368 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:28,368 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:28,368 INFO  L87              Difference]: Start difference. First operand 84 states and 102 transitions. Second operand  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 4 states have call successors, (17), 1 states have call predecessors, (17), 4 states have return successors, (17), 4 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:28:28,405 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:28,405 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:28:28,406 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:28,406 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 4 states have call successors, (17), 1 states have call predecessors, (17), 4 states have return successors, (17), 4 states have call predecessors, (17), 4 states have call successors, (17) Word has length 67
[2025-05-07 17:28:28,406 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:28,407 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:28:28,408 INFO  L226             Difference]: Without dead ends: 84
[2025-05-07 17:28:28,408 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:28,409 INFO  L437           NwaCegarLoop]: 101 mSDtfsCounter, 1 mSDsluCounter, 289 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 390 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:28,409 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 390 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:28,410 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-05-07 17:28:28,417 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 82.
[2025-05-07 17:28:28,417 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 33 states have (on average 1.0606060606060606) internal successors, (35), 35 states have internal predecessors, (35), 29 states have call successors, (31), 19 states have call predecessors, (31), 19 states have return successors, (31), 28 states have call predecessors, (31), 29 states have call successors, (31)
[2025-05-07 17:28:28,419 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 97 transitions.
[2025-05-07 17:28:28,419 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 97 transitions. Word has length 67
[2025-05-07 17:28:28,419 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:28,419 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 97 transitions.
[2025-05-07 17:28:28,419 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 4 states have call successors, (17), 1 states have call predecessors, (17), 4 states have return successors, (17), 4 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:28:28,420 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 97 transitions.
[2025-05-07 17:28:28,421 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-05-07 17:28:28,421 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:28,422 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:28:28,422 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:28,422 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:28,422 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:28,422 INFO  L85        PathProgramCache]: Analyzing trace with hash 271404638, now seen corresponding path program 1 times
[2025-05-07 17:28:28,422 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:28,423 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1134317508]
[2025-05-07 17:28:28,423 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:28,423 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:28,447 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-05-07 17:28:28,463 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-05-07 17:28:28,463 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:28,463 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:28,548 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-05-07 17:28:28,549 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:28,549 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1134317508]
[2025-05-07 17:28:28,549 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1134317508] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:28,549 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1067504233]
[2025-05-07 17:28:28,549 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:28,549 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:28,552 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:28,554 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:28,555 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:28:28,732 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-05-07 17:28:28,824 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-05-07 17:28:28,824 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:28,824 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:28,828 INFO  L256         TraceCheckSpWp]: Trace formula consists of 739 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:28,835 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:28,908 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:28,908 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:28,908 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1067504233] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:28,909 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:28,909 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [4] total 7
[2025-05-07 17:28:28,909 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [981806851]
[2025-05-07 17:28:28,909 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:28,909 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:28,909 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:28,910 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:28,910 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:28,910 INFO  L87              Difference]: Start difference. First operand 82 states and 97 transitions. Second operand  has 6 states, 4 states have (on average 7.75) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (18), 2 states have call predecessors, (18), 3 states have return successors, (18), 2 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:29,010 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:29,010 INFO  L93              Difference]: Finished difference Result 86 states and 108 transitions.
[2025-05-07 17:28:29,010 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:29,010 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 7.75) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (18), 2 states have call predecessors, (18), 3 states have return successors, (18), 2 states have call predecessors, (18), 4 states have call successors, (18) Word has length 67
[2025-05-07 17:28:29,010 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:29,011 INFO  L225             Difference]: With dead ends: 86
[2025-05-07 17:28:29,011 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:28:29,011 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 65 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:29,012 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 3 mSDsluCounter, 322 mSDsCounter, 0 mSdLazyCounter, 91 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 409 SdHoareTripleChecker+Invalid, 91 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 91 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:29,012 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 409 Invalid, 91 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 91 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:29,012 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:28:29,017 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:28:29,017 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 35 states have (on average 1.0571428571428572) internal successors, (37), 37 states have internal predecessors, (37), 29 states have call successors, (31), 19 states have call predecessors, (31), 21 states have return successors, (40), 29 states have call predecessors, (40), 29 states have call successors, (40)
[2025-05-07 17:28:29,018 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 108 transitions.
[2025-05-07 17:28:29,018 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 108 transitions. Word has length 67
[2025-05-07 17:28:29,018 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:29,018 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 108 transitions.
[2025-05-07 17:28:29,018 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 7.75) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (18), 2 states have call predecessors, (18), 3 states have return successors, (18), 2 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:29,018 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 108 transitions.
[2025-05-07 17:28:29,020 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:28:29,020 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:29,020 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 3, 3, 3, 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]
[2025-05-07 17:28:29,026 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:28:29,221 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:29,221 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:29,222 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:29,222 INFO  L85        PathProgramCache]: Analyzing trace with hash 1386543063, now seen corresponding path program 1 times
[2025-05-07 17:28:29,222 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:29,222 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1964804304]
[2025-05-07 17:28:29,222 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:29,222 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:29,253 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:29,275 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:29,276 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:29,276 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:29,505 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-05-07 17:28:29,505 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:29,505 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1964804304]
[2025-05-07 17:28:29,505 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1964804304] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:29,505 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:29,505 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-05-07 17:28:29,505 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [381068207]
[2025-05-07 17:28:29,505 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:29,506 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-05-07 17:28:29,506 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:29,506 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-05-07 17:28:29,506 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:28:29,507 INFO  L87              Difference]: Start difference. First operand 86 states and 108 transitions. Second operand  has 9 states, 6 states have (on average 5.0) internal successors, (30), 9 states have internal predecessors, (30), 8 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 8 states have call successors, (20)
[2025-05-07 17:28:29,596 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:29,596 INFO  L93              Difference]: Finished difference Result 91 states and 114 transitions.
[2025-05-07 17:28:29,597 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:28:29,597 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 5.0) internal successors, (30), 9 states have internal predecessors, (30), 8 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 8 states have call successors, (20) Word has length 91
[2025-05-07 17:28:29,597 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:29,598 INFO  L225             Difference]: With dead ends: 91
[2025-05-07 17:28:29,598 INFO  L226             Difference]: Without dead ends: 91
[2025-05-07 17:28:29,598 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=20, Invalid=70, Unknown=0, NotChecked=0, Total=90
[2025-05-07 17:28:29,598 INFO  L437           NwaCegarLoop]: 92 mSDtfsCounter, 3 mSDsluCounter, 609 mSDsCounter, 0 mSdLazyCounter, 64 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 701 SdHoareTripleChecker+Invalid, 67 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 64 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:29,599 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 701 Invalid, 67 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 64 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:29,599 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-05-07 17:28:29,603 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 91.
[2025-05-07 17:28:29,603 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 37 states have (on average 1.054054054054054) internal successors, (39), 39 states have internal predecessors, (39), 30 states have call successors, (32), 19 states have call predecessors, (32), 23 states have return successors, (43), 32 states have call predecessors, (43), 30 states have call successors, (43)
[2025-05-07 17:28:29,604 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 114 transitions.
[2025-05-07 17:28:29,604 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 114 transitions. Word has length 91
[2025-05-07 17:28:29,604 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:29,604 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 114 transitions.
[2025-05-07 17:28:29,604 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 5.0) internal successors, (30), 9 states have internal predecessors, (30), 8 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 8 states have call successors, (20)
[2025-05-07 17:28:29,604 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 114 transitions.
[2025-05-07 17:28:29,605 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:28:29,605 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:29,605 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:29,605 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:29,605 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:29,606 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:29,606 INFO  L85        PathProgramCache]: Analyzing trace with hash -471989669, now seen corresponding path program 1 times
[2025-05-07 17:28:29,606 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:29,606 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [225617801]
[2025-05-07 17:28:29,606 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:29,606 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:29,628 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:28:29,638 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:28:29,639 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:29,639 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:29,709 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-05-07 17:28:29,709 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:29,709 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [225617801]
[2025-05-07 17:28:29,709 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [225617801] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:29,709 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:29,709 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:29,709 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2078274975]
[2025-05-07 17:28:29,709 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:29,710 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:29,710 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:29,710 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:29,710 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:29,710 INFO  L87              Difference]: Start difference. First operand 91 states and 114 transitions. Second operand  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 5 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:28:29,739 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:29,739 INFO  L93              Difference]: Finished difference Result 96 states and 120 transitions.
[2025-05-07 17:28:29,740 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:29,740 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), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 5 states have call predecessors, (18), 5 states have call successors, (18) Word has length 75
[2025-05-07 17:28:29,740 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:29,741 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:28:29,741 INFO  L226             Difference]: Without dead ends: 96
[2025-05-07 17:28:29,741 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:29,742 INFO  L437           NwaCegarLoop]: 100 mSDtfsCounter, 1 mSDsluCounter, 383 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 483 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:28:29,742 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 483 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:29,742 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-05-07 17:28:29,747 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 91.
[2025-05-07 17:28:29,747 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 37 states have (on average 1.054054054054054) internal successors, (39), 39 states have internal predecessors, (39), 30 states have call successors, (32), 19 states have call predecessors, (32), 23 states have return successors, (43), 32 states have call predecessors, (43), 30 states have call successors, (43)
[2025-05-07 17:28:29,748 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 114 transitions.
[2025-05-07 17:28:29,748 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 114 transitions. Word has length 75
[2025-05-07 17:28:29,748 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:29,748 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 114 transitions.
[2025-05-07 17:28:29,748 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), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 5 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:28:29,749 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 114 transitions.
[2025-05-07 17:28:29,749 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:28:29,749 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:29,749 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:29,749 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:29,750 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:29,750 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:29,750 INFO  L85        PathProgramCache]: Analyzing trace with hash -1969450456, now seen corresponding path program 1 times
[2025-05-07 17:28:29,750 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:29,750 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [581189973]
[2025-05-07 17:28:29,750 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:29,750 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:29,768 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:29,781 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:29,781 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:29,781 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:29,963 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 0 proven. 16 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-05-07 17:28:29,963 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:29,964 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [581189973]
[2025-05-07 17:28:29,964 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [581189973] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:29,964 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2120938840]
[2025-05-07 17:28:29,964 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:29,964 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:29,966 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:29,967 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:29,968 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:28:30,124 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:28:30,206 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:28:30,207 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:30,207 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:30,210 INFO  L256         TraceCheckSpWp]: Trace formula consists of 799 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:30,213 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:30,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 21 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-05-07 17:28:30,279 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:31,197 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 0 proven. 16 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-05-07 17:28:31,197 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2120938840] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:31,197 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:31,198 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 16
[2025-05-07 17:28:31,198 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1150128229]
[2025-05-07 17:28:31,198 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:31,198 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:28:31,198 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:31,198 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:28:31,199 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=198, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:28:31,199 INFO  L87              Difference]: Start difference. First operand 91 states and 114 transitions. Second operand  has 16 states, 8 states have (on average 8.25) internal successors, (66), 16 states have internal predecessors, (66), 10 states have call successors, (39), 2 states have call predecessors, (39), 8 states have return successors, (42), 6 states have call predecessors, (42), 10 states have call successors, (42)
[2025-05-07 17:28:31,350 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:31,351 INFO  L93              Difference]: Finished difference Result 97 states and 127 transitions.
[2025-05-07 17:28:31,351 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-05-07 17:28:31,351 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 8.25) internal successors, (66), 16 states have internal predecessors, (66), 10 states have call successors, (39), 2 states have call predecessors, (39), 8 states have return successors, (42), 6 states have call predecessors, (42), 10 states have call successors, (42) Word has length 83
[2025-05-07 17:28:31,351 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:31,352 INFO  L225             Difference]: With dead ends: 97
[2025-05-07 17:28:31,353 INFO  L226             Difference]: Without dead ends: 97
[2025-05-07 17:28:31,353 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 179 GetRequests, 159 SyntacticMatches, 4 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 53 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=52, Invalid=254, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:28:31,353 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 7 mSDsluCounter, 797 mSDsCounter, 0 mSdLazyCounter, 193 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 882 SdHoareTripleChecker+Invalid, 194 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 193 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:31,354 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 882 Invalid, 194 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 193 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:31,354 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 97 states.
[2025-05-07 17:28:31,361 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 97 to 95.
[2025-05-07 17:28:31,362 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 95 states, 39 states have (on average 1.0512820512820513) internal successors, (41), 41 states have internal predecessors, (41), 30 states have call successors, (32), 19 states have call predecessors, (32), 25 states have return successors, (46), 34 states have call predecessors, (46), 30 states have call successors, (46)
[2025-05-07 17:28:31,363 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 95 states to 95 states and 119 transitions.
[2025-05-07 17:28:31,363 INFO  L79                 Accepts]: Start accepts. Automaton has 95 states and 119 transitions. Word has length 83
[2025-05-07 17:28:31,363 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:31,363 INFO  L485      AbstractCegarLoop]: Abstraction has 95 states and 119 transitions.
[2025-05-07 17:28:31,363 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 8.25) internal successors, (66), 16 states have internal predecessors, (66), 10 states have call successors, (39), 2 states have call predecessors, (39), 8 states have return successors, (42), 6 states have call predecessors, (42), 10 states have call successors, (42)
[2025-05-07 17:28:31,363 INFO  L278                IsEmpty]: Start isEmpty. Operand 95 states and 119 transitions.
[2025-05-07 17:28:31,365 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 100
[2025-05-07 17:28:31,365 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:31,365 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 4, 4, 4, 4, 4, 4, 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]
[2025-05-07 17:28:31,369 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:28:31,566 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:31,566 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:31,567 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:31,567 INFO  L85        PathProgramCache]: Analyzing trace with hash 1039358194, now seen corresponding path program 2 times
[2025-05-07 17:28:31,568 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:31,568 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [262544001]
[2025-05-07 17:28:31,568 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:28:31,569 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:31,620 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 99 statements into 2 equivalence classes.
[2025-05-07 17:28:31,640 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 99 of 99 statements.
[2025-05-07 17:28:31,640 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:28:31,641 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:31,884 INFO  L134       CoverageAnalysis]: Checked inductivity of 79 backedges. 1 proven. 41 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-05-07 17:28:31,884 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:31,884 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [262544001]
[2025-05-07 17:28:31,884 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [262544001] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:31,884 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1154671664]
[2025-05-07 17:28:31,884 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:28:31,884 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:31,886 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:31,888 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:31,889 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:28:32,039 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 99 statements into 2 equivalence classes.
[2025-05-07 17:28:32,119 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 99 of 99 statements.
[2025-05-07 17:28:32,119 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:28:32,119 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:32,122 INFO  L256         TraceCheckSpWp]: Trace formula consists of 859 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:32,126 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:32,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 79 backedges. 51 proven. 8 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-05-07 17:28:32,189 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:33,748 INFO  L134       CoverageAnalysis]: Checked inductivity of 79 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-05-07 17:28:33,748 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1154671664] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:33,748 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:33,748 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 11, 12] total 20
[2025-05-07 17:28:33,748 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1096489882]
[2025-05-07 17:28:33,748 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:33,749 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-05-07 17:28:33,749 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:33,749 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-05-07 17:28:33,749 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=317, Unknown=0, NotChecked=0, Total=380
[2025-05-07 17:28:33,750 INFO  L87              Difference]: Start difference. First operand 95 states and 119 transitions. Second operand  has 20 states, 10 states have (on average 7.0) internal successors, (70), 20 states have internal predecessors, (70), 12 states have call successors, (41), 2 states have call predecessors, (41), 10 states have return successors, (45), 8 states have call predecessors, (45), 12 states have call successors, (45)
[2025-05-07 17:28:33,894 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:33,894 INFO  L93              Difference]: Finished difference Result 101 states and 132 transitions.
[2025-05-07 17:28:33,894 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-05-07 17:28:33,894 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 7.0) internal successors, (70), 20 states have internal predecessors, (70), 12 states have call successors, (41), 2 states have call predecessors, (41), 10 states have return successors, (45), 8 states have call predecessors, (45), 12 states have call successors, (45) Word has length 99
[2025-05-07 17:28:33,895 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:33,895 INFO  L225             Difference]: With dead ends: 101
[2025-05-07 17:28:33,895 INFO  L226             Difference]: Without dead ends: 101
[2025-05-07 17:28:33,896 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 215 GetRequests, 188 SyntacticMatches, 6 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 141 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=84, Invalid=422, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:28:33,896 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 8 mSDsluCounter, 886 mSDsCounter, 0 mSdLazyCounter, 202 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 971 SdHoareTripleChecker+Invalid, 203 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 202 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:33,897 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 971 Invalid, 203 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 202 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:33,897 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-05-07 17:28:33,904 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 99.
[2025-05-07 17:28:33,904 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 30 states have call successors, (32), 19 states have call predecessors, (32), 27 states have return successors, (49), 36 states have call predecessors, (49), 30 states have call successors, (49)
[2025-05-07 17:28:33,905 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 124 transitions.
[2025-05-07 17:28:33,905 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 124 transitions. Word has length 99
[2025-05-07 17:28:33,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:33,906 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 124 transitions.
[2025-05-07 17:28:33,906 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 7.0) internal successors, (70), 20 states have internal predecessors, (70), 12 states have call successors, (41), 2 states have call predecessors, (41), 10 states have return successors, (45), 8 states have call predecessors, (45), 12 states have call successors, (45)
[2025-05-07 17:28:33,906 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 124 transitions.
[2025-05-07 17:28:33,907 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 116
[2025-05-07 17:28:33,907 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:33,908 INFO  L218           NwaCegarLoop]: trace histogram [8, 6, 6, 6, 6, 6, 6, 6, 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]
[2025-05-07 17:28:33,912 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:28:34,108 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:34,109 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:34,110 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:34,110 INFO  L85        PathProgramCache]: Analyzing trace with hash 1302635196, now seen corresponding path program 3 times
[2025-05-07 17:28:34,110 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:34,110 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [418673612]
[2025-05-07 17:28:34,110 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:28:34,111 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:34,165 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 115 statements into 5 equivalence classes.
[2025-05-07 17:28:34,215 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 107 of 115 statements.
[2025-05-07 17:28:34,215 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-05-07 17:28:34,215 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,445 INFO  L134       CoverageAnalysis]: Checked inductivity of 163 backedges. 63 proven. 19 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-05-07 17:28:34,446 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:34,446 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [418673612]
[2025-05-07 17:28:34,446 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [418673612] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:34,446 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [981905795]
[2025-05-07 17:28:34,446 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:28:34,446 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:34,448 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:34,450 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:34,451 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:28:34,658 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 115 statements into 5 equivalence classes.
[2025-05-07 17:28:34,730 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 107 of 115 statements.
[2025-05-07 17:28:34,730 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-05-07 17:28:34,730 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:34,733 INFO  L256         TraceCheckSpWp]: Trace formula consists of 889 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:34,735 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:34,795 INFO  L134       CoverageAnalysis]: Checked inductivity of 163 backedges. 62 proven. 18 refuted. 0 times theorem prover too weak. 83 trivial. 0 not checked.
[2025-05-07 17:28:34,795 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:37,818 INFO  L134       CoverageAnalysis]: Checked inductivity of 163 backedges. 62 proven. 21 refuted. 0 times theorem prover too weak. 80 trivial. 0 not checked.
[2025-05-07 17:28:37,818 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [981905795] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:37,818 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:37,818 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 13, 15] total 22
[2025-05-07 17:28:37,819 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2132294467]
[2025-05-07 17:28:37,819 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:37,819 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-05-07 17:28:37,819 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:37,820 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-05-07 17:28:37,820 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=81, Invalid=381, Unknown=0, NotChecked=0, Total=462
[2025-05-07 17:28:37,820 INFO  L87              Difference]: Start difference. First operand 99 states and 124 transitions. Second operand  has 22 states, 12 states have (on average 5.416666666666667) internal successors, (65), 22 states have internal predecessors, (65), 12 states have call successors, (39), 2 states have call predecessors, (39), 12 states have return successors, (46), 13 states have call predecessors, (46), 12 states have call successors, (46)
[2025-05-07 17:28:37,959 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:37,959 INFO  L93              Difference]: Finished difference Result 105 states and 136 transitions.
[2025-05-07 17:28:37,960 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:28:37,960 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 12 states have (on average 5.416666666666667) internal successors, (65), 22 states have internal predecessors, (65), 12 states have call successors, (39), 2 states have call predecessors, (39), 12 states have return successors, (46), 13 states have call predecessors, (46), 12 states have call successors, (46) Word has length 115
[2025-05-07 17:28:37,961 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:37,961 INFO  L225             Difference]: With dead ends: 105
[2025-05-07 17:28:37,962 INFO  L226             Difference]: Without dead ends: 105
[2025-05-07 17:28:37,962 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 249 GetRequests, 217 SyntacticMatches, 8 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 227 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=116, Invalid=534, Unknown=0, NotChecked=0, Total=650
[2025-05-07 17:28:37,962 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 17 mSDsluCounter, 579 mSDsCounter, 0 mSdLazyCounter, 141 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 666 SdHoareTripleChecker+Invalid, 152 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 141 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:37,963 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 666 Invalid, 152 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 141 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:37,963 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 105 states.
[2025-05-07 17:28:37,971 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 105 to 105.
[2025-05-07 17:28:37,971 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 44 states have (on average 1.0454545454545454) internal successors, (46), 46 states have internal predecessors, (46), 30 states have call successors, (32), 19 states have call predecessors, (32), 30 states have return successors, (58), 39 states have call predecessors, (58), 30 states have call successors, (58)
[2025-05-07 17:28:37,972 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 136 transitions.
[2025-05-07 17:28:37,972 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 136 transitions. Word has length 115
[2025-05-07 17:28:37,973 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:37,973 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 136 transitions.
[2025-05-07 17:28:37,973 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 12 states have (on average 5.416666666666667) internal successors, (65), 22 states have internal predecessors, (65), 12 states have call successors, (39), 2 states have call predecessors, (39), 12 states have return successors, (46), 13 states have call predecessors, (46), 12 states have call successors, (46)
[2025-05-07 17:28:37,973 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 136 transitions.
[2025-05-07 17:28:37,974 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 124
[2025-05-07 17:28:37,974 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:37,975 INFO  L218           NwaCegarLoop]: trace histogram [9, 7, 7, 7, 7, 7, 7, 7, 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]
[2025-05-07 17:28:37,979 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:28:38,175 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:38,175 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,176 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,176 INFO  L85        PathProgramCache]: Analyzing trace with hash -103781343, now seen corresponding path program 4 times
[2025-05-07 17:28:38,176 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,176 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1303169836]
[2025-05-07 17:28:38,176 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:28:38,176 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,205 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 123 statements into 2 equivalence classes.
[2025-05-07 17:28:38,236 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 123 of 123 statements.
[2025-05-07 17:28:38,236 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:28:38,236 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,936 INFO  L134       CoverageAnalysis]: Checked inductivity of 217 backedges. 36 proven. 103 refuted. 0 times theorem prover too weak. 78 trivial. 0 not checked.
[2025-05-07 17:28:38,936 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1303169836]
[2025-05-07 17:28:38,936 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1303169836] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:38,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1880926290]
[2025-05-07 17:28:38,936 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:28:38,937 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:38,938 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:38,940 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:38,941 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-05-07 17:28:39,241 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 123 statements into 2 equivalence classes.
[2025-05-07 17:28:39,350 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 123 of 123 statements.
[2025-05-07 17:28:39,350 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:28:39,350 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,353 INFO  L256         TraceCheckSpWp]: Trace formula consists of 949 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:39,355 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:39,438 INFO  L134       CoverageAnalysis]: Checked inductivity of 217 backedges. 124 proven. 18 refuted. 0 times theorem prover too weak. 75 trivial. 0 not checked.
[2025-05-07 17:28:39,438 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:42,069 INFO  L134       CoverageAnalysis]: Checked inductivity of 217 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 117 trivial. 0 not checked.
[2025-05-07 17:28:42,069 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1880926290] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:42,069 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:42,069 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [25, 13, 15] total 33
[2025-05-07 17:28:42,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [185496204]
[2025-05-07 17:28:42,069 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:42,070 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-05-07 17:28:42,070 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:42,071 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-05-07 17:28:42,071 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=108, Invalid=948, Unknown=0, NotChecked=0, Total=1056
[2025-05-07 17:28:42,071 INFO  L87              Difference]: Start difference. First operand 105 states and 136 transitions. Second operand  has 33 states, 21 states have (on average 3.9523809523809526) internal successors, (83), 32 states have internal predecessors, (83), 15 states have call successors, (44), 2 states have call predecessors, (44), 21 states have return successors, (58), 20 states have call predecessors, (58), 15 states have call successors, (58)
[2025-05-07 17:28:42,759 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:42,760 INFO  L93              Difference]: Finished difference Result 136 states and 186 transitions.
[2025-05-07 17:28:42,760 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 38 states. 
[2025-05-07 17:28:42,760 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 21 states have (on average 3.9523809523809526) internal successors, (83), 32 states have internal predecessors, (83), 15 states have call successors, (44), 2 states have call predecessors, (44), 21 states have return successors, (58), 20 states have call predecessors, (58), 15 states have call successors, (58) Word has length 123
[2025-05-07 17:28:42,760 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:42,761 INFO  L225             Difference]: With dead ends: 136
[2025-05-07 17:28:42,761 INFO  L226             Difference]: Without dead ends: 136
[2025-05-07 17:28:42,762 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 305 GetRequests, 236 SyntacticMatches, 8 SemanticMatches, 61 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 898 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=409, Invalid=3497, Unknown=0, NotChecked=0, Total=3906
[2025-05-07 17:28:42,762 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 34 mSDsluCounter, 1871 mSDsCounter, 0 mSdLazyCounter, 766 mSolverCounterSat, 46 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 43 SdHoareTripleChecker+Valid, 1961 SdHoareTripleChecker+Invalid, 812 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 46 IncrementalHoareTripleChecker+Valid, 766 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:42,762 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [43 Valid, 1961 Invalid, 812 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [46 Valid, 766 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:28:42,763 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 136 states.
[2025-05-07 17:28:42,768 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 136 to 133.
[2025-05-07 17:28:42,769 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 58 states have (on average 1.0517241379310345) internal successors, (61), 61 states have internal predecessors, (61), 38 states have call successors, (40), 27 states have call predecessors, (40), 36 states have return successors, (72), 44 states have call predecessors, (72), 38 states have call successors, (72)
[2025-05-07 17:28:42,769 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 173 transitions.
[2025-05-07 17:28:42,769 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 173 transitions. Word has length 123
[2025-05-07 17:28:42,769 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:42,770 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 173 transitions.
[2025-05-07 17:28:42,770 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 21 states have (on average 3.9523809523809526) internal successors, (83), 32 states have internal predecessors, (83), 15 states have call successors, (44), 2 states have call predecessors, (44), 21 states have return successors, (58), 20 states have call predecessors, (58), 15 states have call successors, (58)
[2025-05-07 17:28:42,770 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 173 transitions.
[2025-05-07 17:28:42,771 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 132
[2025-05-07 17:28:42,771 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:42,771 INFO  L218           NwaCegarLoop]: trace histogram [10, 8, 8, 8, 8, 8, 8, 8, 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]
[2025-05-07 17:28:42,775 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-05-07 17:28:42,971 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:42,972 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:42,973 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:42,973 INFO  L85        PathProgramCache]: Analyzing trace with hash -144478330, now seen corresponding path program 5 times
[2025-05-07 17:28:42,973 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:42,974 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [201094035]
[2025-05-07 17:28:42,974 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-05-07 17:28:42,974 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:43,033 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 131 statements into 6 equivalence classes.
[2025-05-07 17:28:43,053 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 131 of 131 statements.
[2025-05-07 17:28:43,053 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-05-07 17:28:43,053 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:43,342 INFO  L134       CoverageAnalysis]: Checked inductivity of 279 backedges. 3 proven. 133 refuted. 0 times theorem prover too weak. 143 trivial. 0 not checked.
[2025-05-07 17:28:43,342 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:43,343 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [201094035]
[2025-05-07 17:28:43,343 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [201094035] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:43,343 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [138266929]
[2025-05-07 17:28:43,343 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-05-07 17:28:43,343 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:43,345 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:43,347 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:43,348 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-05-07 17:28:43,697 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 131 statements into 6 equivalence classes.
[2025-05-07 17:28:43,812 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 131 of 131 statements.
[2025-05-07 17:28:43,812 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-05-07 17:28:43,812 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:43,815 INFO  L256         TraceCheckSpWp]: Trace formula consists of 979 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:43,817 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:43,878 INFO  L134       CoverageAnalysis]: Checked inductivity of 279 backedges. 159 proven. 32 refuted. 0 times theorem prover too weak. 88 trivial. 0 not checked.
[2025-05-07 17:28:43,878 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:48,449 INFO  L134       CoverageAnalysis]: Checked inductivity of 279 backedges. 0 proven. 139 refuted. 0 times theorem prover too weak. 140 trivial. 0 not checked.
[2025-05-07 17:28:48,449 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [138266929] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:48,449 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:48,449 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 15, 18] total 25
[2025-05-07 17:28:48,450 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1111709260]
[2025-05-07 17:28:48,450 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:48,450 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-05-07 17:28:48,450 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:48,450 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-05-07 17:28:48,451 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=104, Invalid=496, Unknown=0, NotChecked=0, Total=600
[2025-05-07 17:28:48,451 INFO  L87              Difference]: Start difference. First operand 133 states and 173 transitions. Second operand  has 25 states, 14 states have (on average 5.357142857142857) internal successors, (75), 25 states have internal predecessors, (75), 13 states have call successors, (42), 2 states have call predecessors, (42), 14 states have return successors, (52), 12 states have call predecessors, (52), 13 states have call successors, (52)
[2025-05-07 17:28:48,611 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:48,611 INFO  L93              Difference]: Finished difference Result 139 states and 194 transitions.
[2025-05-07 17:28:48,611 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-05-07 17:28:48,612 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 14 states have (on average 5.357142857142857) internal successors, (75), 25 states have internal predecessors, (75), 13 states have call successors, (42), 2 states have call predecessors, (42), 14 states have return successors, (52), 12 states have call predecessors, (52), 13 states have call successors, (52) Word has length 131
[2025-05-07 17:28:48,612 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:48,613 INFO  L225             Difference]: With dead ends: 139
[2025-05-07 17:28:48,613 INFO  L226             Difference]: Without dead ends: 139
[2025-05-07 17:28:48,613 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 285 GetRequests, 247 SyntacticMatches, 10 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 329 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=157, Invalid=713, Unknown=0, NotChecked=0, Total=870
[2025-05-07 17:28:48,613 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 12 mSDsluCounter, 901 mSDsCounter, 0 mSdLazyCounter, 200 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 988 SdHoareTripleChecker+Invalid, 206 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 200 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:48,613 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 988 Invalid, 206 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 200 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:48,614 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 139 states.
[2025-05-07 17:28:48,619 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 139 to 139.
[2025-05-07 17:28:48,619 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 61 states have (on average 1.0491803278688525) internal successors, (64), 64 states have internal predecessors, (64), 38 states have call successors, (40), 27 states have call predecessors, (40), 39 states have return successors, (90), 47 states have call predecessors, (90), 38 states have call successors, (90)
[2025-05-07 17:28:48,620 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 194 transitions.
[2025-05-07 17:28:48,620 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 194 transitions. Word has length 131
[2025-05-07 17:28:48,620 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:48,620 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 194 transitions.
[2025-05-07 17:28:48,620 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 14 states have (on average 5.357142857142857) internal successors, (75), 25 states have internal predecessors, (75), 13 states have call successors, (42), 2 states have call predecessors, (42), 14 states have return successors, (52), 12 states have call predecessors, (52), 13 states have call successors, (52)
[2025-05-07 17:28:48,620 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 194 transitions.
[2025-05-07 17:28:48,621 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 140
[2025-05-07 17:28:48,621 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:48,621 INFO  L218           NwaCegarLoop]: trace histogram [11, 9, 9, 9, 9, 9, 9, 9, 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]
[2025-05-07 17:28:48,626 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-05-07 17:28:48,822 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:48,823 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:48,823 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:48,824 INFO  L85        PathProgramCache]: Analyzing trace with hash -785159829, now seen corresponding path program 6 times
[2025-05-07 17:28:48,824 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:48,824 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1712443030]
[2025-05-07 17:28:48,824 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-05-07 17:28:48,825 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:48,901 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 139 statements into 7 equivalence classes.
[2025-05-07 17:28:48,946 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 139 of 139 statements.
[2025-05-07 17:28:48,946 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-05-07 17:28:48,946 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:49,213 INFO  L134       CoverageAnalysis]: Checked inductivity of 349 backedges. 125 proven. 35 refuted. 0 times theorem prover too weak. 189 trivial. 0 not checked.
[2025-05-07 17:28:49,213 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:49,213 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1712443030]
[2025-05-07 17:28:49,213 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1712443030] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:49,213 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1499304049]
[2025-05-07 17:28:49,213 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-05-07 17:28:49,214 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:49,215 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:49,217 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:49,218 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-05-07 17:28:49,609 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 139 statements into 7 equivalence classes.
[2025-05-07 17:28:49,702 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 139 of 139 statements.
[2025-05-07 17:28:49,702 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-05-07 17:28:49,702 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:49,705 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1009 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:49,707 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:49,773 INFO  L134       CoverageAnalysis]: Checked inductivity of 349 backedges. 123 proven. 32 refuted. 0 times theorem prover too weak. 194 trivial. 0 not checked.
[2025-05-07 17:28:49,773 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:54,282 INFO  L134       CoverageAnalysis]: Checked inductivity of 349 backedges. 123 proven. 38 refuted. 0 times theorem prover too weak. 188 trivial. 0 not checked.
[2025-05-07 17:28:54,283 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1499304049] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:54,283 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:54,283 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [17, 15, 18] total 26
[2025-05-07 17:28:54,283 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [327430377]
[2025-05-07 17:28:54,283 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:54,283 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-05-07 17:28:54,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:54,283 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-05-07 17:28:54,284 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=112, Invalid=538, Unknown=0, NotChecked=0, Total=650
[2025-05-07 17:28:54,284 INFO  L87              Difference]: Start difference. First operand 139 states and 194 transitions. Second operand  has 26 states, 14 states have (on average 4.928571428571429) internal successors, (69), 26 states have internal predecessors, (69), 14 states have call successors, (41), 2 states have call predecessors, (41), 14 states have return successors, (50), 15 states have call predecessors, (50), 14 states have call successors, (50)
[2025-05-07 17:28:54,430 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:54,430 INFO  L93              Difference]: Finished difference Result 139 states and 193 transitions.
[2025-05-07 17:28:54,430 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-05-07 17:28:54,431 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 14 states have (on average 4.928571428571429) internal successors, (69), 26 states have internal predecessors, (69), 14 states have call successors, (41), 2 states have call predecessors, (41), 14 states have return successors, (50), 15 states have call predecessors, (50), 14 states have call successors, (50) Word has length 139
[2025-05-07 17:28:54,431 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:54,432 INFO  L225             Difference]: With dead ends: 139
[2025-05-07 17:28:54,432 INFO  L226             Difference]: Without dead ends: 139
[2025-05-07 17:28:54,432 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 300 GetRequests, 261 SyntacticMatches, 10 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 405 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=169, Invalid=761, Unknown=0, NotChecked=0, Total=930
[2025-05-07 17:28:54,432 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 15 mSDsluCounter, 982 mSDsCounter, 0 mSdLazyCounter, 204 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 1069 SdHoareTripleChecker+Invalid, 212 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 204 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:54,432 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 1069 Invalid, 212 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 204 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:54,433 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 139 states.
[2025-05-07 17:28:54,437 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 139 to 137.
[2025-05-07 17:28:54,437 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 38 states have call successors, (40), 27 states have call predecessors, (40), 38 states have return successors, (77), 46 states have call predecessors, (77), 38 states have call successors, (77)
[2025-05-07 17:28:54,438 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 180 transitions.
[2025-05-07 17:28:54,438 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 180 transitions. Word has length 139
[2025-05-07 17:28:54,438 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:54,438 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 180 transitions.
[2025-05-07 17:28:54,438 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 14 states have (on average 4.928571428571429) internal successors, (69), 26 states have internal predecessors, (69), 14 states have call successors, (41), 2 states have call predecessors, (41), 14 states have return successors, (50), 15 states have call predecessors, (50), 14 states have call successors, (50)
[2025-05-07 17:28:54,438 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 180 transitions.
[2025-05-07 17:28:54,440 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 148
[2025-05-07 17:28:54,440 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:54,440 INFO  L218           NwaCegarLoop]: trace histogram [12, 10, 10, 10, 10, 10, 10, 10, 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]
[2025-05-07 17:28:54,445 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-05-07 17:28:54,640 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-05-07 17:28:54,641 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:54,642 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:54,642 INFO  L85        PathProgramCache]: Analyzing trace with hash 1394786128, now seen corresponding path program 7 times
[2025-05-07 17:28:54,642 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:54,642 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1922524798]
[2025-05-07 17:28:54,642 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-05-07 17:28:54,643 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:54,699 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 147 statements into 1 equivalence classes.
[2025-05-07 17:28:54,713 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 147 of 147 statements.
[2025-05-07 17:28:54,713 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:54,713 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:55,085 INFO  L134       CoverageAnalysis]: Checked inductivity of 427 backedges. 4 proven. 200 refuted. 0 times theorem prover too weak. 223 trivial. 0 not checked.
[2025-05-07 17:28:55,085 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:55,085 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1922524798]
[2025-05-07 17:28:55,085 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1922524798] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:55,085 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1475177930]
[2025-05-07 17:28:55,085 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-05-07 17:28:55,085 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:55,087 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:55,088 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:55,089 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-05-07 17:28:55,595 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 147 statements into 1 equivalence classes.
[2025-05-07 17:28:55,682 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 147 of 147 statements.
[2025-05-07 17:28:55,682 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:55,682 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:55,686 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1039 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:55,696 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:55,757 INFO  L134       CoverageAnalysis]: Checked inductivity of 427 backedges. 237 proven. 50 refuted. 0 times theorem prover too weak. 140 trivial. 0 not checked.
[2025-05-07 17:28:55,757 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:02,511 INFO  L134       CoverageAnalysis]: Checked inductivity of 427 backedges. 0 proven. 210 refuted. 0 times theorem prover too weak. 217 trivial. 0 not checked.
[2025-05-07 17:29:02,511 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1475177930] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:02,511 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:02,512 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [19, 17, 21] total 29
[2025-05-07 17:29:02,512 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1344534692]
[2025-05-07 17:29:02,512 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:02,512 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 29 states
[2025-05-07 17:29:02,512 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:02,512 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 29 interpolants.
[2025-05-07 17:29:02,513 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=132, Invalid=680, Unknown=0, NotChecked=0, Total=812
[2025-05-07 17:29:02,513 INFO  L87              Difference]: Start difference. First operand 137 states and 180 transitions. Second operand  has 29 states, 16 states have (on average 4.9375) internal successors, (79), 29 states have internal predecessors, (79), 15 states have call successors, (44), 2 states have call predecessors, (44), 16 states have return successors, (57), 14 states have call predecessors, (57), 15 states have call successors, (57)
[2025-05-07 17:29:02,697 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:02,697 INFO  L93              Difference]: Finished difference Result 143 states and 201 transitions.
[2025-05-07 17:29:02,697 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-05-07 17:29:02,697 INFO  L79                 Accepts]: Start accepts. Automaton has  has 29 states, 16 states have (on average 4.9375) internal successors, (79), 29 states have internal predecessors, (79), 15 states have call successors, (44), 2 states have call predecessors, (44), 16 states have return successors, (57), 14 states have call predecessors, (57), 15 states have call successors, (57) Word has length 147
[2025-05-07 17:29:02,697 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:02,698 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:29:02,698 INFO  L226             Difference]: Without dead ends: 143
[2025-05-07 17:29:02,698 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 323 GetRequests, 278 SyntacticMatches, 12 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 447 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=207, Invalid=983, Unknown=0, NotChecked=0, Total=1190
[2025-05-07 17:29:02,699 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 30 mSDsluCounter, 1049 mSDsCounter, 0 mSdLazyCounter, 284 mSolverCounterSat, 20 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 48 SdHoareTripleChecker+Valid, 1134 SdHoareTripleChecker+Invalid, 304 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 20 IncrementalHoareTripleChecker+Valid, 284 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:02,699 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [48 Valid, 1134 Invalid, 304 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [20 Valid, 284 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:02,699 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-05-07 17:29:02,704 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 143.
[2025-05-07 17:29:02,704 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 143 states, 63 states have (on average 1.0476190476190477) internal successors, (66), 66 states have internal predecessors, (66), 38 states have call successors, (40), 27 states have call predecessors, (40), 41 states have return successors, (95), 49 states have call predecessors, (95), 38 states have call successors, (95)
[2025-05-07 17:29:02,705 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 143 states to 143 states and 201 transitions.
[2025-05-07 17:29:02,705 INFO  L79                 Accepts]: Start accepts. Automaton has 143 states and 201 transitions. Word has length 147
[2025-05-07 17:29:02,705 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:02,705 INFO  L485      AbstractCegarLoop]: Abstraction has 143 states and 201 transitions.
[2025-05-07 17:29:02,705 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 29 states, 16 states have (on average 4.9375) internal successors, (79), 29 states have internal predecessors, (79), 15 states have call successors, (44), 2 states have call predecessors, (44), 16 states have return successors, (57), 14 states have call predecessors, (57), 15 states have call successors, (57)
[2025-05-07 17:29:02,705 INFO  L278                IsEmpty]: Start isEmpty. Operand 143 states and 201 transitions.
[2025-05-07 17:29:02,706 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 156
[2025-05-07 17:29:02,706 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:02,706 INFO  L218           NwaCegarLoop]: trace histogram [13, 11, 11, 11, 11, 11, 11, 11, 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]
[2025-05-07 17:29:02,712 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-05-07 17:29:02,907 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-05-07 17:29:02,907 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:02,908 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:02,908 INFO  L85        PathProgramCache]: Analyzing trace with hash 1046428341, now seen corresponding path program 8 times
[2025-05-07 17:29:02,909 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:02,909 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1866199542]
[2025-05-07 17:29:02,909 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:29:02,909 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:02,972 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 155 statements into 2 equivalence classes.
[2025-05-07 17:29:02,990 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 155 of 155 statements.
[2025-05-07 17:29:02,991 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:29:02,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:03,405 INFO  L134       CoverageAnalysis]: Checked inductivity of 513 backedges. 5 proven. 249 refuted. 0 times theorem prover too weak. 259 trivial. 0 not checked.
[2025-05-07 17:29:03,405 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:03,405 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1866199542]
[2025-05-07 17:29:03,405 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1866199542] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:03,405 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [406261871]
[2025-05-07 17:29:03,406 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:29:03,406 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:03,407 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:03,408 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:03,409 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-05-07 17:29:03,826 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 155 statements into 2 equivalence classes.
[2025-05-07 17:29:03,899 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 155 of 155 statements.
[2025-05-07 17:29:03,899 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:29:03,899 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:03,902 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1069 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:03,905 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:03,971 INFO  L134       CoverageAnalysis]: Checked inductivity of 513 backedges. 280 proven. 72 refuted. 0 times theorem prover too weak. 161 trivial. 0 not checked.
[2025-05-07 17:29:03,971 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:14,626 INFO  L134       CoverageAnalysis]: Checked inductivity of 513 backedges. 0 proven. 264 refuted. 0 times theorem prover too weak. 249 trivial. 0 not checked.
[2025-05-07 17:29:14,627 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [406261871] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:14,627 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:14,627 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [21, 19, 24] total 32
[2025-05-07 17:29:14,627 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1767257444]
[2025-05-07 17:29:14,627 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:14,627 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 32 states
[2025-05-07 17:29:14,627 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:14,628 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 32 interpolants.
[2025-05-07 17:29:14,628 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=161, Invalid=831, Unknown=0, NotChecked=0, Total=992
[2025-05-07 17:29:14,628 INFO  L87              Difference]: Start difference. First operand 143 states and 201 transitions. Second operand  has 32 states, 18 states have (on average 4.555555555555555) internal successors, (82), 32 states have internal predecessors, (82), 16 states have call successors, (45), 2 states have call predecessors, (45), 18 states have return successors, (61), 16 states have call predecessors, (61), 16 states have call successors, (61)
[2025-05-07 17:29:14,840 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:14,840 INFO  L93              Difference]: Finished difference Result 149 states and 222 transitions.
[2025-05-07 17:29:14,840 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-05-07 17:29:14,840 INFO  L79                 Accepts]: Start accepts. Automaton has  has 32 states, 18 states have (on average 4.555555555555555) internal successors, (82), 32 states have internal predecessors, (82), 16 states have call successors, (45), 2 states have call predecessors, (45), 18 states have return successors, (61), 16 states have call predecessors, (61), 16 states have call successors, (61) Word has length 155
[2025-05-07 17:29:14,840 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:14,841 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:29:14,841 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:29:14,841 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 343 GetRequests, 292 SyntacticMatches, 14 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 581 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=262, Invalid=1220, Unknown=0, NotChecked=0, Total=1482
[2025-05-07 17:29:14,842 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 27 mSDsluCounter, 1364 mSDsCounter, 0 mSdLazyCounter, 328 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 47 SdHoareTripleChecker+Valid, 1449 SdHoareTripleChecker+Invalid, 344 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 328 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:14,842 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [47 Valid, 1449 Invalid, 344 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 328 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:14,842 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:29:14,847 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 147.
[2025-05-07 17:29:14,847 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 147 states, 65 states have (on average 1.0461538461538462) internal successors, (68), 68 states have internal predecessors, (68), 38 states have call successors, (40), 27 states have call predecessors, (40), 43 states have return successors, (106), 51 states have call predecessors, (106), 38 states have call successors, (106)
[2025-05-07 17:29:14,848 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 147 states to 147 states and 214 transitions.
[2025-05-07 17:29:14,848 INFO  L79                 Accepts]: Start accepts. Automaton has 147 states and 214 transitions. Word has length 155
[2025-05-07 17:29:14,848 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:14,848 INFO  L485      AbstractCegarLoop]: Abstraction has 147 states and 214 transitions.
[2025-05-07 17:29:14,848 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 32 states, 18 states have (on average 4.555555555555555) internal successors, (82), 32 states have internal predecessors, (82), 16 states have call successors, (45), 2 states have call predecessors, (45), 18 states have return successors, (61), 16 states have call predecessors, (61), 16 states have call successors, (61)
[2025-05-07 17:29:14,848 INFO  L278                IsEmpty]: Start isEmpty. Operand 147 states and 214 transitions.
[2025-05-07 17:29:14,849 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 164
[2025-05-07 17:29:14,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:14,849 INFO  L218           NwaCegarLoop]: trace histogram [14, 12, 12, 12, 12, 12, 12, 12, 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]
[2025-05-07 17:29:14,855 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-05-07 17:29:15,050 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable13
[2025-05-07 17:29:15,051 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:15,052 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:15,052 INFO  L85        PathProgramCache]: Analyzing trace with hash 1578740890, now seen corresponding path program 9 times
[2025-05-07 17:29:15,052 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:15,052 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [543433844]
[2025-05-07 17:29:15,053 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:29:15,053 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:15,113 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 163 statements into 9 equivalence classes.
[2025-05-07 17:29:15,138 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 139 of 163 statements.
[2025-05-07 17:29:15,138 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-05-07 17:29:15,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:15,410 INFO  L134       CoverageAnalysis]: Checked inductivity of 607 backedges. 207 proven. 55 refuted. 0 times theorem prover too weak. 345 trivial. 0 not checked.
[2025-05-07 17:29:15,410 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:15,410 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [543433844]
[2025-05-07 17:29:15,410 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [543433844] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:15,410 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2054183353]
[2025-05-07 17:29:15,410 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:29:15,410 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:15,412 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:15,413 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:15,414 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-05-07 17:29:15,985 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 163 statements into 9 equivalence classes.
[2025-05-07 17:29:16,072 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 139 of 163 statements.
[2025-05-07 17:29:16,072 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-05-07 17:29:16,072 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:16,075 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1009 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:16,078 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:16,139 INFO  L134       CoverageAnalysis]: Checked inductivity of 607 backedges. 204 proven. 50 refuted. 0 times theorem prover too weak. 353 trivial. 0 not checked.
[2025-05-07 17:29:16,139 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:23,114 INFO  L134       CoverageAnalysis]: Checked inductivity of 607 backedges. 204 proven. 60 refuted. 0 times theorem prover too weak. 343 trivial. 0 not checked.
[2025-05-07 17:29:23,114 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2054183353] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:23,114 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:23,114 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [19, 17, 21] total 29
[2025-05-07 17:29:23,114 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1905077366]
[2025-05-07 17:29:23,114 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:23,115 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 29 states
[2025-05-07 17:29:23,115 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:23,115 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 29 interpolants.
[2025-05-07 17:29:23,116 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=138, Invalid=674, Unknown=0, NotChecked=0, Total=812
[2025-05-07 17:29:23,116 INFO  L87              Difference]: Start difference. First operand 147 states and 214 transitions. Second operand  has 29 states, 16 states have (on average 4.5) internal successors, (72), 29 states have internal predecessors, (72), 15 states have call successors, (42), 2 states have call predecessors, (42), 16 states have return successors, (53), 17 states have call predecessors, (53), 15 states have call successors, (53)
[2025-05-07 17:29:23,255 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:23,255 INFO  L93              Difference]: Finished difference Result 149 states and 221 transitions.
[2025-05-07 17:29:23,255 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-05-07 17:29:23,255 INFO  L79                 Accepts]: Start accepts. Automaton has  has 29 states, 16 states have (on average 4.5) internal successors, (72), 29 states have internal predecessors, (72), 15 states have call successors, (42), 2 states have call predecessors, (42), 16 states have return successors, (53), 17 states have call predecessors, (53), 15 states have call successors, (53) Word has length 163
[2025-05-07 17:29:23,255 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:23,256 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:29:23,256 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:29:23,257 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 352 GetRequests, 307 SyntacticMatches, 12 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 537 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=218, Invalid=972, Unknown=0, NotChecked=0, Total=1190
[2025-05-07 17:29:23,257 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 16 mSDsluCounter, 901 mSDsCounter, 0 mSdLazyCounter, 198 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 31 SdHoareTripleChecker+Valid, 988 SdHoareTripleChecker+Invalid, 206 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 198 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:23,257 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [31 Valid, 988 Invalid, 206 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 198 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:23,258 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:29:23,264 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 147.
[2025-05-07 17:29:23,264 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 147 states, 65 states have (on average 1.0461538461538462) internal successors, (68), 68 states have internal predecessors, (68), 38 states have call successors, (40), 27 states have call predecessors, (40), 43 states have return successors, (100), 51 states have call predecessors, (100), 38 states have call successors, (100)
[2025-05-07 17:29:23,265 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 147 states to 147 states and 208 transitions.
[2025-05-07 17:29:23,265 INFO  L79                 Accepts]: Start accepts. Automaton has 147 states and 208 transitions. Word has length 163
[2025-05-07 17:29:23,265 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:23,265 INFO  L485      AbstractCegarLoop]: Abstraction has 147 states and 208 transitions.
[2025-05-07 17:29:23,265 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 29 states, 16 states have (on average 4.5) internal successors, (72), 29 states have internal predecessors, (72), 15 states have call successors, (42), 2 states have call predecessors, (42), 16 states have return successors, (53), 17 states have call predecessors, (53), 15 states have call successors, (53)
[2025-05-07 17:29:23,265 INFO  L278                IsEmpty]: Start isEmpty. Operand 147 states and 208 transitions.
[2025-05-07 17:29:23,267 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 180
[2025-05-07 17:29:23,267 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:23,267 INFO  L218           NwaCegarLoop]: trace histogram [16, 14, 14, 14, 14, 14, 14, 14, 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]
[2025-05-07 17:29:23,275 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-05-07 17:29:23,467 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:23,468 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:23,469 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:23,469 INFO  L85        PathProgramCache]: Analyzing trace with hash 1135536100, now seen corresponding path program 10 times
[2025-05-07 17:29:23,469 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:23,469 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1883079264]
[2025-05-07 17:29:23,469 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:29:23,470 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:23,524 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 179 statements into 2 equivalence classes.
[2025-05-07 17:29:23,541 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 179 of 179 statements.
[2025-05-07 17:29:23,541 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:29:23,541 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:24,103 INFO  L134       CoverageAnalysis]: Checked inductivity of 819 backedges. 6 proven. 376 refuted. 0 times theorem prover too weak. 437 trivial. 0 not checked.
[2025-05-07 17:29:24,103 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:24,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1883079264]
[2025-05-07 17:29:24,103 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1883079264] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:24,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [566739380]
[2025-05-07 17:29:24,103 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:29:24,104 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:24,105 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:24,107 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:24,108 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-05-07 17:29:24,821 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 179 statements into 2 equivalence classes.
[2025-05-07 17:29:24,940 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 179 of 179 statements.
[2025-05-07 17:29:24,940 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:29:24,940 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:24,944 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1159 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:24,948 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:25,028 INFO  L134       CoverageAnalysis]: Checked inductivity of 819 backedges. 441 proven. 98 refuted. 0 times theorem prover too weak. 280 trivial. 0 not checked.
[2025-05-07 17:29:25,028 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:42,012 INFO  L134       CoverageAnalysis]: Checked inductivity of 819 backedges. 0 proven. 397 refuted. 0 times theorem prover too weak. 422 trivial. 0 not checked.
[2025-05-07 17:29:42,013 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [566739380] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:42,013 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:42,013 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [22, 21, 27] total 34
[2025-05-07 17:29:42,013 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1313078914]
[2025-05-07 17:29:42,013 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:42,013 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 34 states
[2025-05-07 17:29:42,013 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:42,014 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 34 interpolants.
[2025-05-07 17:29:42,014 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=191, Invalid=931, Unknown=0, NotChecked=0, Total=1122
[2025-05-07 17:29:42,014 INFO  L87              Difference]: Start difference. First operand 147 states and 208 transitions. Second operand  has 34 states, 20 states have (on average 4.2) internal successors, (84), 34 states have internal predecessors, (84), 16 states have call successors, (45), 2 states have call predecessors, (45), 20 states have return successors, (64), 18 states have call predecessors, (64), 16 states have call successors, (64)
[2025-05-07 17:29:42,236 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:42,236 INFO  L93              Difference]: Finished difference Result 153 states and 229 transitions.
[2025-05-07 17:29:42,237 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-05-07 17:29:42,237 INFO  L79                 Accepts]: Start accepts. Automaton has  has 34 states, 20 states have (on average 4.2) internal successors, (84), 34 states have internal predecessors, (84), 16 states have call successors, (45), 2 states have call predecessors, (45), 20 states have return successors, (64), 18 states have call predecessors, (64), 16 states have call successors, (64) Word has length 179
[2025-05-07 17:29:42,237 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:42,238 INFO  L225             Difference]: With dead ends: 153
[2025-05-07 17:29:42,238 INFO  L226             Difference]: Without dead ends: 153
[2025-05-07 17:29:42,239 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 395 GetRequests, 339 SyntacticMatches, 16 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 721 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=322, Invalid=1400, Unknown=0, NotChecked=0, Total=1722
[2025-05-07 17:29:42,239 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 30 mSDsluCounter, 1408 mSDsCounter, 0 mSdLazyCounter, 265 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 51 SdHoareTripleChecker+Valid, 1495 SdHoareTripleChecker+Invalid, 284 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 265 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:42,239 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [51 Valid, 1495 Invalid, 284 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 265 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:42,240 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-05-07 17:29:42,247 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 151.
[2025-05-07 17:29:42,247 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 151 states, 67 states have (on average 1.044776119402985) internal successors, (70), 70 states have internal predecessors, (70), 38 states have call successors, (40), 27 states have call predecessors, (40), 45 states have return successors, (111), 53 states have call predecessors, (111), 38 states have call successors, (111)
[2025-05-07 17:29:42,248 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 151 states to 151 states and 221 transitions.
[2025-05-07 17:29:42,248 INFO  L79                 Accepts]: Start accepts. Automaton has 151 states and 221 transitions. Word has length 179
[2025-05-07 17:29:42,248 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:42,249 INFO  L485      AbstractCegarLoop]: Abstraction has 151 states and 221 transitions.
[2025-05-07 17:29:42,249 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 34 states, 20 states have (on average 4.2) internal successors, (84), 34 states have internal predecessors, (84), 16 states have call successors, (45), 2 states have call predecessors, (45), 20 states have return successors, (64), 18 states have call predecessors, (64), 16 states have call successors, (64)
[2025-05-07 17:29:42,249 INFO  L278                IsEmpty]: Start isEmpty. Operand 151 states and 221 transitions.
[2025-05-07 17:29:42,249 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 196
[2025-05-07 17:29:42,250 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:42,250 INFO  L218           NwaCegarLoop]: trace histogram [18, 16, 16, 16, 16, 16, 16, 16, 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]
[2025-05-07 17:29:42,256 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Ended with exit code 0
[2025-05-07 17:29:42,450 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-05-07 17:29:42,451 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:42,452 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:42,452 INFO  L85        PathProgramCache]: Analyzing trace with hash 195149998, now seen corresponding path program 11 times
[2025-05-07 17:29:42,452 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:42,452 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1294802598]
[2025-05-07 17:29:42,453 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-05-07 17:29:42,453 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:42,508 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 195 statements into 10 equivalence classes.
[2025-05-07 17:29:42,542 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s) and asserted 195 of 195 statements.
[2025-05-07 17:29:42,542 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s)
[2025-05-07 17:29:42,542 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:43,091 INFO  L134       CoverageAnalysis]: Checked inductivity of 1063 backedges. 12 proven. 485 refuted. 0 times theorem prover too weak. 566 trivial. 0 not checked.
[2025-05-07 17:29:43,091 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:43,091 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1294802598]
[2025-05-07 17:29:43,091 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1294802598] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:43,091 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1000883278]
[2025-05-07 17:29:43,091 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-05-07 17:29:43,091 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:43,092 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:43,094 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:43,095 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-05-07 17:29:43,869 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 195 statements into 10 equivalence classes.
[2025-05-07 17:29:43,967 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s) and asserted 195 of 195 statements.
[2025-05-07 17:29:43,967 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s)
[2025-05-07 17:29:43,967 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:43,971 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1219 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:43,974 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:44,059 INFO  L134       CoverageAnalysis]: Checked inductivity of 1063 backedges. 567 proven. 128 refuted. 0 times theorem prover too weak. 368 trivial. 0 not checked.
[2025-05-07 17:29:44,060 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:30:09,594 INFO  L134       CoverageAnalysis]: Checked inductivity of 1063 backedges. 0 proven. 513 refuted. 0 times theorem prover too weak. 550 trivial. 0 not checked.
[2025-05-07 17:30:09,594 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1000883278] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:30:09,594 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:30:09,594 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [24, 23, 30] total 37
[2025-05-07 17:30:09,594 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2039113697]
[2025-05-07 17:30:09,594 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:30:09,595 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 37 states
[2025-05-07 17:30:09,595 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:30:09,595 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 37 interpolants.
[2025-05-07 17:30:09,595 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=226, Invalid=1106, Unknown=0, NotChecked=0, Total=1332
[2025-05-07 17:30:09,595 INFO  L87              Difference]: Start difference. First operand 151 states and 221 transitions. Second operand  has 37 states, 22 states have (on average 3.9545454545454546) internal successors, (87), 37 states have internal predecessors, (87), 17 states have call successors, (46), 2 states have call predecessors, (46), 22 states have return successors, (67), 20 states have call predecessors, (67), 17 states have call successors, (67)
[2025-05-07 17:30:09,868 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:30:09,869 INFO  L93              Difference]: Finished difference Result 157 states and 242 transitions.
[2025-05-07 17:30:09,869 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-05-07 17:30:09,869 INFO  L79                 Accepts]: Start accepts. Automaton has  has 37 states, 22 states have (on average 3.9545454545454546) internal successors, (87), 37 states have internal predecessors, (87), 17 states have call successors, (46), 2 states have call predecessors, (46), 22 states have return successors, (67), 20 states have call predecessors, (67), 17 states have call successors, (67) Word has length 195
[2025-05-07 17:30:09,869 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:30:09,870 INFO  L225             Difference]: With dead ends: 157
[2025-05-07 17:30:09,870 INFO  L226             Difference]: Without dead ends: 157
[2025-05-07 17:30:09,871 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 429 GetRequests, 367 SyntacticMatches, 18 SemanticMatches, 44 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 897 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=391, Invalid=1679, Unknown=0, NotChecked=0, Total=2070
[2025-05-07 17:30:09,871 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 33 mSDsluCounter, 1496 mSDsCounter, 0 mSdLazyCounter, 283 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 56 SdHoareTripleChecker+Valid, 1583 SdHoareTripleChecker+Invalid, 304 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 283 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:30:09,871 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [56 Valid, 1583 Invalid, 304 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 283 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:30:09,872 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 157 states.
[2025-05-07 17:30:09,876 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 157 to 155.
[2025-05-07 17:30:09,876 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 155 states, 69 states have (on average 1.0434782608695652) internal successors, (72), 72 states have internal predecessors, (72), 38 states have call successors, (40), 27 states have call predecessors, (40), 47 states have return successors, (122), 55 states have call predecessors, (122), 38 states have call successors, (122)
[2025-05-07 17:30:09,877 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 155 states to 155 states and 234 transitions.
[2025-05-07 17:30:09,877 INFO  L79                 Accepts]: Start accepts. Automaton has 155 states and 234 transitions. Word has length 195
[2025-05-07 17:30:09,877 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:30:09,877 INFO  L485      AbstractCegarLoop]: Abstraction has 155 states and 234 transitions.
[2025-05-07 17:30:09,878 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 37 states, 22 states have (on average 3.9545454545454546) internal successors, (87), 37 states have internal predecessors, (87), 17 states have call successors, (46), 2 states have call predecessors, (46), 22 states have return successors, (67), 20 states have call predecessors, (67), 17 states have call successors, (67)
[2025-05-07 17:30:09,878 INFO  L278                IsEmpty]: Start isEmpty. Operand 155 states and 234 transitions.
[2025-05-07 17:30:09,879 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 212
[2025-05-07 17:30:09,879 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:30:09,879 INFO  L218           NwaCegarLoop]: trace histogram [20, 18, 18, 18, 18, 18, 18, 18, 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]
[2025-05-07 17:30:09,887 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Ended with exit code 0
[2025-05-07 17:30:10,080 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 13 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable16
[2025-05-07 17:30:10,080 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:30:10,081 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:30:10,081 INFO  L85        PathProgramCache]: Analyzing trace with hash 1809915000, now seen corresponding path program 12 times
[2025-05-07 17:30:10,082 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:30:10,082 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1082176278]
[2025-05-07 17:30:10,082 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-05-07 17:30:10,082 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:30:10,141 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 211 statements into 11 equivalence classes.
[2025-05-07 17:30:10,205 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s) and asserted 211 of 211 statements.
[2025-05-07 17:30:10,205 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s)
[2025-05-07 17:30:10,205 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:11,018 INFO  L134       CoverageAnalysis]: Checked inductivity of 1339 backedges. 109 proven. 614 refuted. 0 times theorem prover too weak. 616 trivial. 0 not checked.
[2025-05-07 17:30:11,018 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:30:11,018 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1082176278]
[2025-05-07 17:30:11,018 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1082176278] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:30:11,018 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [335706422]
[2025-05-07 17:30:11,018 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-05-07 17:30:11,018 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:30:11,020 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:30:11,021 INFO  L229       MonitoredProcess]: Starting monitored process 14 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:30:11,022 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Waiting until timeout for monitored process
[2025-05-07 17:30:12,115 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 211 statements into 11 equivalence classes.
[2025-05-07 17:30:12,240 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s) and asserted 211 of 211 statements.
[2025-05-07 17:30:12,240 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s)
[2025-05-07 17:30:12,240 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:12,244 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1279 conjuncts, 34 conjuncts are in the unsatisfiable core
[2025-05-07 17:30:12,247 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:30:12,381 INFO  L134       CoverageAnalysis]: Checked inductivity of 1339 backedges. 709 proven. 162 refuted. 0 times theorem prover too weak. 468 trivial. 0 not checked.
[2025-05-07 17:30:12,381 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:30:48,471 INFO  L134       CoverageAnalysis]: Checked inductivity of 1339 backedges. 0 proven. 644 refuted. 0 times theorem prover too weak. 695 trivial. 0 not checked.
[2025-05-07 17:30:48,472 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [335706422] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:30:48,472 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:30:48,472 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [28, 25, 33] total 45
[2025-05-07 17:30:48,472 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1506131299]
[2025-05-07 17:30:48,472 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:30:48,472 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 45 states
[2025-05-07 17:30:48,472 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:30:48,473 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 45 interpolants.
[2025-05-07 17:30:48,473 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=325, Invalid=1655, Unknown=0, NotChecked=0, Total=1980
[2025-05-07 17:30:48,473 INFO  L87              Difference]: Start difference. First operand 155 states and 234 transitions. Second operand  has 45 states, 28 states have (on average 3.392857142857143) internal successors, (95), 45 states have internal predecessors, (95), 19 states have call successors, (48), 2 states have call predecessors, (48), 28 states have return successors, (73), 26 states have call predecessors, (73), 19 states have call successors, (73)
[2025-05-07 17:30:48,873 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:30:48,873 INFO  L93              Difference]: Finished difference Result 161 states and 255 transitions.
[2025-05-07 17:30:48,873 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 25 states. 
[2025-05-07 17:30:48,874 INFO  L79                 Accepts]: Start accepts. Automaton has  has 45 states, 28 states have (on average 3.392857142857143) internal successors, (95), 45 states have internal predecessors, (95), 19 states have call successors, (48), 2 states have call predecessors, (48), 28 states have return successors, (73), 26 states have call predecessors, (73), 19 states have call successors, (73) Word has length 211
[2025-05-07 17:30:48,874 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:30:48,875 INFO  L225             Difference]: With dead ends: 161
[2025-05-07 17:30:48,875 INFO  L226             Difference]: Without dead ends: 161
[2025-05-07 17:30:48,876 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 474 GetRequests, 400 SyntacticMatches, 21 SemanticMatches, 53 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1469 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=547, Invalid=2423, Unknown=0, NotChecked=0, Total=2970
[2025-05-07 17:30:48,876 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 62 mSDsluCounter, 1696 mSDsCounter, 0 mSdLazyCounter, 425 mSolverCounterSat, 52 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 87 SdHoareTripleChecker+Valid, 1786 SdHoareTripleChecker+Invalid, 477 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 52 IncrementalHoareTripleChecker+Valid, 425 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:30:48,876 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [87 Valid, 1786 Invalid, 477 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [52 Valid, 425 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:30:48,876 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 161 states.
[2025-05-07 17:30:48,881 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 161 to 159.
[2025-05-07 17:30:48,882 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 71 states have (on average 1.0422535211267605) internal successors, (74), 74 states have internal predecessors, (74), 38 states have call successors, (40), 27 states have call predecessors, (40), 49 states have return successors, (133), 57 states have call predecessors, (133), 38 states have call successors, (133)
[2025-05-07 17:30:48,882 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 247 transitions.
[2025-05-07 17:30:48,882 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 247 transitions. Word has length 211
[2025-05-07 17:30:48,883 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:30:48,883 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 247 transitions.
[2025-05-07 17:30:48,883 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 45 states, 28 states have (on average 3.392857142857143) internal successors, (95), 45 states have internal predecessors, (95), 19 states have call successors, (48), 2 states have call predecessors, (48), 28 states have return successors, (73), 26 states have call predecessors, (73), 19 states have call successors, (73)
[2025-05-07 17:30:48,883 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 247 transitions.
[2025-05-07 17:30:48,884 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 228
[2025-05-07 17:30:48,884 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:30:48,884 INFO  L218           NwaCegarLoop]: trace histogram [22, 20, 20, 20, 20, 20, 20, 20, 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]
[2025-05-07 17:30:48,893 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Ended with exit code 0
[2025-05-07 17:30:49,084 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 14 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-05-07 17:30:49,085 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:30:49,085 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:30:49,085 INFO  L85        PathProgramCache]: Analyzing trace with hash -6292670, now seen corresponding path program 13 times
[2025-05-07 17:30:49,086 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:30:49,086 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1569119413]
[2025-05-07 17:30:49,086 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-05-07 17:30:49,086 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:30:49,149 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 227 statements into 1 equivalence classes.
[2025-05-07 17:30:49,179 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 227 of 227 statements.
[2025-05-07 17:30:49,179 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:30:49,179 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:51,368 INFO  L134       CoverageAnalysis]: Checked inductivity of 1647 backedges. 17 proven. 764 refuted. 0 times theorem prover too weak. 866 trivial. 0 not checked.
[2025-05-07 17:30:51,368 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:30:51,368 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1569119413]
[2025-05-07 17:30:51,368 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1569119413] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:30:51,368 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1245325482]
[2025-05-07 17:30:51,368 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-05-07 17:30:51,369 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:30:51,371 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:30:51,373 INFO  L229       MonitoredProcess]: Starting monitored process 15 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:30:51,373 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Waiting until timeout for monitored process
[2025-05-07 17:30:52,946 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 227 statements into 1 equivalence classes.
[2025-05-07 17:30:53,063 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 227 of 227 statements.
[2025-05-07 17:30:53,064 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:30:53,064 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:53,069 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1339 conjuncts, 169 conjuncts are in the unsatisfiable core
[2025-05-07 17:30:53,074 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:30:54,295 INFO  L134       CoverageAnalysis]: Checked inductivity of 1647 backedges. 876 proven. 209 refuted. 0 times theorem prover too weak. 562 trivial. 0 not checked.
[2025-05-07 17:30:54,295 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:30:59,548 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1245325482] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:30:59,548 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 2 imperfect interpolant sequences.
[2025-05-07 17:30:59,548 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [30, 29] total 52
[2025-05-07 17:30:59,548 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [98256512]
[2025-05-07 17:30:59,548 INFO  L85    oduleStraightlineAll]: Using 2 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:30:59,548 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 52 states
[2025-05-07 17:30:59,548 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:30:59,549 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 52 interpolants.
[2025-05-07 17:30:59,549 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=112, Invalid=2644, Unknown=0, NotChecked=0, Total=2756
[2025-05-07 17:30:59,549 INFO  L87              Difference]: Start difference. First operand 159 states and 247 transitions. Second operand  has 52 states, 44 states have (on average 2.2954545454545454) internal successors, (101), 52 states have internal predecessors, (101), 10 states have call successors, (39), 2 states have call predecessors, (39), 44 states have return successors, (74), 43 states have call predecessors, (74), 10 states have call successors, (74)
[2025-05-07 17:31:03,344 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:31:03,344 INFO  L93              Difference]: Finished difference Result 211 states and 323 transitions.
[2025-05-07 17:31:03,345 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 50 states. 
[2025-05-07 17:31:03,345 INFO  L79                 Accepts]: Start accepts. Automaton has  has 52 states, 44 states have (on average 2.2954545454545454) internal successors, (101), 52 states have internal predecessors, (101), 10 states have call successors, (39), 2 states have call predecessors, (39), 44 states have return successors, (74), 43 states have call predecessors, (74), 10 states have call successors, (74) Word has length 227
[2025-05-07 17:31:03,345 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:31:03,347 INFO  L225             Difference]: With dead ends: 211
[2025-05-07 17:31:03,347 INFO  L226             Difference]: Without dead ends: 211
[2025-05-07 17:31:03,348 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 443 GetRequests, 348 SyntacticMatches, 1 SemanticMatches, 94 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1152 ImplicationChecksByTransitivity, 3.0s TimeCoverageRelationStatistics Valid=429, Invalid=8691, Unknown=0, NotChecked=0, Total=9120
[2025-05-07 17:31:03,348 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 38 mSDsluCounter, 5691 mSDsCounter, 0 mSdLazyCounter, 3543 mSolverCounterSat, 20 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 83 SdHoareTripleChecker+Valid, 5815 SdHoareTripleChecker+Invalid, 3563 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 20 IncrementalHoareTripleChecker+Valid, 3543 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:31:03,348 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [83 Valid, 5815 Invalid, 3563 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [20 Valid, 3543 Invalid, 0 Unknown, 0 Unchecked, 2.1s Time]
[2025-05-07 17:31:03,349 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 211 states.
[2025-05-07 17:31:03,355 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 211 to 179.
[2025-05-07 17:31:03,355 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 179 states, 81 states have (on average 1.0493827160493827) internal successors, (85), 84 states have internal predecessors, (85), 40 states have call successors, (42), 29 states have call predecessors, (42), 57 states have return successors, (147), 65 states have call predecessors, (147), 40 states have call successors, (147)
[2025-05-07 17:31:03,356 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 179 states to 179 states and 274 transitions.
[2025-05-07 17:31:03,356 INFO  L79                 Accepts]: Start accepts. Automaton has 179 states and 274 transitions. Word has length 227
[2025-05-07 17:31:03,356 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:31:03,356 INFO  L485      AbstractCegarLoop]: Abstraction has 179 states and 274 transitions.
[2025-05-07 17:31:03,356 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 52 states, 44 states have (on average 2.2954545454545454) internal successors, (101), 52 states have internal predecessors, (101), 10 states have call successors, (39), 2 states have call predecessors, (39), 44 states have return successors, (74), 43 states have call predecessors, (74), 10 states have call successors, (74)
[2025-05-07 17:31:03,356 INFO  L278                IsEmpty]: Start isEmpty. Operand 179 states and 274 transitions.
[2025-05-07 17:31:03,357 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 244
[2025-05-07 17:31:03,357 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:31:03,357 INFO  L218           NwaCegarLoop]: trace histogram [24, 22, 22, 22, 22, 22, 22, 22, 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]
[2025-05-07 17:31:03,367 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Ended with exit code 0
[2025-05-07 17:31:03,557 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,15 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:31:03,558 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:31:03,558 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:31:03,558 INFO  L85        PathProgramCache]: Analyzing trace with hash -1135518452, now seen corresponding path program 14 times
[2025-05-07 17:31:03,558 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:31:03,558 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [235156796]
[2025-05-07 17:31:03,558 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:31:03,558 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:31:03,599 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 243 statements into 2 equivalence classes.
[2025-05-07 17:31:03,621 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 243 of 243 statements.
[2025-05-07 17:31:03,621 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:31:03,621 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:31:04,437 INFO  L134       CoverageAnalysis]: Checked inductivity of 1987 backedges. 221 proven. 690 refuted. 0 times theorem prover too weak. 1076 trivial. 0 not checked.
[2025-05-07 17:31:04,437 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:31:04,437 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [235156796]
[2025-05-07 17:31:04,437 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [235156796] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:31:04,437 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [473008416]
[2025-05-07 17:31:04,437 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:31:04,437 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:31:04,440 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:31:04,441 INFO  L229       MonitoredProcess]: Starting monitored process 16 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:31:04,442 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (16)] Waiting until timeout for monitored process
[2025-05-07 17:31:06,270 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 243 statements into 2 equivalence classes.
[2025-05-07 17:31:06,380 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 243 of 243 statements.
[2025-05-07 17:31:06,380 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:31:06,380 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:31:06,384 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1399 conjuncts, 40 conjuncts are in the unsatisfiable core
[2025-05-07 17:31:06,387 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:31:06,492 INFO  L134       CoverageAnalysis]: Checked inductivity of 1987 backedges. 1262 proven. 50 refuted. 0 times theorem prover too weak. 675 trivial. 0 not checked.
[2025-05-07 17:31:06,492 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:32:07,079 INFO  L134       CoverageAnalysis]: Checked inductivity of 1987 backedges. 221 proven. 735 refuted. 0 times theorem prover too weak. 1031 trivial. 0 not checked.
[2025-05-07 17:32:07,079 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [473008416] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:32:07,079 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:32:07,080 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [28, 28, 37] total 41
[2025-05-07 17:32:07,080 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [292506742]
[2025-05-07 17:32:07,080 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:32:07,080 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 41 states
[2025-05-07 17:32:07,080 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:32:07,080 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 41 interpolants.
[2025-05-07 17:32:07,081 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=248, Invalid=1392, Unknown=0, NotChecked=0, Total=1640
[2025-05-07 17:32:07,081 INFO  L87              Difference]: Start difference. First operand 179 states and 274 transitions. Second operand  has 41 states, 25 states have (on average 3.6) internal successors, (90), 41 states have internal predecessors, (90), 19 states have call successors, (48), 2 states have call predecessors, (48), 25 states have return successors, (77), 25 states have call predecessors, (77), 19 states have call successors, (77)
[2025-05-07 17:32:07,600 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:32:07,600 INFO  L93              Difference]: Finished difference Result 168 states and 261 transitions.
[2025-05-07 17:32:07,600 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 27 states. 
[2025-05-07 17:32:07,601 INFO  L79                 Accepts]: Start accepts. Automaton has  has 41 states, 25 states have (on average 3.6) internal successors, (90), 41 states have internal predecessors, (90), 19 states have call successors, (48), 2 states have call predecessors, (48), 25 states have return successors, (77), 25 states have call predecessors, (77), 19 states have call successors, (77) Word has length 243
[2025-05-07 17:32:07,601 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:32:07,601 INFO  L225             Difference]: With dead ends: 168
[2025-05-07 17:32:07,601 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:32:07,601 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 544 GetRequests, 458 SyntacticMatches, 25 SemanticMatches, 61 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1333 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=688, Invalid=3218, Unknown=0, NotChecked=0, Total=3906
[2025-05-07 17:32:07,602 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 6 mSDsluCounter, 1207 mSDsCounter, 0 mSdLazyCounter, 665 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1285 SdHoareTripleChecker+Invalid, 670 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 665 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:32:07,602 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1285 Invalid, 670 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 665 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:32:07,602 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:32:07,602 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:32:07,602 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:32:07,602 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:32:07,602 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 243
[2025-05-07 17:32:07,602 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:32:07,602 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:32:07,602 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 41 states, 25 states have (on average 3.6) internal successors, (90), 41 states have internal predecessors, (90), 19 states have call successors, (48), 2 states have call predecessors, (48), 25 states have return successors, (77), 25 states have call predecessors, (77), 19 states have call successors, (77)
[2025-05-07 17:32:07,603 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:32:07,603 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:32:07,604 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:32:07,614 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (16)] Forceful destruction successful, exit code 0
[2025-05-07 17:32:07,805 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,16 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:32:07,813 INFO  L422         BasicCegarLoop]: Path program histogram: [14, 1, 1, 1, 1, 1]
[2025-05-07 17:32:07,819 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:32:07,822 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:32:07 BoogieIcfgContainer
[2025-05-07 17:32:07,822 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:32:07,823 INFO  L158              Benchmark]: Toolchain (without parser) took 220728.41ms. Allocated memory was 234.9MB in the beginning and 620.8MB in the end (delta: 385.9MB). Free memory was 140.9MB in the beginning and 268.8MB in the end (delta: -127.9MB). Peak memory consumption was 260.3MB. Max. memory is 33.6GB.
[2025-05-07 17:32:07,823 INFO  L158              Benchmark]: SmtParser took 0.24ms. Allocated memory is still 234.9MB. Free memory is still 171.3MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:32:07,823 INFO  L158              Benchmark]: ChcToBoogie took 46.29ms. Allocated memory is still 234.9MB. Free memory was 140.9MB in the beginning and 137.2MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:32:07,823 INFO  L158              Benchmark]: Boogie Preprocessor took 71.93ms. Allocated memory is still 234.9MB. Free memory was 137.2MB in the beginning and 133.7MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:32:07,823 INFO  L158              Benchmark]: RCFGBuilder took 434.59ms. Allocated memory is still 234.9MB. Free memory was 133.7MB in the beginning and 164.9MB in the end (delta: -31.2MB). Peak memory consumption was 26.0MB. Max. memory is 33.6GB.
[2025-05-07 17:32:07,823 INFO  L158              Benchmark]: TraceAbstraction took 220171.67ms. Allocated memory was 234.9MB in the beginning and 620.8MB in the end (delta: 385.9MB). Free memory was 164.4MB in the beginning and 268.8MB in the end (delta: -104.4MB). Peak memory consumption was 284.6MB. Max. memory is 33.6GB.
[2025-05-07 17:32:07,824 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.24ms. Allocated memory is still 234.9MB. Free memory is still 171.3MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 46.29ms. Allocated memory is still 234.9MB. Free memory was 140.9MB in the beginning and 137.2MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 71.93ms. Allocated memory is still 234.9MB. Free memory was 137.2MB in the beginning and 133.7MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 434.59ms. Allocated memory is still 234.9MB. Free memory was 133.7MB in the beginning and 164.9MB in the end (delta: -31.2MB). Peak memory consumption was 26.0MB. Max. memory is 33.6GB.
 * TraceAbstraction took 220171.67ms. Allocated memory was 234.9MB in the beginning and 620.8MB in the end (delta: 385.9MB). Free memory was 164.4MB in the beginning and 268.8MB in the end (delta: -104.4MB). Peak memory consumption was 284.6MB. 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, 108 locations, 187 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 220.1s, OverallIterations: 19, TraceHistogramMax: 24, PathProgramHistogramMax: 14, EmptinessCheckTime: 0.0s, AutomataDifference: 7.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 595 SdHoareTripleChecker+Valid, 4.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 343 mSDsluCounter, 24161 SdHoareTripleChecker+Invalid, 3.8s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 22431 mSDsCounter, 237 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 7881 IncrementalHoareTripleChecker+Invalid, 8118 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 237 mSolverCounterUnsat, 1730 mSDtfsCounter, 7881 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 4932 GetRequests, 4172 SyntacticMatches, 165 SemanticMatches, 595 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9191 ImplicationChecksByTransitivity, 8.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=179occurred in iteration=18, InterpolantAutomatonStates: 332, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 19 MinimizatonAttempts, 58 StatesRemovedByMinimization, 12 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.8s SsaConstructionTime, 2.0s SatisfiabilityAnalysisTime, 197.0s InterpolantComputationTime, 4838 NumberOfCodeBlocks, 4774 NumberOfCodeBlocksAsserted, 120 NumberOfCheckSat, 6774 ConstructedInterpolants, 4 QuantifiedInterpolants, 11547 SizeOfPredicates, 231 NumberOfNonLiveVariables, 15735 ConjunctsInSsa, 471 ConjunctsInUnsatCore, 47 InterpolantComputations, 5 PerfectInterpolantSequences, 19097/26990 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:32:07,868 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
