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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:05,281 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:05,318 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6bc5e11d-9e0b-4574-963a-c668ccfc64b0/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:05,321 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:05,322 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:05,334 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:05,335 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:05,335 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:05,335 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:05,335 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:05,335 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:05,335 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:05,335 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:05,335 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:05,336 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:05,336 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:05,336 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:05,337 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:05,337 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:05,520 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:05,526 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:05,527 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:05,528 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:05,528 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:05,529 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6bc5e11d-9e0b-4574-963a-c668ccfc64b0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/natspec/safe_assert_false_positive_pure.sol_2_no_adts_000.smt2
[2025-05-07 17:28:05,530 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:05,532 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:05,783 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6bc5e11d-9e0b-4574-963a-c668ccfc64b0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/natspec/safe_assert_false_positive_pure.sol_2_no_adts_000.smt2
[2025-05-07 17:28:05,785 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:05,786 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:05,787 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:05,787 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:05,787 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:05,789 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,821 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05 Unit
[2025-05-07 17:28:05,821 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:05,821 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:05,822 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:05,822 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:05,833 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,833 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,855 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,855 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,860 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,861 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,862 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,864 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,866 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,877 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:05,878 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:05,878 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:05,878 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:05,879 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (1/1) ...
[2025-05-07 17:28:05,880 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:05,889 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:05,897 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:28:05,900 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:28:05,907 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:05,907 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:05,907 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:05,907 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_9_0 given in one single declaration
[2025-05-07 17:28:05,907 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_9_0
[2025-05-07 17:28:05,907 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_9_0
[2025-05-07 17:28:05,907 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_68_0 given in one single declaration
[2025-05-07 17:28:05,907 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_68_0
[2025-05-07 17:28:05,907 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_68_0
[2025-05-07 17:28:05,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_68_0 given in one single declaration
[2025-05-07 17:28:05,908 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_68_0
[2025-05-07 17:28:05,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_68_0
[2025-05-07 17:28:05,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_21_C_68_0 given in one single declaration
[2025-05-07 17:28:05,908 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_21_C_68_0
[2025-05-07 17:28:05,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_21_C_68_0
[2025-05-07 17:28:05,908 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:28:05,908 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_23_C_68_0
[2025-05-07 17:28:05,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_23_C_68_0
[2025-05-07 17:28:05,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_22_C_68_0 given in one single declaration
[2025-05-07 17:28:05,909 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_22_C_68_0
[2025-05-07 17:28:05,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_22_C_68_0
[2025-05-07 17:28:05,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_24_C_68_0 given in one single declaration
[2025-05-07 17:28:05,909 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_24_C_68_0
[2025-05-07 17:28:05,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_24_C_68_0
[2025-05-07 17:28:05,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,909 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_g__46_68_0
[2025-05-07 17:28:05,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_g__46_68_0
[2025-05-07 17:28:05,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,909 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_g__46_68_0
[2025-05-07 17:28:05,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_g__46_68_0
[2025-05-07 17:28:05,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,910 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,910 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_g__46_68_0
[2025-05-07 17:28:05,910 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:28:05,910 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,910 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_g__46_68_0
[2025-05-07 17:28:05,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,911 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_g__46_68_0
[2025-05-07 17:28:05,911 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_g__46_68_0
[2025-05-07 17:28:05,911 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:28:05,911 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_f2__67_68_0
[2025-05-07 17:28:05,911 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_f2__67_68_0
[2025-05-07 17:28:05,911 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:28:05,911 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_f2__67_68_0
[2025-05-07 17:28:05,911 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_f2__67_68_0
[2025-05-07 17:28:05,911 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:28:05,911 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_return_function_f2__67_68_0
[2025-05-07 17:28:05,911 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_return_function_f2__67_68_0
[2025-05-07 17:28:05,911 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_f2_66_68_0 given in one single declaration
[2025-05-07 17:28:05,912 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_f2_66_68_0
[2025-05-07 17:28:05,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_f2_66_68_0
[2025-05-07 17:28:05,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_f2__67_68_0 given in one single declaration
[2025-05-07 17:28:05,912 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_f2__67_68_0
[2025-05-07 17:28:05,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_f2__67_68_0
[2025-05-07 17:28:05,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_g_45_68_0 given in one single declaration
[2025-05-07 17:28:05,912 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_g_45_68_0
[2025-05-07 17:28:05,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_g_45_68_0
[2025-05-07 17:28:05,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,912 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_g__46_68_0
[2025-05-07 17:28:05,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_g__46_68_0
[2025-05-07 17:28:05,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_f1__57_68_0 given in one single declaration
[2025-05-07 17:28:05,913 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_f1__57_68_0
[2025-05-07 17:28:05,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_f1__57_68_0
[2025-05-07 17:28:05,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_f1__57_68_0 given in one single declaration
[2025-05-07 17:28:05,913 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_f1__57_68_0
[2025-05-07 17:28:05,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_f1__57_68_0
[2025-05-07 17:28:05,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_g__46_68_0 given in one single declaration
[2025-05-07 17:28:05,913 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_g__46_68_0
[2025-05-07 17:28:05,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_g__46_68_0
[2025-05-07 17:28:05,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:05,913 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:05,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:06,072 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:06,073 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:06,323 INFO  L?                        ?]: Removed 244 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:06,323 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:06,331 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:06,332 INFO  L312             CfgBuilder]: Removed 14 assume(true) statements.
[2025-05-07 17:28:06,332 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:06 BoogieIcfgContainer
[2025-05-07 17:28:06,332 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:06,333 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:06,333 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:06,336 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:06,336 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:05" (1/3) ...
[2025-05-07 17:28:06,336 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:28:06, skipping insertion in model container
[2025-05-07 17:28:06,336 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:05" (2/3) ...
[2025-05-07 17:28:06,337 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:28:06, skipping insertion in model container
[2025-05-07 17:28:06,337 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:06" (3/3) ...
[2025-05-07 17:28:06,338 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:06,348 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:06,350 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:28:06,379 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:06,387 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:28:06,387 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:06,390 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:28:06,397 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-05-07 17:28:06,397 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,397 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:28:06,397 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,401 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,401 INFO  L85        PathProgramCache]: Analyzing trace with hash 681061035, now seen corresponding path program 1 times
[2025-05-07 17:28:06,406 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,406 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [13049931]
[2025-05-07 17:28:06,406 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,407 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,452 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-05-07 17:28:06,501 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-05-07 17:28:06,502 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,502 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,697 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:06,698 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [13049931]
[2025-05-07 17:28:06,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [13049931] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,698 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,700 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:06,701 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1019916014]
[2025-05-07 17:28:06,702 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,705 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:06,705 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,734 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:06,734 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:06,736 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:28:06,784 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:06,785 INFO  L93              Difference]: Finished difference Result 111 states and 137 transitions.
[2025-05-07 17:28:06,786 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:06,787 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:28:06,787 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:06,793 INFO  L225             Difference]: With dead ends: 111
[2025-05-07 17:28:06,793 INFO  L226             Difference]: Without dead ends: 107
[2025-05-07 17:28:06,795 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:06,797 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:28:06,798 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:28:06,810 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-05-07 17:28:06,829 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 105.
[2025-05-07 17:28:06,830 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:28:06,834 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 128 transitions.
[2025-05-07 17:28:06,834 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 128 transitions. Word has length 55
[2025-05-07 17:28:06,835 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:06,835 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 128 transitions.
[2025-05-07 17:28:06,835 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:28:06,835 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 128 transitions.
[2025-05-07 17:28:06,837 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-05-07 17:28:06,837 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:06,837 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:28:06,837 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:06,837 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:06,838 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:06,838 INFO  L85        PathProgramCache]: Analyzing trace with hash -407146457, now seen corresponding path program 1 times
[2025-05-07 17:28:06,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:06,838 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1905192466]
[2025-05-07 17:28:06,838 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,838 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:06,867 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-05-07 17:28:06,887 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-05-07 17:28:06,887 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,887 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,978 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:06,978 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,978 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1905192466]
[2025-05-07 17:28:06,978 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1905192466] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:06,978 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:06,978 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:06,979 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [706027579]
[2025-05-07 17:28:06,979 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:06,979 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:06,979 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:06,980 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:06,980 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:06,980 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:28:07,063 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,063 INFO  L93              Difference]: Finished difference Result 107 states and 129 transitions.
[2025-05-07 17:28:07,064 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:07,064 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:28:07,064 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,065 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:28:07,065 INFO  L226             Difference]: Without dead ends: 105
[2025-05-07 17:28:07,065 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:28:07,066 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:28:07,066 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:28:07,067 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 105 states.
[2025-05-07 17:28:07,071 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 105 to 103.
[2025-05-07 17:28:07,072 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:28:07,073 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 103 states to 103 states and 123 transitions.
[2025-05-07 17:28:07,073 INFO  L79                 Accepts]: Start accepts. Automaton has 103 states and 123 transitions. Word has length 55
[2025-05-07 17:28:07,073 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,073 INFO  L485      AbstractCegarLoop]: Abstraction has 103 states and 123 transitions.
[2025-05-07 17:28:07,073 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:28:07,073 INFO  L278                IsEmpty]: Start isEmpty. Operand 103 states and 123 transitions.
[2025-05-07 17:28:07,074 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:28:07,074 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:07,075 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:28:07,075 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:07,075 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:07,075 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:07,075 INFO  L85        PathProgramCache]: Analyzing trace with hash 1331848602, now seen corresponding path program 1 times
[2025-05-07 17:28:07,075 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:07,075 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [458960515]
[2025-05-07 17:28:07,075 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,075 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:07,101 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:28:07,113 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:28:07,113 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:07,113 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,455 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:07,455 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:07,455 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [458960515]
[2025-05-07 17:28:07,455 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [458960515] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:07,455 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:07,455 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [] total 16
[2025-05-07 17:28:07,456 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [989702368]
[2025-05-07 17:28:07,456 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:07,456 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:28:07,456 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:07,457 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:28:07,457 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=211, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:28:07,458 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:28:07,758 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,758 INFO  L93              Difference]: Finished difference Result 113 states and 137 transitions.
[2025-05-07 17:28:07,758 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:28:07,759 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:28:07,759 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,760 INFO  L225             Difference]: With dead ends: 113
[2025-05-07 17:28:07,760 INFO  L226             Difference]: Without dead ends: 113
[2025-05-07 17:28:07,760 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:28:07,760 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.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:07,761 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.2s Time]
[2025-05-07 17:28:07,761 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-05-07 17:28:07,767 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 111.
[2025-05-07 17:28:07,768 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:28:07,769 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 135 transitions.
[2025-05-07 17:28:07,769 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 135 transitions. Word has length 58
[2025-05-07 17:28:07,769 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,769 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 135 transitions.
[2025-05-07 17:28:07,769 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:28:07,770 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 135 transitions.
[2025-05-07 17:28:07,771 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:28:07,771 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:07,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, 1, 1, 1]
[2025-05-07 17:28:07,771 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:07,771 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:07,771 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:07,771 INFO  L85        PathProgramCache]: Analyzing trace with hash -527012006, now seen corresponding path program 1 times
[2025-05-07 17:28:07,771 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:07,771 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1932828914]
[2025-05-07 17:28:07,771 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,771 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:07,795 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:28:07,804 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:28:07,804 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:07,804 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:07,871 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:07,871 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:07,871 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1932828914]
[2025-05-07 17:28:07,871 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1932828914] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:07,871 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:07,872 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:07,872 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [252644876]
[2025-05-07 17:28:07,872 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:07,872 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:07,872 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:07,873 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:07,873 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:07,873 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:28:07,907 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:07,907 INFO  L93              Difference]: Finished difference Result 116 states and 141 transitions.
[2025-05-07 17:28:07,907 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:07,908 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:28:07,908 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:07,909 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:28:07,909 INFO  L226             Difference]: Without dead ends: 116
[2025-05-07 17:28:07,909 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:07,910 INFO  L437           NwaCegarLoop]: 126 mSDtfsCounter, 1 mSDsluCounter, 488 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 614 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:28:07,911 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 614 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:07,911 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-05-07 17:28:07,921 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 116.
[2025-05-07 17:28:07,921 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:28:07,923 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 141 transitions.
[2025-05-07 17:28:07,923 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 141 transitions. Word has length 58
[2025-05-07 17:28:07,923 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:07,923 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 141 transitions.
[2025-05-07 17:28:07,923 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:28:07,923 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 141 transitions.
[2025-05-07 17:28:07,925 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-05-07 17:28:07,926 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:07,926 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:28:07,926 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:07,926 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:07,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:07,926 INFO  L85        PathProgramCache]: Analyzing trace with hash -573067730, now seen corresponding path program 1 times
[2025-05-07 17:28:07,927 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:07,927 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1410226002]
[2025-05-07 17:28:07,927 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:07,927 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:07,965 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-05-07 17:28:07,975 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-05-07 17:28:07,975 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:07,975 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,062 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:08,062 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,062 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1410226002]
[2025-05-07 17:28:08,063 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1410226002] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,063 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,063 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:08,063 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1738416965]
[2025-05-07 17:28:08,063 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,063 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:08,063 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,064 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:08,064 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:08,064 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:28:08,127 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:08,127 INFO  L93              Difference]: Finished difference Result 116 states and 140 transitions.
[2025-05-07 17:28:08,128 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:08,128 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:28:08,128 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:08,129 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:28:08,129 INFO  L226             Difference]: Without dead ends: 113
[2025-05-07 17:28:08,129 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:28:08,130 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:28:08,130 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:28:08,131 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-05-07 17:28:08,136 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 113.
[2025-05-07 17:28:08,136 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:28:08,137 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 134 transitions.
[2025-05-07 17:28:08,137 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 134 transitions. Word has length 72
[2025-05-07 17:28:08,137 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:08,137 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 134 transitions.
[2025-05-07 17:28:08,137 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:28:08,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 134 transitions.
[2025-05-07 17:28:08,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:28:08,138 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:08,139 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:28:08,139 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:08,139 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:08,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:08,139 INFO  L85        PathProgramCache]: Analyzing trace with hash -1219152724, now seen corresponding path program 1 times
[2025-05-07 17:28:08,139 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:08,139 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [220795601]
[2025-05-07 17:28:08,140 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:08,140 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:08,168 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:28:08,177 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:28:08,177 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,178 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,481 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:08,481 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,481 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [220795601]
[2025-05-07 17:28:08,481 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [220795601] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,481 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,481 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [] total 16
[2025-05-07 17:28:08,481 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1310345573]
[2025-05-07 17:28:08,481 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,482 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:28:08,482 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,482 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:28:08,483 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=211, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:28:08,483 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:28:08,732 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:08,732 INFO  L93              Difference]: Finished difference Result 121 states and 145 transitions.
[2025-05-07 17:28:08,732 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:28:08,733 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:28:08,733 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:08,734 INFO  L225             Difference]: With dead ends: 121
[2025-05-07 17:28:08,734 INFO  L226             Difference]: Without dead ends: 121
[2025-05-07 17:28:08,735 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:28:08,736 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:28:08,736 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:28:08,737 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-05-07 17:28:08,743 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 113.
[2025-05-07 17:28:08,743 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:28:08,744 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 134 transitions.
[2025-05-07 17:28:08,744 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 134 transitions. Word has length 75
[2025-05-07 17:28:08,744 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:08,744 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 134 transitions.
[2025-05-07 17:28:08,744 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:28:08,744 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 134 transitions.
[2025-05-07 17:28:08,745 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:28:08,745 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:08,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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:08,745 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:08,745 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:08,746 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:08,746 INFO  L85        PathProgramCache]: Analyzing trace with hash -1998637698, now seen corresponding path program 1 times
[2025-05-07 17:28:08,746 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:08,746 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [999301807]
[2025-05-07 17:28:08,746 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:08,746 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:08,772 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:28:08,782 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:28:08,782 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,783 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:08,890 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:08,890 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:08,891 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [999301807]
[2025-05-07 17:28:08,891 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [999301807] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:08,891 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:08,891 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:08,891 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [170586113]
[2025-05-07 17:28:08,891 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:08,891 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:08,891 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:08,892 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:08,892 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:08,892 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:28:08,922 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:08,922 INFO  L93              Difference]: Finished difference Result 118 states and 140 transitions.
[2025-05-07 17:28:08,923 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:08,923 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:28:08,923 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:08,924 INFO  L225             Difference]: With dead ends: 118
[2025-05-07 17:28:08,924 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:28:08,924 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:08,925 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:28:08,925 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:28:08,925 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:28:08,929 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 113.
[2025-05-07 17:28:08,930 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:28:08,930 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 134 transitions.
[2025-05-07 17:28:08,930 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 134 transitions. Word has length 75
[2025-05-07 17:28:08,931 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:08,931 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 134 transitions.
[2025-05-07 17:28:08,931 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:28:08,931 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 134 transitions.
[2025-05-07 17:28:08,932 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-05-07 17:28:08,932 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:08,932 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:28:08,932 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:08,932 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:08,932 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:08,932 INFO  L85        PathProgramCache]: Analyzing trace with hash -513377056, now seen corresponding path program 1 times
[2025-05-07 17:28:08,932 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:08,933 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [960837847]
[2025-05-07 17:28:08,933 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:08,933 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:08,959 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 75 statements into 1 equivalence classes.
[2025-05-07 17:28:08,971 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 75 of 75 statements.
[2025-05-07 17:28:08,971 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:08,971 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:09,284 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:09,285 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:09,285 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [960837847]
[2025-05-07 17:28:09,285 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [960837847] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:09,285 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:09,285 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:09,285 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [166037837]
[2025-05-07 17:28:09,285 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:09,286 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:09,286 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:09,286 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:09,286 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:09,287 INFO  L87              Difference]: Start difference. First operand 113 states and 134 transitions. Second operand  has 8 states, 6 states have (on average 5.5) internal successors, (33), 8 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 7 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:28:09,341 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:09,342 INFO  L93              Difference]: Finished difference Result 104 states and 119 transitions.
[2025-05-07 17:28:09,342 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:09,342 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 5.5) internal successors, (33), 8 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 7 states have call predecessors, (21), 5 states have call successors, (21) Word has length 75
[2025-05-07 17:28:09,343 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:09,343 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:28:09,344 INFO  L226             Difference]: Without dead ends: 101
[2025-05-07 17:28:09,344 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:09,344 INFO  L437           NwaCegarLoop]: 106 mSDtfsCounter, 0 mSDsluCounter, 514 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 620 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:09,345 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 620 Invalid, 35 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:09,345 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-05-07 17:28:09,349 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 101.
[2025-05-07 17:28:09,349 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 101 states, 42 states have (on average 1.0238095238095237) internal successors, (43), 43 states have internal predecessors, (43), 31 states have call successors, (34), 24 states have call predecessors, (34), 27 states have return successors, (37), 33 states have call predecessors, (37), 31 states have call successors, (37)
[2025-05-07 17:28:09,350 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 101 states to 101 states and 114 transitions.
[2025-05-07 17:28:09,350 INFO  L79                 Accepts]: Start accepts. Automaton has 101 states and 114 transitions. Word has length 75
[2025-05-07 17:28:09,350 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:09,350 INFO  L485      AbstractCegarLoop]: Abstraction has 101 states and 114 transitions.
[2025-05-07 17:28:09,350 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 5.5) internal successors, (33), 8 states have internal predecessors, (33), 5 states have call successors, (21), 1 states have call predecessors, (21), 6 states have return successors, (21), 7 states have call predecessors, (21), 5 states have call successors, (21)
[2025-05-07 17:28:09,351 INFO  L278                IsEmpty]: Start isEmpty. Operand 101 states and 114 transitions.
[2025-05-07 17:28:09,351 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:28:09,351 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:09,352 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:28:09,352 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:09,352 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:09,352 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:09,352 INFO  L85        PathProgramCache]: Analyzing trace with hash 2075161442, now seen corresponding path program 1 times
[2025-05-07 17:28:09,352 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:09,352 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1290783115]
[2025-05-07 17:28:09,352 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:09,353 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:09,390 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:28:09,406 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:28:09,406 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:09,407 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:09,524 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:28:09,524 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:09,525 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1290783115]
[2025-05-07 17:28:09,525 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1290783115] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:09,525 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:09,525 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:09,525 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [313410175]
[2025-05-07 17:28:09,525 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:09,525 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:09,525 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:09,526 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:09,526 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:09,526 INFO  L87              Difference]: Start difference. First operand 101 states and 114 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:28:09,558 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:09,558 INFO  L93              Difference]: Finished difference Result 106 states and 120 transitions.
[2025-05-07 17:28:09,559 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:09,559 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:28:09,559 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:09,560 INFO  L225             Difference]: With dead ends: 106
[2025-05-07 17:28:09,560 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:28:09,560 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:09,560 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 1 mSDsluCounter, 423 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 533 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:28:09,560 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 533 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:09,561 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:28:09,563 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:28:09,563 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 44 states have (on average 1.0227272727272727) internal successors, (45), 45 states have internal predecessors, (45), 32 states have call successors, (35), 24 states have call predecessors, (35), 29 states have return successors, (40), 36 states have call predecessors, (40), 32 states have call successors, (40)
[2025-05-07 17:28:09,564 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 120 transitions.
[2025-05-07 17:28:09,564 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 120 transitions. Word has length 90
[2025-05-07 17:28:09,564 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:09,564 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 120 transitions.
[2025-05-07 17:28:09,564 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:28:09,565 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 120 transitions.
[2025-05-07 17:28:09,565 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-05-07 17:28:09,565 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:09,565 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:28:09,566 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:09,566 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:09,566 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:09,566 INFO  L85        PathProgramCache]: Analyzing trace with hash -1878455006, now seen corresponding path program 1 times
[2025-05-07 17:28:09,566 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:09,566 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [17975982]
[2025-05-07 17:28:09,566 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:09,566 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:09,601 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-05-07 17:28:09,609 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-05-07 17:28:09,609 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:09,609 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:09,696 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:28:09,696 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:09,696 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [17975982]
[2025-05-07 17:28:09,696 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [17975982] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:09,696 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:09,696 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:09,696 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [694297872]
[2025-05-07 17:28:09,696 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:09,697 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:09,697 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:09,697 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:09,697 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:09,697 INFO  L87              Difference]: Start difference. First operand 106 states and 120 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:28:09,722 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:09,722 INFO  L93              Difference]: Finished difference Result 111 states and 125 transitions.
[2025-05-07 17:28:09,723 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:09,723 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:28:09,723 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:09,723 INFO  L225             Difference]: With dead ends: 111
[2025-05-07 17:28:09,723 INFO  L226             Difference]: Without dead ends: 101
[2025-05-07 17:28:09,724 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:09,724 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 421 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 530 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:28:09,724 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 530 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:09,725 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-05-07 17:28:09,726 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 101.
[2025-05-07 17:28:09,727 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 101 states, 42 states have (on average 1.0238095238095237) internal successors, (43), 43 states have internal predecessors, (43), 30 states have call successors, (32), 23 states have call predecessors, (32), 28 states have return successors, (37), 34 states have call predecessors, (37), 30 states have call successors, (37)
[2025-05-07 17:28:09,727 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 101 states to 101 states and 112 transitions.
[2025-05-07 17:28:09,727 INFO  L79                 Accepts]: Start accepts. Automaton has 101 states and 112 transitions. Word has length 90
[2025-05-07 17:28:09,727 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:09,727 INFO  L485      AbstractCegarLoop]: Abstraction has 101 states and 112 transitions.
[2025-05-07 17:28:09,728 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:28:09,728 INFO  L278                IsEmpty]: Start isEmpty. Operand 101 states and 112 transitions.
[2025-05-07 17:28:09,728 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 108
[2025-05-07 17:28:09,728 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:09,729 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:28:09,729 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:09,729 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:09,729 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:09,729 INFO  L85        PathProgramCache]: Analyzing trace with hash -559131904, now seen corresponding path program 1 times
[2025-05-07 17:28:09,729 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:09,729 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [158887392]
[2025-05-07 17:28:09,729 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:09,729 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:09,770 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:28:09,779 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:28:09,780 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:09,780 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:09,872 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:28:09,872 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:09,873 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [158887392]
[2025-05-07 17:28:09,873 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [158887392] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:09,873 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:09,873 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:09,873 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1842512510]
[2025-05-07 17:28:09,873 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:09,873 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:09,873 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:09,874 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:09,874 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:09,874 INFO  L87              Difference]: Start difference. First operand 101 states and 112 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:28:09,906 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:09,906 INFO  L93              Difference]: Finished difference Result 101 states and 111 transitions.
[2025-05-07 17:28:09,906 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:09,907 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:28:09,907 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:09,907 INFO  L225             Difference]: With dead ends: 101
[2025-05-07 17:28:09,907 INFO  L226             Difference]: Without dead ends: 101
[2025-05-07 17:28:09,908 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:09,908 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 1 mSDsluCounter, 394 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 497 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:28:09,908 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 497 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:09,908 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-05-07 17:28:09,910 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 96.
[2025-05-07 17:28:09,910 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 96 states, 40 states have (on average 1.025) internal successors, (41), 41 states have internal predecessors, (41), 29 states have call successors, (31), 23 states have call predecessors, (31), 26 states have return successors, (33), 31 states have call predecessors, (33), 29 states have call successors, (33)
[2025-05-07 17:28:09,911 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 96 states to 96 states and 105 transitions.
[2025-05-07 17:28:09,911 INFO  L79                 Accepts]: Start accepts. Automaton has 96 states and 105 transitions. Word has length 107
[2025-05-07 17:28:09,911 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:09,911 INFO  L485      AbstractCegarLoop]: Abstraction has 96 states and 105 transitions.
[2025-05-07 17:28:09,912 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:28:09,912 INFO  L278                IsEmpty]: Start isEmpty. Operand 96 states and 105 transitions.
[2025-05-07 17:28:09,912 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 108
[2025-05-07 17:28:09,912 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:09,913 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:28:09,913 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:09,913 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:09,913 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:09,913 INFO  L85        PathProgramCache]: Analyzing trace with hash 1975084882, now seen corresponding path program 1 times
[2025-05-07 17:28:09,913 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:09,913 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [224264852]
[2025-05-07 17:28:09,913 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:09,913 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:09,957 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:28:09,975 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:28:09,975 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:09,975 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:10,454 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:28:10,455 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:10,455 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [224264852]
[2025-05-07 17:28:10,455 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [224264852] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:10,455 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [200695895]
[2025-05-07 17:28:10,455 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:10,455 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:10,457 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:10,459 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:10,460 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:28:10,784 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 107 statements into 1 equivalence classes.
[2025-05-07 17:28:10,966 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 107 of 107 statements.
[2025-05-07 17:28:10,967 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:10,967 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:10,973 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1790 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:10,981 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:11,090 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 22 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:28:11,090 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:11,091 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [200695895] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:11,091 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:11,091 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [20] total 24
[2025-05-07 17:28:11,091 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1026177063]
[2025-05-07 17:28:11,091 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:11,091 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:11,091 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:11,092 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:11,092 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=507, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:28:11,093 INFO  L87              Difference]: Start difference. First operand 96 states and 105 transitions. Second operand  has 6 states, 5 states have (on average 9.2) internal successors, (46), 6 states have internal predecessors, (46), 5 states have call successors, (30), 2 states have call predecessors, (30), 5 states have return successors, (30), 5 states have call predecessors, (30), 5 states have call successors, (30)
[2025-05-07 17:28:11,116 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:11,116 INFO  L93              Difference]: Finished difference Result 101 states and 110 transitions.
[2025-05-07 17:28:11,117 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:11,117 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.2) internal successors, (46), 6 states have internal predecessors, (46), 5 states have call successors, (30), 2 states have call predecessors, (30), 5 states have return successors, (30), 5 states have call predecessors, (30), 5 states have call successors, (30) Word has length 107
[2025-05-07 17:28:11,117 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:11,118 INFO  L225             Difference]: With dead ends: 101
[2025-05-07 17:28:11,118 INFO  L226             Difference]: Without dead ends: 91
[2025-05-07 17:28:11,118 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 129 GetRequests, 107 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:28:11,119 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 1 mSDsluCounter, 379 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 477 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:11,119 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 477 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:11,119 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-05-07 17:28:11,122 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 91.
[2025-05-07 17:28:11,122 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:28:11,123 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 97 transitions.
[2025-05-07 17:28:11,123 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 97 transitions. Word has length 107
[2025-05-07 17:28:11,123 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:11,123 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 97 transitions.
[2025-05-07 17:28:11,124 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.2) internal successors, (46), 6 states have internal predecessors, (46), 5 states have call successors, (30), 2 states have call predecessors, (30), 5 states have return successors, (30), 5 states have call predecessors, (30), 5 states have call successors, (30)
[2025-05-07 17:28:11,124 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 97 transitions.
[2025-05-07 17:28:11,124 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 125
[2025-05-07 17:28:11,125 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:11,125 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:28:11,132 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:28:11,325 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:28:11,326 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:11,326 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:11,327 INFO  L85        PathProgramCache]: Analyzing trace with hash 591931008, now seen corresponding path program 1 times
[2025-05-07 17:28:11,327 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:11,327 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1064493361]
[2025-05-07 17:28:11,327 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:11,327 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:11,484 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 124 statements into 1 equivalence classes.
[2025-05-07 17:28:11,506 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 124 of 124 statements.
[2025-05-07 17:28:11,506 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:11,506 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:12,022 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:28:12,022 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:12,022 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1064493361]
[2025-05-07 17:28:12,022 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1064493361] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:12,022 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [545450492]
[2025-05-07 17:28:12,022 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:12,022 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:12,025 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:12,026 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:12,027 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:28:12,381 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 124 statements into 1 equivalence classes.
[2025-05-07 17:28:12,585 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 124 of 124 statements.
[2025-05-07 17:28:12,585 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:12,585 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:12,591 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2126 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:12,595 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:12,666 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:28:12,666 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:12,666 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [545450492] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:12,666 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:12,666 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [20] total 24
[2025-05-07 17:28:12,666 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [590145114]
[2025-05-07 17:28:12,666 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:12,666 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:12,666 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:12,667 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:12,667 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=507, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:28:12,667 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:28:12,684 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:12,684 INFO  L93              Difference]: Finished difference Result 59 states and 62 transitions.
[2025-05-07 17:28:12,684 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:12,685 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:28:12,685 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:12,685 INFO  L225             Difference]: With dead ends: 59
[2025-05-07 17:28:12,685 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:12,685 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:28:12,685 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:28:12,685 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:28:12,686 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:12,686 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:12,686 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:28:12,686 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:12,686 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 124
[2025-05-07 17:28:12,686 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:12,686 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:12,686 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:28:12,686 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:12,686 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:12,688 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:12,694 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:28:12,888 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:12,891 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:12,892 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:12,894 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:12 BoogieIcfgContainer
[2025-05-07 17:28:12,894 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:12,895 INFO  L158              Benchmark]: Toolchain (without parser) took 7108.58ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 140.5MB in the beginning and 217.5MB in the end (delta: -77.0MB). Peak memory consumption was 70.4MB. Max. memory is 33.6GB.
[2025-05-07 17:28:12,895 INFO  L158              Benchmark]: SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 173.0MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:12,895 INFO  L158              Benchmark]: ChcToBoogie took 34.27ms. Allocated memory is still 234.9MB. Free memory was 140.5MB in the beginning and 136.9MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:12,895 INFO  L158              Benchmark]: Boogie Preprocessor took 56.09ms. Allocated memory is still 234.9MB. Free memory was 136.9MB in the beginning and 132.9MB in the end (delta: 4.0MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:12,895 INFO  L158              Benchmark]: RCFGBuilder took 454.00ms. Allocated memory is still 234.9MB. Free memory was 132.7MB in the beginning and 154.9MB in the end (delta: -22.2MB). Peak memory consumption was 25.9MB. Max. memory is 33.6GB.
[2025-05-07 17:28:12,895 INFO  L158              Benchmark]: TraceAbstraction took 6561.02ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 154.4MB in the beginning and 217.5MB in the end (delta: -63.1MB). Peak memory consumption was 61.2MB. Max. memory is 33.6GB.
[2025-05-07 17:28:12,896 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 173.0MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 34.27ms. Allocated memory is still 234.9MB. Free memory was 140.5MB in the beginning and 136.9MB in the end (delta: 3.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 56.09ms. Allocated memory is still 234.9MB. Free memory was 136.9MB in the beginning and 132.9MB in the end (delta: 4.0MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 454.00ms. Allocated memory is still 234.9MB. Free memory was 132.7MB in the beginning and 154.9MB in the end (delta: -22.2MB). Peak memory consumption was 25.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 6561.02ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 154.4MB in the beginning and 217.5MB in the end (delta: -63.1MB). Peak memory consumption was 61.2MB. 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: 6.5s, OverallIterations: 13, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 43 SdHoareTripleChecker+Valid, 0.8s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 17 mSDsluCounter, 8887 SdHoareTripleChecker+Invalid, 0.7s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 7466 mSDsCounter, 4 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 772 IncrementalHoareTripleChecker+Invalid, 776 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 4 mSolverCounterUnsat, 1421 mSDtfsCounter, 772 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 367 GetRequests, 253 SyntacticMatches, 0 SemanticMatches, 114 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.7s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=116occurred in iteration=4, InterpolantAutomatonStates: 98, 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, 13 MinimizatonAttempts, 24 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.3s SsaConstructionTime, 0.6s SatisfiabilityAnalysisTime, 3.0s InterpolantComputationTime, 1272 NumberOfCodeBlocks, 1272 NumberOfCodeBlocksAsserted, 15 NumberOfCheckSat, 1257 ConstructedInterpolants, 0 QuantifiedInterpolants, 1813 SizeOfPredicates, 0 NumberOfNonLiveVariables, 3916 ConjunctsInSsa, 10 ConjunctsInUnsatCore, 15 InterpolantComputations, 13 PerfectInterpolantSequences, 202/212 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:28:12,905 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
