./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/invariants/loop_nested.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:58,162 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:58,213 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_235f73c1-5fcb-419a-bdfa-77093c7a8519/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:58,216 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:58,217 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:58,229 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:58,229 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:58,229 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:58,230 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:58,230 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:58,230 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:58,230 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:58,230 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:58,230 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:58,230 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:58,230 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:58,230 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:58,230 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:58,231 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:58,231 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:58,231 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:58,408 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:58,416 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:58,418 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:58,419 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:58,419 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:58,421 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_235f73c1-5fcb-419a-bdfa-77093c7a8519/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/invariants/loop_nested.sol_0_no_adts_000.smt2
[2025-05-07 17:28:58,422 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:58,425 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:58,657 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_235f73c1-5fcb-419a-bdfa-77093c7a8519/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/invariants/loop_nested.sol_0_no_adts_000.smt2
[2025-05-07 17:28:58,659 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:58,660 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:58,661 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:58,661 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:58,661 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:58,663 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,698 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58 Unit
[2025-05-07 17:28:58,698 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:58,699 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:58,699 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:58,699 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:58,710 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,710 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,736 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,736 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,741 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,742 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,743 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,745 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,746 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,759 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:58,759 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:58,759 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:58,759 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:58,760 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (1/1) ...
[2025-05-07 17:28:58,762 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:58,773 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:58,782 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:58,784 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:58,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:58,791 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:58,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:58,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_5_0 given in one single declaration
[2025-05-07 17:28:58,792 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_5_0
[2025-05-07 17:28:58,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_5_0
[2025-05-07 17:28:58,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,792 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,792 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__42_43_0
[2025-05-07 17:28:58,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__42_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_f_41_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_f_41_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_f_41_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_while_header_f_34_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_while_header_f_34_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_while_header_f_34_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_f_41_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_f_41_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_f_41_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_while_header_f_26_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_while_header_f_26_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_while_header_f_26_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_while_body_f_25_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_while_body_f_25_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_while_body_f_25_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_while_body_f_33_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_while_body_f_33_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_while_body_f_33_43_0
[2025-05-07 17:28:58,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_f_41_43_0 given in one single declaration
[2025-05-07 17:28:58,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_f_41_43_0
[2025-05-07 17:28:58,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_f_41_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_5_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure block_5_function_f__42_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_5_function_f__42_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_return_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_return_function_f__42_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_return_function_f__42_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__42_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__42_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__42_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_Simple_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_Simple_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_17_Simple_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_17_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_17_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_19_Simple_43_0 given in one single declaration
[2025-05-07 17:28:58,794 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_19_Simple_43_0
[2025-05-07 17:28:58,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_19_Simple_43_0
[2025-05-07 17:28:58,795 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_18_Simple_43_0 given in one single declaration
[2025-05-07 17:28:58,795 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_18_Simple_43_0
[2025-05-07 17:28:58,795 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_18_Simple_43_0
[2025-05-07 17:28:58,795 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_20_Simple_43_0 given in one single declaration
[2025-05-07 17:28:58,795 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_20_Simple_43_0
[2025-05-07 17:28:58,795 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_20_Simple_43_0
[2025-05-07 17:28:58,795 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:58,795 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:58,795 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:58,911 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:58,913 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:59,124 INFO  L?                        ?]: Removed 139 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:59,124 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:59,132 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:59,132 INFO  L312             CfgBuilder]: Removed 8 assume(true) statements.
[2025-05-07 17:28:59,132 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:59 BoogieIcfgContainer
[2025-05-07 17:28:59,132 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:59,134 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:59,134 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:59,136 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:59,136 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:58" (1/3) ...
[2025-05-07 17:28:59,137 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6aabf76c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:59, skipping insertion in model container
[2025-05-07 17:28:59,137 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:58" (2/3) ...
[2025-05-07 17:28:59,137 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6aabf76c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:59, skipping insertion in model container
[2025-05-07 17:28:59,137 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:59" (3/3) ...
[2025-05-07 17:28:59,138 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:59,148 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:59,150 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 23 procedures, 92 locations, 135 edges, 23 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:59,179 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:59,187 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;@528c389d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:59,188 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:59,190 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 92 states, 40 states have (on average 1.125) internal successors, (45), 45 states have internal predecessors, (45), 28 states have call successors, (30), 22 states have call predecessors, (30), 22 states have return successors, (30), 24 states have call predecessors, (30), 28 states have call successors, (30)
[2025-05-07 17:28:59,197 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:28:59,197 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:59,197 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:59,198 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:59,201 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:59,201 INFO  L85        PathProgramCache]: Analyzing trace with hash 768903076, now seen corresponding path program 1 times
[2025-05-07 17:28:59,206 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:59,207 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [968283802]
[2025-05-07 17:28:59,207 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:59,207 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:59,244 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:28:59,303 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:28:59,304 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:59,304 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:59,697 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:59,697 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:59,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [968283802]
[2025-05-07 17:28:59,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [968283802] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:59,698 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:59,701 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:59,702 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1062646460]
[2025-05-07 17:28:59,703 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:59,707 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:59,707 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:59,734 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:59,734 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:59,736 INFO  L87              Difference]: Start difference. First operand  has 92 states, 40 states have (on average 1.125) internal successors, (45), 45 states have internal predecessors, (45), 28 states have call successors, (30), 22 states have call predecessors, (30), 22 states have return successors, (30), 24 states have call predecessors, (30), 28 states have call successors, (30) Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:28:59,797 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:59,797 INFO  L93              Difference]: Finished difference Result 92 states and 105 transitions.
[2025-05-07 17:28:59,799 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:59,800 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16) Word has length 59
[2025-05-07 17:28:59,800 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:59,808 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:28:59,808 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:28:59,809 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:59,811 INFO  L437           NwaCegarLoop]: 100 mSDtfsCounter, 1 mSDsluCounter, 190 mSDsCounter, 0 mSdLazyCounter, 14 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 290 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 14 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:59,812 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 290 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 14 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:59,822 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:28:59,836 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-05-07 17:28:59,837 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 40 states have (on average 1.1) internal successors, (44), 44 states have internal predecessors, (44), 28 states have call successors, (30), 22 states have call predecessors, (30), 23 states have return successors, (31), 25 states have call predecessors, (31), 28 states have call successors, (31)
[2025-05-07 17:28:59,840 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 105 transitions.
[2025-05-07 17:28:59,841 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 105 transitions. Word has length 59
[2025-05-07 17:28:59,842 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:59,842 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 105 transitions.
[2025-05-07 17:28:59,842 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:28:59,842 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 105 transitions.
[2025-05-07 17:28:59,844 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-05-07 17:28:59,844 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:59,844 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:59,844 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:59,844 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:59,845 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:59,845 INFO  L85        PathProgramCache]: Analyzing trace with hash -1771975969, now seen corresponding path program 1 times
[2025-05-07 17:28:59,845 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:59,845 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1434462456]
[2025-05-07 17:28:59,845 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:59,845 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:59,871 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-05-07 17:28:59,875 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-05-07 17:28:59,875 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:59,875 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:59,969 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:59,969 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:59,969 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1434462456]
[2025-05-07 17:28:59,969 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1434462456] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:59,969 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:59,969 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:59,969 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1009877514]
[2025-05-07 17:28:59,970 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:59,971 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:59,971 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:59,971 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:59,972 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:59,972 INFO  L87              Difference]: Start difference. First operand 92 states and 105 transitions. Second operand  has 4 states, 3 states have (on average 10.333333333333334) internal successors, (31), 4 states have internal predecessors, (31), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:59,988 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:59,988 INFO  L93              Difference]: Finished difference Result 96 states and 109 transitions.
[2025-05-07 17:28:59,988 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:59,988 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.333333333333334) internal successors, (31), 4 states have internal predecessors, (31), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 67
[2025-05-07 17:28:59,989 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:59,990 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:28:59,990 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:28:59,990 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:59,991 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 1 mSDsluCounter, 199 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 302 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:59,991 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 302 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:59,992 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:28:59,999 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 90.
[2025-05-07 17:28:59,999 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 40 states have (on average 1.075) internal successors, (43), 43 states have internal predecessors, (43), 26 states have call successors, (28), 22 states have call predecessors, (28), 23 states have return successors, (29), 24 states have call predecessors, (29), 26 states have call successors, (29)
[2025-05-07 17:29:00,001 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 100 transitions.
[2025-05-07 17:29:00,001 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 100 transitions. Word has length 67
[2025-05-07 17:29:00,001 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:00,001 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 100 transitions.
[2025-05-07 17:29:00,001 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.333333333333334) internal successors, (31), 4 states have internal predecessors, (31), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:00,001 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 100 transitions.
[2025-05-07 17:29:00,003 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-05-07 17:29:00,003 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:00,003 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:00,004 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:00,004 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:00,004 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:00,004 INFO  L85        PathProgramCache]: Analyzing trace with hash 594154203, now seen corresponding path program 1 times
[2025-05-07 17:29:00,004 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:00,004 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [81032330]
[2025-05-07 17:29:00,005 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:00,005 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:00,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-05-07 17:29:00,051 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-05-07 17:29:00,051 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:00,051 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:00,155 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:00,155 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:00,155 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [81032330]
[2025-05-07 17:29:00,155 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [81032330] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:00,155 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:00,155 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:00,155 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2090750140]
[2025-05-07 17:29:00,155 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:00,156 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:00,156 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:00,156 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:00,156 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:00,157 INFO  L87              Difference]: Start difference. First operand 90 states and 100 transitions. Second operand  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:00,196 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:00,197 INFO  L93              Difference]: Finished difference Result 95 states and 106 transitions.
[2025-05-07 17:29:00,197 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:00,197 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18) Word has length 67
[2025-05-07 17:29:00,198 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:00,199 INFO  L225             Difference]: With dead ends: 95
[2025-05-07 17:29:00,199 INFO  L226             Difference]: Without dead ends: 95
[2025-05-07 17:29:00,199 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:00,200 INFO  L437           NwaCegarLoop]: 96 mSDtfsCounter, 1 mSDsluCounter, 374 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 470 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:00,200 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 470 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:00,201 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 95 states.
[2025-05-07 17:29:00,206 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 95 to 95.
[2025-05-07 17:29:00,206 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 95 states, 42 states have (on average 1.0714285714285714) internal successors, (45), 45 states have internal predecessors, (45), 27 states have call successors, (29), 22 states have call predecessors, (29), 25 states have return successors, (32), 27 states have call predecessors, (32), 27 states have call successors, (32)
[2025-05-07 17:29:00,207 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 95 states to 95 states and 106 transitions.
[2025-05-07 17:29:00,208 INFO  L79                 Accepts]: Start accepts. Automaton has 95 states and 106 transitions. Word has length 67
[2025-05-07 17:29:00,208 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:00,208 INFO  L485      AbstractCegarLoop]: Abstraction has 95 states and 106 transitions.
[2025-05-07 17:29:00,208 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:00,208 INFO  L278                IsEmpty]: Start isEmpty. Operand 95 states and 106 transitions.
[2025-05-07 17:29:00,209 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:29:00,209 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:00,210 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:00,210 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:00,210 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:00,210 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:00,210 INFO  L85        PathProgramCache]: Analyzing trace with hash -788284563, now seen corresponding path program 1 times
[2025-05-07 17:29:00,210 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:00,210 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [731733984]
[2025-05-07 17:29:00,211 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:00,211 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:00,241 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:29:00,257 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:29:00,257 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:00,257 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:00,454 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:29:00,454 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:00,454 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [731733984]
[2025-05-07 17:29:00,454 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [731733984] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:00,454 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:00,454 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:00,455 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1997790102]
[2025-05-07 17:29:00,455 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:00,455 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:00,455 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:00,456 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:00,456 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:00,456 INFO  L87              Difference]: Start difference. First operand 95 states and 106 transitions. Second operand  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 4 states have call successors, (20), 1 states have call predecessors, (20), 3 states have return successors, (20), 3 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:29:00,490 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:00,490 INFO  L93              Difference]: Finished difference Result 97 states and 108 transitions.
[2025-05-07 17:29:00,491 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:00,491 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 4 states have call successors, (20), 1 states have call predecessors, (20), 3 states have return successors, (20), 3 states have call predecessors, (20), 4 states have call successors, (20) Word has length 75
[2025-05-07 17:29:00,491 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:00,492 INFO  L225             Difference]: With dead ends: 97
[2025-05-07 17:29:00,493 INFO  L226             Difference]: Without dead ends: 97
[2025-05-07 17:29:00,493 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 6 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:00,493 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 1 mSDsluCounter, 180 mSDsCounter, 0 mSdLazyCounter, 14 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 275 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 14 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:00,494 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 275 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 14 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:00,494 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 97 states.
[2025-05-07 17:29:00,499 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 97 to 97.
[2025-05-07 17:29:00,500 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 97 states, 43 states have (on average 1.069767441860465) internal successors, (46), 46 states have internal predecessors, (46), 27 states have call successors, (29), 22 states have call predecessors, (29), 26 states have return successors, (33), 28 states have call predecessors, (33), 27 states have call successors, (33)
[2025-05-07 17:29:00,501 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 97 states to 97 states and 108 transitions.
[2025-05-07 17:29:00,501 INFO  L79                 Accepts]: Start accepts. Automaton has 97 states and 108 transitions. Word has length 75
[2025-05-07 17:29:00,501 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:00,501 INFO  L485      AbstractCegarLoop]: Abstraction has 97 states and 108 transitions.
[2025-05-07 17:29:00,501 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 11.666666666666666) internal successors, (35), 4 states have internal predecessors, (35), 4 states have call successors, (20), 1 states have call predecessors, (20), 3 states have return successors, (20), 3 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:29:00,501 INFO  L278                IsEmpty]: Start isEmpty. Operand 97 states and 108 transitions.
[2025-05-07 17:29:00,503 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:29:00,503 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:00,503 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:00,503 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:29:00,503 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:00,503 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:00,504 INFO  L85        PathProgramCache]: Analyzing trace with hash 10326191, now seen corresponding path program 1 times
[2025-05-07 17:29:00,504 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:00,504 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [298016036]
[2025-05-07 17:29:00,504 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:00,504 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:00,536 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:29:00,559 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:29:00,559 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:00,559 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:00,957 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-05-07 17:29:00,958 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:00,958 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [298016036]
[2025-05-07 17:29:00,958 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [298016036] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:00,958 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2143412842]
[2025-05-07 17:29:00,958 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:00,958 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:00,960 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:00,962 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:00,963 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:29:01,162 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:29:01,284 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:29:01,284 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:01,284 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:01,290 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1055 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:01,299 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:01,407 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-05-07 17:29:01,407 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:02,705 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-05-07 17:29:02,705 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2143412842] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:02,705 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:02,705 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 7, 7] total 17
[2025-05-07 17:29:02,705 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1441377954]
[2025-05-07 17:29:02,705 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:02,706 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-05-07 17:29:02,706 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:02,706 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-05-07 17:29:02,706 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=36, Invalid=236, Unknown=0, NotChecked=0, Total=272
[2025-05-07 17:29:02,707 INFO  L87              Difference]: Start difference. First operand 97 states and 108 transitions. Second operand  has 17 states, 11 states have (on average 4.7272727272727275) internal successors, (52), 17 states have internal predecessors, (52), 10 states have call successors, (29), 2 states have call predecessors, (29), 11 states have return successors, (33), 11 states have call predecessors, (33), 10 states have call successors, (33)
[2025-05-07 17:29:02,913 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:02,913 INFO  L93              Difference]: Finished difference Result 117 states and 130 transitions.
[2025-05-07 17:29:02,914 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-05-07 17:29:02,914 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 11 states have (on average 4.7272727272727275) internal successors, (52), 17 states have internal predecessors, (52), 10 states have call successors, (29), 2 states have call predecessors, (29), 11 states have return successors, (33), 11 states have call predecessors, (33), 10 states have call successors, (33) Word has length 83
[2025-05-07 17:29:02,914 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:02,915 INFO  L225             Difference]: With dead ends: 117
[2025-05-07 17:29:02,915 INFO  L226             Difference]: Without dead ends: 117
[2025-05-07 17:29:02,915 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 187 GetRequests, 161 SyntacticMatches, 3 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=81, Invalid=519, Unknown=0, NotChecked=0, Total=600
[2025-05-07 17:29:02,915 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 11 mSDsluCounter, 1206 mSDsCounter, 0 mSdLazyCounter, 175 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 1296 SdHoareTripleChecker+Invalid, 181 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 175 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:02,916 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 1296 Invalid, 181 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 175 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:02,916 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-05-07 17:29:02,920 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 117.
[2025-05-07 17:29:02,920 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 53 states have (on average 1.0566037735849056) internal successors, (56), 56 states have internal predecessors, (56), 27 states have call successors, (29), 22 states have call predecessors, (29), 36 states have return successors, (45), 38 states have call predecessors, (45), 27 states have call successors, (45)
[2025-05-07 17:29:02,921 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 130 transitions.
[2025-05-07 17:29:02,921 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 130 transitions. Word has length 83
[2025-05-07 17:29:02,921 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:02,921 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 130 transitions.
[2025-05-07 17:29:02,921 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 11 states have (on average 4.7272727272727275) internal successors, (52), 17 states have internal predecessors, (52), 10 states have call successors, (29), 2 states have call predecessors, (29), 11 states have return successors, (33), 11 states have call predecessors, (33), 10 states have call successors, (33)
[2025-05-07 17:29:02,922 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 130 transitions.
[2025-05-07 17:29:02,922 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 124
[2025-05-07 17:29:02,922 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:02,922 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 4, 4, 4, 4, 4, 4, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:02,927 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:29:03,123 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-05-07 17:29:03,124 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:03,125 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:03,126 INFO  L85        PathProgramCache]: Analyzing trace with hash 850460760, now seen corresponding path program 2 times
[2025-05-07 17:29:03,126 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:03,126 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [837357351]
[2025-05-07 17:29:03,126 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:29:03,127 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:03,209 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 123 statements into 2 equivalence classes.
[2025-05-07 17:29:03,239 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 123 of 123 statements.
[2025-05-07 17:29:03,239 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:29:03,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:03,573 INFO  L134       CoverageAnalysis]: Checked inductivity of 94 backedges. 32 proven. 15 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-05-07 17:29:03,573 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:03,573 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [837357351]
[2025-05-07 17:29:03,573 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [837357351] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:03,573 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [521961807]
[2025-05-07 17:29:03,573 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:29:03,573 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:03,575 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:03,577 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:29:03,578 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:29:03,819 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 123 statements into 2 equivalence classes.
[2025-05-07 17:29:04,011 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 123 of 123 statements.
[2025-05-07 17:29:04,011 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:29:04,011 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:04,016 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1623 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:04,019 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:04,061 INFO  L134       CoverageAnalysis]: Checked inductivity of 94 backedges. 32 proven. 14 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-05-07 17:29:04,062 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:06,661 INFO  L134       CoverageAnalysis]: Checked inductivity of 94 backedges. 32 proven. 15 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-05-07 17:29:06,661 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [521961807] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:06,662 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:06,662 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 10] total 15
[2025-05-07 17:29:06,662 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1134545359]
[2025-05-07 17:29:06,662 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:06,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-05-07 17:29:06,663 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:06,663 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-05-07 17:29:06,663 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=51, Invalid=159, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:29:06,664 INFO  L87              Difference]: Start difference. First operand 117 states and 130 transitions. Second operand  has 15 states, 9 states have (on average 6.111111111111111) internal successors, (55), 15 states have internal predecessors, (55), 10 states have call successors, (31), 2 states have call predecessors, (31), 9 states have return successors, (36), 9 states have call predecessors, (36), 10 states have call successors, (36)
[2025-05-07 17:29:06,766 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:06,767 INFO  L93              Difference]: Finished difference Result 125 states and 138 transitions.
[2025-05-07 17:29:06,767 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-05-07 17:29:06,767 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 9 states have (on average 6.111111111111111) internal successors, (55), 15 states have internal predecessors, (55), 10 states have call successors, (31), 2 states have call predecessors, (31), 9 states have return successors, (36), 9 states have call predecessors, (36), 10 states have call successors, (36) Word has length 123
[2025-05-07 17:29:06,767 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:06,768 INFO  L225             Difference]: With dead ends: 125
[2025-05-07 17:29:06,768 INFO  L226             Difference]: Without dead ends: 125
[2025-05-07 17:29:06,768 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 261 GetRequests, 241 SyntacticMatches, 5 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 101 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=67, Invalid=205, Unknown=0, NotChecked=0, Total=272
[2025-05-07 17:29:06,769 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 5 mSDsluCounter, 892 mSDsCounter, 0 mSdLazyCounter, 84 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 986 SdHoareTripleChecker+Invalid, 85 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 84 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:06,769 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 986 Invalid, 85 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 84 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:06,769 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-05-07 17:29:06,773 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 125.
[2025-05-07 17:29:06,774 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 57 states have (on average 1.0526315789473684) internal successors, (60), 60 states have internal predecessors, (60), 27 states have call successors, (29), 22 states have call predecessors, (29), 40 states have return successors, (49), 42 states have call predecessors, (49), 27 states have call successors, (49)
[2025-05-07 17:29:06,774 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 138 transitions.
[2025-05-07 17:29:06,774 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 138 transitions. Word has length 123
[2025-05-07 17:29:06,774 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:06,775 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 138 transitions.
[2025-05-07 17:29:06,775 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 9 states have (on average 6.111111111111111) internal successors, (55), 15 states have internal predecessors, (55), 10 states have call successors, (31), 2 states have call predecessors, (31), 9 states have return successors, (36), 9 states have call predecessors, (36), 10 states have call successors, (36)
[2025-05-07 17:29:06,775 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 138 transitions.
[2025-05-07 17:29:06,775 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 140
[2025-05-07 17:29:06,775 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:06,776 INFO  L218           NwaCegarLoop]: trace histogram [8, 6, 6, 6, 6, 6, 6, 6, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:06,780 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:29:06,976 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:29:06,977 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:06,978 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:06,978 INFO  L85        PathProgramCache]: Analyzing trace with hash 40296054, now seen corresponding path program 1 times
[2025-05-07 17:29:06,978 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:06,978 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1760938690]
[2025-05-07 17:29:06,979 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:06,979 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:07,040 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 139 statements into 1 equivalence classes.
[2025-05-07 17:29:07,058 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 139 of 139 statements.
[2025-05-07 17:29:07,058 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:07,058 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:07,494 INFO  L134       CoverageAnalysis]: Checked inductivity of 178 backedges. 67 proven. 20 refuted. 0 times theorem prover too weak. 91 trivial. 0 not checked.
[2025-05-07 17:29:07,494 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:07,494 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1760938690]
[2025-05-07 17:29:07,494 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1760938690] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:07,494 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [890949256]
[2025-05-07 17:29:07,494 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:07,494 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:07,497 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:07,499 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:29:07,500 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:29:07,734 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 139 statements into 1 equivalence classes.
[2025-05-07 17:29:07,877 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 139 of 139 statements.
[2025-05-07 17:29:07,877 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:07,877 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:07,884 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1844 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:07,890 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:07,941 INFO  L134       CoverageAnalysis]: Checked inductivity of 178 backedges. 56 proven. 29 refuted. 0 times theorem prover too weak. 93 trivial. 0 not checked.
[2025-05-07 17:29:07,941 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:12,452 INFO  L134       CoverageAnalysis]: Checked inductivity of 178 backedges. 56 proven. 32 refuted. 0 times theorem prover too weak. 90 trivial. 0 not checked.
[2025-05-07 17:29:12,452 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [890949256] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:12,452 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:12,452 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 13] total 18
[2025-05-07 17:29:12,453 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1818975540]
[2025-05-07 17:29:12,453 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:12,453 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-05-07 17:29:12,454 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:12,454 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-05-07 17:29:12,455 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=236, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:29:12,455 INFO  L87              Difference]: Start difference. First operand 125 states and 138 transitions. Second operand  has 18 states, 11 states have (on average 5.545454545454546) internal successors, (61), 18 states have internal predecessors, (61), 11 states have call successors, (32), 2 states have call predecessors, (32), 11 states have return successors, (44), 11 states have call predecessors, (44), 11 states have call successors, (44)
[2025-05-07 17:29:12,535 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:12,535 INFO  L93              Difference]: Finished difference Result 133 states and 146 transitions.
[2025-05-07 17:29:12,535 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-05-07 17:29:12,536 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 11 states have (on average 5.545454545454546) internal successors, (61), 18 states have internal predecessors, (61), 11 states have call successors, (32), 2 states have call predecessors, (32), 11 states have return successors, (44), 11 states have call predecessors, (44), 11 states have call successors, (44) Word has length 139
[2025-05-07 17:29:12,536 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:12,536 INFO  L225             Difference]: With dead ends: 133
[2025-05-07 17:29:12,536 INFO  L226             Difference]: Without dead ends: 133
[2025-05-07 17:29:12,537 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 297 GetRequests, 271 SyntacticMatches, 7 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 179 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=100, Invalid=320, Unknown=0, NotChecked=0, Total=420
[2025-05-07 17:29:12,537 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 5 mSDsluCounter, 801 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 895 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:12,537 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 895 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:12,537 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-05-07 17:29:12,541 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 133.
[2025-05-07 17:29:12,541 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 61 states have (on average 1.0491803278688525) internal successors, (64), 64 states have internal predecessors, (64), 27 states have call successors, (29), 22 states have call predecessors, (29), 44 states have return successors, (53), 46 states have call predecessors, (53), 27 states have call successors, (53)
[2025-05-07 17:29:12,542 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 146 transitions.
[2025-05-07 17:29:12,542 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 146 transitions. Word has length 139
[2025-05-07 17:29:12,542 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:12,542 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 146 transitions.
[2025-05-07 17:29:12,542 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 11 states have (on average 5.545454545454546) internal successors, (61), 18 states have internal predecessors, (61), 11 states have call successors, (32), 2 states have call predecessors, (32), 11 states have return successors, (44), 11 states have call predecessors, (44), 11 states have call successors, (44)
[2025-05-07 17:29:12,542 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 146 transitions.
[2025-05-07 17:29:12,543 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 156
[2025-05-07 17:29:12,543 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:12,543 INFO  L218           NwaCegarLoop]: trace histogram [10, 8, 8, 8, 8, 8, 8, 8, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:12,548 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:29:12,744 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:29:12,745 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:12,746 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:12,746 INFO  L85        PathProgramCache]: Analyzing trace with hash -1262229032, now seen corresponding path program 3 times
[2025-05-07 17:29:12,746 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:12,746 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2058798709]
[2025-05-07 17:29:12,747 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:29:12,747 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:12,816 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 155 statements into 7 equivalence classes.
[2025-05-07 17:29:12,853 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 147 of 155 statements.
[2025-05-07 17:29:12,853 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-05-07 17:29:12,853 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:13,390 INFO  L134       CoverageAnalysis]: Checked inductivity of 294 backedges. 106 proven. 35 refuted. 0 times theorem prover too weak. 153 trivial. 0 not checked.
[2025-05-07 17:29:13,390 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:13,390 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2058798709]
[2025-05-07 17:29:13,390 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2058798709] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:13,390 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1485979714]
[2025-05-07 17:29:13,390 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:29:13,390 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:13,393 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:13,394 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:29:13,395 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:29:13,754 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 155 statements into 7 equivalence classes.
[2025-05-07 17:29:13,949 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 147 of 155 statements.
[2025-05-07 17:29:13,949 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-05-07 17:29:13,949 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:13,955 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1956 conjuncts, 24 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:13,958 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:14,005 INFO  L134       CoverageAnalysis]: Checked inductivity of 294 backedges. 106 proven. 32 refuted. 0 times theorem prover too weak. 156 trivial. 0 not checked.
[2025-05-07 17:29:14,005 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:28,948 INFO  L134       CoverageAnalysis]: Checked inductivity of 294 backedges. 106 proven. 38 refuted. 0 times theorem prover too weak. 150 trivial. 0 not checked.
[2025-05-07 17:29:28,949 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1485979714] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:28,949 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:28,949 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 13, 16] total 21
[2025-05-07 17:29:28,949 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1080441098]
[2025-05-07 17:29:28,949 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,949 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-05-07 17:29:28,949 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,950 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-05-07 17:29:28,950 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=92, Invalid=328, Unknown=0, NotChecked=0, Total=420
[2025-05-07 17:29:28,950 INFO  L87              Difference]: Start difference. First operand 133 states and 146 transitions. Second operand  has 21 states, 13 states have (on average 4.6923076923076925) internal successors, (61), 21 states have internal predecessors, (61), 12 states have call successors, (33), 2 states have call predecessors, (33), 13 states have return successors, (42), 13 states have call predecessors, (42), 12 states have call successors, (42)
[2025-05-07 17:29:29,075 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:29,075 INFO  L93              Difference]: Finished difference Result 141 states and 154 transitions.
[2025-05-07 17:29:29,075 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:29,076 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 13 states have (on average 4.6923076923076925) internal successors, (61), 21 states have internal predecessors, (61), 12 states have call successors, (33), 2 states have call predecessors, (33), 13 states have return successors, (42), 13 states have call predecessors, (42), 12 states have call successors, (42) Word has length 155
[2025-05-07 17:29:29,076 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:29,077 INFO  L225             Difference]: With dead ends: 141
[2025-05-07 17:29:29,077 INFO  L226             Difference]: Without dead ends: 141
[2025-05-07 17:29:29,077 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 332 GetRequests, 300 SyntacticMatches, 9 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 273 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=140, Invalid=460, Unknown=0, NotChecked=0, Total=600
[2025-05-07 17:29:29,078 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 13 mSDsluCounter, 718 mSDsCounter, 0 mSdLazyCounter, 75 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 812 SdHoareTripleChecker+Invalid, 82 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 75 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:29,078 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 812 Invalid, 82 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 75 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:29,079 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-05-07 17:29:29,086 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 141.
[2025-05-07 17:29:29,086 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 141 states, 65 states have (on average 1.0461538461538462) internal successors, (68), 68 states have internal predecessors, (68), 27 states have call successors, (29), 22 states have call predecessors, (29), 48 states have return successors, (57), 50 states have call predecessors, (57), 27 states have call successors, (57)
[2025-05-07 17:29:29,087 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 141 states to 141 states and 154 transitions.
[2025-05-07 17:29:29,087 INFO  L79                 Accepts]: Start accepts. Automaton has 141 states and 154 transitions. Word has length 155
[2025-05-07 17:29:29,088 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:29,088 INFO  L485      AbstractCegarLoop]: Abstraction has 141 states and 154 transitions.
[2025-05-07 17:29:29,088 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 13 states have (on average 4.6923076923076925) internal successors, (61), 21 states have internal predecessors, (61), 12 states have call successors, (33), 2 states have call predecessors, (33), 13 states have return successors, (42), 13 states have call predecessors, (42), 12 states have call successors, (42)
[2025-05-07 17:29:29,088 INFO  L278                IsEmpty]: Start isEmpty. Operand 141 states and 154 transitions.
[2025-05-07 17:29:29,090 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 172
[2025-05-07 17:29:29,090 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:29,090 INFO  L218           NwaCegarLoop]: trace histogram [12, 10, 10, 10, 10, 10, 10, 10, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:29,096 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:29:29,291 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:29:29,292 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:29,292 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:29,293 INFO  L85        PathProgramCache]: Analyzing trace with hash 269693942, now seen corresponding path program 2 times
[2025-05-07 17:29:29,293 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:29,293 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1175544704]
[2025-05-07 17:29:29,293 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:29:29,293 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:29,368 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 171 statements into 2 equivalence classes.
[2025-05-07 17:29:29,391 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 171 of 171 statements.
[2025-05-07 17:29:29,391 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:29:29,391 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:29,979 INFO  L134       CoverageAnalysis]: Checked inductivity of 442 backedges. 128 proven. 81 refuted. 0 times theorem prover too weak. 233 trivial. 0 not checked.
[2025-05-07 17:29:29,979 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:29,979 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1175544704]
[2025-05-07 17:29:29,979 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1175544704] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:29,979 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [474141992]
[2025-05-07 17:29:29,979 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:29:29,979 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:29,981 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:29,982 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:29:29,983 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-05-07 17:29:30,657 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 171 statements into 2 equivalence classes.
[2025-05-07 17:29:30,821 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 171 of 171 statements.
[2025-05-07 17:29:30,821 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:29:30,821 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:30,828 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2288 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:30,833 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:30,893 INFO  L134       CoverageAnalysis]: Checked inductivity of 442 backedges. 128 proven. 77 refuted. 0 times theorem prover too weak. 237 trivial. 0 not checked.
[2025-05-07 17:29:30,893 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:29:44,432 INFO  L134       CoverageAnalysis]: Checked inductivity of 442 backedges. 128 proven. 87 refuted. 0 times theorem prover too weak. 227 trivial. 0 not checked.
[2025-05-07 17:29:44,432 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [474141992] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:29:44,432 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:29:44,432 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 15, 19] total 24
[2025-05-07 17:29:44,432 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [225622195]
[2025-05-07 17:29:44,432 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:29:44,433 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-05-07 17:29:44,433 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:44,433 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-05-07 17:29:44,433 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=117, Invalid=435, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:29:44,434 INFO  L87              Difference]: Start difference. First operand 141 states and 154 transitions. Second operand  has 24 states, 15 states have (on average 4.266666666666667) internal successors, (64), 24 states have internal predecessors, (64), 13 states have call successors, (34), 2 states have call predecessors, (34), 15 states have return successors, (45), 15 states have call predecessors, (45), 13 states have call successors, (45)
[2025-05-07 17:29:44,548 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:44,548 INFO  L93              Difference]: Finished difference Result 149 states and 162 transitions.
[2025-05-07 17:29:44,548 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-05-07 17:29:44,548 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 15 states have (on average 4.266666666666667) internal successors, (64), 24 states have internal predecessors, (64), 13 states have call successors, (34), 2 states have call predecessors, (34), 15 states have return successors, (45), 15 states have call predecessors, (45), 13 states have call successors, (45) Word has length 171
[2025-05-07 17:29:44,549 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:44,549 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:29:44,549 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:29:44,549 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 369 GetRequests, 331 SyntacticMatches, 11 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 383 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=187, Invalid=625, Unknown=0, NotChecked=0, Total=812
[2025-05-07 17:29:44,550 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 20 mSDsluCounter, 985 mSDsCounter, 0 mSdLazyCounter, 95 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 1079 SdHoareTripleChecker+Invalid, 108 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 95 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:44,550 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 1079 Invalid, 108 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 95 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:44,550 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:29:44,556 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 149.
[2025-05-07 17:29:44,557 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 69 states have (on average 1.0434782608695652) internal successors, (72), 72 states have internal predecessors, (72), 27 states have call successors, (29), 22 states have call predecessors, (29), 52 states have return successors, (61), 54 states have call predecessors, (61), 27 states have call successors, (61)
[2025-05-07 17:29:44,558 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 162 transitions.
[2025-05-07 17:29:44,558 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 162 transitions. Word has length 171
[2025-05-07 17:29:44,558 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:44,558 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 162 transitions.
[2025-05-07 17:29:44,558 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 15 states have (on average 4.266666666666667) internal successors, (64), 24 states have internal predecessors, (64), 13 states have call successors, (34), 2 states have call predecessors, (34), 15 states have return successors, (45), 15 states have call predecessors, (45), 13 states have call successors, (45)
[2025-05-07 17:29:44,558 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 162 transitions.
[2025-05-07 17:29:44,560 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 188
[2025-05-07 17:29:44,561 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:44,561 INFO  L218           NwaCegarLoop]: trace histogram [14, 12, 12, 12, 12, 12, 12, 12, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:44,567 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-05-07 17:29:44,761 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:29:44,762 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:44,762 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:44,763 INFO  L85        PathProgramCache]: Analyzing trace with hash -121593000, now seen corresponding path program 4 times
[2025-05-07 17:29:44,763 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:44,763 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1729248431]
[2025-05-07 17:29:44,763 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:29:44,764 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:44,841 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 187 statements into 2 equivalence classes.
[2025-05-07 17:29:44,854 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 187 of 187 statements.
[2025-05-07 17:29:44,854 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:29:44,854 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:45,522 INFO  L134       CoverageAnalysis]: Checked inductivity of 622 backedges. 214 proven. 77 refuted. 0 times theorem prover too weak. 331 trivial. 0 not checked.
[2025-05-07 17:29:45,522 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:45,522 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1729248431]
[2025-05-07 17:29:45,522 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1729248431] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:45,522 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1168598218]
[2025-05-07 17:29:45,522 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:29:45,522 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:45,524 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:45,525 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:29:45,526 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-05-07 17:29:46,199 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 187 statements into 2 equivalence classes.
[2025-05-07 17:29:46,374 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 187 of 187 statements.
[2025-05-07 17:29:46,374 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:29:46,374 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:46,381 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2511 conjuncts, 32 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:46,385 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:46,425 INFO  L134       CoverageAnalysis]: Checked inductivity of 622 backedges. 214 proven. 72 refuted. 0 times theorem prover too weak. 336 trivial. 0 not checked.
[2025-05-07 17:29:46,426 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:30:32,933 INFO  L134       CoverageAnalysis]: Checked inductivity of 622 backedges. 214 proven. 87 refuted. 0 times theorem prover too weak. 321 trivial. 0 not checked.
[2025-05-07 17:30:32,933 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1168598218] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:30:32,934 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:30:32,934 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 17, 22] total 27
[2025-05-07 17:30:32,934 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [204919005]
[2025-05-07 17:30:32,934 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:30:32,934 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-05-07 17:30:32,934 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:30:32,935 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-05-07 17:30:32,935 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=145, Invalid=557, Unknown=0, NotChecked=0, Total=702
[2025-05-07 17:30:32,935 INFO  L87              Difference]: Start difference. First operand 149 states and 162 transitions. Second operand  has 27 states, 17 states have (on average 3.9411764705882355) internal successors, (67), 27 states have internal predecessors, (67), 14 states have call successors, (35), 2 states have call predecessors, (35), 17 states have return successors, (48), 17 states have call predecessors, (48), 14 states have call successors, (48)
[2025-05-07 17:30:33,086 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:30:33,086 INFO  L93              Difference]: Finished difference Result 157 states and 170 transitions.
[2025-05-07 17:30:33,086 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-05-07 17:30:33,086 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 17 states have (on average 3.9411764705882355) internal successors, (67), 27 states have internal predecessors, (67), 14 states have call successors, (35), 2 states have call predecessors, (35), 17 states have return successors, (48), 17 states have call predecessors, (48), 14 states have call successors, (48) Word has length 187
[2025-05-07 17:30:33,087 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:30:33,087 INFO  L225             Difference]: With dead ends: 157
[2025-05-07 17:30:33,087 INFO  L226             Difference]: Without dead ends: 157
[2025-05-07 17:30:33,087 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 403 GetRequests, 359 SyntacticMatches, 13 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 509 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=241, Invalid=815, Unknown=0, NotChecked=0, Total=1056
[2025-05-07 17:30:33,088 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 12 mSDsluCounter, 1168 mSDsCounter, 0 mSdLazyCounter, 112 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 1262 SdHoareTripleChecker+Invalid, 116 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 112 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:30:33,088 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 1262 Invalid, 116 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 112 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:30:33,088 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 157 states.
[2025-05-07 17:30:33,092 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 157 to 157.
[2025-05-07 17:30:33,092 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 157 states, 73 states have (on average 1.0410958904109588) internal successors, (76), 76 states have internal predecessors, (76), 27 states have call successors, (29), 22 states have call predecessors, (29), 56 states have return successors, (65), 58 states have call predecessors, (65), 27 states have call successors, (65)
[2025-05-07 17:30:33,093 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 157 states to 157 states and 170 transitions.
[2025-05-07 17:30:33,093 INFO  L79                 Accepts]: Start accepts. Automaton has 157 states and 170 transitions. Word has length 187
[2025-05-07 17:30:33,093 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:30:33,093 INFO  L485      AbstractCegarLoop]: Abstraction has 157 states and 170 transitions.
[2025-05-07 17:30:33,093 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 17 states have (on average 3.9411764705882355) internal successors, (67), 27 states have internal predecessors, (67), 14 states have call successors, (35), 2 states have call predecessors, (35), 17 states have return successors, (48), 17 states have call predecessors, (48), 14 states have call successors, (48)
[2025-05-07 17:30:33,093 INFO  L278                IsEmpty]: Start isEmpty. Operand 157 states and 170 transitions.
[2025-05-07 17:30:33,094 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 204
[2025-05-07 17:30:33,094 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:30:33,094 INFO  L218           NwaCegarLoop]: trace histogram [16, 14, 14, 14, 14, 14, 14, 14, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:30:33,102 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-05-07 17:30:33,295 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:30:33,295 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:30:33,295 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:30:33,296 INFO  L85        PathProgramCache]: Analyzing trace with hash 1537256984, now seen corresponding path program 5 times
[2025-05-07 17:30:33,296 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:30:33,296 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1361649724]
[2025-05-07 17:30:33,296 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-05-07 17:30:33,296 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:30:33,346 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 203 statements into 10 equivalence classes.
[2025-05-07 17:30:33,364 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s) and asserted 128 of 203 statements.
[2025-05-07 17:30:33,364 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s)
[2025-05-07 17:30:33,364 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:33,901 INFO  L134       CoverageAnalysis]: Checked inductivity of 834 backedges. 232 proven. 149 refuted. 0 times theorem prover too weak. 453 trivial. 0 not checked.
[2025-05-07 17:30:33,901 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:30:33,901 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1361649724]
[2025-05-07 17:30:33,901 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1361649724] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:30:33,901 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1238156646]
[2025-05-07 17:30:33,901 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-05-07 17:30:33,901 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:30:33,903 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:30:33,904 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:30:33,905 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-05-07 17:30:35,185 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 203 statements into 10 equivalence classes.
[2025-05-07 17:30:35,329 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s) and asserted 128 of 203 statements.
[2025-05-07 17:30:35,329 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s)
[2025-05-07 17:30:35,329 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:35,335 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1791 conjuncts, 36 conjuncts are in the unsatisfiable core
[2025-05-07 17:30:35,339 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:30:35,380 INFO  L134       CoverageAnalysis]: Checked inductivity of 834 backedges. 232 proven. 149 refuted. 0 times theorem prover too weak. 453 trivial. 0 not checked.
[2025-05-07 17:30:35,380 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:31:09,700 INFO  L134       CoverageAnalysis]: Checked inductivity of 834 backedges. 232 proven. 170 refuted. 0 times theorem prover too weak. 432 trivial. 0 not checked.
[2025-05-07 17:31:09,700 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1238156646] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:31:09,700 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:31:09,700 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [19, 19, 25] total 27
[2025-05-07 17:31:09,701 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [201641090]
[2025-05-07 17:31:09,701 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:31:09,701 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-05-07 17:31:09,701 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:31:09,701 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-05-07 17:31:09,702 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=143, Invalid=559, Unknown=0, NotChecked=0, Total=702
[2025-05-07 17:31:09,702 INFO  L87              Difference]: Start difference. First operand 157 states and 170 transitions. Second operand  has 27 states, 17 states have (on average 3.8823529411764706) internal successors, (66), 27 states have internal predecessors, (66), 13 states have call successors, (34), 2 states have call predecessors, (34), 17 states have return successors, (48), 17 states have call predecessors, (48), 13 states have call successors, (48)
[2025-05-07 17:31:09,855 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:31:09,855 INFO  L93              Difference]: Finished difference Result 165 states and 178 transitions.
[2025-05-07 17:31:09,856 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-05-07 17:31:09,856 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 17 states have (on average 3.8823529411764706) internal successors, (66), 27 states have internal predecessors, (66), 13 states have call successors, (34), 2 states have call predecessors, (34), 17 states have return successors, (48), 17 states have call predecessors, (48), 13 states have call successors, (48) Word has length 203
[2025-05-07 17:31:09,856 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:31:09,857 INFO  L225             Difference]: With dead ends: 165
[2025-05-07 17:31:09,857 INFO  L226             Difference]: Without dead ends: 165
[2025-05-07 17:31:09,857 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 438 GetRequests, 391 SyntacticMatches, 15 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 400 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=262, Invalid=860, Unknown=0, NotChecked=0, Total=1122
[2025-05-07 17:31:09,857 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 10 mSDsluCounter, 1344 mSDsCounter, 0 mSdLazyCounter, 124 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 1438 SdHoareTripleChecker+Invalid, 125 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 124 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:31:09,858 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 1438 Invalid, 125 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 124 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:31:09,858 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-05-07 17:31:09,861 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 165.
[2025-05-07 17:31:09,862 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 165 states, 77 states have (on average 1.0389610389610389) internal successors, (80), 80 states have internal predecessors, (80), 27 states have call successors, (29), 22 states have call predecessors, (29), 60 states have return successors, (69), 62 states have call predecessors, (69), 27 states have call successors, (69)
[2025-05-07 17:31:09,862 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 165 states to 165 states and 178 transitions.
[2025-05-07 17:31:09,862 INFO  L79                 Accepts]: Start accepts. Automaton has 165 states and 178 transitions. Word has length 203
[2025-05-07 17:31:09,862 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:31:09,863 INFO  L485      AbstractCegarLoop]: Abstraction has 165 states and 178 transitions.
[2025-05-07 17:31:09,863 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 17 states have (on average 3.8823529411764706) internal successors, (66), 27 states have internal predecessors, (66), 13 states have call successors, (34), 2 states have call predecessors, (34), 17 states have return successors, (48), 17 states have call predecessors, (48), 13 states have call successors, (48)
[2025-05-07 17:31:09,863 INFO  L278                IsEmpty]: Start isEmpty. Operand 165 states and 178 transitions.
[2025-05-07 17:31:09,864 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 220
[2025-05-07 17:31:09,864 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:31:09,864 INFO  L218           NwaCegarLoop]: trace histogram [18, 16, 16, 16, 16, 16, 16, 16, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:31:09,874 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-05-07 17:31:10,065 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:31:10,065 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:31:10,066 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:31:10,067 INFO  L85        PathProgramCache]: Analyzing trace with hash -392816074, now seen corresponding path program 3 times
[2025-05-07 17:31:10,067 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:31:10,067 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [153495363]
[2025-05-07 17:31:10,067 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:31:10,067 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:31:10,142 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 219 statements into 11 equivalence classes.
[2025-05-07 17:31:10,191 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 211 of 219 statements.
[2025-05-07 17:31:10,191 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-05-07 17:31:10,191 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:31:11,244 INFO  L134       CoverageAnalysis]: Checked inductivity of 1078 backedges. 362 proven. 135 refuted. 0 times theorem prover too weak. 581 trivial. 0 not checked.
[2025-05-07 17:31:11,245 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:31:11,245 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [153495363]
[2025-05-07 17:31:11,245 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [153495363] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:31:11,245 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [905581847]
[2025-05-07 17:31:11,245 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-05-07 17:31:11,245 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:31:11,246 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:31:11,248 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:31:11,249 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-05-07 17:31:12,555 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 219 statements into 11 equivalence classes.
[2025-05-07 17:31:12,811 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 211 of 219 statements.
[2025-05-07 17:31:12,811 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-05-07 17:31:12,811 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:31:12,821 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2843 conjuncts, 40 conjuncts are in the unsatisfiable core
[2025-05-07 17:31:12,825 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:31:12,884 INFO  L134       CoverageAnalysis]: Checked inductivity of 1078 backedges. 362 proven. 128 refuted. 0 times theorem prover too weak. 588 trivial. 0 not checked.
[2025-05-07 17:31:12,884 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:33:06,205 INFO  L134       CoverageAnalysis]: Checked inductivity of 1078 backedges. 362 proven. 156 refuted. 0 times theorem prover too weak. 560 trivial. 0 not checked.
[2025-05-07 17:33:06,205 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [905581847] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:33:06,205 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:33:06,206 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [22, 21, 28] total 33
[2025-05-07 17:33:06,206 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [947967129]
[2025-05-07 17:33:06,206 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:33:06,207 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-05-07 17:33:06,208 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:33:06,209 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-05-07 17:33:06,209 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=210, Invalid=846, Unknown=0, NotChecked=0, Total=1056
[2025-05-07 17:33:06,211 INFO  L87              Difference]: Start difference. First operand 165 states and 178 transitions. Second operand  has 33 states, 21 states have (on average 3.4761904761904763) internal successors, (73), 33 states have internal predecessors, (73), 16 states have call successors, (37), 2 states have call predecessors, (37), 21 states have return successors, (54), 21 states have call predecessors, (54), 16 states have call successors, (54)
[2025-05-07 17:33:06,479 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:33:06,479 INFO  L93              Difference]: Finished difference Result 173 states and 186 transitions.
[2025-05-07 17:33:06,480 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-05-07 17:33:06,480 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 21 states have (on average 3.4761904761904763) internal successors, (73), 33 states have internal predecessors, (73), 16 states have call successors, (37), 2 states have call predecessors, (37), 21 states have return successors, (54), 21 states have call predecessors, (54), 16 states have call successors, (54) Word has length 219
[2025-05-07 17:33:06,481 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:33:06,483 INFO  L225             Difference]: With dead ends: 173
[2025-05-07 17:33:06,484 INFO  L226             Difference]: Without dead ends: 173
[2025-05-07 17:33:06,485 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 477 GetRequests, 421 SyntacticMatches, 17 SemanticMatches, 39 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 809 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=370, Invalid=1270, Unknown=0, NotChecked=0, Total=1640
[2025-05-07 17:33:06,486 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 11 mSDsluCounter, 1423 mSDsCounter, 0 mSdLazyCounter, 141 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 1517 SdHoareTripleChecker+Invalid, 142 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 141 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:33:06,487 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 1517 Invalid, 142 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 141 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:33:06,488 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 173 states.
[2025-05-07 17:33:06,504 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 173 to 173.
[2025-05-07 17:33:06,505 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 81 states have (on average 1.037037037037037) internal successors, (84), 84 states have internal predecessors, (84), 27 states have call successors, (29), 22 states have call predecessors, (29), 64 states have return successors, (73), 66 states have call predecessors, (73), 27 states have call successors, (73)
[2025-05-07 17:33:06,507 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 186 transitions.
[2025-05-07 17:33:06,507 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 186 transitions. Word has length 219
[2025-05-07 17:33:06,508 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:33:06,508 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 186 transitions.
[2025-05-07 17:33:06,509 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 21 states have (on average 3.4761904761904763) internal successors, (73), 33 states have internal predecessors, (73), 16 states have call successors, (37), 2 states have call predecessors, (37), 21 states have return successors, (54), 21 states have call predecessors, (54), 16 states have call successors, (54)
[2025-05-07 17:33:06,509 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 186 transitions.
[2025-05-07 17:33:06,513 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 236
[2025-05-07 17:33:06,513 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:33:06,514 INFO  L218           NwaCegarLoop]: trace histogram [20, 18, 18, 18, 18, 18, 18, 18, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:33:06,531 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-05-07 17:33:06,715 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:33:06,715 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:33:06,719 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:33:06,720 INFO  L85        PathProgramCache]: Analyzing trace with hash -1334304872, now seen corresponding path program 6 times
[2025-05-07 17:33:06,720 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:33:06,721 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1037492341]
[2025-05-07 17:33:06,721 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-05-07 17:33:06,722 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:33:06,939 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 235 statements into 12 equivalence classes.
[2025-05-07 17:33:07,233 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 12 check-sat command(s) and asserted 235 of 235 statements.
[2025-05-07 17:33:07,233 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 12 check-sat command(s)
[2025-05-07 17:33:07,233 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:33:09,525 INFO  L134       CoverageAnalysis]: Checked inductivity of 1354 backedges. 0 proven. 374 refuted. 0 times theorem prover too weak. 980 trivial. 0 not checked.
[2025-05-07 17:33:09,525 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:33:09,525 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1037492341]
[2025-05-07 17:33:09,525 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1037492341] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:33:09,525 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [151132733]
[2025-05-07 17:33:09,525 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-05-07 17:33:09,526 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:33:09,528 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:33:09,530 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:33:09,531 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-05-07 17:33:12,188 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 235 statements into 12 equivalence classes.
[2025-05-07 17:33:12,523 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 12 check-sat command(s) and asserted 235 of 235 statements.
[2025-05-07 17:33:12,523 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 12 check-sat command(s)
[2025-05-07 17:33:12,523 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:33:12,534 INFO  L256         TraceCheckSpWp]: Trace formula consists of 3177 conjuncts, 44 conjuncts are in the unsatisfiable core
[2025-05-07 17:33:12,540 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:33:12,869 INFO  L134       CoverageAnalysis]: Checked inductivity of 1354 backedges. 451 proven. 162 refuted. 0 times theorem prover too weak. 741 trivial. 0 not checked.
[2025-05-07 17:33:12,869 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:36:13,568 INFO  L134       CoverageAnalysis]: Checked inductivity of 1354 backedges. 451 proven. 198 refuted. 0 times theorem prover too weak. 705 trivial. 0 not checked.
[2025-05-07 17:36:13,569 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [151132733] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:36:13,569 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:36:13,569 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [17, 23, 31] total 46
[2025-05-07 17:36:13,570 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [946395290]
[2025-05-07 17:36:13,570 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:36:13,572 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 46 states
[2025-05-07 17:36:13,572 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:36:13,574 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 46 interpolants.
[2025-05-07 17:36:13,575 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=236, Invalid=1834, Unknown=0, NotChecked=0, Total=2070
[2025-05-07 17:36:13,576 INFO  L87              Difference]: Start difference. First operand 173 states and 186 transitions. Second operand  has 46 states, 32 states have (on average 2.6875) internal successors, (86), 46 states have internal predecessors, (86), 18 states have call successors, (39), 2 states have call predecessors, (39), 32 states have return successors, (67), 32 states have call predecessors, (67), 18 states have call successors, (67)
[2025-05-07 17:36:14,945 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:36:14,945 INFO  L93              Difference]: Finished difference Result 229 states and 244 transitions.
[2025-05-07 17:36:14,945 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 73 states. 
[2025-05-07 17:36:14,946 INFO  L79                 Accepts]: Start accepts. Automaton has  has 46 states, 32 states have (on average 2.6875) internal successors, (86), 46 states have internal predecessors, (86), 18 states have call successors, (39), 2 states have call predecessors, (39), 32 states have return successors, (67), 32 states have call predecessors, (67), 18 states have call successors, (67) Word has length 235
[2025-05-07 17:36:14,947 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:36:14,950 INFO  L225             Difference]: With dead ends: 229
[2025-05-07 17:36:14,950 INFO  L226             Difference]: Without dead ends: 229
[2025-05-07 17:36:14,953 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 580 GetRequests, 462 SyntacticMatches, 20 SemanticMatches, 98 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2204 ImplicationChecksByTransitivity, 1.9s TimeCoverageRelationStatistics Valid=1393, Invalid=8507, Unknown=0, NotChecked=0, Total=9900
[2025-05-07 17:36:14,954 INFO  L437           NwaCegarLoop]: 92 mSDtfsCounter, 108 mSDsluCounter, 2121 mSDsCounter, 0 mSdLazyCounter, 342 mSolverCounterSat, 76 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 142 SdHoareTripleChecker+Valid, 2213 SdHoareTripleChecker+Invalid, 418 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 76 IncrementalHoareTripleChecker+Valid, 342 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:36:14,955 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [142 Valid, 2213 Invalid, 418 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [76 Valid, 342 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:36:14,956 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 229 states.
[2025-05-07 17:36:14,975 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 229 to 229.
[2025-05-07 17:36:14,976 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 229 states, 109 states have (on average 1.0275229357798166) internal successors, (112), 112 states have internal predecessors, (112), 27 states have call successors, (29), 22 states have call predecessors, (29), 92 states have return successors, (103), 94 states have call predecessors, (103), 27 states have call successors, (103)
[2025-05-07 17:36:14,978 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 229 states to 229 states and 244 transitions.
[2025-05-07 17:36:14,979 INFO  L79                 Accepts]: Start accepts. Automaton has 229 states and 244 transitions. Word has length 235
[2025-05-07 17:36:14,979 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:36:14,979 INFO  L485      AbstractCegarLoop]: Abstraction has 229 states and 244 transitions.
[2025-05-07 17:36:14,980 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 46 states, 32 states have (on average 2.6875) internal successors, (86), 46 states have internal predecessors, (86), 18 states have call successors, (39), 2 states have call predecessors, (39), 32 states have return successors, (67), 32 states have call predecessors, (67), 18 states have call successors, (67)
[2025-05-07 17:36:14,980 INFO  L278                IsEmpty]: Start isEmpty. Operand 229 states and 244 transitions.
[2025-05-07 17:36:14,986 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 348
[2025-05-07 17:36:14,987 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:36:14,987 INFO  L218           NwaCegarLoop]: trace histogram [33, 30, 30, 30, 30, 30, 30, 30, 4, 3, 3, 3, 3, 3, 3, 3, 3, 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, 1]
[2025-05-07 17:36:15,011 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-05-07 17:36:15,188 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:36:15,189 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:36:15,192 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:36:15,193 INFO  L85        PathProgramCache]: Analyzing trace with hash 1027494079, now seen corresponding path program 4 times
[2025-05-07 17:36:15,193 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:36:15,194 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1510079785]
[2025-05-07 17:36:15,195 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-05-07 17:36:15,195 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:36:15,374 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 347 statements into 2 equivalence classes.
[2025-05-07 17:36:15,542 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 347 of 347 statements.
[2025-05-07 17:36:15,542 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-05-07 17:36:15,542 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:36:19,801 INFO  L134       CoverageAnalysis]: Checked inductivity of 3807 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3807 trivial. 0 not checked.
[2025-05-07 17:36:19,801 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:36:19,802 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1510079785]
[2025-05-07 17:36:19,802 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1510079785] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:36:19,802 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:36:19,802 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [15] imperfect sequences [] total 15
[2025-05-07 17:36:19,802 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [694350839]
[2025-05-07 17:36:19,802 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:36:19,803 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-05-07 17:36:19,803 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:36:19,804 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-05-07 17:36:19,804 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=182, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:36:19,804 INFO  L87              Difference]: Start difference. First operand 229 states and 244 transitions. Second operand  has 15 states, 12 states have (on average 3.0833333333333335) internal successors, (37), 15 states have internal predecessors, (37), 6 states have call successors, (22), 1 states have call predecessors, (22), 12 states have return successors, (22), 13 states have call predecessors, (22), 6 states have call successors, (22)
[2025-05-07 17:36:19,957 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:36:19,957 INFO  L93              Difference]: Finished difference Result 234 states and 250 transitions.
[2025-05-07 17:36:19,958 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:36:19,958 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 12 states have (on average 3.0833333333333335) internal successors, (37), 15 states have internal predecessors, (37), 6 states have call successors, (22), 1 states have call predecessors, (22), 12 states have return successors, (22), 13 states have call predecessors, (22), 6 states have call successors, (22) Word has length 347
[2025-05-07 17:36:19,958 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:36:19,960 INFO  L225             Difference]: With dead ends: 234
[2025-05-07 17:36:19,960 INFO  L226             Difference]: Without dead ends: 234
[2025-05-07 17:36:19,960 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 86 GetRequests, 72 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=208, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:36:19,961 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 2 mSDsluCounter, 1128 mSDsCounter, 0 mSdLazyCounter, 216 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1218 SdHoareTripleChecker+Invalid, 216 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 216 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:36:19,961 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1218 Invalid, 216 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 216 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:36:19,962 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 234 states.
[2025-05-07 17:36:19,970 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 234 to 229.
[2025-05-07 17:36:19,971 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 229 states, 109 states have (on average 1.0275229357798166) internal successors, (112), 112 states have internal predecessors, (112), 27 states have call successors, (29), 22 states have call predecessors, (29), 92 states have return successors, (103), 94 states have call predecessors, (103), 27 states have call successors, (103)
[2025-05-07 17:36:19,972 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 229 states to 229 states and 244 transitions.
[2025-05-07 17:36:19,972 INFO  L79                 Accepts]: Start accepts. Automaton has 229 states and 244 transitions. Word has length 347
[2025-05-07 17:36:19,972 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:36:19,972 INFO  L485      AbstractCegarLoop]: Abstraction has 229 states and 244 transitions.
[2025-05-07 17:36:19,972 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 12 states have (on average 3.0833333333333335) internal successors, (37), 15 states have internal predecessors, (37), 6 states have call successors, (22), 1 states have call predecessors, (22), 12 states have return successors, (22), 13 states have call predecessors, (22), 6 states have call successors, (22)
[2025-05-07 17:36:19,973 INFO  L278                IsEmpty]: Start isEmpty. Operand 229 states and 244 transitions.
[2025-05-07 17:36:19,975 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 348
[2025-05-07 17:36:19,976 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:36:19,976 INFO  L218           NwaCegarLoop]: trace histogram [33, 30, 30, 30, 30, 30, 30, 30, 4, 3, 3, 3, 3, 3, 3, 3, 3, 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, 1]
[2025-05-07 17:36:19,976 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:36:19,976 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:36:19,976 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:36:19,977 INFO  L85        PathProgramCache]: Analyzing trace with hash -1295166623, now seen corresponding path program 7 times
[2025-05-07 17:36:19,977 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:36:19,977 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1249885418]
[2025-05-07 17:36:19,977 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-05-07 17:36:19,977 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:36:20,085 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 347 statements into 1 equivalence classes.
[2025-05-07 17:36:20,153 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 347 of 347 statements.
[2025-05-07 17:36:20,153 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:36:20,154 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:36:23,181 INFO  L134       CoverageAnalysis]: Checked inductivity of 3807 backedges. 0 proven. 1352 refuted. 0 times theorem prover too weak. 2455 trivial. 0 not checked.
[2025-05-07 17:36:23,182 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:36:23,182 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1249885418]
[2025-05-07 17:36:23,182 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1249885418] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:36:23,182 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1268372687]
[2025-05-07 17:36:23,182 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-05-07 17:36:23,182 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:36:23,188 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:36:23,190 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:36:23,191 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-05-07 17:36:27,312 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 347 statements into 1 equivalence classes.
[2025-05-07 17:36:27,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 347 of 347 statements.
[2025-05-07 17:36:27,815 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:36:27,815 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:36:27,831 INFO  L256         TraceCheckSpWp]: Trace formula consists of 4744 conjuncts, 90 conjuncts are in the unsatisfiable core
[2025-05-07 17:36:27,839 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:36:28,010 INFO  L134       CoverageAnalysis]: Checked inductivity of 3807 backedges. 0 proven. 1352 refuted. 0 times theorem prover too weak. 2455 trivial. 0 not checked.
[2025-05-07 17:36:28,010 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
