./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/blockchain_state/this_does_not_change_internal_call.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:41,540 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:41,593 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_760023ff-ab3a-4798-9c3e-5d0605e205ba/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:41,596 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:41,597 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:41,614 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:41,614 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:41,614 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:41,614 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:41,615 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:41,615 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:41,615 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:41,615 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:41,615 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:41,615 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:41,615 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:41,615 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:41,616 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:41,616 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:41,617 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:41,617 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:41,834 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:41,839 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:41,841 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:41,842 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:41,842 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:41,843 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_760023ff-ab3a-4798-9c3e-5d0605e205ba/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/blockchain_state/this_does_not_change_internal_call.sol_0_no_adts_000.smt2
[2025-05-07 17:27:41,844 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:41,846 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:42,104 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_760023ff-ab3a-4798-9c3e-5d0605e205ba/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/blockchain_state/this_does_not_change_internal_call.sol_0_no_adts_000.smt2
[2025-05-07 17:27:42,106 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:42,107 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:42,107 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:42,107 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:42,108 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:42,110 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,147 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42 Unit
[2025-05-07 17:27:42,147 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:42,148 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:42,148 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:42,148 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:42,160 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,160 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,188 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,188 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,195 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,196 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,198 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,201 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,202 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,215 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:42,216 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:42,216 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:42,216 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:42,217 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,219 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:42,231 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:42,243 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:27:42,246 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:27:42,253 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:42,253 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:42,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:42,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_3_0 given in one single declaration
[2025-05-07 17:27:42,254 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_3_0
[2025-05-07 17:27:42,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_3_0
[2025-05-07 17:27:42,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_f__24_46_0 given in one single declaration
[2025-05-07 17:27:42,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_f__24_46_0
[2025-05-07 17:27:42,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_f__24_46_0
[2025-05-07 17:27:42,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_f__24_46_0 given in one single declaration
[2025-05-07 17:27:42,254 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_f__24_46_0
[2025-05-07 17:27:42,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_f__24_46_0
[2025-05-07 17:27:42,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__24_46_0 given in one single declaration
[2025-05-07 17:27:42,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__24_46_0
[2025-05-07 17:27:42,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__24_46_0
[2025-05-07 17:27:42,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_g__45_46_0 given in one single declaration
[2025-05-07 17:27:42,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_g__45_46_0
[2025-05-07 17:27:42,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_g__45_46_0
[2025-05-07 17:27:42,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_g__45_46_0 given in one single declaration
[2025-05-07 17:27:42,254 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_return_function_g__45_46_0 given in one single declaration
[2025-05-07 17:27:42,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_return_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_return_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_g_44_46_0 given in one single declaration
[2025-05-07 17:27:42,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_g_44_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_g_44_46_0
[2025-05-07 17:27:42,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_g__45_46_0 given in one single declaration
[2025-05-07 17:27:42,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_g__45_46_0 given in one single declaration
[2025-05-07 17:27:42,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_g__45_46_0 given in one single declaration
[2025-05-07 17:27:42,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_g__45_46_0
[2025-05-07 17:27:42,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_23_46_0 given in one single declaration
[2025-05-07 17:27:42,255 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_23_46_0
[2025-05-07 17:27:42,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_23_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__24_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__24_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__24_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__24_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__24_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__24_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_20_C_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_20_C_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_20_C_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_constructor_13_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_constructor_13_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_constructor_13_46_0
[2025-05-07 17:27:42,256 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_return_constructor_13_46_0 given in one single declaration
[2025-05-07 17:27:42,256 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_return_constructor_13_46_0
[2025-05-07 17:27:42,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_return_constructor_13_46_0
[2025-05-07 17:27:42,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18__12_46_0 given in one single declaration
[2025-05-07 17:27:42,257 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18__12_46_0
[2025-05-07 17:27:42,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18__12_46_0
[2025-05-07 17:27:42,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_constructor_13_46_0 given in one single declaration
[2025-05-07 17:27:42,257 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_constructor_13_46_0
[2025-05-07 17:27:42,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_constructor_13_46_0
[2025-05-07 17:27:42,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_22_C_46_0 given in one single declaration
[2025-05-07 17:27:42,257 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_22_C_46_0
[2025-05-07 17:27:42,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_22_C_46_0
[2025-05-07 17:27:42,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_21_C_46_0 given in one single declaration
[2025-05-07 17:27:42,257 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_21_C_46_0
[2025-05-07 17:27:42,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_21_C_46_0
[2025-05-07 17:27:42,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_23_C_46_0 given in one single declaration
[2025-05-07 17:27:42,257 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_23_C_46_0
[2025-05-07 17:27:42,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_23_C_46_0
[2025-05-07 17:27:42,257 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:42,257 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:42,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:42,391 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:42,394 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:42,593 INFO  L?                        ?]: Removed 184 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:42,593 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:42,602 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:42,602 INFO  L312             CfgBuilder]: Removed 12 assume(true) statements.
[2025-05-07 17:27:42,603 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:42 BoogieIcfgContainer
[2025-05-07 17:27:42,603 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:42,604 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:42,604 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:42,607 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:42,607 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:42" (1/3) ...
[2025-05-07 17:27:42,607 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7b392939 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:42, skipping insertion in model container
[2025-05-07 17:27:42,607 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (2/3) ...
[2025-05-07 17:27:42,608 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7b392939 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:42, skipping insertion in model container
[2025-05-07 17:27:42,608 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:42" (3/3) ...
[2025-05-07 17:27:42,609 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:42,619 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:42,621 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 26 procedures, 102 locations, 152 edges, 26 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:42,650 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:42,658 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;@3cb7ca7f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:42,658 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:42,660 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 102 states, 43 states have (on average 1.0930232558139534) internal successors, (47), 47 states have internal predecessors, (47), 33 states have call successors, (35), 25 states have call predecessors, (35), 25 states have return successors, (35), 29 states have call predecessors, (35), 33 states have call successors, (35)
[2025-05-07 17:27:42,667 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:27:42,667 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:42,668 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:42,668 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:42,671 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:42,671 INFO  L85        PathProgramCache]: Analyzing trace with hash -756324580, now seen corresponding path program 1 times
[2025-05-07 17:27:42,676 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:42,676 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [36715870]
[2025-05-07 17:27:42,676 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:42,677 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:42,729 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:27:42,809 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:27:42,810 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:42,810 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:43,099 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:43,100 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:43,100 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [36715870]
[2025-05-07 17:27:43,100 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [36715870] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:43,100 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:43,102 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:27:43,103 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1020651860]
[2025-05-07 17:27:43,104 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:43,107 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:27:43,107 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:43,130 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:27:43,130 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:27:43,133 INFO  L87              Difference]: Start difference. First operand  has 102 states, 43 states have (on average 1.0930232558139534) internal successors, (47), 47 states have internal predecessors, (47), 33 states have call successors, (35), 25 states have call predecessors, (35), 25 states have return successors, (35), 29 states have call predecessors, (35), 33 states have call successors, (35) Second operand  has 8 states, 6 states have (on average 6.0) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 7 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:27:43,271 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:43,271 INFO  L93              Difference]: Finished difference Result 106 states and 121 transitions.
[2025-05-07 17:27:43,272 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:27:43,273 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 6.0) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 7 states have call predecessors, (22), 5 states have call successors, (22) Word has length 80
[2025-05-07 17:27:43,274 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:43,282 INFO  L225             Difference]: With dead ends: 106
[2025-05-07 17:27:43,282 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:27:43,284 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:27:43,287 INFO  L437           NwaCegarLoop]: 113 mSDtfsCounter, 2 mSDsluCounter, 656 mSDsCounter, 0 mSdLazyCounter, 55 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 769 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 55 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:43,287 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 769 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 55 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:43,301 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:27:43,321 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 104.
[2025-05-07 17:27:43,322 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 104 states, 44 states have (on average 1.0681818181818181) internal successors, (47), 47 states have internal predecessors, (47), 33 states have call successors, (35), 25 states have call predecessors, (35), 27 states have return successors, (37), 31 states have call predecessors, (37), 33 states have call successors, (37)
[2025-05-07 17:27:43,325 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 104 states to 104 states and 119 transitions.
[2025-05-07 17:27:43,326 INFO  L79                 Accepts]: Start accepts. Automaton has 104 states and 119 transitions. Word has length 80
[2025-05-07 17:27:43,326 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:43,326 INFO  L485      AbstractCegarLoop]: Abstraction has 104 states and 119 transitions.
[2025-05-07 17:27:43,327 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 6.0) internal successors, (36), 8 states have internal predecessors, (36), 5 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 7 states have call predecessors, (22), 5 states have call successors, (22)
[2025-05-07 17:27:43,327 INFO  L278                IsEmpty]: Start isEmpty. Operand 104 states and 119 transitions.
[2025-05-07 17:27:43,328 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:27:43,329 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:43,329 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:43,329 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:43,329 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:43,329 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:43,330 INFO  L85        PathProgramCache]: Analyzing trace with hash 273137230, now seen corresponding path program 1 times
[2025-05-07 17:27:43,330 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:43,330 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1916870693]
[2025-05-07 17:27:43,330 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:43,330 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:43,372 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:27:43,378 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:27:43,378 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:43,379 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:43,475 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:43,475 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:43,475 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1916870693]
[2025-05-07 17:27:43,475 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1916870693] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:43,475 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:43,475 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:43,476 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1858561665]
[2025-05-07 17:27:43,476 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:43,476 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:43,477 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:43,477 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:43,477 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:43,477 INFO  L87              Difference]: Start difference. First operand 104 states and 119 transitions. Second operand  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:43,492 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:43,492 INFO  L93              Difference]: Finished difference Result 106 states and 120 transitions.
[2025-05-07 17:27:43,492 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:43,493 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22) Word has length 80
[2025-05-07 17:27:43,493 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:43,494 INFO  L225             Difference]: With dead ends: 106
[2025-05-07 17:27:43,494 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:27:43,495 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:43,495 INFO  L437           NwaCegarLoop]: 116 mSDtfsCounter, 1 mSDsluCounter, 220 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 336 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:43,496 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 336 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:43,496 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:27:43,504 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:27:43,504 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 44 states have (on average 1.0454545454545454) internal successors, (46), 46 states have internal predecessors, (46), 31 states have call successors, (33), 25 states have call predecessors, (33), 27 states have return successors, (35), 30 states have call predecessors, (35), 31 states have call successors, (35)
[2025-05-07 17:27:43,505 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 114 transitions.
[2025-05-07 17:27:43,506 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 114 transitions. Word has length 80
[2025-05-07 17:27:43,506 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:43,506 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 114 transitions.
[2025-05-07 17:27:43,506 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.0) internal successors, (36), 4 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 3 states have return successors, (22), 3 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:43,506 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 114 transitions.
[2025-05-07 17:27:43,508 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:27:43,508 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:43,508 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:43,509 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:43,509 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:43,509 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:43,509 INFO  L85        PathProgramCache]: Analyzing trace with hash -118273500, now seen corresponding path program 1 times
[2025-05-07 17:27:43,509 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:43,509 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1193351225]
[2025-05-07 17:27:43,509 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:43,510 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:43,538 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:27:43,565 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:27:43,565 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:43,565 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,241 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:44,241 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,241 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1193351225]
[2025-05-07 17:27:44,241 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1193351225] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,241 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,241 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [19] imperfect sequences [] total 19
[2025-05-07 17:27:44,241 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1141050806]
[2025-05-07 17:27:44,241 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,242 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-05-07 17:27:44,242 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,242 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-05-07 17:27:44,242 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=36, Invalid=306, Unknown=0, NotChecked=0, Total=342
[2025-05-07 17:27:44,242 INFO  L87              Difference]: Start difference. First operand 102 states and 114 transitions. Second operand  has 19 states, 14 states have (on average 2.5714285714285716) internal successors, (36), 17 states have internal predecessors, (36), 10 states have call successors, (22), 1 states have call predecessors, (22), 14 states have return successors, (22), 16 states have call predecessors, (22), 10 states have call successors, (22)
[2025-05-07 17:27:44,624 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,624 INFO  L93              Difference]: Finished difference Result 118 states and 135 transitions.
[2025-05-07 17:27:44,625 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-05-07 17:27:44,625 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 14 states have (on average 2.5714285714285716) internal successors, (36), 17 states have internal predecessors, (36), 10 states have call successors, (22), 1 states have call predecessors, (22), 14 states have return successors, (22), 16 states have call predecessors, (22), 10 states have call successors, (22) Word has length 80
[2025-05-07 17:27:44,625 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,627 INFO  L225             Difference]: With dead ends: 118
[2025-05-07 17:27:44,627 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:27:44,627 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 22 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-05-07 17:27:44,628 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 7 mSDsluCounter, 1549 mSDsCounter, 0 mSdLazyCounter, 374 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 1643 SdHoareTripleChecker+Invalid, 380 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 374 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:44,628 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 1643 Invalid, 380 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 374 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:27:44,629 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:27:44,638 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 114.
[2025-05-07 17:27:44,639 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 114 states, 49 states have (on average 1.0408163265306123) internal successors, (51), 51 states have internal predecessors, (51), 33 states have call successors, (35), 25 states have call predecessors, (35), 32 states have return successors, (45), 37 states have call predecessors, (45), 33 states have call successors, (45)
[2025-05-07 17:27:44,640 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 131 transitions.
[2025-05-07 17:27:44,640 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 131 transitions. Word has length 80
[2025-05-07 17:27:44,640 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,640 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 131 transitions.
[2025-05-07 17:27:44,641 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 14 states have (on average 2.5714285714285716) internal successors, (36), 17 states have internal predecessors, (36), 10 states have call successors, (22), 1 states have call predecessors, (22), 14 states have return successors, (22), 16 states have call predecessors, (22), 10 states have call successors, (22)
[2025-05-07 17:27:44,641 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 131 transitions.
[2025-05-07 17:27:44,642 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-05-07 17:27:44,642 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,642 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:44,642 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:44,643 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,643 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,643 INFO  L85        PathProgramCache]: Analyzing trace with hash -1450833582, now seen corresponding path program 1 times
[2025-05-07 17:27:44,643 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,643 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1378497751]
[2025-05-07 17:27:44,644 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,644 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,682 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-05-07 17:27:44,700 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-05-07 17:27:44,700 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,700 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,819 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:44,819 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,819 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1378497751]
[2025-05-07 17:27:44,820 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1378497751] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,820 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,820 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:27:44,820 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [234488068]
[2025-05-07 17:27:44,820 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,820 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:27:44,820 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,821 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:27:44,821 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:27:44,821 INFO  L87              Difference]: Start difference. First operand 114 states and 131 transitions. Second operand  has 8 states, 7 states have (on average 5.142857142857143) internal successors, (36), 8 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (22), 8 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:44,885 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,885 INFO  L93              Difference]: Finished difference Result 119 states and 137 transitions.
[2025-05-07 17:27:44,886 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:27:44,886 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 5.142857142857143) internal successors, (36), 8 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (22), 8 states have call predecessors, (22), 4 states have call successors, (22) Word has length 80
[2025-05-07 17:27:44,886 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,888 INFO  L225             Difference]: With dead ends: 119
[2025-05-07 17:27:44,888 INFO  L226             Difference]: Without dead ends: 119
[2025-05-07 17:27:44,888 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:27:44,889 INFO  L437           NwaCegarLoop]: 111 mSDtfsCounter, 1 mSDsluCounter, 648 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 759 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:44,889 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 759 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:44,890 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 119 states.
[2025-05-07 17:27:44,898 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 119 to 119.
[2025-05-07 17:27:44,898 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 119 states, 51 states have (on average 1.0392156862745099) internal successors, (53), 53 states have internal predecessors, (53), 34 states have call successors, (36), 25 states have call predecessors, (36), 34 states have return successors, (48), 40 states have call predecessors, (48), 34 states have call successors, (48)
[2025-05-07 17:27:44,900 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 119 states to 119 states and 137 transitions.
[2025-05-07 17:27:44,900 INFO  L79                 Accepts]: Start accepts. Automaton has 119 states and 137 transitions. Word has length 80
[2025-05-07 17:27:44,900 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,900 INFO  L485      AbstractCegarLoop]: Abstraction has 119 states and 137 transitions.
[2025-05-07 17:27:44,900 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 5.142857142857143) internal successors, (36), 8 states have internal predecessors, (36), 4 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (22), 8 states have call predecessors, (22), 4 states have call successors, (22)
[2025-05-07 17:27:44,900 INFO  L278                IsEmpty]: Start isEmpty. Operand 119 states and 137 transitions.
[2025-05-07 17:27:44,902 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:27:44,902 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,902 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:44,902 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:44,903 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,903 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,903 INFO  L85        PathProgramCache]: Analyzing trace with hash 2136743167, now seen corresponding path program 1 times
[2025-05-07 17:27:44,903 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,903 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [822497222]
[2025-05-07 17:27:44,903 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,903 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,935 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:27:44,939 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:27:44,939 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,939 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,985 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:44,985 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,985 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [822497222]
[2025-05-07 17:27:44,985 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [822497222] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,985 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,985 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:44,985 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1792255632]
[2025-05-07 17:27:44,985 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,986 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:44,986 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,987 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:44,987 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:44,987 INFO  L87              Difference]: Start difference. First operand 119 states and 137 transitions. Second operand  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:27:45,000 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,000 INFO  L93              Difference]: Finished difference Result 121 states and 138 transitions.
[2025-05-07 17:27:45,001 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:45,001 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 4 states have call successors, (23) Word has length 83
[2025-05-07 17:27:45,002 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,002 INFO  L225             Difference]: With dead ends: 121
[2025-05-07 17:27:45,002 INFO  L226             Difference]: Without dead ends: 117
[2025-05-07 17:27:45,003 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:45,003 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 209 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 319 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:45,004 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 319 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:45,004 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-05-07 17:27:45,011 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 117.
[2025-05-07 17:27:45,011 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 51 states have (on average 1.0196078431372548) internal successors, (52), 52 states have internal predecessors, (52), 32 states have call successors, (34), 25 states have call predecessors, (34), 34 states have return successors, (46), 39 states have call predecessors, (46), 32 states have call successors, (46)
[2025-05-07 17:27:45,012 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 132 transitions.
[2025-05-07 17:27:45,012 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 132 transitions. Word has length 83
[2025-05-07 17:27:45,013 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,013 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 132 transitions.
[2025-05-07 17:27:45,013 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:27:45,013 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 132 transitions.
[2025-05-07 17:27:45,014 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:27:45,014 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,014 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:45,014 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:45,015 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:45,015 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:45,015 INFO  L85        PathProgramCache]: Analyzing trace with hash 2113217915, now seen corresponding path program 1 times
[2025-05-07 17:27:45,015 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:45,015 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [460666819]
[2025-05-07 17:27:45,015 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,015 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:45,040 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:27:45,050 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:27:45,050 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,050 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,131 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:45,132 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:45,132 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [460666819]
[2025-05-07 17:27:45,132 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [460666819] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:45,132 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:45,132 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:45,132 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [976144310]
[2025-05-07 17:27:45,132 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:45,132 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:45,132 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:45,133 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:45,133 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:45,133 INFO  L87              Difference]: Start difference. First operand 117 states and 132 transitions. Second operand  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:27:45,163 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,163 INFO  L93              Difference]: Finished difference Result 117 states and 130 transitions.
[2025-05-07 17:27:45,164 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:45,164 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23) Word has length 83
[2025-05-07 17:27:45,164 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,165 INFO  L225             Difference]: With dead ends: 117
[2025-05-07 17:27:45,165 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:27:45,165 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:45,166 INFO  L437           NwaCegarLoop]: 108 mSDtfsCounter, 1 mSDsluCounter, 416 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 524 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:45,166 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 524 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:45,167 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:27:45,171 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 111.
[2025-05-07 17:27:45,172 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 111 states, 49 states have (on average 1.0204081632653061) internal successors, (50), 50 states have internal predecessors, (50), 30 states have call successors, (32), 25 states have call predecessors, (32), 32 states have return successors, (40), 35 states have call predecessors, (40), 30 states have call successors, (40)
[2025-05-07 17:27:45,173 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 122 transitions.
[2025-05-07 17:27:45,173 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 122 transitions. Word has length 83
[2025-05-07 17:27:45,173 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,173 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 122 transitions.
[2025-05-07 17:27:45,173 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 4 states have call successors, (23)
[2025-05-07 17:27:45,173 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 122 transitions.
[2025-05-07 17:27:45,175 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 120
[2025-05-07 17:27:45,175 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,175 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:45,175 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:45,175 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:45,175 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:45,176 INFO  L85        PathProgramCache]: Analyzing trace with hash 1273294880, now seen corresponding path program 1 times
[2025-05-07 17:27:45,176 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:45,176 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1173512475]
[2025-05-07 17:27:45,176 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,176 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:45,219 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:27:45,239 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:27:45,239 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,311 INFO  L134       CoverageAnalysis]: Checked inductivity of 33 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 24 trivial. 0 not checked.
[2025-05-07 17:27:45,311 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:45,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1173512475]
[2025-05-07 17:27:45,311 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1173512475] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:45,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [446859425]
[2025-05-07 17:27:45,311 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,311 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:45,313 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:45,315 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:27:45,316 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:27:45,583 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:27:45,760 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:27:45,760 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,760 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,766 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1658 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:45,777 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:45,822 INFO  L134       CoverageAnalysis]: Checked inductivity of 33 backedges. 32 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:27:45,822 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:27:45,822 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [446859425] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:45,822 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:27:45,822 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [5] total 5
[2025-05-07 17:27:45,822 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [930343848]
[2025-05-07 17:27:45,822 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:45,822 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:27:45,822 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:45,823 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:27:45,823 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:45,823 INFO  L87              Difference]: Start difference. First operand 111 states and 122 transitions. Second operand  has 5 states, 4 states have (on average 13.25) internal successors, (53), 5 states have internal predecessors, (53), 5 states have call successors, (33), 2 states have call predecessors, (33), 4 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:27:45,846 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,846 INFO  L93              Difference]: Finished difference Result 116 states and 126 transitions.
[2025-05-07 17:27:45,846 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:45,846 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 13.25) internal successors, (53), 5 states have internal predecessors, (53), 5 states have call successors, (33), 2 states have call predecessors, (33), 4 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33) Word has length 119
[2025-05-07 17:27:45,847 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,847 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:45,847 INFO  L226             Difference]: Without dead ends: 111
[2025-05-07 17:27:45,848 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 123 GetRequests, 119 SyntacticMatches, 1 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:45,848 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 1 mSDsluCounter, 298 mSDsCounter, 0 mSdLazyCounter, 10 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 401 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 10 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:45,848 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 401 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 10 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:45,849 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 111 states.
[2025-05-07 17:27:45,852 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 111 to 107.
[2025-05-07 17:27:45,853 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 47 states have (on average 1.0212765957446808) internal successors, (48), 48 states have internal predecessors, (48), 30 states have call successors, (32), 25 states have call predecessors, (32), 30 states have return successors, (36), 33 states have call predecessors, (36), 30 states have call successors, (36)
[2025-05-07 17:27:45,854 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 116 transitions.
[2025-05-07 17:27:45,854 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 116 transitions. Word has length 119
[2025-05-07 17:27:45,854 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,854 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 116 transitions.
[2025-05-07 17:27:45,854 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 13.25) internal successors, (53), 5 states have internal predecessors, (53), 5 states have call successors, (33), 2 states have call predecessors, (33), 4 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:27:45,854 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 116 transitions.
[2025-05-07 17:27:45,855 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:27:45,856 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,856 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:45,863 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:27:46,057 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-05-07 17:27:46,058 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:46,059 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:46,060 INFO  L85        PathProgramCache]: Analyzing trace with hash -1582367133, now seen corresponding path program 1 times
[2025-05-07 17:27:46,060 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:46,060 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [789790082]
[2025-05-07 17:27:46,061 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:46,061 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:46,207 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:27:46,224 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:27:46,224 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:46,224 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:46,314 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 2 proven. 9 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-05-07 17:27:46,315 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:46,315 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [789790082]
[2025-05-07 17:27:46,315 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [789790082] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:46,315 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [325715370]
[2025-05-07 17:27:46,315 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:46,315 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:46,317 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:46,319 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:27:46,320 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:27:46,576 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:27:46,761 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:27:46,761 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:46,761 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:46,768 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1705 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:46,774 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:46,800 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 23 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:27:46,800 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:27:46,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [325715370] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:46,801 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:27:46,801 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 6
[2025-05-07 17:27:46,801 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [40847851]
[2025-05-07 17:27:46,801 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:46,801 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:46,801 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:46,802 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:46,802 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:46,802 INFO  L87              Difference]: Start difference. First operand 107 states and 116 transitions. Second operand  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:27:46,833 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:46,833 INFO  L93              Difference]: Finished difference Result 111 states and 119 transitions.
[2025-05-07 17:27:46,834 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:46,834 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33) Word has length 122
[2025-05-07 17:27:46,834 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:46,835 INFO  L225             Difference]: With dead ends: 111
[2025-05-07 17:27:46,835 INFO  L226             Difference]: Without dead ends: 103
[2025-05-07 17:27:46,835 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 127 GetRequests, 123 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:46,836 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 1 mSDsluCounter, 397 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 499 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:46,836 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 499 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:46,836 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 103 states.
[2025-05-07 17:27:46,840 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 103 to 103.
[2025-05-07 17:27:46,840 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 103 states, 45 states have (on average 1.0222222222222221) internal successors, (46), 46 states have internal predecessors, (46), 29 states have call successors, (30), 24 states have call predecessors, (30), 29 states have return successors, (34), 32 states have call predecessors, (34), 29 states have call successors, (34)
[2025-05-07 17:27:46,841 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 103 states to 103 states and 110 transitions.
[2025-05-07 17:27:46,841 INFO  L79                 Accepts]: Start accepts. Automaton has 103 states and 110 transitions. Word has length 122
[2025-05-07 17:27:46,841 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:46,841 INFO  L485      AbstractCegarLoop]: Abstraction has 103 states and 110 transitions.
[2025-05-07 17:27:46,841 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 4 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 6 states have call predecessors, (33), 4 states have call successors, (33)
[2025-05-07 17:27:46,841 INFO  L278                IsEmpty]: Start isEmpty. Operand 103 states and 110 transitions.
[2025-05-07 17:27:46,842 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-05-07 17:27:46,842 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:46,843 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:46,849 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:27:47,043 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:47,044 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:47,045 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:47,045 INFO  L85        PathProgramCache]: Analyzing trace with hash -20246183, now seen corresponding path program 1 times
[2025-05-07 17:27:47,045 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:47,045 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1790587538]
[2025-05-07 17:27:47,045 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:47,046 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:47,181 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:27:47,216 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:27:47,217 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:47,217 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:47,995 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 7 proven. 5 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-05-07 17:27:47,995 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:47,995 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1790587538]
[2025-05-07 17:27:47,995 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1790587538] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:47,995 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1855435307]
[2025-05-07 17:27:47,995 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:47,996 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:47,998 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:48,000 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:27:48,000 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:27:48,229 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-05-07 17:27:48,374 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-05-07 17:27:48,374 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:48,374 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:48,381 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1704 conjuncts, 98 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:48,385 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:48,488 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 7 proven. 5 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-05-07 17:27:48,488 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:27:50,445 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 7 proven. 6 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-05-07 17:27:50,445 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1855435307] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:27:50,445 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:27:50,445 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [23, 23, 24] total 30
[2025-05-07 17:27:50,446 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [100253504]
[2025-05-07 17:27:50,446 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:27:50,446 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-05-07 17:27:50,446 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:50,447 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-05-07 17:27:50,447 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=74, Invalid=796, Unknown=0, NotChecked=0, Total=870
[2025-05-07 17:27:50,447 INFO  L87              Difference]: Start difference. First operand 103 states and 110 transitions. Second operand  has 30 states, 18 states have (on average 2.888888888888889) internal successors, (52), 25 states have internal predecessors, (52), 19 states have call successors, (37), 1 states have call predecessors, (37), 18 states have return successors, (42), 23 states have call predecessors, (42), 19 states have call successors, (42)
[2025-05-07 17:27:50,742 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:50,742 INFO  L93              Difference]: Finished difference Result 97 states and 104 transitions.
[2025-05-07 17:27:50,742 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-05-07 17:27:50,742 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 18 states have (on average 2.888888888888889) internal successors, (52), 25 states have internal predecessors, (52), 19 states have call successors, (37), 1 states have call predecessors, (37), 18 states have return successors, (42), 23 states have call predecessors, (42), 19 states have call successors, (42) Word has length 122
[2025-05-07 17:27:50,743 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:50,743 INFO  L225             Difference]: With dead ends: 97
[2025-05-07 17:27:50,743 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:50,743 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 274 GetRequests, 241 SyntacticMatches, 0 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 45 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=109, Invalid=1081, Unknown=0, NotChecked=0, Total=1190
[2025-05-07 17:27:50,744 INFO  L437           NwaCegarLoop]: 77 mSDtfsCounter, 6 mSDsluCounter, 1630 mSDsCounter, 0 mSdLazyCounter, 426 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1707 SdHoareTripleChecker+Invalid, 434 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 426 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:50,744 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1707 Invalid, 434 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 426 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:27:50,745 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:50,745 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:50,745 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:27:50,745 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:50,745 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 122
[2025-05-07 17:27:50,745 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:50,745 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:50,745 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 18 states have (on average 2.888888888888889) internal successors, (52), 25 states have internal predecessors, (52), 19 states have call successors, (37), 1 states have call predecessors, (37), 18 states have return successors, (42), 23 states have call predecessors, (42), 19 states have call successors, (42)
[2025-05-07 17:27:50,745 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:50,746 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:50,748 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:50,753 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:27:50,949 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:50,960 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:50,968 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:50,979 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:50 BoogieIcfgContainer
[2025-05-07 17:27:50,979 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:50,981 INFO  L158              Benchmark]: Toolchain (without parser) took 8872.89ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 151.4MB in the beginning and 135.1MB in the end (delta: 16.2MB). Peak memory consumption was 53.2MB. Max. memory is 33.6GB.
[2025-05-07 17:27:50,981 INFO  L158              Benchmark]: SmtParser took 0.20ms. Allocated memory is still 234.9MB. Free memory is still 173.0MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:50,982 INFO  L158              Benchmark]: ChcToBoogie took 40.25ms. Allocated memory is still 234.9MB. Free memory was 151.4MB in the beginning and 148.6MB in the end (delta: 2.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:50,982 INFO  L158              Benchmark]: Boogie Preprocessor took 67.45ms. Allocated memory is still 234.9MB. Free memory was 148.6MB in the beginning and 145.4MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:50,983 INFO  L158              Benchmark]: RCFGBuilder took 386.83ms. Allocated memory is still 234.9MB. Free memory was 145.4MB in the beginning and 184.6MB in the end (delta: -39.2MB). Peak memory consumption was 42.4MB. Max. memory is 33.6GB.
[2025-05-07 17:27:50,983 INFO  L158              Benchmark]: TraceAbstraction took 8375.06ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 184.1MB in the beginning and 135.1MB in the end (delta: 48.9MB). Peak memory consumption was 94.7MB. Max. memory is 33.6GB.
[2025-05-07 17:27:50,985 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.20ms. Allocated memory is still 234.9MB. Free memory is still 173.0MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 40.25ms. Allocated memory is still 234.9MB. Free memory was 151.4MB in the beginning and 148.6MB in the end (delta: 2.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 67.45ms. Allocated memory is still 234.9MB. Free memory was 148.6MB in the beginning and 145.4MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 386.83ms. Allocated memory is still 234.9MB. Free memory was 145.4MB in the beginning and 184.6MB in the end (delta: -39.2MB). Peak memory consumption was 42.4MB. Max. memory is 33.6GB.
 * TraceAbstraction took 8375.06ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 184.1MB in the beginning and 135.1MB in the end (delta: 48.9MB). Peak memory consumption was 94.7MB. 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 26 procedures, 102 locations, 152 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 8.3s, OverallIterations: 9, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 42 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 21 mSDsluCounter, 6957 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 6023 mSDsCounter, 16 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 955 IncrementalHoareTripleChecker+Invalid, 971 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 16 mSolverCounterUnsat, 934 mSDtfsCounter, 955 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 577 GetRequests, 495 SyntacticMatches, 1 SemanticMatches, 81 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 54 ImplicationChecksByTransitivity, 0.6s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=119occurred in iteration=4, InterpolantAutomatonStates: 84, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 9 MinimizatonAttempts, 15 StatesRemovedByMinimization, 4 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.4s SsaConstructionTime, 0.7s SatisfiabilityAnalysisTime, 4.4s InterpolantComputationTime, 1212 NumberOfCodeBlocks, 1212 NumberOfCodeBlocksAsserted, 12 NumberOfCheckSat, 1321 ConstructedInterpolants, 0 QuantifiedInterpolants, 1965 SizeOfPredicates, 21 NumberOfNonLiveVariables, 5067 ConjunctsInSsa, 107 ConjunctsInUnsatCore, 13 InterpolantComputations, 8 PerfectInterpolantSequences, 189/221 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:27:51,002 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
