./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_value_3.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:29:22,832 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:29:22,902 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f8c2415e-ff15-4720-953d-9cec2a7e5db2/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:29:22,907 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:29:22,907 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:29:22,928 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:29:22,929 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:29:22,929 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:29:22,930 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:29:22,930 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:29:22,930 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:29:22,930 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:29:22,930 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:29:22,930 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:29:22,930 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:29:22,931 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:22,931 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:29:22,931 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:29:22,932 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:29:22,932 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:29:22,932 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:29:23,111 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:29:23,116 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:29:23,118 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:29:23,119 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:29:23,119 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:29:23,120 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f8c2415e-ff15-4720-953d-9cec2a7e5db2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_value_3.sol_0_no_adts_000.smt2
[2025-05-07 17:29:23,121 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:29:23,123 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:29:23,323 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f8c2415e-ff15-4720-953d-9cec2a7e5db2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_value_3.sol_0_no_adts_000.smt2
[2025-05-07 17:29:23,326 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:29:23,327 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:29:23,327 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:29:23,327 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:29:23,327 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:29:23,329 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,357 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23 Unit
[2025-05-07 17:29:23,357 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:29:23,358 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:29:23,358 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:29:23,358 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:29:23,369 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,369 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,390 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,390 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,394 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,394 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,396 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,397 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,399 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,408 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:29:23,409 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:29:23,409 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:29:23,409 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:29:23,410 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (1/1) ...
[2025-05-07 17:29:23,412 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:23,420 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:23,428 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:29:23,430 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:29:23,441 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:29:23,441 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:29:23,441 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:29:23,441 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_3_0 given in one single declaration
[2025-05-07 17:29:23,441 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_3_0
[2025-05-07 17:29:23,441 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_3_0
[2025-05-07 17:29:23,441 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__18_36_0 given in one single declaration
[2025-05-07 17:29:23,441 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__18_36_0
[2025-05-07 17:29:23,441 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__18_36_0
[2025-05-07 17:29:23,441 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_f__18_36_0 given in one single declaration
[2025-05-07 17:29:23,441 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_f__18_36_0
[2025-05-07 17:29:23,441 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_f__18_36_0
[2025-05-07 17:29:23,441 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__18_36_0 given in one single declaration
[2025-05-07 17:29:23,441 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__18_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__18_36_0
[2025-05-07 17:29:23,442 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__18_36_0 given in one single declaration
[2025-05-07 17:29:23,442 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__18_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__18_36_0
[2025-05-07 17:29:23,442 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_17_36_0 given in one single declaration
[2025-05-07 17:29:23,442 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_17_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_17_36_0
[2025-05-07 17:29:23,442 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__18_36_0 given in one single declaration
[2025-05-07 17:29:23,442 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__18_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__18_36_0
[2025-05-07 17:29:23,442 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,442 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_g__35_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_g__35_36_0
[2025-05-07 17:29:23,442 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,442 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_g__35_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_g__35_36_0
[2025-05-07 17:29:23,442 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_return_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,442 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_return_function_g__35_36_0
[2025-05-07 17:29:23,442 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_return_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_g_34_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_g_34_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_g_34_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_g__35_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_g__35_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_36_0
[2025-05-07 17:29:23,443 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_36_0 given in one single declaration
[2025-05-07 17:29:23,443 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_36_0
[2025-05-07 17:29:23,443 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_36_0
[2025-05-07 17:29:23,444 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_20_C_36_0 given in one single declaration
[2025-05-07 17:29:23,444 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_20_C_36_0
[2025-05-07 17:29:23,444 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_20_C_36_0
[2025-05-07 17:29:23,444 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_17_C_36_0 given in one single declaration
[2025-05-07 17:29:23,444 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_17_C_36_0
[2025-05-07 17:29:23,444 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_17_C_36_0
[2025-05-07 17:29:23,444 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_19_C_36_0 given in one single declaration
[2025-05-07 17:29:23,444 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_19_C_36_0
[2025-05-07 17:29:23,444 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_19_C_36_0
[2025-05-07 17:29:23,444 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_18_C_36_0 given in one single declaration
[2025-05-07 17:29:23,444 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_18_C_36_0
[2025-05-07 17:29:23,444 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_18_C_36_0
[2025-05-07 17:29:23,444 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:29:23,444 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:29:23,444 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:29:23,560 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:29:23,562 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:29:23,793 INFO  L?                        ?]: Removed 180 outVars from TransFormulas that were not future-live.
[2025-05-07 17:29:23,794 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:29:23,805 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:29:23,805 INFO  L312             CfgBuilder]: Removed 10 assume(true) statements.
[2025-05-07 17:29:23,806 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:23 BoogieIcfgContainer
[2025-05-07 17:29:23,806 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:29:23,808 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:29:23,808 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:29:23,812 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:29:23,812 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:23" (1/3) ...
[2025-05-07 17:29:23,813 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7ef9b9eb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:29:23, skipping insertion in model container
[2025-05-07 17:29:23,813 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:23" (2/3) ...
[2025-05-07 17:29:23,813 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7ef9b9eb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:29:23, skipping insertion in model container
[2025-05-07 17:29:23,813 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:23" (3/3) ...
[2025-05-07 17:29:23,814 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:29:23,829 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:29:23,831 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 23 procedures, 93 locations, 142 edges, 23 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:29:23,871 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:29:23,882 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;@27d5bebf, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:29:23,882 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:29:23,886 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 93 states, 38 states have (on average 1.131578947368421) internal successors, (43), 43 states have internal predecessors, (43), 32 states have call successors, (33), 22 states have call predecessors, (33), 22 states have return successors, (33), 27 states have call predecessors, (33), 32 states have call successors, (33)
[2025-05-07 17:29:23,895 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-05-07 17:29:23,895 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:23,896 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]
[2025-05-07 17:29:23,896 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:23,900 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:23,900 INFO  L85        PathProgramCache]: Analyzing trace with hash 183057033, now seen corresponding path program 1 times
[2025-05-07 17:29:23,905 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:23,905 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2143522736]
[2025-05-07 17:29:23,905 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:23,906 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:23,959 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-05-07 17:29:24,011 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-05-07 17:29:24,012 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:24,012 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:24,637 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:24,637 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:24,638 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2143522736]
[2025-05-07 17:29:24,638 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2143522736] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:24,638 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:24,641 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:29:24,642 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [719343740]
[2025-05-07 17:29:24,643 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:24,646 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:24,647 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:24,667 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:24,668 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=132, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:29:24,669 INFO  L87              Difference]: Start difference. First operand  has 93 states, 38 states have (on average 1.131578947368421) internal successors, (43), 43 states have internal predecessors, (43), 32 states have call successors, (33), 22 states have call predecessors, (33), 22 states have return successors, (33), 27 states have call predecessors, (33), 32 states have call successors, (33) Second operand  has 13 states, 10 states have (on average 2.4) internal successors, (24), 12 states have internal predecessors, (24), 7 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14)
[2025-05-07 17:29:24,920 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:24,920 INFO  L93              Difference]: Finished difference Result 102 states and 126 transitions.
[2025-05-07 17:29:24,921 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:24,922 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 2.4) internal successors, (24), 12 states have internal predecessors, (24), 7 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14) Word has length 52
[2025-05-07 17:29:24,923 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:24,931 INFO  L225             Difference]: With dead ends: 102
[2025-05-07 17:29:24,931 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:29:24,933 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=154, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:29:24,936 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 3 mSDsluCounter, 948 mSDsCounter, 0 mSdLazyCounter, 195 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1046 SdHoareTripleChecker+Invalid, 197 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 195 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:24,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1046 Invalid, 197 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 195 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:29:24,950 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:29:24,977 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 99.
[2025-05-07 17:29:24,978 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 40 states have (on average 1.1) internal successors, (44), 44 states have internal predecessors, (44), 34 states have call successors, (35), 22 states have call predecessors, (35), 25 states have return successors, (43), 32 states have call predecessors, (43), 34 states have call successors, (43)
[2025-05-07 17:29:24,983 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 122 transitions.
[2025-05-07 17:29:24,984 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 122 transitions. Word has length 52
[2025-05-07 17:29:24,984 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:24,985 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 122 transitions.
[2025-05-07 17:29:24,985 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 2.4) internal successors, (24), 12 states have internal predecessors, (24), 7 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14)
[2025-05-07 17:29:24,985 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 122 transitions.
[2025-05-07 17:29:24,987 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-05-07 17:29:24,987 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:24,988 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]
[2025-05-07 17:29:24,988 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:29:24,988 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:24,989 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:24,989 INFO  L85        PathProgramCache]: Analyzing trace with hash 2146094265, now seen corresponding path program 1 times
[2025-05-07 17:29:24,989 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:24,989 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [13573965]
[2025-05-07 17:29:24,989 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:24,989 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,021 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-05-07 17:29:25,040 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-05-07 17:29:25,040 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,040 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,404 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:25,404 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,404 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [13573965]
[2025-05-07 17:29:25,404 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [13573965] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:25,404 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:25,404 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:29:25,404 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1419068930]
[2025-05-07 17:29:25,405 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:25,406 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:25,406 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:25,406 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:25,407 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=132, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:29:25,407 INFO  L87              Difference]: Start difference. First operand 99 states and 122 transitions. Second operand  has 13 states, 10 states have (on average 2.4) internal successors, (24), 12 states have internal predecessors, (24), 7 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14)
[2025-05-07 17:29:25,578 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:25,578 INFO  L93              Difference]: Finished difference Result 102 states and 125 transitions.
[2025-05-07 17:29:25,578 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:25,578 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 2.4) internal successors, (24), 12 states have internal predecessors, (24), 7 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14) Word has length 52
[2025-05-07 17:29:25,579 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:25,579 INFO  L225             Difference]: With dead ends: 102
[2025-05-07 17:29:25,579 INFO  L226             Difference]: Without dead ends: 101
[2025-05-07 17:29:25,580 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=154, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:29:25,580 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 3 mSDsluCounter, 948 mSDsCounter, 0 mSdLazyCounter, 185 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 1046 SdHoareTripleChecker+Invalid, 187 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 185 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:25,580 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 1046 Invalid, 187 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 185 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:25,581 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-05-07 17:29:25,586 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 93.
[2025-05-07 17:29:25,586 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 38 states have (on average 1.105263157894737) internal successors, (42), 42 states have internal predecessors, (42), 32 states have call successors, (33), 22 states have call predecessors, (33), 23 states have return successors, (36), 28 states have call predecessors, (36), 32 states have call successors, (36)
[2025-05-07 17:29:25,587 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 111 transitions.
[2025-05-07 17:29:25,587 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 111 transitions. Word has length 52
[2025-05-07 17:29:25,587 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:25,587 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 111 transitions.
[2025-05-07 17:29:25,587 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 2.4) internal successors, (24), 12 states have internal predecessors, (24), 7 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14)
[2025-05-07 17:29:25,587 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 111 transitions.
[2025-05-07 17:29:25,588 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-05-07 17:29:25,589 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:25,589 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:25,589 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:25,589 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:25,589 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:25,589 INFO  L85        PathProgramCache]: Analyzing trace with hash 822815101, now seen corresponding path program 1 times
[2025-05-07 17:29:25,589 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:25,589 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2134465275]
[2025-05-07 17:29:25,590 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,590 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,615 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-05-07 17:29:25,628 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-05-07 17:29:25,628 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,628 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,705 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:25,705 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,705 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2134465275]
[2025-05-07 17:29:25,705 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2134465275] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:25,705 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:25,705 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:25,705 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1725913812]
[2025-05-07 17:29:25,705 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:25,706 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:25,706 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:25,706 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:25,706 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:25,707 INFO  L87              Difference]: Start difference. First operand 93 states and 111 transitions. Second operand  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:29:25,748 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:25,749 INFO  L93              Difference]: Finished difference Result 98 states and 117 transitions.
[2025-05-07 17:29:25,749 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:25,749 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 4 states have call successors, (19) Word has length 69
[2025-05-07 17:29:25,750 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:25,751 INFO  L225             Difference]: With dead ends: 98
[2025-05-07 17:29:25,751 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:29:25,751 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:25,751 INFO  L437           NwaCegarLoop]: 105 mSDtfsCounter, 1 mSDsluCounter, 405 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 510 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:25,752 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 510 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:25,752 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:29:25,756 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:29:25,757 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 40 states have (on average 1.1) internal successors, (44), 44 states have internal predecessors, (44), 33 states have call successors, (34), 22 states have call predecessors, (34), 25 states have return successors, (39), 31 states have call predecessors, (39), 33 states have call successors, (39)
[2025-05-07 17:29:25,757 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 117 transitions.
[2025-05-07 17:29:25,757 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 117 transitions. Word has length 69
[2025-05-07 17:29:25,758 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:25,758 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 117 transitions.
[2025-05-07 17:29:25,758 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.2) internal successors, (31), 6 states have internal predecessors, (31), 4 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 6 states have call predecessors, (19), 4 states have call successors, (19)
[2025-05-07 17:29:25,758 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 117 transitions.
[2025-05-07 17:29:25,761 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 78
[2025-05-07 17:29:25,761 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:25,761 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:25,762 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:25,762 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:25,762 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:25,762 INFO  L85        PathProgramCache]: Analyzing trace with hash 1048712877, now seen corresponding path program 1 times
[2025-05-07 17:29:25,762 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:25,762 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1501290976]
[2025-05-07 17:29:25,762 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,763 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,791 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 77 statements into 1 equivalence classes.
[2025-05-07 17:29:25,797 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 77 of 77 statements.
[2025-05-07 17:29:25,797 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,797 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,257 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 2 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-05-07 17:29:26,257 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:26,257 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1501290976]
[2025-05-07 17:29:26,257 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1501290976] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:26,257 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1728567883]
[2025-05-07 17:29:26,257 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,258 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:26,260 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:26,262 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:26,263 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:29:26,467 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 77 statements into 1 equivalence classes.
[2025-05-07 17:29:26,587 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 77 of 77 statements.
[2025-05-07 17:29:26,588 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:26,588 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,592 INFO  L256         TraceCheckSpWp]: Trace formula consists of 949 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:26,598 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:26,695 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 22 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:29:26,695 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:29:26,696 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1728567883] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:26,696 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:29:26,696 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [13] total 15
[2025-05-07 17:29:26,696 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1940019372]
[2025-05-07 17:29:26,696 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:26,696 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:26,696 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:26,697 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:26,697 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=180, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:29:26,698 INFO  L87              Difference]: Start difference. First operand 98 states and 117 transitions. Second operand  has 13 states, 10 states have (on average 3.5) internal successors, (35), 12 states have internal predecessors, (35), 8 states have call successors, (21), 2 states have call predecessors, (21), 10 states have return successors, (21), 11 states have call predecessors, (21), 8 states have call successors, (21)
[2025-05-07 17:29:26,894 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,894 INFO  L93              Difference]: Finished difference Result 107 states and 135 transitions.
[2025-05-07 17:29:26,895 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:26,895 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 3.5) internal successors, (35), 12 states have internal predecessors, (35), 8 states have call successors, (21), 2 states have call predecessors, (21), 10 states have return successors, (21), 11 states have call predecessors, (21), 8 states have call successors, (21) Word has length 77
[2025-05-07 17:29:26,895 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,897 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:29:26,897 INFO  L226             Difference]: Without dead ends: 107
[2025-05-07 17:29:26,897 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 91 GetRequests, 76 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=39, Invalid=233, Unknown=0, NotChecked=0, Total=272
[2025-05-07 17:29:26,898 INFO  L437           NwaCegarLoop]: 99 mSDtfsCounter, 4 mSDsluCounter, 1051 mSDsCounter, 0 mSdLazyCounter, 202 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 1150 SdHoareTripleChecker+Invalid, 205 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 202 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:26,898 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 1150 Invalid, 205 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 202 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:29:26,899 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-05-07 17:29:26,907 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 104.
[2025-05-07 17:29:26,908 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 104 states, 42 states have (on average 1.0952380952380953) internal successors, (46), 46 states have internal predecessors, (46), 35 states have call successors, (36), 22 states have call predecessors, (36), 27 states have return successors, (45), 35 states have call predecessors, (45), 35 states have call successors, (45)
[2025-05-07 17:29:26,909 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 104 states to 104 states and 127 transitions.
[2025-05-07 17:29:26,909 INFO  L79                 Accepts]: Start accepts. Automaton has 104 states and 127 transitions. Word has length 77
[2025-05-07 17:29:26,909 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,909 INFO  L485      AbstractCegarLoop]: Abstraction has 104 states and 127 transitions.
[2025-05-07 17:29:26,910 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 3.5) internal successors, (35), 12 states have internal predecessors, (35), 8 states have call successors, (21), 2 states have call predecessors, (21), 10 states have return successors, (21), 11 states have call predecessors, (21), 8 states have call successors, (21)
[2025-05-07 17:29:26,910 INFO  L278                IsEmpty]: Start isEmpty. Operand 104 states and 127 transitions.
[2025-05-07 17:29:26,911 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 78
[2025-05-07 17:29:26,911 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,911 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:29:26,916 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:29:27,112 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:27,113 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,114 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,114 INFO  L85        PathProgramCache]: Analyzing trace with hash -601420163, now seen corresponding path program 1 times
[2025-05-07 17:29:27,115 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,115 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2107030897]
[2025-05-07 17:29:27,115 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,116 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,246 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 77 statements into 1 equivalence classes.
[2025-05-07 17:29:27,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 77 of 77 statements.
[2025-05-07 17:29:27,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,688 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 2 proven. 9 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:29:27,688 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,688 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2107030897]
[2025-05-07 17:29:27,688 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2107030897] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:27,688 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [538471893]
[2025-05-07 17:29:27,688 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,688 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:27,690 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:27,692 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:27,693 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:29:27,883 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 77 statements into 1 equivalence classes.
[2025-05-07 17:29:27,989 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 77 of 77 statements.
[2025-05-07 17:29:27,989 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,989 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,993 INFO  L256         TraceCheckSpWp]: Trace formula consists of 950 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:27,995 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:28,061 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 18 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:29:28,061 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:29:28,062 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [538471893] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,062 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:29:28,062 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [13] total 15
[2025-05-07 17:29:28,062 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [919728453]
[2025-05-07 17:29:28,062 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,062 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:28,062 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,063 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:28,063 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=180, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:29:28,064 INFO  L87              Difference]: Start difference. First operand 104 states and 127 transitions. Second operand  has 13 states, 10 states have (on average 3.5) internal successors, (35), 12 states have internal predecessors, (35), 8 states have call successors, (21), 2 states have call predecessors, (21), 10 states have return successors, (21), 11 states have call predecessors, (21), 8 states have call successors, (21)
[2025-05-07 17:29:28,219 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,219 INFO  L93              Difference]: Finished difference Result 107 states and 134 transitions.
[2025-05-07 17:29:28,220 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:28,220 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 3.5) internal successors, (35), 12 states have internal predecessors, (35), 8 states have call successors, (21), 2 states have call predecessors, (21), 10 states have return successors, (21), 11 states have call predecessors, (21), 8 states have call successors, (21) Word has length 77
[2025-05-07 17:29:28,220 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,221 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:29:28,221 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:29:28,221 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 91 GetRequests, 76 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=39, Invalid=233, Unknown=0, NotChecked=0, Total=272
[2025-05-07 17:29:28,221 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 3 mSDsluCounter, 1089 mSDsCounter, 0 mSdLazyCounter, 178 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 1192 SdHoareTripleChecker+Invalid, 180 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 178 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,221 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 1192 Invalid, 180 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 178 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:28,222 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:29:28,226 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 98.
[2025-05-07 17:29:28,226 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 40 states have (on average 1.1) internal successors, (44), 44 states have internal predecessors, (44), 33 states have call successors, (34), 22 states have call predecessors, (34), 25 states have return successors, (38), 31 states have call predecessors, (38), 33 states have call successors, (38)
[2025-05-07 17:29:28,227 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 116 transitions.
[2025-05-07 17:29:28,227 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 116 transitions. Word has length 77
[2025-05-07 17:29:28,227 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,227 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 116 transitions.
[2025-05-07 17:29:28,227 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 3.5) internal successors, (35), 12 states have internal predecessors, (35), 8 states have call successors, (21), 2 states have call predecessors, (21), 10 states have return successors, (21), 11 states have call predecessors, (21), 8 states have call successors, (21)
[2025-05-07 17:29:28,227 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 116 transitions.
[2025-05-07 17:29:28,228 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:29:28,228 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,228 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,232 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:29:28,429 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:28,429 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,430 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,430 INFO  L85        PathProgramCache]: Analyzing trace with hash 130709888, now seen corresponding path program 1 times
[2025-05-07 17:29:28,431 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,431 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [124252450]
[2025-05-07 17:29:28,431 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,431 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,495 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:29:28,505 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:29:28,505 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,505 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,595 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,596 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,596 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [124252450]
[2025-05-07 17:29:28,596 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [124252450] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,596 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,596 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:29:28,596 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1297178449]
[2025-05-07 17:29:28,596 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,596 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:29:28,597 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,597 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:29:28,597 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:29:28,597 INFO  L87              Difference]: Start difference. First operand 98 states and 116 transitions. Second operand  has 8 states, 6 states have (on average 5.0) internal successors, (30), 8 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:29:28,671 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,672 INFO  L93              Difference]: Finished difference Result 102 states and 121 transitions.
[2025-05-07 17:29:28,672 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:29:28,672 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 5.0) internal successors, (30), 8 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18) Word has length 66
[2025-05-07 17:29:28,673 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,674 INFO  L225             Difference]: With dead ends: 102
[2025-05-07 17:29:28,674 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:29:28,674 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:29:28,674 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 2 mSDsluCounter, 593 mSDsCounter, 0 mSdLazyCounter, 55 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 695 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 55 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,675 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 695 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 55 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:28,676 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:29:28,681 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:29:28,682 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 42 states have (on average 1.0952380952380953) internal successors, (46), 46 states have internal predecessors, (46), 33 states have call successors, (34), 22 states have call predecessors, (34), 27 states have return successors, (41), 33 states have call predecessors, (41), 33 states have call successors, (41)
[2025-05-07 17:29:28,682 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 121 transitions.
[2025-05-07 17:29:28,683 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 121 transitions. Word has length 66
[2025-05-07 17:29:28,683 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,683 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 121 transitions.
[2025-05-07 17:29:28,683 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 5.0) internal successors, (30), 8 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:29:28,683 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 121 transitions.
[2025-05-07 17:29:28,684 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:29:28,684 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,684 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,684 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:29:28,684 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,685 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,685 INFO  L85        PathProgramCache]: Analyzing trace with hash -641160880, now seen corresponding path program 1 times
[2025-05-07 17:29:28,685 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,685 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [178050470]
[2025-05-07 17:29:28,685 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,685 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,707 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:29:28,731 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:29:28,731 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,731 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,854 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,854 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,854 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [178050470]
[2025-05-07 17:29:28,854 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [178050470] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,855 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,855 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:28,855 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1976575561]
[2025-05-07 17:29:28,855 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,855 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:28,855 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,856 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:28,856 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,856 INFO  L87              Difference]: Start difference. First operand 102 states and 121 transitions. Second operand  has 7 states, 6 states have (on average 5.0) internal successors, (30), 7 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:29:28,906 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,906 INFO  L93              Difference]: Finished difference Result 99 states and 115 transitions.
[2025-05-07 17:29:28,906 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:28,907 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.0) internal successors, (30), 7 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18) Word has length 66
[2025-05-07 17:29:28,907 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,908 INFO  L225             Difference]: With dead ends: 99
[2025-05-07 17:29:28,908 INFO  L226             Difference]: Without dead ends: 93
[2025-05-07 17:29:28,908 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:29:28,908 INFO  L437           NwaCegarLoop]: 102 mSDtfsCounter, 1 mSDsluCounter, 494 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 596 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.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,909 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 596 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,909 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-05-07 17:29:28,913 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 89.
[2025-05-07 17:29:28,914 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 89 states, 37 states have (on average 1.0810810810810811) internal successors, (40), 40 states have internal predecessors, (40), 28 states have call successors, (29), 22 states have call predecessors, (29), 23 states have return successors, (30), 26 states have call predecessors, (30), 28 states have call successors, (30)
[2025-05-07 17:29:28,915 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 89 states to 89 states and 99 transitions.
[2025-05-07 17:29:28,915 INFO  L79                 Accepts]: Start accepts. Automaton has 89 states and 99 transitions. Word has length 66
[2025-05-07 17:29:28,915 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,915 INFO  L485      AbstractCegarLoop]: Abstraction has 89 states and 99 transitions.
[2025-05-07 17:29:28,915 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.0) internal successors, (30), 7 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:29:28,915 INFO  L278                IsEmpty]: Start isEmpty. Operand 89 states and 99 transitions.
[2025-05-07 17:29:28,916 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 95
[2025-05-07 17:29:28,916 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,916 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:29:28,916 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:29:28,917 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,917 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,917 INFO  L85        PathProgramCache]: Analyzing trace with hash 642257425, now seen corresponding path program 1 times
[2025-05-07 17:29:28,917 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,917 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [133536448]
[2025-05-07 17:29:28,917 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,917 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,949 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 94 statements into 1 equivalence classes.
[2025-05-07 17:29:28,965 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 94 of 94 statements.
[2025-05-07 17:29:28,965 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,965 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:29,397 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:29:29,397 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:29,397 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [133536448]
[2025-05-07 17:29:29,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [133536448] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:29,397 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:29,397 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:29:29,397 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1912290363]
[2025-05-07 17:29:29,397 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:29,398 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:29,398 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:29,398 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:29,399 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=132, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:29:29,399 INFO  L87              Difference]: Start difference. First operand 89 states and 99 transitions. Second operand  has 13 states, 10 states have (on average 4.1) internal successors, (41), 12 states have internal predecessors, (41), 8 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (26), 11 states have call predecessors, (26), 8 states have call successors, (26)
[2025-05-07 17:29:29,549 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:29,549 INFO  L93              Difference]: Finished difference Result 99 states and 115 transitions.
[2025-05-07 17:29:29,550 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:29,550 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 4.1) internal successors, (41), 12 states have internal predecessors, (41), 8 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (26), 11 states have call predecessors, (26), 8 states have call successors, (26) Word has length 94
[2025-05-07 17:29:29,550 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:29,551 INFO  L225             Difference]: With dead ends: 99
[2025-05-07 17:29:29,551 INFO  L226             Difference]: Without dead ends: 99
[2025-05-07 17:29:29,551 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=154, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:29:29,552 INFO  L437           NwaCegarLoop]: 88 mSDtfsCounter, 3 mSDsluCounter, 933 mSDsCounter, 0 mSdLazyCounter, 178 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1021 SdHoareTripleChecker+Invalid, 178 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 178 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:29,552 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1021 Invalid, 178 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 178 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:29,552 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 99 states.
[2025-05-07 17:29:29,558 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 99 to 97.
[2025-05-07 17:29:29,559 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 97 states, 40 states have (on average 1.075) internal successors, (43), 43 states have internal predecessors, (43), 30 states have call successors, (31), 22 states have call predecessors, (31), 26 states have return successors, (39), 31 states have call predecessors, (39), 30 states have call successors, (39)
[2025-05-07 17:29:29,560 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 97 states to 97 states and 113 transitions.
[2025-05-07 17:29:29,560 INFO  L79                 Accepts]: Start accepts. Automaton has 97 states and 113 transitions. Word has length 94
[2025-05-07 17:29:29,560 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:29,560 INFO  L485      AbstractCegarLoop]: Abstraction has 97 states and 113 transitions.
[2025-05-07 17:29:29,561 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 4.1) internal successors, (41), 12 states have internal predecessors, (41), 8 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (26), 11 states have call predecessors, (26), 8 states have call successors, (26)
[2025-05-07 17:29:29,561 INFO  L278                IsEmpty]: Start isEmpty. Operand 97 states and 113 transitions.
[2025-05-07 17:29:29,562 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 95
[2025-05-07 17:29:29,562 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:29,562 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-05-07 17:29:29,562 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:29:29,562 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:29,563 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:29,563 INFO  L85        PathProgramCache]: Analyzing trace with hash -1943437295, now seen corresponding path program 1 times
[2025-05-07 17:29:29,563 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:29,563 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1359150769]
[2025-05-07 17:29:29,563 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:29,563 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:29,604 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 94 statements into 1 equivalence classes.
[2025-05-07 17:29:29,615 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 94 of 94 statements.
[2025-05-07 17:29:29,615 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:29,615 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:30,038 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-05-07 17:29:30,038 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:30,038 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1359150769]
[2025-05-07 17:29:30,038 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1359150769] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:30,038 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:30,038 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-05-07 17:29:30,038 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1357977705]
[2025-05-07 17:29:30,038 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:30,039 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:30,039 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:30,039 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:30,039 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=132, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:29:30,040 INFO  L87              Difference]: Start difference. First operand 97 states and 113 transitions. Second operand  has 13 states, 10 states have (on average 4.1) internal successors, (41), 12 states have internal predecessors, (41), 8 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (26), 11 states have call predecessors, (26), 8 states have call successors, (26)
[2025-05-07 17:29:30,177 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:30,177 INFO  L93              Difference]: Finished difference Result 97 states and 112 transitions.
[2025-05-07 17:29:30,177 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:29:30,178 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 4.1) internal successors, (41), 12 states have internal predecessors, (41), 8 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (26), 11 states have call predecessors, (26), 8 states have call successors, (26) Word has length 94
[2025-05-07 17:29:30,178 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:30,179 INFO  L225             Difference]: With dead ends: 97
[2025-05-07 17:29:30,179 INFO  L226             Difference]: Without dead ends: 96
[2025-05-07 17:29:30,179 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=154, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:29:30,180 INFO  L437           NwaCegarLoop]: 92 mSDtfsCounter, 2 mSDsluCounter, 971 mSDsCounter, 0 mSdLazyCounter, 178 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1063 SdHoareTripleChecker+Invalid, 178 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 178 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:30,180 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1063 Invalid, 178 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 178 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:30,180 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-05-07 17:29:30,184 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 91.
[2025-05-07 17:29:30,185 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 38 states have (on average 1.0789473684210527) internal successors, (41), 41 states have internal predecessors, (41), 28 states have call successors, (29), 22 states have call predecessors, (29), 24 states have return successors, (32), 27 states have call predecessors, (32), 28 states have call successors, (32)
[2025-05-07 17:29:30,185 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 102 transitions.
[2025-05-07 17:29:30,186 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 102 transitions. Word has length 94
[2025-05-07 17:29:30,186 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:30,186 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 102 transitions.
[2025-05-07 17:29:30,186 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 4.1) internal successors, (41), 12 states have internal predecessors, (41), 8 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (26), 11 states have call predecessors, (26), 8 states have call successors, (26)
[2025-05-07 17:29:30,186 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 102 transitions.
[2025-05-07 17:29:30,187 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 120
[2025-05-07 17:29:30,187 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:30,187 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-05-07 17:29:30,188 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:29:30,188 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:30,188 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:30,188 INFO  L85        PathProgramCache]: Analyzing trace with hash 1187518309, now seen corresponding path program 1 times
[2025-05-07 17:29:30,188 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:30,188 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1894279731]
[2025-05-07 17:29:30,188 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:30,188 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:30,226 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:29:30,238 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:29:30,238 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:30,238 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:30,701 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 14 proven. 12 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-05-07 17:29:30,701 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:30,701 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1894279731]
[2025-05-07 17:29:30,701 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1894279731] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:30,701 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1278640556]
[2025-05-07 17:29:30,701 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:30,701 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:30,703 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:30,704 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:30,705 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:29:30,942 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:29:31,095 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:29:31,095 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:31,095 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:31,100 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1523 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:31,106 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:31,181 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 47 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:29:31,181 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:29:31,181 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1278640556] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:31,181 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:29:31,181 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [13] total 15
[2025-05-07 17:29:31,181 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [536559620]
[2025-05-07 17:29:31,181 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:31,181 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:31,182 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:31,182 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:31,182 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=180, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:29:31,182 INFO  L87              Difference]: Start difference. First operand 91 states and 102 transitions. Second operand  has 13 states, 10 states have (on average 5.2) internal successors, (52), 12 states have internal predecessors, (52), 9 states have call successors, (32), 2 states have call predecessors, (32), 10 states have return successors, (33), 11 states have call predecessors, (33), 9 states have call successors, (33)
[2025-05-07 17:29:31,341 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:31,341 INFO  L93              Difference]: Finished difference Result 102 states and 121 transitions.
[2025-05-07 17:29:31,341 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:29:31,341 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 5.2) internal successors, (52), 12 states have internal predecessors, (52), 9 states have call successors, (32), 2 states have call predecessors, (32), 10 states have return successors, (33), 11 states have call predecessors, (33), 9 states have call successors, (33) Word has length 119
[2025-05-07 17:29:31,342 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:31,342 INFO  L225             Difference]: With dead ends: 102
[2025-05-07 17:29:31,342 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:29:31,343 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 135 GetRequests, 119 SyntacticMatches, 0 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=43, Invalid=263, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:29:31,343 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 5 mSDsluCounter, 965 mSDsCounter, 0 mSdLazyCounter, 197 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 1056 SdHoareTripleChecker+Invalid, 199 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 197 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:31,343 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 1056 Invalid, 199 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 197 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:31,343 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:29:31,346 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 97.
[2025-05-07 17:29:31,346 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 97 states, 40 states have (on average 1.075) internal successors, (43), 43 states have internal predecessors, (43), 30 states have call successors, (31), 22 states have call predecessors, (31), 26 states have return successors, (38), 31 states have call predecessors, (38), 30 states have call successors, (38)
[2025-05-07 17:29:31,347 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 97 states to 97 states and 112 transitions.
[2025-05-07 17:29:31,347 INFO  L79                 Accepts]: Start accepts. Automaton has 97 states and 112 transitions. Word has length 119
[2025-05-07 17:29:31,347 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:31,347 INFO  L485      AbstractCegarLoop]: Abstraction has 97 states and 112 transitions.
[2025-05-07 17:29:31,347 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 5.2) internal successors, (52), 12 states have internal predecessors, (52), 9 states have call successors, (32), 2 states have call predecessors, (32), 10 states have return successors, (33), 11 states have call predecessors, (33), 9 states have call successors, (33)
[2025-05-07 17:29:31,347 INFO  L278                IsEmpty]: Start isEmpty. Operand 97 states and 112 transitions.
[2025-05-07 17:29:31,348 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 120
[2025-05-07 17:29:31,348 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:31,348 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:31,353 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:29:31,548 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:31,548 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:31,548 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:31,549 INFO  L85        PathProgramCache]: Analyzing trace with hash 1500422501, now seen corresponding path program 1 times
[2025-05-07 17:29:31,549 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:31,549 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [954137292]
[2025-05-07 17:29:31,549 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:31,549 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:31,588 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:29:31,597 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:29:31,597 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:31,597 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:32,029 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 11 proven. 12 refuted. 0 times theorem prover too weak. 24 trivial. 0 not checked.
[2025-05-07 17:29:32,029 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:32,029 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [954137292]
[2025-05-07 17:29:32,029 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [954137292] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:29:32,029 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [640872334]
[2025-05-07 17:29:32,029 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:32,029 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:29:32,031 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:32,032 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:29:32,033 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:29:32,233 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 119 statements into 1 equivalence classes.
[2025-05-07 17:29:32,347 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 119 of 119 statements.
[2025-05-07 17:29:32,347 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:32,347 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:32,352 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1525 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-05-07 17:29:32,355 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:29:32,421 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 40 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-05-07 17:29:32,422 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:29:32,422 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [640872334] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:32,422 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:29:32,422 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [13] total 15
[2025-05-07 17:29:32,422 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [227600687]
[2025-05-07 17:29:32,422 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:32,423 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-05-07 17:29:32,423 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:32,423 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-05-07 17:29:32,423 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=180, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:29:32,423 INFO  L87              Difference]: Start difference. First operand 97 states and 112 transitions. Second operand  has 13 states, 10 states have (on average 5.2) internal successors, (52), 12 states have internal predecessors, (52), 9 states have call successors, (33), 2 states have call predecessors, (33), 10 states have return successors, (33), 11 states have call predecessors, (33), 9 states have call successors, (33)
[2025-05-07 17:29:32,549 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:32,549 INFO  L93              Difference]: Finished difference Result 90 states and 101 transitions.
[2025-05-07 17:29:32,550 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:29:32,550 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 5.2) internal successors, (52), 12 states have internal predecessors, (52), 9 states have call successors, (33), 2 states have call predecessors, (33), 10 states have return successors, (33), 11 states have call predecessors, (33), 9 states have call successors, (33) Word has length 119
[2025-05-07 17:29:32,550 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:32,550 INFO  L225             Difference]: With dead ends: 90
[2025-05-07 17:29:32,550 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:29:32,550 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 135 GetRequests, 119 SyntacticMatches, 0 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=43, Invalid=263, Unknown=0, NotChecked=0, Total=306
[2025-05-07 17:29:32,551 INFO  L437           NwaCegarLoop]: 88 mSDtfsCounter, 3 mSDsluCounter, 925 mSDsCounter, 0 mSdLazyCounter, 160 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1013 SdHoareTripleChecker+Invalid, 161 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 160 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:32,551 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1013 Invalid, 161 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 160 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:32,552 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:29:32,552 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:29:32,552 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:29:32,552 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:29:32,552 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 119
[2025-05-07 17:29:32,552 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:32,552 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:29:32,552 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 5.2) internal successors, (52), 12 states have internal predecessors, (52), 9 states have call successors, (33), 2 states have call predecessors, (33), 10 states have return successors, (33), 11 states have call predecessors, (33), 9 states have call successors, (33)
[2025-05-07 17:29:32,552 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:29:32,552 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:29:32,554 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:29:32,560 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:29:32,755 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-05-07 17:29:32,764 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:32,770 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:29:32,778 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:29:32 BoogieIcfgContainer
[2025-05-07 17:29:32,779 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:29:32,781 INFO  L158              Benchmark]: Toolchain (without parser) took 9452.67ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 151.1MB in the beginning and 224.1MB in the end (delta: -73.1MB). Peak memory consumption was 49.1MB. Max. memory is 33.6GB.
[2025-05-07 17:29:32,782 INFO  L158              Benchmark]: SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 171.9MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:32,783 INFO  L158              Benchmark]: ChcToBoogie took 30.10ms. Allocated memory is still 234.9MB. Free memory was 151.1MB in the beginning and 147.7MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:32,783 INFO  L158              Benchmark]: Boogie Preprocessor took 50.99ms. Allocated memory is still 234.9MB. Free memory was 147.7MB in the beginning and 144.6MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:32,784 INFO  L158              Benchmark]: RCFGBuilder took 397.02ms. Allocated memory is still 234.9MB. Free memory was 144.5MB in the beginning and 185.5MB in the end (delta: -41.0MB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
[2025-05-07 17:29:32,785 INFO  L158              Benchmark]: TraceAbstraction took 8970.51ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 184.7MB in the beginning and 224.1MB in the end (delta: -39.5MB). Peak memory consumption was 73.9MB. Max. memory is 33.6GB.
[2025-05-07 17:29:32,788 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 171.9MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 30.10ms. Allocated memory is still 234.9MB. Free memory was 151.1MB in the beginning and 147.7MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 50.99ms. Allocated memory is still 234.9MB. Free memory was 147.7MB in the beginning and 144.6MB in the end (delta: 3.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 397.02ms. Allocated memory is still 234.9MB. Free memory was 144.5MB in the beginning and 185.5MB in the end (delta: -41.0MB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 8970.51ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 184.7MB in the beginning and 224.1MB in the end (delta: -39.5MB). Peak memory consumption was 73.9MB. 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 23 procedures, 93 locations, 142 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 8.9s, OverallIterations: 11, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 78 SdHoareTripleChecker+Valid, 1.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 30 mSDsluCounter, 10388 SdHoareTripleChecker+Invalid, 1.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 9322 mSDsCounter, 13 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1587 IncrementalHoareTripleChecker+Invalid, 1600 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 13 mSolverCounterUnsat, 1066 mSDtfsCounter, 1587 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 530 GetRequests, 404 SyntacticMatches, 0 SemanticMatches, 126 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 42 ImplicationChecksByTransitivity, 0.7s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=104occurred in iteration=4, InterpolantAutomatonStates: 127, 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, 11 MinimizatonAttempts, 38 StatesRemovedByMinimization, 8 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.4s SsaConstructionTime, 0.7s SatisfiabilityAnalysisTime, 4.2s InterpolantComputationTime, 1277 NumberOfCodeBlocks, 1277 NumberOfCodeBlocksAsserted, 15 NumberOfCheckSat, 1262 ConstructedInterpolants, 0 QuantifiedInterpolants, 1658 SizeOfPredicates, 8 NumberOfNonLiveVariables, 4947 ConjunctsInSsa, 70 ConjunctsInUnsatCore, 15 InterpolantComputations, 11 PerfectInterpolantSequences, 275/320 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:29:32,805 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
