./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/natspec/safe_assert_false_positive_pure.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:19,119 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:19,156 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_55e36cd0-0a2e-47e7-b6b8-819bff4b7a73/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:19,159 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:19,160 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:19,172 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:19,173 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:19,173 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:19,173 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:19,173 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:19,173 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:19,173 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:19,174 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:19,174 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:19,174 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:19,174 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:19,175 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:19,175 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:19,363 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:19,369 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:19,370 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:19,371 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:19,372 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:19,372 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_55e36cd0-0a2e-47e7-b6b8-819bff4b7a73/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/natspec/safe_assert_false_positive_pure.sol_0_no_adts_000.smt2
[2025-05-07 17:27:19,373 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:19,375 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:19,620 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_55e36cd0-0a2e-47e7-b6b8-819bff4b7a73/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/natspec/safe_assert_false_positive_pure.sol_0_no_adts_000.smt2
[2025-05-07 17:27:19,623 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:19,624 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:19,624 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:19,624 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:19,624 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:19,626 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,657 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19 Unit
[2025-05-07 17:27:19,657 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:19,658 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:19,658 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:19,658 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:19,669 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,670 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,694 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,694 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,700 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,701 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,703 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,705 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,706 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,718 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:19,719 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:19,719 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:19,719 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:19,720 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (1/1) ...
[2025-05-07 17:27:19,722 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:19,732 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:19,741 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:19,744 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:19,755 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:19,755 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:19,755 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:19,755 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_6_0 given in one single declaration
[2025-05-07 17:27:19,755 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_6_0
[2025-05-07 17:27:19,755 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_6_0
[2025-05-07 17:27:19,755 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_68_0 given in one single declaration
[2025-05-07 17:27:19,755 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_68_0
[2025-05-07 17:27:19,755 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_68_0
[2025-05-07 17:27:19,756 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_68_0 given in one single declaration
[2025-05-07 17:27:19,756 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_68_0
[2025-05-07 17:27:19,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_68_0
[2025-05-07 17:27:19,756 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_21_C_68_0 given in one single declaration
[2025-05-07 17:27:19,756 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_21_C_68_0
[2025-05-07 17:27:19,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_21_C_68_0
[2025-05-07 17:27:19,756 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_23_C_68_0 given in one single declaration
[2025-05-07 17:27:19,756 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_23_C_68_0
[2025-05-07 17:27:19,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_23_C_68_0
[2025-05-07 17:27:19,756 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_22_C_68_0 given in one single declaration
[2025-05-07 17:27:19,756 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_22_C_68_0
[2025-05-07 17:27:19,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_22_C_68_0
[2025-05-07 17:27:19,757 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_24_C_68_0 given in one single declaration
[2025-05-07 17:27:19,757 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_24_C_68_0
[2025-05-07 17:27:19,757 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_24_C_68_0
[2025-05-07 17:27:19,757 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,757 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_g__46_68_0
[2025-05-07 17:27:19,757 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_g__46_68_0
[2025-05-07 17:27:19,757 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,757 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_g__46_68_0
[2025-05-07 17:27:19,757 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_g__46_68_0
[2025-05-07 17:27:19,757 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,757 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_g__46_68_0
[2025-05-07 17:27:19,757 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_g__46_68_0
[2025-05-07 17:27:19,757 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,758 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,758 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,758 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,758 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_g__46_68_0
[2025-05-07 17:27:19,758 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:27:19,758 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:27:19,759 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_return_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:27:19,759 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_return_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_return_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_f2_66_68_0 given in one single declaration
[2025-05-07 17:27:19,759 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_f2_66_68_0
[2025-05-07 17:27:19,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_f2_66_68_0
[2025-05-07 17:27:19,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:27:19,759 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_f2__67_68_0
[2025-05-07 17:27:19,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_g_45_68_0 given in one single declaration
[2025-05-07 17:27:19,760 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_g_45_68_0
[2025-05-07 17:27:19,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_g_45_68_0
[2025-05-07 17:27:19,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,760 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_g__46_68_0
[2025-05-07 17:27:19,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_g__46_68_0
[2025-05-07 17:27:19,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_f1__57_68_0 given in one single declaration
[2025-05-07 17:27:19,760 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_f1__57_68_0
[2025-05-07 17:27:19,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_f1__57_68_0
[2025-05-07 17:27:19,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_f1__57_68_0 given in one single declaration
[2025-05-07 17:27:19,760 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_f1__57_68_0
[2025-05-07 17:27:19,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_f1__57_68_0
[2025-05-07 17:27:19,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_g__46_68_0 given in one single declaration
[2025-05-07 17:27:19,760 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_g__46_68_0
[2025-05-07 17:27:19,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_g__46_68_0
[2025-05-07 17:27:19,761 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:19,761 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:19,761 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:19,931 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:19,934 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:20,201 INFO  L?                        ?]: Removed 244 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:20,201 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:20,211 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:20,211 INFO  L312             CfgBuilder]: Removed 14 assume(true) statements.
[2025-05-07 17:27:20,212 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:20 BoogieIcfgContainer
[2025-05-07 17:27:20,212 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:20,214 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:20,214 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:20,217 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:20,217 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:19" (1/3) ...
[2025-05-07 17:27:20,218 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@374f33b1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:20, skipping insertion in model container
[2025-05-07 17:27:20,218 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:19" (2/3) ...
[2025-05-07 17:27:20,218 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@374f33b1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:20, skipping insertion in model container
[2025-05-07 17:27:20,218 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:20" (3/3) ...
[2025-05-07 17:27:20,219 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:20,230 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:20,232 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 26 procedures, 109 locations, 179 edges, 26 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:20,269 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:20,281 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;@402df6c4, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:20,281 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:20,285 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 109 states, 43 states have (on average 1.0930232558139534) internal successors, (47), 47 states have internal predecessors, (47), 40 states have call successors, (44), 25 states have call predecessors, (44), 25 states have return successors, (44), 36 states have call predecessors, (44), 40 states have call successors, (44)
[2025-05-07 17:27:20,295 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-05-07 17:27:20,295 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:20,296 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]
[2025-05-07 17:27:20,296 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:20,300 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:20,300 INFO  L85        PathProgramCache]: Analyzing trace with hash -849430167, now seen corresponding path program 1 times
[2025-05-07 17:27:20,306 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:20,307 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [13049931]
[2025-05-07 17:27:20,307 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:20,307 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:20,360 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-05-07 17:27:20,424 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-05-07 17:27:20,424 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:20,424 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:20,606 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:20,606 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:20,607 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [13049931]
[2025-05-07 17:27:20,607 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [13049931] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:20,607 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:20,609 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:20,611 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1019916014]
[2025-05-07 17:27:20,611 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:20,614 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:20,615 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:20,656 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:20,657 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:20,659 INFO  L87              Difference]: Start difference. First operand  has 109 states, 43 states have (on average 1.0930232558139534) internal successors, (47), 47 states have internal predecessors, (47), 40 states have call successors, (44), 25 states have call predecessors, (44), 25 states have return successors, (44), 36 states have call predecessors, (44), 40 states have call successors, (44) Second operand  has 4 states, 3 states have (on average 8.333333333333334) internal successors, (25), 4 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 3 states have return successors, (15), 3 states have call predecessors, (15), 3 states have call successors, (15)
[2025-05-07 17:27:20,702 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:20,703 INFO  L93              Difference]: Finished difference Result 111 states and 137 transitions.
[2025-05-07 17:27:20,705 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:20,706 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.333333333333334) internal successors, (25), 4 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 3 states have return successors, (15), 3 states have call predecessors, (15), 3 states have call successors, (15) Word has length 55
[2025-05-07 17:27:20,707 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:20,716 INFO  L225             Difference]: With dead ends: 111
[2025-05-07 17:27:20,716 INFO  L226             Difference]: Without dead ends: 107
[2025-05-07 17:27:20,718 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:20,722 INFO  L437           NwaCegarLoop]: 134 mSDtfsCounter, 1 mSDsluCounter, 260 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 394 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:20,723 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 394 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:20,737 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-05-07 17:27:20,761 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 105.
[2025-05-07 17:27:20,762 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 42 states have (on average 1.0476190476190477) internal successors, (44), 44 states have internal predecessors, (44), 38 states have call successors, (42), 25 states have call predecessors, (42), 25 states have return successors, (42), 35 states have call predecessors, (42), 38 states have call successors, (42)
[2025-05-07 17:27:20,767 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 128 transitions.
[2025-05-07 17:27:20,768 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 128 transitions. Word has length 55
[2025-05-07 17:27:20,769 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:20,769 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 128 transitions.
[2025-05-07 17:27:20,769 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.333333333333334) internal successors, (25), 4 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 3 states have return successors, (15), 3 states have call predecessors, (15), 3 states have call successors, (15)
[2025-05-07 17:27:20,769 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 128 transitions.
[2025-05-07 17:27:20,771 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-05-07 17:27:20,771 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:20,771 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]
[2025-05-07 17:27:20,771 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:20,771 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:20,772 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:20,772 INFO  L85        PathProgramCache]: Analyzing trace with hash -1937637659, now seen corresponding path program 1 times
[2025-05-07 17:27:20,772 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:20,772 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [309239621]
[2025-05-07 17:27:20,772 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:20,772 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:20,806 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-05-07 17:27:20,826 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-05-07 17:27:20,826 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:20,826 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:20,918 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:20,918 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:20,918 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [309239621]
[2025-05-07 17:27:20,918 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [309239621] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:20,918 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:20,918 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:27:20,918 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2125478242]
[2025-05-07 17:27:20,919 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:20,920 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:27:20,920 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:20,920 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:27:20,920 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:20,921 INFO  L87              Difference]: Start difference. First operand 105 states and 128 transitions. Second operand  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 3 states have call successors, (15)
[2025-05-07 17:27:21,017 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:21,017 INFO  L93              Difference]: Finished difference Result 107 states and 129 transitions.
[2025-05-07 17:27:21,018 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:21,018 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 3 states have call successors, (15) Word has length 55
[2025-05-07 17:27:21,018 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:21,019 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:27:21,019 INFO  L226             Difference]: Without dead ends: 105
[2025-05-07 17:27:21,019 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:27:21,020 INFO  L437           NwaCegarLoop]: 121 mSDtfsCounter, 1 mSDsluCounter, 345 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 466 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:21,020 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 466 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:21,021 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 105 states.
[2025-05-07 17:27:21,025 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 105 to 103.
[2025-05-07 17:27:21,025 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 103 states, 42 states have (on average 1.0238095238095237) internal successors, (43), 43 states have internal predecessors, (43), 36 states have call successors, (40), 25 states have call predecessors, (40), 25 states have return successors, (40), 34 states have call predecessors, (40), 36 states have call successors, (40)
[2025-05-07 17:27:21,026 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 103 states to 103 states and 123 transitions.
[2025-05-07 17:27:21,026 INFO  L79                 Accepts]: Start accepts. Automaton has 103 states and 123 transitions. Word has length 55
[2025-05-07 17:27:21,027 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:21,027 INFO  L485      AbstractCegarLoop]: Abstraction has 103 states and 123 transitions.
[2025-05-07 17:27:21,027 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 3 states have call successors, (15)
[2025-05-07 17:27:21,027 INFO  L278                IsEmpty]: Start isEmpty. Operand 103 states and 123 transitions.
[2025-05-07 17:27:21,028 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:27:21,028 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,028 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]
[2025-05-07 17:27:21,028 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:21,028 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,029 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,029 INFO  L85        PathProgramCache]: Analyzing trace with hash -1589732742, now seen corresponding path program 1 times
[2025-05-07 17:27:21,029 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,029 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [600467898]
[2025-05-07 17:27:21,029 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,029 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,056 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:27:21,067 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:27:21,067 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,068 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:21,412 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:21,412 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:21,412 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [600467898]
[2025-05-07 17:27:21,412 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [600467898] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:21,412 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:21,413 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [] total 16
[2025-05-07 17:27:21,413 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1688550946]
[2025-05-07 17:27:21,413 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:21,413 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:27:21,413 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:21,414 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:27:21,414 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=211, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:27:21,414 INFO  L87              Difference]: Start difference. First operand 103 states and 123 transitions. Second operand  has 16 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 14 states have internal predecessors, (26), 7 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (16), 13 states have call predecessors, (16), 7 states have call successors, (16)
[2025-05-07 17:27:21,732 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:21,733 INFO  L93              Difference]: Finished difference Result 113 states and 137 transitions.
[2025-05-07 17:27:21,733 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:27:21,733 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 14 states have internal predecessors, (26), 7 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (16), 13 states have call predecessors, (16), 7 states have call successors, (16) Word has length 58
[2025-05-07 17:27:21,733 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:21,734 INFO  L225             Difference]: With dead ends: 113
[2025-05-07 17:27:21,734 INFO  L226             Difference]: Without dead ends: 113
[2025-05-07 17:27:21,734 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-05-07 17:27:21,735 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 5 mSDsluCounter, 1523 mSDsCounter, 0 mSdLazyCounter, 282 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1635 SdHoareTripleChecker+Invalid, 283 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 282 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:21,735 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1635 Invalid, 283 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 282 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:27:21,736 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-05-07 17:27:21,742 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 111.
[2025-05-07 17:27:21,742 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 111 states, 45 states have (on average 1.0222222222222221) internal successors, (46), 46 states have internal predecessors, (46), 38 states have call successors, (42), 25 states have call predecessors, (42), 28 states have return successors, (47), 39 states have call predecessors, (47), 38 states have call successors, (47)
[2025-05-07 17:27:21,743 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 135 transitions.
[2025-05-07 17:27:21,743 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 135 transitions. Word has length 58
[2025-05-07 17:27:21,744 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:21,744 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 135 transitions.
[2025-05-07 17:27:21,744 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 14 states have internal predecessors, (26), 7 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (16), 13 states have call predecessors, (16), 7 states have call successors, (16)
[2025-05-07 17:27:21,744 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 135 transitions.
[2025-05-07 17:27:21,745 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:27:21,745 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,745 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]
[2025-05-07 17:27:21,746 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:21,746 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,746 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,746 INFO  L85        PathProgramCache]: Analyzing trace with hash 846373946, now seen corresponding path program 1 times
[2025-05-07 17:27:21,746 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,746 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1887835400]
[2025-05-07 17:27:21,746 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,746 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,771 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:27:21,781 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:27:21,781 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,781 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:21,852 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:21,852 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:21,852 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1887835400]
[2025-05-07 17:27:21,853 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1887835400] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:21,853 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:21,853 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:21,853 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1934079742]
[2025-05-07 17:27:21,853 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:21,853 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:21,853 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:21,854 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:21,854 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:21,854 INFO  L87              Difference]: Start difference. First operand 111 states and 135 transitions. Second operand  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16)
[2025-05-07 17:27:21,893 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:21,893 INFO  L93              Difference]: Finished difference Result 116 states and 141 transitions.
[2025-05-07 17:27:21,894 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:21,894 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16) Word has length 58
[2025-05-07 17:27:21,894 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:21,895 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:21,895 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:27:21,896 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:21,897 INFO  L437           NwaCegarLoop]: 125 mSDtfsCounter, 1 mSDsluCounter, 484 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 609 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:21,897 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 609 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:21,898 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:27:21,908 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 116.
[2025-05-07 17:27:21,908 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 116 states, 47 states have (on average 1.0212765957446808) internal successors, (48), 48 states have internal predecessors, (48), 39 states have call successors, (43), 25 states have call predecessors, (43), 30 states have return successors, (50), 42 states have call predecessors, (50), 39 states have call successors, (50)
[2025-05-07 17:27:21,910 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 141 transitions.
[2025-05-07 17:27:21,910 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 141 transitions. Word has length 58
[2025-05-07 17:27:21,910 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:21,910 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 141 transitions.
[2025-05-07 17:27:21,910 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16)
[2025-05-07 17:27:21,910 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 141 transitions.
[2025-05-07 17:27:21,911 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-05-07 17:27:21,911 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:21,912 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]
[2025-05-07 17:27:21,912 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:21,912 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:21,912 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:21,912 INFO  L85        PathProgramCache]: Analyzing trace with hash 1153881422, now seen corresponding path program 1 times
[2025-05-07 17:27:21,912 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:21,912 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1466632293]
[2025-05-07 17:27:21,912 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:21,912 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:21,956 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-05-07 17:27:21,975 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-05-07 17:27:21,975 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:21,976 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,077 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:22,077 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,077 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1466632293]
[2025-05-07 17:27:22,078 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1466632293] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,078 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,078 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:22,078 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [967862599]
[2025-05-07 17:27:22,078 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,078 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:22,078 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,079 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:22,079 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:22,079 INFO  L87              Difference]: Start difference. First operand 116 states and 141 transitions. Second operand  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:27:22,141 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,141 INFO  L93              Difference]: Finished difference Result 116 states and 140 transitions.
[2025-05-07 17:27:22,141 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:22,141 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20) Word has length 72
[2025-05-07 17:27:22,142 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,142 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:22,142 INFO  L226             Difference]: Without dead ends: 113
[2025-05-07 17:27:22,142 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:22,143 INFO  L437           NwaCegarLoop]: 116 mSDtfsCounter, 0 mSDsluCounter, 563 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 679 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:22,143 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 679 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:22,144 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-05-07 17:27:22,149 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 113.
[2025-05-07 17:27:22,149 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 46 states have (on average 1.0217391304347827) internal successors, (47), 47 states have internal predecessors, (47), 36 states have call successors, (40), 25 states have call predecessors, (40), 30 states have return successors, (47), 40 states have call predecessors, (47), 36 states have call successors, (47)
[2025-05-07 17:27:22,150 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 134 transitions.
[2025-05-07 17:27:22,150 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 134 transitions. Word has length 72
[2025-05-07 17:27:22,150 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:22,150 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 134 transitions.
[2025-05-07 17:27:22,150 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:27:22,150 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 134 transitions.
[2025-05-07 17:27:22,151 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:27:22,151 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:22,151 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]
[2025-05-07 17:27:22,151 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:22,151 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:22,151 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:22,152 INFO  L85        PathProgramCache]: Analyzing trace with hash 2100002282, now seen corresponding path program 1 times
[2025-05-07 17:27:22,152 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:22,152 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [392638287]
[2025-05-07 17:27:22,152 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:22,152 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:22,176 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:27:22,187 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:27:22,187 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:22,187 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,536 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:22,536 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,536 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [392638287]
[2025-05-07 17:27:22,536 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [392638287] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,536 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,537 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [] total 16
[2025-05-07 17:27:22,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1235599152]
[2025-05-07 17:27:22,537 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,537 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:27:22,537 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,538 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:27:22,538 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=211, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:27:22,538 INFO  L87              Difference]: Start difference. First operand 113 states and 134 transitions. Second operand  has 16 states, 12 states have (on average 2.75) internal successors, (33), 14 states have internal predecessors, (33), 8 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 12 states have call predecessors, (21), 8 states have call successors, (21)
[2025-05-07 17:27:22,785 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,785 INFO  L93              Difference]: Finished difference Result 121 states and 145 transitions.
[2025-05-07 17:27:22,785 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:27:22,786 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 12 states have (on average 2.75) internal successors, (33), 14 states have internal predecessors, (33), 8 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 12 states have call predecessors, (21), 8 states have call successors, (21) Word has length 75
[2025-05-07 17:27:22,786 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,787 INFO  L225             Difference]: With dead ends: 121
[2025-05-07 17:27:22,787 INFO  L226             Difference]: Without dead ends: 121
[2025-05-07 17:27:22,787 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-05-07 17:27:22,788 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 4 mSDsluCounter, 1474 mSDsCounter, 0 mSdLazyCounter, 266 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1583 SdHoareTripleChecker+Invalid, 268 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 266 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:22,788 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1583 Invalid, 268 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 266 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:27:22,789 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-05-07 17:27:22,801 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 113.
[2025-05-07 17:27:22,801 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 46 states have (on average 1.0217391304347827) internal successors, (47), 47 states have internal predecessors, (47), 36 states have call successors, (40), 25 states have call predecessors, (40), 30 states have return successors, (47), 40 states have call predecessors, (47), 36 states have call successors, (47)
[2025-05-07 17:27:22,802 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 134 transitions.
[2025-05-07 17:27:22,802 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 134 transitions. Word has length 75
[2025-05-07 17:27:22,803 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:22,803 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 134 transitions.
[2025-05-07 17:27:22,803 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 12 states have (on average 2.75) internal successors, (33), 14 states have internal predecessors, (33), 8 states have call successors, (21), 1 states have call predecessors, (21), 12 states have return successors, (21), 12 states have call predecessors, (21), 8 states have call successors, (21)
[2025-05-07 17:27:22,804 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 134 transitions.
[2025-05-07 17:27:22,805 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:27:22,805 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:22,805 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]
[2025-05-07 17:27:22,805 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:22,805 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:22,806 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:22,806 INFO  L85        PathProgramCache]: Analyzing trace with hash 927227580, now seen corresponding path program 1 times
[2025-05-07 17:27:22,806 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:22,806 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1007730459]
[2025-05-07 17:27:22,806 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:22,806 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:22,841 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:27:22,857 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:27:22,857 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:22,857 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:22,964 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:22,964 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:22,964 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1007730459]
[2025-05-07 17:27:22,964 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1007730459] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:22,964 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:22,964 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:22,965 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [571355467]
[2025-05-07 17:27:22,965 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:22,965 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:22,965 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:22,965 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:22,965 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:22,965 INFO  L87              Difference]: Start difference. First operand 113 states and 134 transitions. Second operand  has 6 states, 5 states have (on average 6.6) internal successors, (33), 6 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:27:22,992 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:22,992 INFO  L93              Difference]: Finished difference Result 118 states and 140 transitions.
[2025-05-07 17:27:22,993 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:22,993 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.6) internal successors, (33), 6 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 5 states have call successors, (21) Word has length 75
[2025-05-07 17:27:22,993 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:22,993 INFO  L225             Difference]: With dead ends: 118
[2025-05-07 17:27:22,993 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:27:22,994 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:22,994 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 1 mSDsluCounter, 454 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 571 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:22,994 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 571 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:22,995 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:27:22,999 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 113.
[2025-05-07 17:27:22,999 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 46 states have (on average 1.0217391304347827) internal successors, (47), 47 states have internal predecessors, (47), 36 states have call successors, (40), 25 states have call predecessors, (40), 30 states have return successors, (47), 40 states have call predecessors, (47), 36 states have call successors, (47)
[2025-05-07 17:27:23,000 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 134 transitions.
[2025-05-07 17:27:23,000 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 134 transitions. Word has length 75
[2025-05-07 17:27:23,000 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,000 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 134 transitions.
[2025-05-07 17:27:23,000 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.6) internal successors, (33), 6 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:27:23,000 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 134 transitions.
[2025-05-07 17:27:23,001 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:27:23,001 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:23,001 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]
[2025-05-07 17:27:23,001 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:23,001 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:23,001 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:23,001 INFO  L85        PathProgramCache]: Analyzing trace with hash -1882479074, now seen corresponding path program 1 times
[2025-05-07 17:27:23,001 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:23,001 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [232171694]
[2025-05-07 17:27:23,002 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:23,002 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,024 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:27:23,034 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:27:23,034 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,034 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:23,127 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:23,128 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:23,128 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [232171694]
[2025-05-07 17:27:23,128 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [232171694] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:23,128 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:23,128 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:23,128 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1516707047]
[2025-05-07 17:27:23,128 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:23,129 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:23,129 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:23,129 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:23,129 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:23,130 INFO  L87              Difference]: Start difference. First operand 113 states and 134 transitions. Second operand  has 6 states, 5 states have (on average 6.6) internal successors, (33), 6 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:27:23,157 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:23,157 INFO  L93              Difference]: Finished difference Result 112 states and 130 transitions.
[2025-05-07 17:27:23,157 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:23,158 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.6) internal successors, (33), 6 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 5 states have call successors, (21) Word has length 75
[2025-05-07 17:27:23,158 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:23,159 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:27:23,159 INFO  L226             Difference]: Without dead ends: 112
[2025-05-07 17:27:23,159 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:23,159 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 1 mSDsluCounter, 454 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 571 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:23,160 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 571 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:23,160 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-05-07 17:27:23,164 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 107.
[2025-05-07 17:27:23,165 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 44 states have (on average 1.0227272727272727) internal successors, (45), 45 states have internal predecessors, (45), 34 states have call successors, (38), 25 states have call predecessors, (38), 28 states have return successors, (41), 36 states have call predecessors, (41), 34 states have call successors, (41)
[2025-05-07 17:27:23,165 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 124 transitions.
[2025-05-07 17:27:23,165 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 124 transitions. Word has length 75
[2025-05-07 17:27:23,165 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,165 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 124 transitions.
[2025-05-07 17:27:23,166 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.6) internal successors, (33), 6 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:27:23,166 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 124 transitions.
[2025-05-07 17:27:23,166 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:27:23,166 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:23,166 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:27:23,167 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:23,167 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:23,167 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:23,167 INFO  L85        PathProgramCache]: Analyzing trace with hash 1524792834, now seen corresponding path program 1 times
[2025-05-07 17:27:23,167 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:23,167 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1295608958]
[2025-05-07 17:27:23,167 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:23,167 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,195 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:27:23,205 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:27:23,205 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,205 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:23,296 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-05-07 17:27:23,296 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:23,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1295608958]
[2025-05-07 17:27:23,296 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1295608958] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:23,296 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:23,296 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:23,296 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [68738506]
[2025-05-07 17:27:23,296 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:23,297 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:23,297 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:23,297 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:23,297 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:23,297 INFO  L87              Difference]: Start difference. First operand 107 states and 124 transitions. Second operand  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 5 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (23), 5 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:27:23,322 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:23,322 INFO  L93              Difference]: Finished difference Result 112 states and 129 transitions.
[2025-05-07 17:27:23,322 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:23,322 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 5 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (23), 5 states have call predecessors, (23), 5 states have call successors, (23) Word has length 90
[2025-05-07 17:27:23,322 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:23,323 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:27:23,323 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:27:23,323 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:23,324 INFO  L437           NwaCegarLoop]: 121 mSDtfsCounter, 1 mSDsluCounter, 467 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 588 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:23,324 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 588 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:23,325 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:27:23,328 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:27:23,328 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 42 states have (on average 1.0238095238095237) internal successors, (43), 43 states have internal predecessors, (43), 32 states have call successors, (35), 24 states have call predecessors, (35), 27 states have return successors, (38), 34 states have call predecessors, (38), 32 states have call successors, (38)
[2025-05-07 17:27:23,329 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 116 transitions.
[2025-05-07 17:27:23,329 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 116 transitions. Word has length 90
[2025-05-07 17:27:23,329 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,330 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 116 transitions.
[2025-05-07 17:27:23,330 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 5 states have call successors, (22), 1 states have call predecessors, (22), 5 states have return successors, (23), 5 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:27:23,330 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 116 transitions.
[2025-05-07 17:27:23,330 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:27:23,330 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:23,330 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:23,330 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:23,331 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:23,331 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:23,331 INFO  L85        PathProgramCache]: Analyzing trace with hash 1183441986, now seen corresponding path program 1 times
[2025-05-07 17:27:23,331 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:23,331 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1485357633]
[2025-05-07 17:27:23,331 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:23,331 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,358 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:27:23,368 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:27:23,368 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,368 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:23,463 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 11 proven. 0 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-05-07 17:27:23,463 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:23,463 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1485357633]
[2025-05-07 17:27:23,463 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1485357633] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:23,463 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:23,463 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:23,463 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1868922697]
[2025-05-07 17:27:23,463 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:23,463 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:23,464 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:23,464 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:23,464 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:23,464 INFO  L87              Difference]: Start difference. First operand 102 states and 116 transitions. Second operand  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (23), 5 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:27:23,494 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:23,494 INFO  L93              Difference]: Finished difference Result 107 states and 122 transitions.
[2025-05-07 17:27:23,495 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:23,495 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (23), 5 states have call predecessors, (23), 5 states have call successors, (23) Word has length 90
[2025-05-07 17:27:23,495 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:23,496 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:27:23,496 INFO  L226             Difference]: Without dead ends: 107
[2025-05-07 17:27:23,496 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:23,496 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 425 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 535 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:23,497 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 535 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:23,497 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-05-07 17:27:23,502 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 107.
[2025-05-07 17:27:23,502 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 44 states have (on average 1.0227272727272727) internal successors, (45), 45 states have internal predecessors, (45), 33 states have call successors, (36), 24 states have call predecessors, (36), 29 states have return successors, (41), 37 states have call predecessors, (41), 33 states have call successors, (41)
[2025-05-07 17:27:23,503 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 122 transitions.
[2025-05-07 17:27:23,503 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 122 transitions. Word has length 90
[2025-05-07 17:27:23,503 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,503 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 122 transitions.
[2025-05-07 17:27:23,503 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 5 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (23), 5 states have call predecessors, (23), 5 states have call successors, (23)
[2025-05-07 17:27:23,503 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 122 transitions.
[2025-05-07 17:27:23,504 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 108
[2025-05-07 17:27:23,504 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:23,504 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:27:23,504 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:23,504 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:23,505 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:23,505 INFO  L85        PathProgramCache]: Analyzing trace with hash 866826430, now seen corresponding path program 1 times
[2025-05-07 17:27:23,505 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:23,505 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [212256202]
[2025-05-07 17:27:23,505 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:23,505 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,547 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:27:23,556 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:27:23,556 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,556 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:23,671 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-05-07 17:27:23,671 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:23,671 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [212256202]
[2025-05-07 17:27:23,671 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [212256202] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:23,671 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:23,671 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:23,671 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1546041205]
[2025-05-07 17:27:23,671 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:23,672 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:23,672 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:23,672 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:23,672 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:23,672 INFO  L87              Difference]: Start difference. First operand 107 states and 122 transitions. Second operand  has 6 states, 5 states have (on average 7.8) internal successors, (39), 6 states have internal predecessors, (39), 5 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (28), 5 states have call predecessors, (28), 5 states have call successors, (28)
[2025-05-07 17:27:23,706 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:23,706 INFO  L93              Difference]: Finished difference Result 107 states and 121 transitions.
[2025-05-07 17:27:23,707 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:23,707 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.8) internal successors, (39), 6 states have internal predecessors, (39), 5 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (28), 5 states have call predecessors, (28), 5 states have call successors, (28) Word has length 107
[2025-05-07 17:27:23,707 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:23,708 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:27:23,708 INFO  L226             Difference]: Without dead ends: 107
[2025-05-07 17:27:23,708 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:23,708 INFO  L437           NwaCegarLoop]: 113 mSDtfsCounter, 1 mSDsluCounter, 434 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 547 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:23,708 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 547 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:23,709 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-05-07 17:27:23,711 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 102.
[2025-05-07 17:27:23,711 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 42 states have (on average 1.0238095238095237) internal successors, (43), 43 states have internal predecessors, (43), 32 states have call successors, (35), 24 states have call predecessors, (35), 27 states have return successors, (37), 34 states have call predecessors, (37), 32 states have call successors, (37)
[2025-05-07 17:27:23,712 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 115 transitions.
[2025-05-07 17:27:23,712 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 115 transitions. Word has length 107
[2025-05-07 17:27:23,712 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,712 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 115 transitions.
[2025-05-07 17:27:23,712 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.8) internal successors, (39), 6 states have internal predecessors, (39), 5 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (28), 5 states have call predecessors, (28), 5 states have call successors, (28)
[2025-05-07 17:27:23,712 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 115 transitions.
[2025-05-07 17:27:23,713 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 108
[2025-05-07 17:27:23,713 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:23,713 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:27:23,713 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:27:23,713 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:23,714 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:23,714 INFO  L85        PathProgramCache]: Analyzing trace with hash -888230640, now seen corresponding path program 1 times
[2025-05-07 17:27:23,714 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:23,714 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2071985048]
[2025-05-07 17:27:23,714 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:23,714 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,749 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:27:23,763 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:27:23,763 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,763 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:24,310 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-05-07 17:27:24,310 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:24,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2071985048]
[2025-05-07 17:27:24,311 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2071985048] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:24,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1468196520]
[2025-05-07 17:27:24,311 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:24,311 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:24,314 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:24,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:24,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:24,645 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:27:24,845 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:27:24,845 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:24,845 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:24,852 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1790 conjuncts, 64 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:24,860 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:24,943 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-05-07 17:27:24,943 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:27:26,269 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 3 proven. 6 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:27:26,269 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1468196520] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:27:26,269 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:27:26,269 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [20, 20, 22] total 33
[2025-05-07 17:27:26,269 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1304576813]
[2025-05-07 17:27:26,269 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:27:26,270 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-05-07 17:27:26,270 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:26,270 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-05-07 17:27:26,270 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=86, Invalid=970, Unknown=0, NotChecked=0, Total=1056
[2025-05-07 17:27:26,271 INFO  L87              Difference]: Start difference. First operand 102 states and 115 transitions. Second operand  has 33 states, 23 states have (on average 2.260869565217391) internal successors, (52), 28 states have internal predecessors, (52), 17 states have call successors, (36), 1 states have call predecessors, (36), 23 states have return successors, (43), 27 states have call predecessors, (43), 17 states have call successors, (43)
[2025-05-07 17:27:26,616 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:26,616 INFO  L93              Difference]: Finished difference Result 120 states and 143 transitions.
[2025-05-07 17:27:26,616 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-05-07 17:27:26,616 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 23 states have (on average 2.260869565217391) internal successors, (52), 28 states have internal predecessors, (52), 17 states have call successors, (36), 1 states have call predecessors, (36), 23 states have return successors, (43), 27 states have call predecessors, (43), 17 states have call successors, (43) Word has length 107
[2025-05-07 17:27:26,617 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:26,617 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:27:26,617 INFO  L226             Difference]: Without dead ends: 120
[2025-05-07 17:27:26,618 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 241 GetRequests, 205 SyntacticMatches, 0 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 91 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=115, Invalid=1291, Unknown=0, NotChecked=0, Total=1406
[2025-05-07 17:27:26,618 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 10 mSDsluCounter, 1772 mSDsCounter, 0 mSdLazyCounter, 404 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 1875 SdHoareTripleChecker+Invalid, 410 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 404 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:26,618 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 1875 Invalid, 410 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 404 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:27:26,619 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-05-07 17:27:26,622 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 116.
[2025-05-07 17:27:26,622 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 116 states, 47 states have (on average 1.0212765957446808) internal successors, (48), 48 states have internal predecessors, (48), 36 states have call successors, (39), 24 states have call predecessors, (39), 32 states have return successors, (49), 43 states have call predecessors, (49), 36 states have call successors, (49)
[2025-05-07 17:27:26,623 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 136 transitions.
[2025-05-07 17:27:26,623 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 136 transitions. Word has length 107
[2025-05-07 17:27:26,623 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:26,623 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 136 transitions.
[2025-05-07 17:27:26,623 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 23 states have (on average 2.260869565217391) internal successors, (52), 28 states have internal predecessors, (52), 17 states have call successors, (36), 1 states have call predecessors, (36), 23 states have return successors, (43), 27 states have call predecessors, (43), 17 states have call successors, (43)
[2025-05-07 17:27:26,623 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 136 transitions.
[2025-05-07 17:27:26,624 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 125
[2025-05-07 17:27:26,624 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:26,624 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, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:26,632 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:27:26,825 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-05-07 17:27:26,825 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:26,826 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:26,826 INFO  L85        PathProgramCache]: Analyzing trace with hash -251933054, now seen corresponding path program 1 times
[2025-05-07 17:27:26,826 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:26,826 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [283904679]
[2025-05-07 17:27:26,826 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:26,826 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:26,906 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 124 statements into 1 equivalence classes.
[2025-05-07 17:27:26,920 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 124 of 124 statements.
[2025-05-07 17:27:26,920 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:26,920 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:27,038 INFO  L134       CoverageAnalysis]: Checked inductivity of 41 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 34 trivial. 0 not checked.
[2025-05-07 17:27:27,039 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:27,039 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [283904679]
[2025-05-07 17:27:27,039 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [283904679] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:27,039 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:27,039 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:27,039 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [11235432]
[2025-05-07 17:27:27,039 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:27,040 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:27,040 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:27,040 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:27,040 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:27,040 INFO  L87              Difference]: Start difference. First operand 116 states and 136 transitions. Second operand  has 6 states, 5 states have (on average 7.8) internal successors, (39), 6 states have internal predecessors, (39), 5 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (29), 5 states have call predecessors, (29), 5 states have call successors, (29)
[2025-05-07 17:27:27,069 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:27,069 INFO  L93              Difference]: Finished difference Result 113 states and 127 transitions.
[2025-05-07 17:27:27,070 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:27,070 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.8) internal successors, (39), 6 states have internal predecessors, (39), 5 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (29), 5 states have call predecessors, (29), 5 states have call successors, (29) Word has length 124
[2025-05-07 17:27:27,070 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:27,070 INFO  L225             Difference]: With dead ends: 113
[2025-05-07 17:27:27,070 INFO  L226             Difference]: Without dead ends: 91
[2025-05-07 17:27:27,070 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:27,071 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 424 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 534 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:27,071 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 534 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:27,071 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-05-07 17:27:27,073 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 91.
[2025-05-07 17:27:27,073 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 38 states have (on average 1.0263157894736843) internal successors, (39), 39 states have internal predecessors, (39), 27 states have call successors, (28), 22 states have call predecessors, (28), 25 states have return successors, (30), 29 states have call predecessors, (30), 27 states have call successors, (30)
[2025-05-07 17:27:27,074 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 97 transitions.
[2025-05-07 17:27:27,074 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 97 transitions. Word has length 124
[2025-05-07 17:27:27,074 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:27,074 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 97 transitions.
[2025-05-07 17:27:27,074 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.8) internal successors, (39), 6 states have internal predecessors, (39), 5 states have call successors, (28), 1 states have call predecessors, (28), 5 states have return successors, (29), 5 states have call predecessors, (29), 5 states have call successors, (29)
[2025-05-07 17:27:27,074 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 97 transitions.
[2025-05-07 17:27:27,075 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 125
[2025-05-07 17:27:27,075 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:27,075 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, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:27,075 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:27:27,075 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:27,075 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:27,075 INFO  L85        PathProgramCache]: Analyzing trace with hash -1658267744, now seen corresponding path program 1 times
[2025-05-07 17:27:27,075 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:27,076 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [558625687]
[2025-05-07 17:27:27,076 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:27,076 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:27,119 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 124 statements into 1 equivalence classes.
[2025-05-07 17:27:27,132 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 124 of 124 statements.
[2025-05-07 17:27:27,132 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:27,132 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:27,679 INFO  L134       CoverageAnalysis]: Checked inductivity of 41 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-05-07 17:27:27,679 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:27,679 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [558625687]
[2025-05-07 17:27:27,679 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [558625687] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:27,679 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1570922490]
[2025-05-07 17:27:27,679 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:27,679 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:27,681 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:27,682 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:27,683 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:27:28,005 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 124 statements into 1 equivalence classes.
[2025-05-07 17:27:28,183 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 124 of 124 statements.
[2025-05-07 17:27:28,183 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:28,183 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:28,188 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2126 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:28,193 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:28,269 INFO  L134       CoverageAnalysis]: Checked inductivity of 41 backedges. 38 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:27:28,269 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:27:28,269 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1570922490] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:28,269 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:27:28,269 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [20] total 24
[2025-05-07 17:27:28,269 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1029882246]
[2025-05-07 17:27:28,269 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:28,269 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:28,269 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:28,270 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:28,270 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=507, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:27:28,270 INFO  L87              Difference]: Start difference. First operand 91 states and 97 transitions. Second operand  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 5 states have call successors, (35), 2 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 5 states have call successors, (35)
[2025-05-07 17:27:28,286 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:28,286 INFO  L93              Difference]: Finished difference Result 59 states and 62 transitions.
[2025-05-07 17:27:28,286 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:28,286 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 5 states have call successors, (35), 2 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 5 states have call successors, (35) Word has length 124
[2025-05-07 17:27:28,286 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:28,286 INFO  L225             Difference]: With dead ends: 59
[2025-05-07 17:27:28,286 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:28,287 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 146 GetRequests, 124 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=45, Invalid=507, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:27:28,287 INFO  L437           NwaCegarLoop]: 60 mSDtfsCounter, 0 mSDsluCounter, 228 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 288 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:28,287 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 288 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:28,287 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:28,288 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:28,288 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:28,288 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:28,288 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 124
[2025-05-07 17:27:28,288 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:28,288 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:28,288 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.6) internal successors, (53), 6 states have internal predecessors, (53), 5 states have call successors, (35), 2 states have call predecessors, (35), 5 states have return successors, (35), 5 states have call predecessors, (35), 5 states have call successors, (35)
[2025-05-07 17:27:28,288 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:28,288 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:28,290 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:28,296 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:27:28,491 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-05-07 17:27:28,498 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:28,503 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:28,511 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:28 BoogieIcfgContainer
[2025-05-07 17:27:28,511 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:28,513 INFO  L158              Benchmark]: Toolchain (without parser) took 8888.12ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 141.3MB in the beginning and 260.6MB in the end (delta: -119.3MB). Peak memory consumption was 6.2MB. Max. memory is 33.6GB.
[2025-05-07 17:27:28,514 INFO  L158              Benchmark]: SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 172.6MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:28,515 INFO  L158              Benchmark]: ChcToBoogie took 33.53ms. Allocated memory is still 234.9MB. Free memory was 141.3MB in the beginning and 137.7MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:28,516 INFO  L158              Benchmark]: Boogie Preprocessor took 60.50ms. Allocated memory is still 234.9MB. Free memory was 137.7MB in the beginning and 134.1MB in the end (delta: 3.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:28,516 INFO  L158              Benchmark]: RCFGBuilder took 492.93ms. Allocated memory is still 234.9MB. Free memory was 134.1MB in the beginning and 157.0MB in the end (delta: -22.9MB). Peak memory consumption was 26.0MB. Max. memory is 33.6GB.
[2025-05-07 17:27:28,517 INFO  L158              Benchmark]: TraceAbstraction took 8296.91ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 156.4MB in the beginning and 260.6MB in the end (delta: -104.2MB). Peak memory consumption was 13.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:28,521 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.18ms. Allocated memory is still 234.9MB. Free memory is still 172.6MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 33.53ms. Allocated memory is still 234.9MB. Free memory was 141.3MB in the beginning and 137.7MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 60.50ms. Allocated memory is still 234.9MB. Free memory was 137.7MB in the beginning and 134.1MB in the end (delta: 3.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 492.93ms. Allocated memory is still 234.9MB. Free memory was 134.1MB in the beginning and 157.0MB in the end (delta: -22.9MB). Peak memory consumption was 26.0MB. Max. memory is 33.6GB.
 * TraceAbstraction took 8296.91ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 156.4MB in the beginning and 260.6MB in the end (delta: -104.2MB). Peak memory consumption was 13.8MB. 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, 109 locations, 179 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 8.2s, OverallIterations: 14, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 63 SdHoareTripleChecker+Valid, 1.0s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 28 mSDsluCounter, 10875 SdHoareTripleChecker+Invalid, 0.9s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 9307 mSDsCounter, 10 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1159 IncrementalHoareTripleChecker+Invalid, 1169 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 10 mSolverCounterUnsat, 1568 mSDtfsCounter, 1159 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 483 GetRequests, 353 SyntacticMatches, 0 SemanticMatches, 130 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 97 ImplicationChecksByTransitivity, 0.9s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=116occurred in iteration=4, InterpolantAutomatonStates: 117, 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, 14 MinimizatonAttempts, 33 StatesRemovedByMinimization, 8 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.3s SsaConstructionTime, 0.6s SatisfiabilityAnalysisTime, 4.4s InterpolantComputationTime, 1396 NumberOfCodeBlocks, 1396 NumberOfCodeBlocksAsserted, 16 NumberOfCheckSat, 1486 ConstructedInterpolants, 0 QuantifiedInterpolants, 2324 SizeOfPredicates, 5 NumberOfNonLiveVariables, 3916 ConjunctsInSsa, 69 ConjunctsInUnsatCore, 17 InterpolantComputations, 13 PerfectInterpolantSequences, 257/278 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:28,544 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
