./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_3_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:58,992 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:59,042 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34c2dc65-b0f2-4c18-a180-467e3d195b40/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:59,046 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:59,046 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:59,063 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:59,063 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:59,063 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:59,064 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:59,064 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:59,064 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:59,064 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:59,064 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:59,064 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:59,064 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:59,065 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:59,065 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:59,065 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:59,066 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:59,066 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:59,262 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:59,270 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:59,272 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:59,273 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:59,273 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:59,274 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34c2dc65-b0f2-4c18-a180-467e3d195b40/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_3_no_adts_000.smt2
[2025-05-07 17:26:59,275 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:59,277 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:59,638 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34c2dc65-b0f2-4c18-a180-467e3d195b40/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_3_no_adts_000.smt2
[2025-05-07 17:26:59,640 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:59,641 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:59,641 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:59,641 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:59,641 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:59,643 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,686 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59 Unit
[2025-05-07 17:26:59,687 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:59,687 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:59,687 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:59,687 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:59,698 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,698 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,723 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,724 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,733 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,734 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,736 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,739 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,742 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,758 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:59,759 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:59,759 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:59,759 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:59,760 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (1/1) ...
[2025-05-07 17:26:59,762 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:59,770 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:59,778 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:26:59,780 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:26:59,788 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:59,788 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:59,788 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:59,788 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_80_0 given in one single declaration
[2025-05-07 17:26:59,788 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_80_0
[2025-05-07 17:26:59,788 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_80_0
[2025-05-07 17:26:59,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_6_D_407_0 given in one single declaration
[2025-05-07 17:26:59,789 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_6_D_407_0
[2025-05-07 17:26:59,789 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_6_D_407_0
[2025-05-07 17:26:59,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_58_D_407_0 given in one single declaration
[2025-05-07 17:26:59,789 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_58_D_407_0
[2025-05-07 17:26:59,789 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_58_D_407_0
[2025-05-07 17:26:59,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_7_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,789 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_7_constructor_406_407_0
[2025-05-07 17:26:59,789 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_7_constructor_406_407_0
[2025-05-07 17:26:59,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,789 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_constructor_406_407_0
[2025-05-07 17:26:59,789 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_constructor_406_407_0
[2025-05-07 17:26:59,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36__405_407_0 given in one single declaration
[2025-05-07 17:26:59,789 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36__405_407_0
[2025-05-07 17:26:59,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36__405_407_0
[2025-05-07 17:26:59,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,790 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,790 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,790 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,790 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_constructor_406_407_0
[2025-05-07 17:26:59,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,791 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,791 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,791 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,791 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,791 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_constructor_406_407_0
[2025-05-07 17:26:59,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,792 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_constructor_406_407_0
[2025-05-07 17:26:59,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_return_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,793 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:26:59,793 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,794 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_constructor_406_407_0
[2025-05-07 17:26:59,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_constructor_406_407_0
[2025-05-07 17:26:59,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_constructor_406_407_0 given in one single declaration
[2025-05-07 17:26:59,794 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_constructor_406_407_0
[2025-05-07 17:26:59,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_constructor_406_407_0
[2025-05-07 17:26:59,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_60_D_407_0 given in one single declaration
[2025-05-07 17:26:59,794 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:26:59,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:26:59,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_59_D_407_0 given in one single declaration
[2025-05-07 17:26:59,794 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:26:59,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:26:59,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_61_D_407_0 given in one single declaration
[2025-05-07 17:26:59,794 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:26:59,794 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:26:59,794 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:59,794 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:59,795 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:00,045 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:00,047 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:00,535 INFO  L?                        ?]: Removed 1077 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:00,536 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:00,545 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:00,545 INFO  L312             CfgBuilder]: Removed 24 assume(true) statements.
[2025-05-07 17:27:00,545 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:00 BoogieIcfgContainer
[2025-05-07 17:27:00,546 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:00,547 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:00,547 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:00,550 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:00,550 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:59" (1/3) ...
[2025-05-07 17:27:00,550 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@38c6ebcb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:00, skipping insertion in model container
[2025-05-07 17:27:00,550 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:59" (2/3) ...
[2025-05-07 17:27:00,551 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@38c6ebcb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:00, skipping insertion in model container
[2025-05-07 17:27:00,551 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:00" (3/3) ...
[2025-05-07 17:27:00,552 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:00,562 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:00,564 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 32 procedures, 128 locations, 228 edges, 32 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:00,595 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:00,604 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;@1dfc417c, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:00,604 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:00,607 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 128 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 35 states have call successors, (55), 31 states have call predecessors, (55), 31 states have return successors, (55), 33 states have call predecessors, (55), 35 states have call successors, (55)
[2025-05-07 17:27:00,614 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:00,614 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:00,615 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]
[2025-05-07 17:27:00,615 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:00,619 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:00,619 INFO  L85        PathProgramCache]: Analyzing trace with hash 657751246, now seen corresponding path program 1 times
[2025-05-07 17:27:00,625 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:00,625 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1857782095]
[2025-05-07 17:27:00,625 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:00,626 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:00,671 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:00,700 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:00,700 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:00,700 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:00,866 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:00,867 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:00,867 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1857782095]
[2025-05-07 17:27:00,867 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1857782095] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:00,867 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:00,869 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:00,870 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1722964633]
[2025-05-07 17:27:00,871 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:00,874 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:00,874 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:00,892 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:00,892 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:00,894 INFO  L87              Difference]: Start difference. First operand  has 128 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 35 states have call successors, (55), 31 states have call predecessors, (55), 31 states have return successors, (55), 33 states have call predecessors, (55), 35 states have call successors, (55) Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:00,967 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:00,968 INFO  L93              Difference]: Finished difference Result 130 states and 175 transitions.
[2025-05-07 17:27:00,969 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:00,971 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:00,971 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:00,978 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:00,979 INFO  L226             Difference]: Without dead ends: 130
[2025-05-07 17:27:00,980 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:00,982 INFO  L437           NwaCegarLoop]: 171 mSDtfsCounter, 1 mSDsluCounter, 330 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 501 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:00,983 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 501 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:00,997 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-05-07 17:27:01,018 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 128.
[2025-05-07 17:27:01,019 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 60 states have (on average 1.0333333333333334) internal successors, (62), 62 states have internal predecessors, (62), 35 states have call successors, (55), 31 states have call predecessors, (55), 32 states have return successors, (56), 34 states have call predecessors, (56), 35 states have call successors, (56)
[2025-05-07 17:27:01,022 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 173 transitions.
[2025-05-07 17:27:01,023 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 173 transitions. Word has length 41
[2025-05-07 17:27:01,024 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,024 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 173 transitions.
[2025-05-07 17:27:01,024 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:01,024 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 173 transitions.
[2025-05-07 17:27:01,025 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,026 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,026 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]
[2025-05-07 17:27:01,026 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:01,026 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,027 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,027 INFO  L85        PathProgramCache]: Analyzing trace with hash 1358563878, now seen corresponding path program 1 times
[2025-05-07 17:27:01,027 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,027 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [940983631]
[2025-05-07 17:27:01,027 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,027 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,041 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,048 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:01,048 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,048 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,122 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:01,122 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [940983631]
[2025-05-07 17:27:01,122 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [940983631] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,122 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,122 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:01,122 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [990648131]
[2025-05-07 17:27:01,122 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,123 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:01,123 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:01,124 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:01,124 INFO  L87              Difference]: Start difference. First operand 128 states and 173 transitions. Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:01,138 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,138 INFO  L93              Difference]: Finished difference Result 130 states and 174 transitions.
[2025-05-07 17:27:01,139 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:01,139 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:01,139 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,140 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:01,140 INFO  L226             Difference]: Without dead ends: 122
[2025-05-07 17:27:01,140 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:01,141 INFO  L437           NwaCegarLoop]: 172 mSDtfsCounter, 1 mSDsluCounter, 335 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 507 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:01,141 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 507 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:01,142 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 122 states.
[2025-05-07 17:27:01,149 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 122 to 122.
[2025-05-07 17:27:01,149 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 59 states have (on average 1.0) internal successors, (59), 59 states have internal predecessors, (59), 31 states have call successors, (51), 31 states have call predecessors, (51), 31 states have return successors, (51), 31 states have call predecessors, (51), 31 states have call successors, (51)
[2025-05-07 17:27:01,150 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 161 transitions.
[2025-05-07 17:27:01,150 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 161 transitions. Word has length 41
[2025-05-07 17:27:01,150 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,151 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 161 transitions.
[2025-05-07 17:27:01,151 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:01,151 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 161 transitions.
[2025-05-07 17:27:01,153 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,153 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,153 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]
[2025-05-07 17:27:01,154 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:01,154 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,154 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,154 INFO  L85        PathProgramCache]: Analyzing trace with hash 698049852, now seen corresponding path program 1 times
[2025-05-07 17:27:01,154 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,154 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2064824171]
[2025-05-07 17:27:01,154 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,170 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,190 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:01,190 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,190 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,487 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:01,487 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,487 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2064824171]
[2025-05-07 17:27:01,487 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2064824171] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,487 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,487 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,487 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [289031938]
[2025-05-07 17:27:01,487 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,488 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,488 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,488 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,488 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,488 INFO  L87              Difference]: Start difference. First operand 122 states and 161 transitions. Second operand  has 7 states, 5 states have (on average 3.8) internal successors, (19), 7 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 6 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:27:01,697 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,697 INFO  L93              Difference]: Finished difference Result 124 states and 162 transitions.
[2025-05-07 17:27:01,697 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:01,697 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.8) internal successors, (19), 7 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 6 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:27:01,698 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,699 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:27:01,699 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:27:01,699 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,699 INFO  L437           NwaCegarLoop]: 139 mSDtfsCounter, 1 mSDsluCounter, 658 mSDsCounter, 0 mSdLazyCounter, 161 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 797 SdHoareTripleChecker+Invalid, 161 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 161 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:01,699 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 797 Invalid, 161 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 161 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:27:01,700 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:27:01,705 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 118.
[2025-05-07 17:27:01,706 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 118 states, 57 states have (on average 1.0) internal successors, (57), 57 states have internal predecessors, (57), 30 states have call successors, (49), 30 states have call predecessors, (49), 30 states have return successors, (49), 30 states have call predecessors, (49), 30 states have call successors, (49)
[2025-05-07 17:27:01,707 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 155 transitions.
[2025-05-07 17:27:01,707 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 155 transitions. Word has length 41
[2025-05-07 17:27:01,707 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,707 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 155 transitions.
[2025-05-07 17:27:01,707 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.8) internal successors, (19), 7 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 6 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:27:01,707 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 155 transitions.
[2025-05-07 17:27:01,708 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,708 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,708 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]
[2025-05-07 17:27:01,708 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:01,708 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,709 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,709 INFO  L85        PathProgramCache]: Analyzing trace with hash 1800785280, now seen corresponding path program 1 times
[2025-05-07 17:27:01,709 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,709 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [819587991]
[2025-05-07 17:27:01,709 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,709 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,728 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,738 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:01,738 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,738 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,815 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:01,816 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,816 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [819587991]
[2025-05-07 17:27:01,816 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [819587991] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,816 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,816 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,816 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2024328608]
[2025-05-07 17:27:01,816 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,816 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,816 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,817 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,817 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,817 INFO  L87              Difference]: Start difference. First operand 118 states and 155 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:01,850 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,850 INFO  L93              Difference]: Finished difference Result 124 states and 160 transitions.
[2025-05-07 17:27:01,851 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:01,851 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:01,851 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,853 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:27:01,853 INFO  L226             Difference]: Without dead ends: 114
[2025-05-07 17:27:01,853 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,854 INFO  L437           NwaCegarLoop]: 157 mSDtfsCounter, 1 mSDsluCounter, 770 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 927 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:01,854 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 927 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:01,855 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-05-07 17:27:01,862 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 114.
[2025-05-07 17:27:01,863 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 114 states, 55 states have (on average 1.0) internal successors, (55), 55 states have internal predecessors, (55), 29 states have call successors, (47), 29 states have call predecessors, (47), 29 states have return successors, (47), 29 states have call predecessors, (47), 29 states have call successors, (47)
[2025-05-07 17:27:01,864 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 149 transitions.
[2025-05-07 17:27:01,864 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 149 transitions. Word has length 41
[2025-05-07 17:27:01,864 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,864 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 149 transitions.
[2025-05-07 17:27:01,864 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:01,865 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 149 transitions.
[2025-05-07 17:27:01,866 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,866 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,866 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]
[2025-05-07 17:27:01,866 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:01,866 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,866 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,867 INFO  L85        PathProgramCache]: Analyzing trace with hash -1023257280, now seen corresponding path program 1 times
[2025-05-07 17:27:01,867 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,867 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [692139499]
[2025-05-07 17:27:01,867 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,867 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,885 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,900 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:01,900 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,900 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,997 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:01,997 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [692139499]
[2025-05-07 17:27:01,997 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [692139499] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,997 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,997 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,997 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1145286032]
[2025-05-07 17:27:01,998 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,998 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,998 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,998 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,998 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,999 INFO  L87              Difference]: Start difference. First operand 114 states and 149 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,028 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,028 INFO  L93              Difference]: Finished difference Result 120 states and 154 transitions.
[2025-05-07 17:27:02,029 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,029 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,029 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,030 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:27:02,030 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:27:02,030 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,030 INFO  L437           NwaCegarLoop]: 151 mSDtfsCounter, 1 mSDsluCounter, 740 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 891 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,031 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 891 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,031 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:27:02,035 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 110.
[2025-05-07 17:27:02,035 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 110 states, 53 states have (on average 1.0) internal successors, (53), 53 states have internal predecessors, (53), 28 states have call successors, (45), 28 states have call predecessors, (45), 28 states have return successors, (45), 28 states have call predecessors, (45), 28 states have call successors, (45)
[2025-05-07 17:27:02,036 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 110 states to 110 states and 143 transitions.
[2025-05-07 17:27:02,036 INFO  L79                 Accepts]: Start accepts. Automaton has 110 states and 143 transitions. Word has length 41
[2025-05-07 17:27:02,036 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,036 INFO  L485      AbstractCegarLoop]: Abstraction has 110 states and 143 transitions.
[2025-05-07 17:27:02,036 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,036 INFO  L278                IsEmpty]: Start isEmpty. Operand 110 states and 143 transitions.
[2025-05-07 17:27:02,037 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,037 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,037 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]
[2025-05-07 17:27:02,037 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:02,037 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,037 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,037 INFO  L85        PathProgramCache]: Analyzing trace with hash 676925722, now seen corresponding path program 1 times
[2025-05-07 17:27:02,037 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,037 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [732227170]
[2025-05-07 17:27:02,037 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,038 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,049 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,067 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,067 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,067 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,127 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,127 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,127 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [732227170]
[2025-05-07 17:27:02,127 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [732227170] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,127 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,127 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,128 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1451642158]
[2025-05-07 17:27:02,128 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,128 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,128 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,128 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,129 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,129 INFO  L87              Difference]: Start difference. First operand 110 states and 143 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,161 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,161 INFO  L93              Difference]: Finished difference Result 116 states and 148 transitions.
[2025-05-07 17:27:02,162 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,162 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,162 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,163 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:02,163 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:27:02,163 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,163 INFO  L437           NwaCegarLoop]: 140 mSDtfsCounter, 1 mSDsluCounter, 690 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 830 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,164 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 830 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,164 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:27:02,167 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:27:02,168 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 51 states have (on average 1.0) internal successors, (51), 51 states have internal predecessors, (51), 27 states have call successors, (43), 27 states have call predecessors, (43), 27 states have return successors, (43), 27 states have call predecessors, (43), 27 states have call successors, (43)
[2025-05-07 17:27:02,168 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 137 transitions.
[2025-05-07 17:27:02,168 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 137 transitions. Word has length 41
[2025-05-07 17:27:02,168 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,168 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 137 transitions.
[2025-05-07 17:27:02,168 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,168 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 137 transitions.
[2025-05-07 17:27:02,169 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,169 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,169 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]
[2025-05-07 17:27:02,169 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:02,169 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,169 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,169 INFO  L85        PathProgramCache]: Analyzing trace with hash -585507496, now seen corresponding path program 1 times
[2025-05-07 17:27:02,169 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,170 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1885605717]
[2025-05-07 17:27:02,170 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,170 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,187 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,194 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,194 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,194 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,258 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,258 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,258 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1885605717]
[2025-05-07 17:27:02,259 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1885605717] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,259 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,259 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,259 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [393298383]
[2025-05-07 17:27:02,259 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,259 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,259 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,260 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,260 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,260 INFO  L87              Difference]: Start difference. First operand 106 states and 137 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,288 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,289 INFO  L93              Difference]: Finished difference Result 112 states and 142 transitions.
[2025-05-07 17:27:02,289 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,289 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,289 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,290 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:27:02,290 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:27:02,290 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,290 INFO  L437           NwaCegarLoop]: 139 mSDtfsCounter, 1 mSDsluCounter, 680 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 819 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,290 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 819 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,291 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:27:02,294 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:27:02,294 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 49 states have (on average 1.0) internal successors, (49), 49 states have internal predecessors, (49), 26 states have call successors, (41), 26 states have call predecessors, (41), 26 states have return successors, (41), 26 states have call predecessors, (41), 26 states have call successors, (41)
[2025-05-07 17:27:02,295 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 131 transitions.
[2025-05-07 17:27:02,295 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 131 transitions. Word has length 41
[2025-05-07 17:27:02,295 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,295 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 131 transitions.
[2025-05-07 17:27:02,295 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,295 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 131 transitions.
[2025-05-07 17:27:02,295 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,295 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,296 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:02,296 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:02,296 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,296 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,296 INFO  L85        PathProgramCache]: Analyzing trace with hash 387871054, now seen corresponding path program 1 times
[2025-05-07 17:27:02,296 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,296 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [362857739]
[2025-05-07 17:27:02,296 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,296 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,307 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,312 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,312 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,312 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,363 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,363 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,363 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [362857739]
[2025-05-07 17:27:02,363 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [362857739] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,363 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,363 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,363 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [258499903]
[2025-05-07 17:27:02,363 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,363 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,363 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,364 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,364 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,364 INFO  L87              Difference]: Start difference. First operand 102 states and 131 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,392 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,392 INFO  L93              Difference]: Finished difference Result 108 states and 136 transitions.
[2025-05-07 17:27:02,393 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,393 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,393 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,394 INFO  L225             Difference]: With dead ends: 108
[2025-05-07 17:27:02,394 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:27:02,394 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,394 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 650 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 783 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,394 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 783 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,395 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:27:02,397 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:27:02,398 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 47 states have (on average 1.0) internal successors, (47), 47 states have internal predecessors, (47), 25 states have call successors, (39), 25 states have call predecessors, (39), 25 states have return successors, (39), 25 states have call predecessors, (39), 25 states have call successors, (39)
[2025-05-07 17:27:02,398 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 125 transitions.
[2025-05-07 17:27:02,398 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 125 transitions. Word has length 41
[2025-05-07 17:27:02,398 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,398 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 125 transitions.
[2025-05-07 17:27:02,398 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,398 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 125 transitions.
[2025-05-07 17:27:02,399 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,399 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,399 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]
[2025-05-07 17:27:02,399 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:02,399 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,399 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,399 INFO  L85        PathProgramCache]: Analyzing trace with hash 615343428, now seen corresponding path program 1 times
[2025-05-07 17:27:02,399 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,399 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [178238213]
[2025-05-07 17:27:02,399 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,399 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,414 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,420 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,421 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,421 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,478 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,478 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,478 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [178238213]
[2025-05-07 17:27:02,479 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [178238213] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,479 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,479 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,479 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1061146982]
[2025-05-07 17:27:02,479 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,479 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,479 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,479 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,479 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,480 INFO  L87              Difference]: Start difference. First operand 98 states and 125 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,508 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,508 INFO  L93              Difference]: Finished difference Result 104 states and 130 transitions.
[2025-05-07 17:27:02,509 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,509 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,509 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,510 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:27:02,510 INFO  L226             Difference]: Without dead ends: 94
[2025-05-07 17:27:02,510 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,511 INFO  L437           NwaCegarLoop]: 122 mSDtfsCounter, 1 mSDsluCounter, 600 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 722 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,511 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 722 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,512 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-05-07 17:27:02,515 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 94.
[2025-05-07 17:27:02,516 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 45 states have (on average 1.0) internal successors, (45), 45 states have internal predecessors, (45), 24 states have call successors, (37), 24 states have call predecessors, (37), 24 states have return successors, (37), 24 states have call predecessors, (37), 24 states have call successors, (37)
[2025-05-07 17:27:02,517 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 119 transitions.
[2025-05-07 17:27:02,517 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 119 transitions. Word has length 41
[2025-05-07 17:27:02,517 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,517 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 119 transitions.
[2025-05-07 17:27:02,517 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,517 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 119 transitions.
[2025-05-07 17:27:02,518 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,518 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,518 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]
[2025-05-07 17:27:02,518 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:02,518 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,518 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,519 INFO  L85        PathProgramCache]: Analyzing trace with hash 2067584256, now seen corresponding path program 1 times
[2025-05-07 17:27:02,519 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,519 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1509935921]
[2025-05-07 17:27:02,519 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,519 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,535 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,544 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,544 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,544 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,611 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,611 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,611 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1509935921]
[2025-05-07 17:27:02,612 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1509935921] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,612 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,612 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,612 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1974820972]
[2025-05-07 17:27:02,612 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,612 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,612 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,613 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,613 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,613 INFO  L87              Difference]: Start difference. First operand 94 states and 119 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,639 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,640 INFO  L93              Difference]: Finished difference Result 100 states and 124 transitions.
[2025-05-07 17:27:02,640 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,640 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,640 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,641 INFO  L225             Difference]: With dead ends: 100
[2025-05-07 17:27:02,641 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:27:02,641 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,641 INFO  L437           NwaCegarLoop]: 121 mSDtfsCounter, 1 mSDsluCounter, 590 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 711 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,642 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 711 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,642 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:27:02,644 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:27:02,644 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 43 states have (on average 1.0) internal successors, (43), 43 states have internal predecessors, (43), 23 states have call successors, (35), 23 states have call predecessors, (35), 23 states have return successors, (35), 23 states have call predecessors, (35), 23 states have call successors, (35)
[2025-05-07 17:27:02,645 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 113 transitions.
[2025-05-07 17:27:02,645 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 113 transitions. Word has length 41
[2025-05-07 17:27:02,645 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,645 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 113 transitions.
[2025-05-07 17:27:02,645 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,645 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 113 transitions.
[2025-05-07 17:27:02,646 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,646 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,646 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]
[2025-05-07 17:27:02,646 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:02,646 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,646 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,646 INFO  L85        PathProgramCache]: Analyzing trace with hash 1716292964, now seen corresponding path program 1 times
[2025-05-07 17:27:02,646 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,646 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2145433978]
[2025-05-07 17:27:02,646 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,647 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,658 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,662 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,662 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,662 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,709 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,709 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,709 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2145433978]
[2025-05-07 17:27:02,709 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2145433978] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,709 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,709 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,709 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1097917117]
[2025-05-07 17:27:02,709 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,710 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,710 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,710 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,710 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,710 INFO  L87              Difference]: Start difference. First operand 90 states and 113 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,737 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,738 INFO  L93              Difference]: Finished difference Result 96 states and 118 transitions.
[2025-05-07 17:27:02,738 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,738 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,738 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,739 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:27:02,739 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:27:02,739 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,739 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 1 mSDsluCounter, 560 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 675 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,739 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 675 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,739 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:27:02,741 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:27:02,741 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 41 states have (on average 1.0) internal successors, (41), 41 states have internal predecessors, (41), 22 states have call successors, (33), 22 states have call predecessors, (33), 22 states have return successors, (33), 22 states have call predecessors, (33), 22 states have call successors, (33)
[2025-05-07 17:27:02,742 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 107 transitions.
[2025-05-07 17:27:02,742 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 107 transitions. Word has length 41
[2025-05-07 17:27:02,742 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,742 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 107 transitions.
[2025-05-07 17:27:02,742 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,742 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 107 transitions.
[2025-05-07 17:27:02,742 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,743 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,743 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]
[2025-05-07 17:27:02,743 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:27:02,743 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,743 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,743 INFO  L85        PathProgramCache]: Analyzing trace with hash -1914880684, now seen corresponding path program 1 times
[2025-05-07 17:27:02,743 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,743 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1049870242]
[2025-05-07 17:27:02,743 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,743 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,759 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,768 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,768 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,768 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,866 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:02,866 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,866 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1049870242]
[2025-05-07 17:27:02,866 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1049870242] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,866 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,866 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,866 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [934698695]
[2025-05-07 17:27:02,866 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,866 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,866 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,867 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,867 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,867 INFO  L87              Difference]: Start difference. First operand 86 states and 107 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,892 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,892 INFO  L93              Difference]: Finished difference Result 92 states and 112 transitions.
[2025-05-07 17:27:02,892 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,893 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:02,893 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,893 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:27:02,893 INFO  L226             Difference]: Without dead ends: 82
[2025-05-07 17:27:02,893 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,894 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 532 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 641 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:02,894 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 641 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:02,894 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-05-07 17:27:02,896 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 82.
[2025-05-07 17:27:02,896 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 39 states have (on average 1.0) internal successors, (39), 39 states have internal predecessors, (39), 21 states have call successors, (31), 21 states have call predecessors, (31), 21 states have return successors, (31), 21 states have call predecessors, (31), 21 states have call successors, (31)
[2025-05-07 17:27:02,896 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 101 transitions.
[2025-05-07 17:27:02,896 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 101 transitions. Word has length 41
[2025-05-07 17:27:02,896 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,896 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 101 transitions.
[2025-05-07 17:27:02,896 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:02,897 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 101 transitions.
[2025-05-07 17:27:02,897 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,897 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,897 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]
[2025-05-07 17:27:02,897 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:27:02,897 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,897 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,897 INFO  L85        PathProgramCache]: Analyzing trace with hash -630786620, now seen corresponding path program 1 times
[2025-05-07 17:27:02,897 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,898 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [854402261]
[2025-05-07 17:27:02,898 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,898 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,917 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,930 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:02,930 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,931 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,005 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,005 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,006 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [854402261]
[2025-05-07 17:27:03,006 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [854402261] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,006 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,006 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,006 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [363438970]
[2025-05-07 17:27:03,006 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,006 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,006 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,007 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,007 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,007 INFO  L87              Difference]: Start difference. First operand 82 states and 101 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,037 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,037 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:27:03,037 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,037 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,038 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,038 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:27:03,038 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:27:03,038 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,039 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 1 mSDsluCounter, 500 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 603 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,039 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 603 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,039 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:27:03,041 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:27:03,041 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 37 states have (on average 1.0) internal successors, (37), 37 states have internal predecessors, (37), 20 states have call successors, (29), 20 states have call predecessors, (29), 20 states have return successors, (29), 20 states have call predecessors, (29), 20 states have call successors, (29)
[2025-05-07 17:27:03,041 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 95 transitions.
[2025-05-07 17:27:03,041 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 95 transitions. Word has length 41
[2025-05-07 17:27:03,042 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,042 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 95 transitions.
[2025-05-07 17:27:03,042 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,042 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 95 transitions.
[2025-05-07 17:27:03,042 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,042 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,042 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]
[2025-05-07 17:27:03,042 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:27:03,042 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,042 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,043 INFO  L85        PathProgramCache]: Analyzing trace with hash -692311734, now seen corresponding path program 1 times
[2025-05-07 17:27:03,043 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,043 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1028440324]
[2025-05-07 17:27:03,043 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,043 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,055 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,060 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,060 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,060 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,122 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,122 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1028440324]
[2025-05-07 17:27:03,123 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1028440324] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,123 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,123 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,123 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [93599316]
[2025-05-07 17:27:03,123 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,123 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,123 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,123 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,123 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,123 INFO  L87              Difference]: Start difference. First operand 78 states and 95 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,151 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,151 INFO  L93              Difference]: Finished difference Result 84 states and 100 transitions.
[2025-05-07 17:27:03,151 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,151 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,151 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,152 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:27:03,152 INFO  L226             Difference]: Without dead ends: 74
[2025-05-07 17:27:03,152 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,152 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 1 mSDsluCounter, 470 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 567 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,152 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 567 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,153 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-05-07 17:27:03,154 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 74.
[2025-05-07 17:27:03,154 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 74 states, 35 states have (on average 1.0) internal successors, (35), 35 states have internal predecessors, (35), 19 states have call successors, (27), 19 states have call predecessors, (27), 19 states have return successors, (27), 19 states have call predecessors, (27), 19 states have call successors, (27)
[2025-05-07 17:27:03,154 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 89 transitions.
[2025-05-07 17:27:03,155 INFO  L79                 Accepts]: Start accepts. Automaton has 74 states and 89 transitions. Word has length 41
[2025-05-07 17:27:03,155 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,155 INFO  L485      AbstractCegarLoop]: Abstraction has 74 states and 89 transitions.
[2025-05-07 17:27:03,155 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,155 INFO  L278                IsEmpty]: Start isEmpty. Operand 74 states and 89 transitions.
[2025-05-07 17:27:03,155 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,155 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,155 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]
[2025-05-07 17:27:03,155 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:27:03,155 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,156 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,156 INFO  L85        PathProgramCache]: Analyzing trace with hash 593625402, now seen corresponding path program 1 times
[2025-05-07 17:27:03,156 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,156 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1200883293]
[2025-05-07 17:27:03,156 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,156 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,168 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,173 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,173 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,173 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,224 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,224 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,224 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1200883293]
[2025-05-07 17:27:03,224 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1200883293] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,224 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,224 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,224 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1395691248]
[2025-05-07 17:27:03,224 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,225 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,225 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,225 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,225 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,225 INFO  L87              Difference]: Start difference. First operand 74 states and 89 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,251 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,251 INFO  L93              Difference]: Finished difference Result 80 states and 94 transitions.
[2025-05-07 17:27:03,251 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,251 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,251 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,251 INFO  L225             Difference]: With dead ends: 80
[2025-05-07 17:27:03,251 INFO  L226             Difference]: Without dead ends: 70
[2025-05-07 17:27:03,252 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,252 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 1 mSDsluCounter, 440 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 531 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,252 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 531 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,252 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-05-07 17:27:03,255 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-05-07 17:27:03,255 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 33 states have (on average 1.0) internal successors, (33), 33 states have internal predecessors, (33), 18 states have call successors, (25), 18 states have call predecessors, (25), 18 states have return successors, (25), 18 states have call predecessors, (25), 18 states have call successors, (25)
[2025-05-07 17:27:03,256 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 83 transitions.
[2025-05-07 17:27:03,256 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 83 transitions. Word has length 41
[2025-05-07 17:27:03,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,256 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 83 transitions.
[2025-05-07 17:27:03,256 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 83 transitions.
[2025-05-07 17:27:03,257 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,257 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,257 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]
[2025-05-07 17:27:03,257 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:27:03,257 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,258 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,258 INFO  L85        PathProgramCache]: Analyzing trace with hash 1736225098, now seen corresponding path program 1 times
[2025-05-07 17:27:03,258 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,258 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [264931346]
[2025-05-07 17:27:03,258 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,258 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,276 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,285 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,285 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,285 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,351 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,351 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,351 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [264931346]
[2025-05-07 17:27:03,351 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [264931346] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,352 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,352 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,352 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1143566335]
[2025-05-07 17:27:03,352 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,352 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,352 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,352 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,353 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,353 INFO  L87              Difference]: Start difference. First operand 70 states and 83 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,380 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,381 INFO  L93              Difference]: Finished difference Result 76 states and 88 transitions.
[2025-05-07 17:27:03,381 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,381 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,381 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,382 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:27:03,382 INFO  L226             Difference]: Without dead ends: 66
[2025-05-07 17:27:03,382 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,382 INFO  L437           NwaCegarLoop]: 80 mSDtfsCounter, 1 mSDsluCounter, 390 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 470 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,383 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 470 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,383 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-05-07 17:27:03,385 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-05-07 17:27:03,385 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 31 states have (on average 1.0) internal successors, (31), 31 states have internal predecessors, (31), 17 states have call successors, (23), 17 states have call predecessors, (23), 17 states have return successors, (23), 17 states have call predecessors, (23), 17 states have call successors, (23)
[2025-05-07 17:27:03,386 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 77 transitions.
[2025-05-07 17:27:03,386 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 77 transitions. Word has length 41
[2025-05-07 17:27:03,386 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,386 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 77 transitions.
[2025-05-07 17:27:03,386 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,386 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 77 transitions.
[2025-05-07 17:27:03,387 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,387 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,387 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]
[2025-05-07 17:27:03,387 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:27:03,387 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,387 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,388 INFO  L85        PathProgramCache]: Analyzing trace with hash -941859516, now seen corresponding path program 1 times
[2025-05-07 17:27:03,388 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,388 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [221328789]
[2025-05-07 17:27:03,388 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,388 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,403 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,410 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,411 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,411 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,457 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,457 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,457 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [221328789]
[2025-05-07 17:27:03,458 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [221328789] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,458 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,458 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,458 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1427930644]
[2025-05-07 17:27:03,458 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,458 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,458 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,459 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,459 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,459 INFO  L87              Difference]: Start difference. First operand 66 states and 77 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,485 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,485 INFO  L93              Difference]: Finished difference Result 72 states and 82 transitions.
[2025-05-07 17:27:03,486 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,486 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,486 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,487 INFO  L225             Difference]: With dead ends: 72
[2025-05-07 17:27:03,487 INFO  L226             Difference]: Without dead ends: 62
[2025-05-07 17:27:03,487 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,487 INFO  L437           NwaCegarLoop]: 74 mSDtfsCounter, 1 mSDsluCounter, 360 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 434 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,487 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 434 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,488 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-05-07 17:27:03,489 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 62.
[2025-05-07 17:27:03,489 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 29 states have (on average 1.0) internal successors, (29), 29 states have internal predecessors, (29), 16 states have call successors, (21), 16 states have call predecessors, (21), 16 states have return successors, (21), 16 states have call predecessors, (21), 16 states have call successors, (21)
[2025-05-07 17:27:03,489 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 71 transitions.
[2025-05-07 17:27:03,489 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 71 transitions. Word has length 41
[2025-05-07 17:27:03,489 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,489 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 71 transitions.
[2025-05-07 17:27:03,489 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,490 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 71 transitions.
[2025-05-07 17:27:03,490 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,490 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,490 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]
[2025-05-07 17:27:03,490 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:27:03,490 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,491 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,491 INFO  L85        PathProgramCache]: Analyzing trace with hash 1859630404, now seen corresponding path program 1 times
[2025-05-07 17:27:03,491 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,491 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [294773320]
[2025-05-07 17:27:03,491 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,491 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,505 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,512 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,512 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,512 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,561 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,561 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [294773320]
[2025-05-07 17:27:03,562 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [294773320] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,562 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,562 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,562 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1560951552]
[2025-05-07 17:27:03,562 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,562 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,562 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,562 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,562 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,563 INFO  L87              Difference]: Start difference. First operand 62 states and 71 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,591 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,591 INFO  L93              Difference]: Finished difference Result 68 states and 76 transitions.
[2025-05-07 17:27:03,592 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,592 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,592 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,592 INFO  L225             Difference]: With dead ends: 68
[2025-05-07 17:27:03,592 INFO  L226             Difference]: Without dead ends: 58
[2025-05-07 17:27:03,593 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,593 INFO  L437           NwaCegarLoop]: 73 mSDtfsCounter, 1 mSDsluCounter, 350 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 423 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,593 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 423 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,594 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-05-07 17:27:03,595 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 58.
[2025-05-07 17:27:03,595 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 58 states, 27 states have (on average 1.0) internal successors, (27), 27 states have internal predecessors, (27), 15 states have call successors, (19), 15 states have call predecessors, (19), 15 states have return successors, (19), 15 states have call predecessors, (19), 15 states have call successors, (19)
[2025-05-07 17:27:03,596 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 65 transitions.
[2025-05-07 17:27:03,596 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 65 transitions. Word has length 41
[2025-05-07 17:27:03,596 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,596 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 65 transitions.
[2025-05-07 17:27:03,596 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,596 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 65 transitions.
[2025-05-07 17:27:03,597 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,597 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,597 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]
[2025-05-07 17:27:03,597 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:27:03,597 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,597 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,597 INFO  L85        PathProgramCache]: Analyzing trace with hash 1753420062, now seen corresponding path program 1 times
[2025-05-07 17:27:03,597 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,597 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1293583854]
[2025-05-07 17:27:03,597 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,598 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,613 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,619 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,619 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,619 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,665 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,665 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,665 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1293583854]
[2025-05-07 17:27:03,665 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1293583854] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,665 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,665 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,665 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1624755011]
[2025-05-07 17:27:03,666 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,666 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,666 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,666 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,666 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,666 INFO  L87              Difference]: Start difference. First operand 58 states and 65 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,689 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,690 INFO  L93              Difference]: Finished difference Result 64 states and 70 transitions.
[2025-05-07 17:27:03,690 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,690 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,690 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,690 INFO  L225             Difference]: With dead ends: 64
[2025-05-07 17:27:03,690 INFO  L226             Difference]: Without dead ends: 54
[2025-05-07 17:27:03,691 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,691 INFO  L437           NwaCegarLoop]: 67 mSDtfsCounter, 1 mSDsluCounter, 320 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 387 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,691 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 387 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,691 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-05-07 17:27:03,693 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 54.
[2025-05-07 17:27:03,693 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 54 states, 25 states have (on average 1.0) internal successors, (25), 25 states have internal predecessors, (25), 14 states have call successors, (17), 14 states have call predecessors, (17), 14 states have return successors, (17), 14 states have call predecessors, (17), 14 states have call successors, (17)
[2025-05-07 17:27:03,693 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 59 transitions.
[2025-05-07 17:27:03,693 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 59 transitions. Word has length 41
[2025-05-07 17:27:03,693 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,693 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 59 transitions.
[2025-05-07 17:27:03,693 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,694 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 59 transitions.
[2025-05-07 17:27:03,694 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,694 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,694 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]
[2025-05-07 17:27:03,694 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:27:03,694 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,694 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,694 INFO  L85        PathProgramCache]: Analyzing trace with hash -1375086238, now seen corresponding path program 1 times
[2025-05-07 17:27:03,695 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,695 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1716439287]
[2025-05-07 17:27:03,695 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,695 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,709 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,713 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,713 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,714 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,760 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,760 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,760 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1716439287]
[2025-05-07 17:27:03,760 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1716439287] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,760 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,760 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,760 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [746345043]
[2025-05-07 17:27:03,760 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,760 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,761 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,761 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,761 INFO  L87              Difference]: Start difference. First operand 54 states and 59 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,787 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,787 INFO  L93              Difference]: Finished difference Result 60 states and 64 transitions.
[2025-05-07 17:27:03,788 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,788 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,788 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,788 INFO  L225             Difference]: With dead ends: 60
[2025-05-07 17:27:03,788 INFO  L226             Difference]: Without dead ends: 50
[2025-05-07 17:27:03,788 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,789 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 1 mSDsluCounter, 290 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 351 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,789 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 351 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,789 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-05-07 17:27:03,790 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 50.
[2025-05-07 17:27:03,790 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 23 states have (on average 1.0) internal successors, (23), 23 states have internal predecessors, (23), 13 states have call successors, (15), 13 states have call predecessors, (15), 13 states have return successors, (15), 13 states have call predecessors, (15), 13 states have call successors, (15)
[2025-05-07 17:27:03,791 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 53 transitions.
[2025-05-07 17:27:03,791 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 53 transitions. Word has length 41
[2025-05-07 17:27:03,791 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,791 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 53 transitions.
[2025-05-07 17:27:03,791 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,791 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 53 transitions.
[2025-05-07 17:27:03,791 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,791 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,791 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]
[2025-05-07 17:27:03,792 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:27:03,792 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,792 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,792 INFO  L85        PathProgramCache]: Analyzing trace with hash 36635992, now seen corresponding path program 1 times
[2025-05-07 17:27:03,792 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,792 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [558714084]
[2025-05-07 17:27:03,792 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,792 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,808 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,814 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,814 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,884 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,884 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,884 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [558714084]
[2025-05-07 17:27:03,884 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [558714084] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,884 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,884 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,884 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1205024967]
[2025-05-07 17:27:03,884 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,884 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,884 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,885 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,885 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,885 INFO  L87              Difference]: Start difference. First operand 50 states and 53 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,910 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,910 INFO  L93              Difference]: Finished difference Result 56 states and 58 transitions.
[2025-05-07 17:27:03,910 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,910 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:03,910 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,911 INFO  L225             Difference]: With dead ends: 56
[2025-05-07 17:27:03,911 INFO  L226             Difference]: Without dead ends: 46
[2025-05-07 17:27:03,911 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,911 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 1 mSDsluCounter, 260 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 315 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,911 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 315 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:03,912 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-05-07 17:27:03,913 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 46.
[2025-05-07 17:27:03,913 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 21 states have (on average 1.0) internal successors, (21), 21 states have internal predecessors, (21), 12 states have call successors, (13), 12 states have call predecessors, (13), 12 states have return successors, (13), 12 states have call predecessors, (13), 12 states have call successors, (13)
[2025-05-07 17:27:03,913 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 47 transitions.
[2025-05-07 17:27:03,913 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 47 transitions. Word has length 41
[2025-05-07 17:27:03,913 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,913 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 47 transitions.
[2025-05-07 17:27:03,913 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:03,913 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 47 transitions.
[2025-05-07 17:27:03,914 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,914 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,914 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]
[2025-05-07 17:27:03,914 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:27:03,914 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,914 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,914 INFO  L85        PathProgramCache]: Analyzing trace with hash -1830388368, now seen corresponding path program 1 times
[2025-05-07 17:27:03,914 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,914 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [872219325]
[2025-05-07 17:27:03,915 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,915 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,929 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,933 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:03,933 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,934 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,982 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:03,982 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,982 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [872219325]
[2025-05-07 17:27:03,982 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [872219325] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,982 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,982 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,982 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [379436804]
[2025-05-07 17:27:03,982 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,983 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,983 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,983 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,983 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,983 INFO  L87              Difference]: Start difference. First operand 46 states and 47 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:04,011 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:04,011 INFO  L93              Difference]: Finished difference Result 52 states and 52 transitions.
[2025-05-07 17:27:04,012 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:04,012 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:04,012 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:04,012 INFO  L225             Difference]: With dead ends: 52
[2025-05-07 17:27:04,012 INFO  L226             Difference]: Without dead ends: 42
[2025-05-07 17:27:04,013 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:04,014 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 1 mSDsluCounter, 230 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 279 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:04,014 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 279 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:04,014 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-05-07 17:27:04,015 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-05-07 17:27:04,015 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 19 states have (on average 1.0) internal successors, (19), 19 states have internal predecessors, (19), 11 states have call successors, (11), 11 states have call predecessors, (11), 11 states have return successors, (11), 11 states have call predecessors, (11), 11 states have call successors, (11)
[2025-05-07 17:27:04,015 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 41 transitions.
[2025-05-07 17:27:04,015 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 41 transitions. Word has length 41
[2025-05-07 17:27:04,015 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:04,015 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 41 transitions.
[2025-05-07 17:27:04,016 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:04,016 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 41 transitions.
[2025-05-07 17:27:04,016 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:04,016 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:04,016 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]
[2025-05-07 17:27:04,016 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:27:04,016 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:04,016 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:04,017 INFO  L85        PathProgramCache]: Analyzing trace with hash -1732630254, now seen corresponding path program 1 times
[2025-05-07 17:27:04,017 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:04,017 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1791995369]
[2025-05-07 17:27:04,017 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:04,017 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:04,032 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:04,038 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:04,038 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:04,038 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:04,088 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:04,088 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:04,088 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1791995369]
[2025-05-07 17:27:04,088 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1791995369] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:04,088 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:04,088 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:04,088 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1023814796]
[2025-05-07 17:27:04,088 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:04,088 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:04,088 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:04,089 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:04,089 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:04,089 INFO  L87              Difference]: Start difference. First operand 42 states and 41 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:04,116 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:04,116 INFO  L93              Difference]: Finished difference Result 36 states and 35 transitions.
[2025-05-07 17:27:04,116 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:04,116 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:04,117 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:04,117 INFO  L225             Difference]: With dead ends: 36
[2025-05-07 17:27:04,117 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:04,117 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:04,117 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 0 mSDsluCounter, 147 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 179 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:04,117 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 179 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:04,118 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:04,118 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:04,118 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:27:04,118 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:04,118 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 41
[2025-05-07 17:27:04,118 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:04,118 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:04,118 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:04,118 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:04,118 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:04,120 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:04,120 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:27:04,123 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:04,124 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:04,127 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:04 BoogieIcfgContainer
[2025-05-07 17:27:04,127 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:04,127 INFO  L158              Benchmark]: Toolchain (without parser) took 4486.60ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 180.0MB in the beginning and 153.7MB in the end (delta: 26.3MB). Peak memory consumption was 71.9MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,127 INFO  L158              Benchmark]: SmtParser took 0.24ms. Allocated memory is still 234.9MB. Free memory is still 173.7MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:04,127 INFO  L158              Benchmark]: ChcToBoogie took 45.78ms. Allocated memory is still 234.9MB. Free memory was 180.0MB in the beginning and 171.7MB in the end (delta: 8.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:04,127 INFO  L158              Benchmark]: Boogie Preprocessor took 71.25ms. Allocated memory is still 234.9MB. Free memory was 171.7MB in the beginning and 166.4MB in the end (delta: 5.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:04,128 INFO  L158              Benchmark]: RCFGBuilder took 786.71ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 166.4MB in the beginning and 230.6MB in the end (delta: -64.2MB). Peak memory consumption was 75.6MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,128 INFO  L158              Benchmark]: TraceAbstraction took 3579.84ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 229.8MB in the beginning and 153.7MB in the end (delta: 76.1MB). Peak memory consumption was 47.4MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,128 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.24ms. Allocated memory is still 234.9MB. Free memory is still 173.7MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 45.78ms. Allocated memory is still 234.9MB. Free memory was 180.0MB in the beginning and 171.7MB in the end (delta: 8.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 71.25ms. Allocated memory is still 234.9MB. Free memory was 171.7MB in the beginning and 166.4MB in the end (delta: 5.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 786.71ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 166.4MB in the beginning and 230.6MB in the end (delta: -64.2MB). Peak memory consumption was 75.6MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3579.84ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 229.8MB in the beginning and 153.7MB in the end (delta: 76.1MB). Peak memory consumption was 47.4MB. 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 32 procedures, 128 locations, 228 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.5s, OverallIterations: 23, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 44 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 22 mSDsluCounter, 13343 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 10892 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 592 IncrementalHoareTripleChecker+Invalid, 592 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 2451 mSDtfsCounter, 592 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 155 GetRequests, 46 SyntacticMatches, 0 SemanticMatches, 109 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.4s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=128occurred in iteration=0, InterpolantAutomatonStates: 155, 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, 23 MinimizatonAttempts, 2 StatesRemovedByMinimization, 1 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.8s InterpolantComputationTime, 943 NumberOfCodeBlocks, 943 NumberOfCodeBlocksAsserted, 23 NumberOfCheckSat, 920 ConstructedInterpolants, 0 QuantifiedInterpolants, 1366 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 23 InterpolantComputations, 23 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:27:04,139 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
