./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-212.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:21,772 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:21,881 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c8850fdd-2248-4329-8b51-641061cc7a8f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:21,886 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:21,886 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:21,919 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:21,921 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:21,921 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:21,922 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:21,922 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:21,923 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:21,924 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:21,925 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:21,925 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:21,925 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:21,925 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:21,925 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:21,926 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:21,926 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:21,926 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:21,926 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:21,926 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:21,927 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:21,927 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:21,927 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:21,928 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:21,928 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:22,305 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:22,317 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:22,320 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:22,323 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:22,323 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:22,324 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c8850fdd-2248-4329-8b51-641061cc7a8f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-212.smt2
[2025-04-28 21:21:22,326 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:22,337 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:22,917 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c8850fdd-2248-4329-8b51-641061cc7a8f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-212.smt2
[2025-04-28 21:21:22,921 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:22,923 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:22,924 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:22,924 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:22,924 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:22,927 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,992 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22 Unit
[2025-04-28 21:21:22,992 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:22,993 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:22,993 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:22,993 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:23,014 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,014 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,068 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,070 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,081 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,084 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,086 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,089 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,091 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,125 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:23,126 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:23,126 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:23,126 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:23,131 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:23,134 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:23,156 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:23,166 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-04-28 21:21:23,168 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:23,184 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:23,185 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:23,185 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:23,185 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_6_0 given in one single declaration
[2025-04-28 21:21:23,185 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_6_0
[2025-04-28 21:21:23,185 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_6_0
[2025-04-28 21:21:23,185 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,185 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_f__59_60_0
[2025-04-28 21:21:23,185 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_f__59_60_0
[2025-04-28 21:21:23,185 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,185 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_f__59_60_0
[2025-04-28 21:21:23,185 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_f__59_60_0
[2025-04-28 21:21:23,185 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,186 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_f__59_60_0
[2025-04-28 21:21:23,186 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_f__59_60_0
[2025-04-28 21:21:23,186 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_try_clause_56f_56_60_0 given in one single declaration
[2025-04-28 21:21:23,186 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_try_clause_56f_56_60_0
[2025-04-28 21:21:23,186 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_try_clause_56f_56_60_0
[2025-04-28 21:21:23,186 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_28_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,186 INFO  L130     BoogieDeclarations]: Found specification of procedure block_28_function_f__59_60_0
[2025-04-28 21:21:23,186 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_28_function_f__59_60_0
[2025-04-28 21:21:23,186 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_try_clause_42f_42_60_0 given in one single declaration
[2025-04-28 21:21:23,186 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_try_clause_42f_42_60_0
[2025-04-28 21:21:23,186 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_try_clause_42f_42_60_0
[2025-04-28 21:21:23,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_return_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,187 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_return_function_f__59_60_0
[2025-04-28 21:21:23,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_return_function_f__59_60_0
[2025-04-28 21:21:23,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_f_58_60_0 given in one single declaration
[2025-04-28 21:21:23,187 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_f_58_60_0
[2025-04-28 21:21:23,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_f_58_60_0
[2025-04-28 21:21:23,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_try_header_f_57_60_0 given in one single declaration
[2025-04-28 21:21:23,187 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_try_header_f_57_60_0
[2025-04-28 21:21:23,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_try_header_f_57_60_0
[2025-04-28 21:21:23,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_f_58_60_0 given in one single declaration
[2025-04-28 21:21:23,187 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_f_58_60_0
[2025-04-28 21:21:23,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_f_58_60_0
[2025-04-28 21:21:23,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,188 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_function_f__59_60_0
[2025-04-28 21:21:23,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_function_f__59_60_0
[2025-04-28 21:21:23,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_call_27_0 given in one single declaration
[2025-04-28 21:21:23,188 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_call_27_0
[2025-04-28 21:21:23,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_call_27_0
[2025-04-28 21:21:23,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_interface_6_C_60_0 given in one single declaration
[2025-04-28 21:21:23,188 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_interface_6_C_60_0
[2025-04-28 21:21:23,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_interface_6_C_60_0
[2025-04-28 21:21:23,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_set__25_60_0 given in one single declaration
[2025-04-28 21:21:23,188 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_function_set__25_60_0 given in one single declaration
[2025-04-28 21:21:23,189 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_8_function_set__25_60_0 given in one single declaration
[2025-04-28 21:21:23,189 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_8_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_8_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_return_function_set__25_60_0 given in one single declaration
[2025-04-28 21:21:23,189 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_return_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_return_function_set__25_60_0
[2025-04-28 21:21:23,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_set_24_60_0 given in one single declaration
[2025-04-28 21:21:23,189 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_set_24_60_0
[2025-04-28 21:21:23,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_set_24_60_0
[2025-04-28 21:21:23,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_set__25_60_0 given in one single declaration
[2025-04-28 21:21:23,190 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_set__25_60_0
[2025-04-28 21:21:23,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_set__25_60_0
[2025-04-28 21:21:23,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_29_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,190 INFO  L130     BoogieDeclarations]: Found specification of procedure block_29_function_f__59_60_0
[2025-04-28 21:21:23,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_29_function_f__59_60_0
[2025-04-28 21:21:23,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_31_function_f__59_60_0 given in one single declaration
[2025-04-28 21:21:23,190 INFO  L130     BoogieDeclarations]: Found specification of procedure block_31_function_f__59_60_0
[2025-04-28 21:21:23,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_31_function_f__59_60_0
[2025-04-28 21:21:23,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_5_C_60_0 given in one single declaration
[2025-04-28 21:21:23,190 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_5_C_60_0
[2025-04-28 21:21:23,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_5_C_60_0
[2025-04-28 21:21:23,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_7_C_60_0 given in one single declaration
[2025-04-28 21:21:23,191 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_7_C_60_0
[2025-04-28 21:21:23,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_7_C_60_0
[2025-04-28 21:21:23,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_35_C_60_0 given in one single declaration
[2025-04-28 21:21:23,191 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_35_C_60_0
[2025-04-28 21:21:23,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_35_C_60_0
[2025-04-28 21:21:23,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_32_C_60_0 given in one single declaration
[2025-04-28 21:21:23,191 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_32_C_60_0
[2025-04-28 21:21:23,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_32_C_60_0
[2025-04-28 21:21:23,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_34_C_60_0 given in one single declaration
[2025-04-28 21:21:23,191 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_34_C_60_0
[2025-04-28 21:21:23,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_34_C_60_0
[2025-04-28 21:21:23,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_33_C_60_0 given in one single declaration
[2025-04-28 21:21:23,191 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_33_C_60_0
[2025-04-28 21:21:23,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_33_C_60_0
[2025-04-28 21:21:23,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:23,192 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:23,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:23,434 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:23,438 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:23,907 INFO  L?                        ?]: Removed 205 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:23,907 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:23,926 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:23,926 INFO  L312             CfgBuilder]: Removed 14 assume(true) statements.
[2025-04-28 21:21:23,927 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:23 BoogieIcfgContainer
[2025-04-28 21:21:23,927 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:23,933 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:23,933 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:23,937 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:23,937 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:22" (1/3) ...
[2025-04-28 21:21:23,938 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5a9b39fa and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:23, skipping insertion in model container
[2025-04-28 21:21:23,938 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (2/3) ...
[2025-04-28 21:21:23,938 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5a9b39fa and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:23, skipping insertion in model container
[2025-04-28 21:21:23,939 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:23" (3/3) ...
[2025-04-28 21:21:23,940 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:23,955 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:23,958 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 30 procedures, 121 locations, 189 edges, 30 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:24,020 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:24,039 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;@7930840e, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:24,040 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:24,045 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 121 states, 50 states have (on average 1.14) internal successors, (57), 57 states have internal predecessors, (57), 41 states have call successors, (44), 29 states have call predecessors, (44), 29 states have return successors, (44), 35 states have call predecessors, (44), 41 states have call successors, (44)
[2025-04-28 21:21:24,061 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:24,062 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,062 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-04-28 21:21:24,064 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,070 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,071 INFO  L85        PathProgramCache]: Analyzing trace with hash 841128328, now seen corresponding path program 1 times
[2025-04-28 21:21:24,079 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,079 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2044711329]
[2025-04-28 21:21:24,079 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,081 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,229 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:24,387 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:24,388 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,388 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,818 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:24,820 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,820 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2044711329]
[2025-04-28 21:21:24,821 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2044711329] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:24,821 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:24,826 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:24,827 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1868415925]
[2025-04-28 21:21:24,829 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,837 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:24,837 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,876 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:24,877 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:24,881 INFO  L87              Difference]: Start difference. First operand  has 121 states, 50 states have (on average 1.14) internal successors, (57), 57 states have internal predecessors, (57), 41 states have call successors, (44), 29 states have call predecessors, (44), 29 states have return successors, (44), 35 states have call predecessors, (44), 41 states have call successors, (44) Second operand  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:25,103 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,104 INFO  L93              Difference]: Finished difference Result 125 states and 151 transitions.
[2025-04-28 21:21:25,109 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:25,111 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16) Word has length 59
[2025-04-28 21:21:25,115 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,132 INFO  L225             Difference]: With dead ends: 125
[2025-04-28 21:21:25,133 INFO  L226             Difference]: Without dead ends: 125
[2025-04-28 21:21:25,142 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:25,145 INFO  L437           NwaCegarLoop]: 140 mSDtfsCounter, 1 mSDsluCounter, 410 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 550 SdHoareTripleChecker+Invalid, 25 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,146 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 550 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:25,191 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-04-28 21:21:25,241 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 123.
[2025-04-28 21:21:25,244 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 123 states, 51 states have (on average 1.1176470588235294) internal successors, (57), 57 states have internal predecessors, (57), 41 states have call successors, (44), 29 states have call predecessors, (44), 31 states have return successors, (48), 36 states have call predecessors, (48), 41 states have call successors, (48)
[2025-04-28 21:21:25,253 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 123 states to 123 states and 149 transitions.
[2025-04-28 21:21:25,257 INFO  L79                 Accepts]: Start accepts. Automaton has 123 states and 149 transitions. Word has length 59
[2025-04-28 21:21:25,258 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,259 INFO  L485      AbstractCegarLoop]: Abstraction has 123 states and 149 transitions.
[2025-04-28 21:21:25,259 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:25,260 INFO  L278                IsEmpty]: Start isEmpty. Operand 123 states and 149 transitions.
[2025-04-28 21:21:25,263 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-04-28 21:21:25,263 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,264 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]
[2025-04-28 21:21:25,264 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:25,264 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,265 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,265 INFO  L85        PathProgramCache]: Analyzing trace with hash -1737234086, now seen corresponding path program 1 times
[2025-04-28 21:21:25,265 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,266 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [493284284]
[2025-04-28 21:21:25,266 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,266 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,317 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-04-28 21:21:25,368 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-04-28 21:21:25,368 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,368 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,630 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:25,631 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,631 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [493284284]
[2025-04-28 21:21:25,631 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [493284284] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:25,631 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:25,631 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:25,631 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [618582729]
[2025-04-28 21:21:25,631 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,632 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:25,632 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,633 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:25,633 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:25,635 INFO  L87              Difference]: Start difference. First operand 123 states and 149 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-04-28 21:21:25,728 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,729 INFO  L93              Difference]: Finished difference Result 127 states and 154 transitions.
[2025-04-28 21:21:25,729 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:25,730 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18) Word has length 66
[2025-04-28 21:21:25,730 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,732 INFO  L225             Difference]: With dead ends: 127
[2025-04-28 21:21:25,732 INFO  L226             Difference]: Without dead ends: 127
[2025-04-28 21:21:25,733 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-04-28 21:21:25,733 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 1 mSDsluCounter, 561 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 705 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,734 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 705 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:25,735 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-04-28 21:21:25,746 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 127.
[2025-04-28 21:21:25,746 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 127 states, 53 states have (on average 1.1132075471698113) internal successors, (59), 59 states have internal predecessors, (59), 41 states have call successors, (44), 29 states have call predecessors, (44), 33 states have return successors, (51), 38 states have call predecessors, (51), 41 states have call successors, (51)
[2025-04-28 21:21:25,748 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 154 transitions.
[2025-04-28 21:21:25,748 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 154 transitions. Word has length 66
[2025-04-28 21:21:25,749 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,750 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 154 transitions.
[2025-04-28 21:21:25,750 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-04-28 21:21:25,750 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 154 transitions.
[2025-04-28 21:21:25,755 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:25,755 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,755 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-04-28 21:21:25,755 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:25,755 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,756 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,756 INFO  L85        PathProgramCache]: Analyzing trace with hash -1177540155, now seen corresponding path program 1 times
[2025-04-28 21:21:25,756 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,756 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1838007223]
[2025-04-28 21:21:25,756 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,756 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,804 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:25,842 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:25,842 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,842 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,069 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:26,069 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,069 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1838007223]
[2025-04-28 21:21:26,069 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1838007223] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,069 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,069 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:26,070 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2049015971]
[2025-04-28 21:21:26,070 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,070 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:26,070 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,071 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:26,071 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:26,071 INFO  L87              Difference]: Start difference. First operand 127 states and 154 transitions. Second operand  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:26,177 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,177 INFO  L93              Difference]: Finished difference Result 131 states and 159 transitions.
[2025-04-28 21:21:26,178 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:26,179 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16) Word has length 59
[2025-04-28 21:21:26,179 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,181 INFO  L225             Difference]: With dead ends: 131
[2025-04-28 21:21:26,181 INFO  L226             Difference]: Without dead ends: 131
[2025-04-28 21:21:26,181 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-04-28 21:21:26,186 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 1 mSDsluCounter, 561 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 705 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,187 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 705 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:26,188 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 131 states.
[2025-04-28 21:21:26,207 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 131 to 127.
[2025-04-28 21:21:26,207 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 127 states, 53 states have (on average 1.1132075471698113) internal successors, (59), 59 states have internal predecessors, (59), 41 states have call successors, (44), 29 states have call predecessors, (44), 33 states have return successors, (51), 38 states have call predecessors, (51), 41 states have call successors, (51)
[2025-04-28 21:21:26,211 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 127 states to 127 states and 154 transitions.
[2025-04-28 21:21:26,211 INFO  L79                 Accepts]: Start accepts. Automaton has 127 states and 154 transitions. Word has length 59
[2025-04-28 21:21:26,212 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,212 INFO  L485      AbstractCegarLoop]: Abstraction has 127 states and 154 transitions.
[2025-04-28 21:21:26,212 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:26,212 INFO  L278                IsEmpty]: Start isEmpty. Operand 127 states and 154 transitions.
[2025-04-28 21:21:26,218 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:26,218 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,218 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-04-28 21:21:26,218 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:26,218 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,219 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,219 INFO  L85        PathProgramCache]: Analyzing trace with hash -540599485, now seen corresponding path program 1 times
[2025-04-28 21:21:26,219 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,219 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1943568377]
[2025-04-28 21:21:26,219 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,219 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,261 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:26,266 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:26,266 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,266 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,453 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:26,453 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,454 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1943568377]
[2025-04-28 21:21:26,454 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1943568377] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,454 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,454 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:26,454 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1712805342]
[2025-04-28 21:21:26,454 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,454 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:26,454 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,455 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:26,455 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:26,455 INFO  L87              Difference]: Start difference. First operand 127 states and 154 transitions. 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-04-28 21:21:26,482 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,482 INFO  L93              Difference]: Finished difference Result 131 states and 159 transitions.
[2025-04-28 21:21:26,486 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:26,486 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-04-28 21:21:26,488 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,490 INFO  L225             Difference]: With dead ends: 131
[2025-04-28 21:21:26,490 INFO  L226             Difference]: Without dead ends: 127
[2025-04-28 21:21:26,490 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-04-28 21:21:26,495 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 1 mSDsluCounter, 279 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 422 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-04-28 21:21:26,495 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 422 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:26,496 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-04-28 21:21:26,512 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 125.
[2025-04-28 21:21:26,512 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 53 states have (on average 1.0943396226415094) internal successors, (58), 58 states have internal predecessors, (58), 39 states have call successors, (42), 29 states have call predecessors, (42), 33 states have return successors, (49), 37 states have call predecessors, (49), 39 states have call successors, (49)
[2025-04-28 21:21:26,514 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 149 transitions.
[2025-04-28 21:21:26,514 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 149 transitions. Word has length 59
[2025-04-28 21:21:26,514 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,514 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 149 transitions.
[2025-04-28 21:21:26,514 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-04-28 21:21:26,517 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 149 transitions.
[2025-04-28 21:21:26,519 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:26,519 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,519 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-04-28 21:21:26,519 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:26,520 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,520 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,520 INFO  L85        PathProgramCache]: Analyzing trace with hash 484147007, now seen corresponding path program 1 times
[2025-04-28 21:21:26,520 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,520 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1436186639]
[2025-04-28 21:21:26,522 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,522 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,569 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:26,600 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:26,601 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,601 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,919 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:26,919 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,919 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1436186639]
[2025-04-28 21:21:26,919 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1436186639] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,919 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,920 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:26,920 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [143936237]
[2025-04-28 21:21:26,920 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,920 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:26,920 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,921 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:26,921 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:26,921 INFO  L87              Difference]: Start difference. First operand 125 states and 149 transitions. Second operand  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 4 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:27,017 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,017 INFO  L93              Difference]: Finished difference Result 123 states and 146 transitions.
[2025-04-28 21:21:27,018 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:27,018 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 4 states have call predecessors, (16), 3 states have call successors, (16) Word has length 59
[2025-04-28 21:21:27,018 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,022 INFO  L225             Difference]: With dead ends: 123
[2025-04-28 21:21:27,023 INFO  L226             Difference]: Without dead ends: 121
[2025-04-28 21:21:27,024 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:27,025 INFO  L437           NwaCegarLoop]: 130 mSDtfsCounter, 0 mSDsluCounter, 378 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 508 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,025 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 508 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,030 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-04-28 21:21:27,045 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 121.
[2025-04-28 21:21:27,046 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 121 states, 51 states have (on average 1.0980392156862746) internal successors, (56), 56 states have internal predecessors, (56), 38 states have call successors, (40), 28 states have call predecessors, (40), 32 states have return successors, (47), 36 states have call predecessors, (47), 38 states have call successors, (47)
[2025-04-28 21:21:27,049 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 121 states to 121 states and 143 transitions.
[2025-04-28 21:21:27,051 INFO  L79                 Accepts]: Start accepts. Automaton has 121 states and 143 transitions. Word has length 59
[2025-04-28 21:21:27,051 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,051 INFO  L485      AbstractCegarLoop]: Abstraction has 121 states and 143 transitions.
[2025-04-28 21:21:27,051 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.75) internal successors, (27), 5 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 4 states have return successors, (16), 4 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:27,051 INFO  L278                IsEmpty]: Start isEmpty. Operand 121 states and 143 transitions.
[2025-04-28 21:21:27,053 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-04-28 21:21:27,053 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,053 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]
[2025-04-28 21:21:27,053 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:27,053 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,054 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,054 INFO  L85        PathProgramCache]: Analyzing trace with hash 1344648804, now seen corresponding path program 1 times
[2025-04-28 21:21:27,054 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,054 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1296894061]
[2025-04-28 21:21:27,054 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,054 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,088 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-04-28 21:21:27,108 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-04-28 21:21:27,108 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,108 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,471 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:27,471 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,472 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1296894061]
[2025-04-28 21:21:27,472 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1296894061] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,472 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,472 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:27,472 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [674849429]
[2025-04-28 21:21:27,472 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,472 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:27,472 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,473 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:27,473 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:27,474 INFO  L87              Difference]: Start difference. First operand 121 states and 143 transitions. Second operand  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17)
[2025-04-28 21:21:27,743 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,744 INFO  L93              Difference]: Finished difference Result 129 states and 152 transitions.
[2025-04-28 21:21:27,744 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:27,745 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17) Word has length 62
[2025-04-28 21:21:27,745 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,748 INFO  L225             Difference]: With dead ends: 129
[2025-04-28 21:21:27,748 INFO  L226             Difference]: Without dead ends: 129
[2025-04-28 21:21:27,748 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=109, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:27,750 INFO  L437           NwaCegarLoop]: 126 mSDtfsCounter, 2 mSDsluCounter, 1107 mSDsCounter, 0 mSdLazyCounter, 120 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1233 SdHoareTripleChecker+Invalid, 120 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 120 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,751 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1233 Invalid, 120 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 120 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:27,752 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-04-28 21:21:27,766 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 125.
[2025-04-28 21:21:27,766 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 53 states have (on average 1.0943396226415094) internal successors, (58), 58 states have internal predecessors, (58), 38 states have call successors, (40), 28 states have call predecessors, (40), 34 states have return successors, (49), 38 states have call predecessors, (49), 38 states have call successors, (49)
[2025-04-28 21:21:27,767 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 147 transitions.
[2025-04-28 21:21:27,768 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 147 transitions. Word has length 62
[2025-04-28 21:21:27,768 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,768 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 147 transitions.
[2025-04-28 21:21:27,768 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17)
[2025-04-28 21:21:27,768 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 147 transitions.
[2025-04-28 21:21:27,772 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:21:27,773 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,773 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,773 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:27,773 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,774 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,775 INFO  L85        PathProgramCache]: Analyzing trace with hash -1287233090, now seen corresponding path program 1 times
[2025-04-28 21:21:27,775 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,775 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1744188514]
[2025-04-28 21:21:27,775 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,776 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,814 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:27,847 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:27,848 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,848 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,100 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:28,100 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,102 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1744188514]
[2025-04-28 21:21:28,102 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1744188514] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,102 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,102 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:28,102 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1536859100]
[2025-04-28 21:21:28,102 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,103 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:28,103 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,104 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:28,104 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,105 INFO  L87              Difference]: Start difference. First operand 125 states and 147 transitions. Second operand  has 9 states, 7 states have (on average 4.428571428571429) internal successors, (31), 9 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 7 states have return successors, (19), 8 states have call predecessors, (19), 4 states have call successors, (19)
[2025-04-28 21:21:28,275 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,276 INFO  L93              Difference]: Finished difference Result 129 states and 152 transitions.
[2025-04-28 21:21:28,276 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:28,277 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 4.428571428571429) internal successors, (31), 9 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 7 states have return successors, (19), 8 states have call predecessors, (19), 4 states have call successors, (19) Word has length 69
[2025-04-28 21:21:28,277 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,278 INFO  L225             Difference]: With dead ends: 129
[2025-04-28 21:21:28,280 INFO  L226             Difference]: Without dead ends: 129
[2025-04-28 21:21:28,280 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:28,281 INFO  L437           NwaCegarLoop]: 134 mSDtfsCounter, 2 mSDsluCounter, 911 mSDsCounter, 0 mSdLazyCounter, 64 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1045 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 64 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,281 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1045 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 64 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:28,282 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-04-28 21:21:28,296 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 121.
[2025-04-28 21:21:28,297 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 121 states, 51 states have (on average 1.0980392156862746) internal successors, (56), 56 states have internal predecessors, (56), 38 states have call successors, (40), 28 states have call predecessors, (40), 32 states have return successors, (47), 36 states have call predecessors, (47), 38 states have call successors, (47)
[2025-04-28 21:21:28,298 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 121 states to 121 states and 143 transitions.
[2025-04-28 21:21:28,298 INFO  L79                 Accepts]: Start accepts. Automaton has 121 states and 143 transitions. Word has length 69
[2025-04-28 21:21:28,298 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,299 INFO  L485      AbstractCegarLoop]: Abstraction has 121 states and 143 transitions.
[2025-04-28 21:21:28,301 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 4.428571428571429) internal successors, (31), 9 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 7 states have return successors, (19), 8 states have call predecessors, (19), 4 states have call successors, (19)
[2025-04-28 21:21:28,301 INFO  L278                IsEmpty]: Start isEmpty. Operand 121 states and 143 transitions.
[2025-04-28 21:21:28,302 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 85
[2025-04-28 21:21:28,303 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,303 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,303 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:28,303 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,304 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,304 INFO  L85        PathProgramCache]: Analyzing trace with hash 1845188990, now seen corresponding path program 1 times
[2025-04-28 21:21:28,304 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,304 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [108691402]
[2025-04-28 21:21:28,304 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,305 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,361 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 84 statements into 1 equivalence classes.
[2025-04-28 21:21:28,388 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 84 of 84 statements.
[2025-04-28 21:21:28,388 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,388 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,709 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:28,710 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,711 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [108691402]
[2025-04-28 21:21:28,711 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [108691402] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,711 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,711 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:28,711 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [482925817]
[2025-04-28 21:21:28,711 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,712 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:28,712 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,713 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:28,714 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,714 INFO  L87              Difference]: Start difference. First operand 121 states and 143 transitions. Second operand  has 9 states, 8 states have (on average 4.75) internal successors, (38), 9 states have internal predecessors, (38), 6 states have call successors, (23), 1 states have call predecessors, (23), 8 states have return successors, (23), 8 states have call predecessors, (23), 6 states have call successors, (23)
[2025-04-28 21:21:28,893 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,893 INFO  L93              Difference]: Finished difference Result 125 states and 149 transitions.
[2025-04-28 21:21:28,893 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:28,894 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 4.75) internal successors, (38), 9 states have internal predecessors, (38), 6 states have call successors, (23), 1 states have call predecessors, (23), 8 states have return successors, (23), 8 states have call predecessors, (23), 6 states have call successors, (23) Word has length 84
[2025-04-28 21:21:28,894 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,895 INFO  L225             Difference]: With dead ends: 125
[2025-04-28 21:21:28,897 INFO  L226             Difference]: Without dead ends: 125
[2025-04-28 21:21:28,897 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,899 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 1 mSDsluCounter, 840 mSDsCounter, 0 mSdLazyCounter, 91 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 964 SdHoareTripleChecker+Invalid, 92 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 91 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,900 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 964 Invalid, 92 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 91 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:28,901 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-04-28 21:21:28,913 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 121.
[2025-04-28 21:21:28,915 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 121 states, 51 states have (on average 1.0980392156862746) internal successors, (56), 56 states have internal predecessors, (56), 38 states have call successors, (40), 28 states have call predecessors, (40), 32 states have return successors, (47), 37 states have call predecessors, (47), 38 states have call successors, (47)
[2025-04-28 21:21:28,919 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 121 states to 121 states and 143 transitions.
[2025-04-28 21:21:28,919 INFO  L79                 Accepts]: Start accepts. Automaton has 121 states and 143 transitions. Word has length 84
[2025-04-28 21:21:28,919 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,919 INFO  L485      AbstractCegarLoop]: Abstraction has 121 states and 143 transitions.
[2025-04-28 21:21:28,920 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 4.75) internal successors, (38), 9 states have internal predecessors, (38), 6 states have call successors, (23), 1 states have call predecessors, (23), 8 states have return successors, (23), 8 states have call predecessors, (23), 6 states have call successors, (23)
[2025-04-28 21:21:28,920 INFO  L278                IsEmpty]: Start isEmpty. Operand 121 states and 143 transitions.
[2025-04-28 21:21:28,921 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 100
[2025-04-28 21:21:28,921 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,921 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:28,925 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:28,925 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,926 INFO  L85        PathProgramCache]: Analyzing trace with hash -417369158, now seen corresponding path program 1 times
[2025-04-28 21:21:28,926 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,926 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2123779018]
[2025-04-28 21:21:28,926 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,926 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,984 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 99 statements into 1 equivalence classes.
[2025-04-28 21:21:29,012 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 99 of 99 statements.
[2025-04-28 21:21:29,012 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,012 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,306 INFO  L134       CoverageAnalysis]: Checked inductivity of 32 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 26 trivial. 0 not checked.
[2025-04-28 21:21:29,307 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,307 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2123779018]
[2025-04-28 21:21:29,307 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2123779018] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,307 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,307 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:29,307 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [814619722]
[2025-04-28 21:21:29,308 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,308 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:29,309 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,309 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:29,310 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,310 INFO  L87              Difference]: Start difference. First operand 121 states and 143 transitions. Second operand  has 8 states, 7 states have (on average 4.857142857142857) internal successors, (34), 8 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (23), 8 states have call predecessors, (23), 4 states have call successors, (23)
[2025-04-28 21:21:29,449 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,449 INFO  L93              Difference]: Finished difference Result 138 states and 168 transitions.
[2025-04-28 21:21:29,450 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:29,451 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 4.857142857142857) internal successors, (34), 8 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (23), 8 states have call predecessors, (23), 4 states have call successors, (23) Word has length 99
[2025-04-28 21:21:29,451 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,452 INFO  L225             Difference]: With dead ends: 138
[2025-04-28 21:21:29,453 INFO  L226             Difference]: Without dead ends: 138
[2025-04-28 21:21:29,453 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,454 INFO  L437           NwaCegarLoop]: 130 mSDtfsCounter, 1 mSDsluCounter, 760 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 890 SdHoareTripleChecker+Invalid, 70 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,455 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 890 Invalid, 70 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,456 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-04-28 21:21:29,467 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 130.
[2025-04-28 21:21:29,468 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 55 states have (on average 1.0909090909090908) internal successors, (60), 60 states have internal predecessors, (60), 39 states have call successors, (41), 28 states have call predecessors, (41), 36 states have return successors, (56), 42 states have call predecessors, (56), 39 states have call successors, (56)
[2025-04-28 21:21:29,469 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 157 transitions.
[2025-04-28 21:21:29,470 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 157 transitions. Word has length 99
[2025-04-28 21:21:29,470 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,471 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 157 transitions.
[2025-04-28 21:21:29,471 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 4.857142857142857) internal successors, (34), 8 states have internal predecessors, (34), 4 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (23), 8 states have call predecessors, (23), 4 states have call successors, (23)
[2025-04-28 21:21:29,472 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 157 transitions.
[2025-04-28 21:21:29,473 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-04-28 21:21:29,473 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,475 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 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]
[2025-04-28 21:21:29,475 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:29,475 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,476 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,476 INFO  L85        PathProgramCache]: Analyzing trace with hash 2131089987, now seen corresponding path program 1 times
[2025-04-28 21:21:29,476 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,476 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [81064107]
[2025-04-28 21:21:29,476 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,476 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,521 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:29,543 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:29,543 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,543 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,811 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:29,811 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,811 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [81064107]
[2025-04-28 21:21:29,812 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [81064107] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,812 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,812 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:29,812 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1695401753]
[2025-04-28 21:21:29,813 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,813 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:29,813 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,814 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:29,814 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,814 INFO  L87              Difference]: Start difference. First operand 130 states and 157 transitions. Second operand  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 4 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (21), 8 states have call predecessors, (21), 4 states have call successors, (21)
[2025-04-28 21:21:29,932 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,932 INFO  L93              Difference]: Finished difference Result 143 states and 176 transitions.
[2025-04-28 21:21:29,933 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:29,933 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 4 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (21), 8 states have call predecessors, (21), 4 states have call successors, (21) Word has length 92
[2025-04-28 21:21:29,934 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,935 INFO  L225             Difference]: With dead ends: 143
[2025-04-28 21:21:29,936 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:21:29,936 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,936 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 778 mSDsCounter, 0 mSdLazyCounter, 70 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 911 SdHoareTripleChecker+Invalid, 70 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 70 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,937 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 911 Invalid, 70 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 70 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,937 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:21:29,944 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 130.
[2025-04-28 21:21:29,944 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 55 states have (on average 1.0909090909090908) internal successors, (60), 60 states have internal predecessors, (60), 39 states have call successors, (41), 28 states have call predecessors, (41), 36 states have return successors, (56), 42 states have call predecessors, (56), 39 states have call successors, (56)
[2025-04-28 21:21:29,945 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 157 transitions.
[2025-04-28 21:21:29,946 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 157 transitions. Word has length 92
[2025-04-28 21:21:29,946 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,946 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 157 transitions.
[2025-04-28 21:21:29,946 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 4 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (21), 8 states have call predecessors, (21), 4 states have call successors, (21)
[2025-04-28 21:21:29,946 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 157 transitions.
[2025-04-28 21:21:29,948 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 103
[2025-04-28 21:21:29,948 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,948 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:29,948 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:29,948 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,949 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,949 INFO  L85        PathProgramCache]: Analyzing trace with hash 1822708010, now seen corresponding path program 1 times
[2025-04-28 21:21:29,949 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,949 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [96272247]
[2025-04-28 21:21:29,949 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,949 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,995 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 102 statements into 1 equivalence classes.
[2025-04-28 21:21:30,018 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 102 of 102 statements.
[2025-04-28 21:21:30,018 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,018 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,339 INFO  L134       CoverageAnalysis]: Checked inductivity of 32 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-04-28 21:21:30,340 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,340 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [96272247]
[2025-04-28 21:21:30,340 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [96272247] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,340 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,340 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:30,340 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1209572765]
[2025-04-28 21:21:30,340 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,341 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:30,341 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,341 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:30,342 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:30,342 INFO  L87              Difference]: Start difference. First operand 130 states and 157 transitions. Second operand  has 11 states, 9 states have (on average 4.111111111111111) internal successors, (37), 11 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (25), 9 states have call predecessors, (25), 5 states have call successors, (25)
[2025-04-28 21:21:30,664 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,664 INFO  L93              Difference]: Finished difference Result 172 states and 228 transitions.
[2025-04-28 21:21:30,665 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:30,665 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 9 states have (on average 4.111111111111111) internal successors, (37), 11 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (25), 9 states have call predecessors, (25), 5 states have call successors, (25) Word has length 102
[2025-04-28 21:21:30,666 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,667 INFO  L225             Difference]: With dead ends: 172
[2025-04-28 21:21:30,668 INFO  L226             Difference]: Without dead ends: 170
[2025-04-28 21:21:30,668 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=109, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:30,668 INFO  L437           NwaCegarLoop]: 152 mSDtfsCounter, 7 mSDsluCounter, 1297 mSDsCounter, 0 mSdLazyCounter, 218 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 1449 SdHoareTripleChecker+Invalid, 227 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 218 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,669 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 1449 Invalid, 227 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 218 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:30,669 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 170 states.
[2025-04-28 21:21:30,684 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 170 to 161.
[2025-04-28 21:21:30,684 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 161 states, 67 states have (on average 1.1194029850746268) internal successors, (75), 73 states have internal predecessors, (75), 49 states have call successors, (53), 34 states have call predecessors, (53), 45 states have return successors, (82), 54 states have call predecessors, (82), 49 states have call successors, (82)
[2025-04-28 21:21:30,686 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 210 transitions.
[2025-04-28 21:21:30,686 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 210 transitions. Word has length 102
[2025-04-28 21:21:30,687 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,688 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 210 transitions.
[2025-04-28 21:21:30,688 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 9 states have (on average 4.111111111111111) internal successors, (37), 11 states have internal predecessors, (37), 5 states have call successors, (23), 1 states have call predecessors, (23), 9 states have return successors, (25), 9 states have call predecessors, (25), 5 states have call successors, (25)
[2025-04-28 21:21:30,688 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 210 transitions.
[2025-04-28 21:21:30,690 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 96
[2025-04-28 21:21:30,691 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,691 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 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, 1]
[2025-04-28 21:21:30,692 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:30,692 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,692 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,692 INFO  L85        PathProgramCache]: Analyzing trace with hash 1111249264, now seen corresponding path program 1 times
[2025-04-28 21:21:30,692 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,692 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1908883457]
[2025-04-28 21:21:30,693 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,693 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,739 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 95 statements into 1 equivalence classes.
[2025-04-28 21:21:30,761 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 95 of 95 statements.
[2025-04-28 21:21:30,761 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,761 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,152 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 6 proven. 5 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:31,152 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,152 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1908883457]
[2025-04-28 21:21:31,153 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1908883457] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,153 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1566312406]
[2025-04-28 21:21:31,153 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,153 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,155 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,160 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,162 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,559 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 95 statements into 1 equivalence classes.
[2025-04-28 21:21:31,816 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 95 of 95 statements.
[2025-04-28 21:21:31,816 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,816 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,824 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1309 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,839 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,986 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:31,987 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,759 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:38,760 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1566312406] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,760 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,760 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 13] total 16
[2025-04-28 21:21:38,760 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [229313095]
[2025-04-28 21:21:38,760 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,761 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:38,761 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,762 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:38,762 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=32, Invalid=208, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:38,762 INFO  L87              Difference]: Start difference. First operand 161 states and 210 transitions. Second operand  has 16 states, 11 states have (on average 3.909090909090909) internal successors, (43), 16 states have internal predecessors, (43), 9 states have call successors, (30), 1 states have call predecessors, (30), 11 states have return successors, (32), 13 states have call predecessors, (32), 9 states have call successors, (32)
[2025-04-28 21:21:39,044 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,044 INFO  L93              Difference]: Finished difference Result 162 states and 212 transitions.
[2025-04-28 21:21:39,045 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:39,045 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 11 states have (on average 3.909090909090909) internal successors, (43), 16 states have internal predecessors, (43), 9 states have call successors, (30), 1 states have call predecessors, (30), 11 states have return successors, (32), 13 states have call predecessors, (32), 9 states have call successors, (32) Word has length 95
[2025-04-28 21:21:39,045 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,045 INFO  L225             Difference]: With dead ends: 162
[2025-04-28 21:21:39,045 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:39,046 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 203 GetRequests, 177 SyntacticMatches, 11 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=37, Invalid=235, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:39,046 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 2 mSDsluCounter, 1483 mSDsCounter, 0 mSdLazyCounter, 239 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1600 SdHoareTripleChecker+Invalid, 240 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 239 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,046 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1600 Invalid, 240 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 239 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:39,047 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:39,047 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:39,047 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:39,047 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:39,047 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 95
[2025-04-28 21:21:39,047 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,047 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:39,048 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 11 states have (on average 3.909090909090909) internal successors, (43), 16 states have internal predecessors, (43), 9 states have call successors, (30), 1 states have call predecessors, (30), 11 states have return successors, (32), 13 states have call predecessors, (32), 9 states have call successors, (32)
[2025-04-28 21:21:39,048 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:39,048 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:39,050 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:39,056 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:39,251 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:39,255 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,257 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:39,261 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:39 BoogieIcfgContainer
[2025-04-28 21:21:39,261 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:39,262 INFO  L158              Benchmark]: Toolchain (without parser) took 16338.99ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 146.1MB in the beginning and 267.4MB in the end (delta: -121.4MB). Peak memory consumption was 18.2MB. Max. memory is 33.6GB.
[2025-04-28 21:21:39,262 INFO  L158              Benchmark]: SmtParser took 0.47ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:39,262 INFO  L158              Benchmark]: ChcToBoogie took 69.06ms. Allocated memory is still 234.9MB. Free memory was 146.1MB in the beginning and 142.8MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:39,262 INFO  L158              Benchmark]: Boogie Preprocessor took 132.53ms. Allocated memory is still 234.9MB. Free memory was 142.8MB in the beginning and 139.5MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:39,268 INFO  L158              Benchmark]: RCFGBuilder took 800.79ms. Allocated memory is still 234.9MB. Free memory was 139.5MB in the beginning and 97.4MB in the end (delta: 42.1MB). Peak memory consumption was 50.3MB. Max. memory is 33.6GB.
[2025-04-28 21:21:39,269 INFO  L158              Benchmark]: TraceAbstraction took 15328.08ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 96.8MB in the beginning and 267.4MB in the end (delta: -170.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:39,270 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.47ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 69.06ms. Allocated memory is still 234.9MB. Free memory was 146.1MB in the beginning and 142.8MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 132.53ms. Allocated memory is still 234.9MB. Free memory was 142.8MB in the beginning and 139.5MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 800.79ms. Allocated memory is still 234.9MB. Free memory was 139.5MB in the beginning and 97.4MB in the end (delta: 42.1MB). Peak memory consumption was 50.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 15328.08ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 96.8MB in the beginning and 267.4MB in the end (delta: -170.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 30 procedures, 121 locations, 189 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 15.3s, OverallIterations: 12, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.1s, AutomataDifference: 2.2s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 47 SdHoareTripleChecker+Valid, 1.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 20 mSDsluCounter, 10982 SdHoareTripleChecker+Invalid, 1.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 9365 mSDsCounter, 12 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 972 IncrementalHoareTripleChecker+Invalid, 984 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 12 mSolverCounterUnsat, 1617 mSDtfsCounter, 972 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 292 GetRequests, 203 SyntacticMatches, 11 SemanticMatches, 78 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.8s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=161occurred in iteration=11, InterpolantAutomatonStates: 97, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 12 MinimizatonAttempts, 54 StatesRemovedByMinimization, 9 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.3s SsaConstructionTime, 0.7s SatisfiabilityAnalysisTime, 10.6s InterpolantComputationTime, 1000 NumberOfCodeBlocks, 1000 NumberOfCodeBlocksAsserted, 13 NumberOfCheckSat, 1081 ConstructedInterpolants, 0 QuantifiedInterpolants, 1510 SizeOfPredicates, 3 NumberOfNonLiveVariables, 1309 ConjunctsInSsa, 15 ConjunctsInUnsatCore, 14 InterpolantComputations, 11 PerfectInterpolantSequences, 144/159 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:39,289 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
