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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:58,995 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:59,033 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_01b96f8f-aab1-4472-b45a-315cbd2a7d36/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:59,036 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:59,036 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:59,049 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:59,049 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:59,049 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:59,050 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:59,050 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:59,050 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:59,050 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:59,050 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:59,051 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:59,051 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:59,051 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:59,051 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:59,051 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:59,051 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:59,051 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:59,051 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:59,244 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:59,252 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:59,254 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:59,255 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:59,255 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:59,256 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_01b96f8f-aab1-4472-b45a-315cbd2a7d36/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_29_no_adts_000.smt2
[2025-05-07 17:26:59,257 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:59,259 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,657 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_01b96f8f-aab1-4472-b45a-315cbd2a7d36/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_29_no_adts_000.smt2
[2025-05-07 17:26:59,659 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:59,660 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:59,660 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:59,660 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:59,660 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:59,662 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,707 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,707 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:59,708 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:59,708 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:59,708 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:59,719 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,719 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,743 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,744 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,753 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,754 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,756 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,759 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,761 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,777 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:59,778 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:59,778 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:59,778 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:59,779 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,780 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:59,789 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:59,798 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,800 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,807 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:59,807 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:59,808 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_73_0 given in one single declaration
[2025-05-07 17:26:59,808 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_73_0
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_73_0
[2025-05-07 17:26:59,808 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,808 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_6_D_407_0
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_6_D_407_0
[2025-05-07 17:26:59,808 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,808 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_58_D_407_0
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_58_D_407_0
[2025-05-07 17:26:59,808 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,808 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_7_constructor_406_407_0
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_7_constructor_406_407_0
[2025-05-07 17:26:59,808 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,808 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_constructor_406_407_0
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_constructor_406_407_0
[2025-05-07 17:26:59,808 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36__405_407_0 given in one single declaration
[2025-05-07 17:26:59,808 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36__405_407_0
[2025-05-07 17:26:59,808 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36__405_407_0
[2025-05-07 17:26:59,808 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_constructor_406_407_0
[2025-05-07 17:26:59,809 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_constructor_406_407_0
[2025-05-07 17:26:59,809 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,809 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_constructor_406_407_0
[2025-05-07 17:26:59,810 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_constructor_406_407_0
[2025-05-07 17:26:59,810 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,810 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_constructor_406_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_constructor_406_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:26:59,811 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:26:59,811 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,811 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:26:59,812 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:26:59,812 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,812 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:26:59,812 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:26:59,812 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:59,812 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:59,812 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:00,084 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:00,086 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:00,537 INFO  L?                        ?]: Removed 1077 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:00,537 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:00,547 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:00,547 INFO  L312             CfgBuilder]: Removed 24 assume(true) statements.
[2025-05-07 17:27:00,548 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,548 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:00,550 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:00,550 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:00,553 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:00,553 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,554 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@307dee7d 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,554 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,554 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@307dee7d 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,554 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,555 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:00,566 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:00,568 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,602 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:00,611 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;@40050b06, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:00,612 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:00,615 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,624 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:00,624 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:00,625 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,625 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:00,629 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:00,630 INFO  L85        PathProgramCache]: Analyzing trace with hash 178904790, now seen corresponding path program 1 times
[2025-05-07 17:27:00,636 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:00,636 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2021396621]
[2025-05-07 17:27:00,636 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:00,636 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:00,683 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:00,725 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,726 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:00,726 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:00,916 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,916 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:00,917 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2021396621]
[2025-05-07 17:27:00,917 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2021396621] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:00,917 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:00,920 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:00,922 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1150776670]
[2025-05-07 17:27:00,922 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:00,927 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:00,927 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:00,960 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:00,961 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:00,963 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:01,030 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,030 INFO  L93              Difference]: Finished difference Result 130 states and 175 transitions.
[2025-05-07 17:27:01,032 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:01,033 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:01,033 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,039 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:01,039 INFO  L226             Difference]: Without dead ends: 130
[2025-05-07 17:27:01,040 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,042 INFO  L437           NwaCegarLoop]: 173 mSDtfsCounter, 1 mSDsluCounter, 333 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 506 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:01,043 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 506 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:01,052 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-05-07 17:27:01,072 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 128.
[2025-05-07 17:27:01,073 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,076 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 173 transitions.
[2025-05-07 17:27:01,077 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 173 transitions. Word has length 41
[2025-05-07 17:27:01,078 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,078 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 173 transitions.
[2025-05-07 17:27:01,078 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,078 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 173 transitions.
[2025-05-07 17:27:01,080 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,080 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,080 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,080 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:01,080 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,081 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,081 INFO  L85        PathProgramCache]: Analyzing trace with hash 947014774, now seen corresponding path program 1 times
[2025-05-07 17:27:01,081 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,081 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [545220205]
[2025-05-07 17:27:01,081 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,081 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,101 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,109 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,109 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,109 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,176 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,176 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,176 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [545220205]
[2025-05-07 17:27:01,176 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [545220205] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,176 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,177 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:01,177 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1514126481]
[2025-05-07 17:27:01,177 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,178 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:01,178 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,178 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:01,178 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:01,178 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,192 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,192 INFO  L93              Difference]: Finished difference Result 130 states and 174 transitions.
[2025-05-07 17:27:01,193 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:01,193 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,193 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,194 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:01,194 INFO  L226             Difference]: Without dead ends: 122
[2025-05-07 17:27:01,194 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,195 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,195 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,196 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 122 states.
[2025-05-07 17:27:01,202 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 122 to 122.
[2025-05-07 17:27:01,202 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,203 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 161 transitions.
[2025-05-07 17:27:01,203 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 161 transitions. Word has length 41
[2025-05-07 17:27:01,204 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,204 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 161 transitions.
[2025-05-07 17:27:01,204 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,204 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 161 transitions.
[2025-05-07 17:27:01,205 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,205 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,205 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,205 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:01,205 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,206 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,206 INFO  L85        PathProgramCache]: Analyzing trace with hash 56527718, now seen corresponding path program 1 times
[2025-05-07 17:27:01,206 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,206 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1147463070]
[2025-05-07 17:27:01,206 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,206 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,222 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,239 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,239 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,335 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,335 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,335 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1147463070]
[2025-05-07 17:27:01,335 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1147463070] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,335 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,335 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,335 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [48163678]
[2025-05-07 17:27:01,335 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,336 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,336 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,336 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,336 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,336 INFO  L87              Difference]: Start difference. First operand 122 states and 161 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,378 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,379 INFO  L93              Difference]: Finished difference Result 128 states and 166 transitions.
[2025-05-07 17:27:01,379 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:01,379 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,379 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,380 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:27:01,380 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:27:01,380 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,381 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 1 mSDsluCounter, 800 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 963 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,381 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 963 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,381 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:27:01,386 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 118.
[2025-05-07 17:27:01,386 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,387 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 155 transitions.
[2025-05-07 17:27:01,387 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 155 transitions. Word has length 41
[2025-05-07 17:27:01,387 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,387 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 155 transitions.
[2025-05-07 17:27:01,387 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,387 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 155 transitions.
[2025-05-07 17:27:01,388 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,388 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,388 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,388 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:01,388 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,388 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,389 INFO  L85        PathProgramCache]: Analyzing trace with hash 489574156, now seen corresponding path program 1 times
[2025-05-07 17:27:01,389 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,389 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [279474562]
[2025-05-07 17:27:01,389 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,389 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,403 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,411 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,411 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,411 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,479 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,479 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,480 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [279474562]
[2025-05-07 17:27:01,480 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [279474562] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,480 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,480 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,480 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1449797339]
[2025-05-07 17:27:01,480 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,480 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,480 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,481 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,481 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,481 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,522 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,522 INFO  L93              Difference]: Finished difference Result 124 states and 160 transitions.
[2025-05-07 17:27:01,523 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:01,523 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,523 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,524 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:27:01,524 INFO  L226             Difference]: Without dead ends: 114
[2025-05-07 17:27:01,524 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,524 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,525 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,525 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-05-07 17:27:01,529 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 114.
[2025-05-07 17:27:01,530 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,530 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 149 transitions.
[2025-05-07 17:27:01,531 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 149 transitions. Word has length 41
[2025-05-07 17:27:01,531 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,531 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 149 transitions.
[2025-05-07 17:27:01,531 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,531 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 149 transitions.
[2025-05-07 17:27:01,532 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,532 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,532 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,532 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:01,532 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,532 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,532 INFO  L85        PathProgramCache]: Analyzing trace with hash 1693699916, now seen corresponding path program 1 times
[2025-05-07 17:27:01,532 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,532 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [768206423]
[2025-05-07 17:27:01,532 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,533 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,547 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,559 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,559 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,559 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,655 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,655 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,655 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [768206423]
[2025-05-07 17:27:01,655 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [768206423] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,655 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,656 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,656 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1099240611]
[2025-05-07 17:27:01,656 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,656 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,656 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,657 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,657 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,657 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:01,696 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,696 INFO  L93              Difference]: Finished difference Result 120 states and 154 transitions.
[2025-05-07 17:27:01,696 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, 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,697 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,698 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:27:01,698 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:27:01,698 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,699 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:01,699 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:01,700 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:27:01,707 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 110.
[2025-05-07 17:27:01,707 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:01,708 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 110 states to 110 states and 143 transitions.
[2025-05-07 17:27:01,708 INFO  L79                 Accepts]: Start accepts. Automaton has 110 states and 143 transitions. Word has length 41
[2025-05-07 17:27:01,708 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,708 INFO  L485      AbstractCegarLoop]: Abstraction has 110 states and 143 transitions.
[2025-05-07 17:27:01,708 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,709 INFO  L278                IsEmpty]: Start isEmpty. Operand 110 states and 143 transitions.
[2025-05-07 17:27:01,709 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,710 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,710 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,710 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:01,710 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,710 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,710 INFO  L85        PathProgramCache]: Analyzing trace with hash 222775180, now seen corresponding path program 1 times
[2025-05-07 17:27:01,710 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,711 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1409517524]
[2025-05-07 17:27:01,711 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,711 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,732 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,744 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,744 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,744 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,809 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,809 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,809 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1409517524]
[2025-05-07 17:27:01,809 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1409517524] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,809 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,810 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,810 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [121442105]
[2025-05-07 17:27:01,810 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,810 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,810 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,810 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,810 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,810 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:01,841 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,841 INFO  L93              Difference]: Finished difference Result 116 states and 148 transitions.
[2025-05-07 17:27:01,841 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:01,842 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,842 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,842 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:01,842 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:27:01,843 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,843 INFO  L437           NwaCegarLoop]: 145 mSDtfsCounter, 1 mSDsluCounter, 710 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 855 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,843 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 855 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,844 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:27:01,847 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:27:01,847 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:01,848 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 137 transitions.
[2025-05-07 17:27:01,848 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 137 transitions. Word has length 41
[2025-05-07 17:27:01,848 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,848 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 137 transitions.
[2025-05-07 17:27:01,848 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,848 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 137 transitions.
[2025-05-07 17:27:01,849 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,849 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,849 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:01,849 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,849 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,849 INFO  L85        PathProgramCache]: Analyzing trace with hash -1899512020, now seen corresponding path program 1 times
[2025-05-07 17:27:01,849 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,849 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [564473870]
[2025-05-07 17:27:01,849 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,849 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,864 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:01,873 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,873 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:01,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:01,936 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,936 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:01,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [564473870]
[2025-05-07 17:27:01,936 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [564473870] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:01,936 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:01,936 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:01,936 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1748103363]
[2025-05-07 17:27:01,936 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:01,937 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:01,937 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:01,937 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:01,937 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:01,937 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:01,972 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:01,972 INFO  L93              Difference]: Finished difference Result 112 states and 142 transitions.
[2025-05-07 17:27:01,972 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:01,973 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,973 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:01,973 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:27:01,973 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:27:01,973 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,974 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:01,974 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:01,975 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:27:01,978 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:27:01,978 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:01,978 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 131 transitions.
[2025-05-07 17:27:01,978 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 131 transitions. Word has length 41
[2025-05-07 17:27:01,979 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:01,979 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 131 transitions.
[2025-05-07 17:27:01,979 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,979 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 131 transitions.
[2025-05-07 17:27:01,979 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:01,979 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:01,979 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,979 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:01,980 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:01,980 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:01,980 INFO  L85        PathProgramCache]: Analyzing trace with hash 1257378642, now seen corresponding path program 1 times
[2025-05-07 17:27:01,980 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:01,980 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1142627162]
[2025-05-07 17:27:01,980 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:01,980 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:01,993 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,000 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,000 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,000 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,070 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,070 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,070 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1142627162]
[2025-05-07 17:27:02,070 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1142627162] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,070 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,070 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,070 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1143977863]
[2025-05-07 17:27:02,070 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,070 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,071 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,071 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,071 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,071 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,104 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,104 INFO  L93              Difference]: Finished difference Result 108 states and 136 transitions.
[2025-05-07 17:27:02,104 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,105 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,105 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,106 INFO  L225             Difference]: With dead ends: 108
[2025-05-07 17:27:02,106 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:27:02,106 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,106 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,107 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,107 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:27:02,112 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:27:02,112 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,113 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 125 transitions.
[2025-05-07 17:27:02,113 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 125 transitions. Word has length 41
[2025-05-07 17:27:02,113 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,113 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 125 transitions.
[2025-05-07 17:27:02,113 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,113 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 125 transitions.
[2025-05-07 17:27:02,114 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,114 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,114 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,114 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:02,114 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,115 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,115 INFO  L85        PathProgramCache]: Analyzing trace with hash -1272845470, now seen corresponding path program 1 times
[2025-05-07 17:27:02,115 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,115 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [496102282]
[2025-05-07 17:27:02,115 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,115 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,130 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,141 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,141 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,141 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,212 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,212 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,212 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [496102282]
[2025-05-07 17:27:02,212 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [496102282] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,212 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,212 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,212 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1713284971]
[2025-05-07 17:27:02,212 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,213 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,213 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,213 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,213 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,213 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,247 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,248 INFO  L93              Difference]: Finished difference Result 104 states and 130 transitions.
[2025-05-07 17:27:02,248 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,248 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,249 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,249 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:27:02,249 INFO  L226             Difference]: Without dead ends: 94
[2025-05-07 17:27:02,250 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,250 INFO  L437           NwaCegarLoop]: 127 mSDtfsCounter, 1 mSDsluCounter, 620 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 747 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,250 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 747 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,251 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-05-07 17:27:02,255 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 94.
[2025-05-07 17:27:02,255 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,256 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 119 transitions.
[2025-05-07 17:27:02,256 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 119 transitions. Word has length 41
[2025-05-07 17:27:02,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,256 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 119 transitions.
[2025-05-07 17:27:02,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:02,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 119 transitions.
[2025-05-07 17:27:02,257 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,257 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,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:02,258 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:02,258 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,258 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,258 INFO  L85        PathProgramCache]: Analyzing trace with hash -1916706984, now seen corresponding path program 1 times
[2025-05-07 17:27:02,258 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,258 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [194868527]
[2025-05-07 17:27:02,258 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,258 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,275 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,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:02,286 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,286 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,364 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,364 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,364 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [194868527]
[2025-05-07 17:27:02,364 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [194868527] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,364 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,364 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,364 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1318515626]
[2025-05-07 17:27:02,364 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,364 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,364 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,365 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,365 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,365 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,397 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,397 INFO  L93              Difference]: Finished difference Result 100 states and 124 transitions.
[2025-05-07 17:27:02,398 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,398 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,398 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,399 INFO  L225             Difference]: With dead ends: 100
[2025-05-07 17:27:02,399 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:27:02,399 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,399 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,399 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,400 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:27:02,402 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:27:02,402 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,402 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 113 transitions.
[2025-05-07 17:27:02,403 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 113 transitions. Word has length 41
[2025-05-07 17:27:02,403 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,403 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 113 transitions.
[2025-05-07 17:27:02,403 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,403 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 113 transitions.
[2025-05-07 17:27:02,403 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,403 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,403 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,403 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:02,404 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,404 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,404 INFO  L85        PathProgramCache]: Analyzing trace with hash -299824302, now seen corresponding path program 1 times
[2025-05-07 17:27:02,404 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,404 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [50174671]
[2025-05-07 17:27:02,404 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,404 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,418 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,423 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,424 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,424 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,483 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,483 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,484 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [50174671]
[2025-05-07 17:27:02,484 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [50174671] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,484 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,484 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,484 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1729462938]
[2025-05-07 17:27:02,484 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,484 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,484 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,485 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,485 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,485 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,515 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,515 INFO  L93              Difference]: Finished difference Result 96 states and 118 transitions.
[2025-05-07 17:27:02,515 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,516 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,516 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,516 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:27:02,516 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:27:02,516 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,517 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,517 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,517 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:27:02,519 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:27:02,519 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,519 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 107 transitions.
[2025-05-07 17:27:02,519 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 107 transitions. Word has length 41
[2025-05-07 17:27:02,520 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,520 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 107 transitions.
[2025-05-07 17:27:02,520 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,520 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 107 transitions.
[2025-05-07 17:27:02,520 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,520 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,520 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,520 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:27:02,520 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,521 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,521 INFO  L85        PathProgramCache]: Analyzing trace with hash 1341870958, now seen corresponding path program 1 times
[2025-05-07 17:27:02,521 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,521 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1396323464]
[2025-05-07 17:27:02,521 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,521 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,541 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,541 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,541 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,597 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,598 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,598 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1396323464]
[2025-05-07 17:27:02,598 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1396323464] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,598 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,598 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,598 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1918248164]
[2025-05-07 17:27:02,598 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,598 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,598 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,599 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,599 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,599 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,630 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,630 INFO  L93              Difference]: Finished difference Result 92 states and 112 transitions.
[2025-05-07 17:27:02,630 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,630 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,631 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,631 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:27:02,631 INFO  L226             Difference]: Without dead ends: 82
[2025-05-07 17:27:02,631 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,631 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 530 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 639 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,632 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 639 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,632 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-05-07 17:27:02,634 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 82.
[2025-05-07 17:27:02,634 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,634 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 101 transitions.
[2025-05-07 17:27:02,634 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 101 transitions. Word has length 41
[2025-05-07 17:27:02,634 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,634 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 101 transitions.
[2025-05-07 17:27:02,634 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,634 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 101 transitions.
[2025-05-07 17:27:02,635 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,635 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,635 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,635 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:27:02,635 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,635 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,635 INFO  L85        PathProgramCache]: Analyzing trace with hash 138282864, now seen corresponding path program 1 times
[2025-05-07 17:27:02,635 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,635 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [437424944]
[2025-05-07 17:27:02,635 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,636 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,649 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,654 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,654 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,654 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,704 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,704 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,705 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [437424944]
[2025-05-07 17:27:02,705 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [437424944] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,705 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,705 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,705 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [548136205]
[2025-05-07 17:27:02,705 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,705 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,705 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,706 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,706 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,706 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:02,737 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,737 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:27:02,737 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,737 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,738 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:27:02,738 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:27:02,738 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,738 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:02,738 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:02,739 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:27:02,740 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:27:02,741 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:02,741 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 95 transitions.
[2025-05-07 17:27:02,741 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 95 transitions. Word has length 41
[2025-05-07 17:27:02,741 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,741 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 95 transitions.
[2025-05-07 17:27:02,741 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,741 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 95 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,742 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,742 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,742 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:27:02,742 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,742 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,742 INFO  L85        PathProgramCache]: Analyzing trace with hash 1318960936, now seen corresponding path program 1 times
[2025-05-07 17:27:02,742 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,742 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [513925642]
[2025-05-07 17:27:02,742 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,742 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,757 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,765 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,765 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:02,823 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,823 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:02,823 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [513925642]
[2025-05-07 17:27:02,823 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [513925642] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:02,823 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:02,824 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:02,824 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [967646573]
[2025-05-07 17:27:02,824 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:02,824 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:02,824 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:02,824 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:02,824 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:02,825 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:02,853 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,853 INFO  L93              Difference]: Finished difference Result 84 states and 100 transitions.
[2025-05-07 17:27:02,854 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:02,854 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,854 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:02,854 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:27:02,854 INFO  L226             Difference]: Without dead ends: 74
[2025-05-07 17:27:02,854 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,855 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:02,855 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:02,855 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-05-07 17:27:02,857 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 74.
[2025-05-07 17:27:02,857 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:02,857 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 89 transitions.
[2025-05-07 17:27:02,857 INFO  L79                 Accepts]: Start accepts. Automaton has 74 states and 89 transitions. Word has length 41
[2025-05-07 17:27:02,857 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:02,858 INFO  L485      AbstractCegarLoop]: Abstraction has 74 states and 89 transitions.
[2025-05-07 17:27:02,858 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,858 INFO  L278                IsEmpty]: Start isEmpty. Operand 74 states and 89 transitions.
[2025-05-07 17:27:02,858 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:02,858 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:02,858 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,858 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:27:02,858 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:02,858 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:02,858 INFO  L85        PathProgramCache]: Analyzing trace with hash -879960248, now seen corresponding path program 1 times
[2025-05-07 17:27:02,858 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:02,859 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [419040900]
[2025-05-07 17:27:02,859 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:02,859 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:02,871 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:02,882 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,882 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:02,882 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,040 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,040 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,040 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [419040900]
[2025-05-07 17:27:03,040 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [419040900] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,040 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,040 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,040 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1447780297]
[2025-05-07 17:27:03,040 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,041 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,041 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,041 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,041 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,041 INFO  L87              Difference]: Start difference. First operand 74 states and 89 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:03,141 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,141 INFO  L93              Difference]: Finished difference Result 76 states and 90 transitions.
[2025-05-07 17:27:03,141 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,141 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:03,141 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,142 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:27:03,142 INFO  L226             Difference]: Without dead ends: 70
[2025-05-07 17:27:03,142 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:03,142 INFO  L437           NwaCegarLoop]: 79 mSDtfsCounter, 1 mSDsluCounter, 370 mSDsCounter, 0 mSdLazyCounter, 77 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 449 SdHoareTripleChecker+Invalid, 77 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 77 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:03,142 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 449 Invalid, 77 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 77 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:03,143 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-05-07 17:27:03,144 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-05-07 17:27:03,144 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,144 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 83 transitions.
[2025-05-07 17:27:03,144 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 83 transitions. Word has length 41
[2025-05-07 17:27:03,144 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,144 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 83 transitions.
[2025-05-07 17:27:03,144 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:03,145 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 83 transitions.
[2025-05-07 17:27:03,145 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,145 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,145 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,145 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:27:03,145 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,146 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,146 INFO  L85        PathProgramCache]: Analyzing trace with hash -1090595040, now seen corresponding path program 1 times
[2025-05-07 17:27:03,146 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,146 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1650613819]
[2025-05-07 17:27:03,146 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,146 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,161 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,168 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,168 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,168 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,238 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,239 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,239 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1650613819]
[2025-05-07 17:27:03,239 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1650613819] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,239 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,239 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,239 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [376497842]
[2025-05-07 17:27:03,239 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,239 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,239 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,240 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,240 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,240 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,269 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,269 INFO  L93              Difference]: Finished difference Result 76 states and 88 transitions.
[2025-05-07 17:27:03,269 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,270 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,270 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,270 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:27:03,270 INFO  L226             Difference]: Without dead ends: 66
[2025-05-07 17:27:03,270 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,271 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,271 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,271 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-05-07 17:27:03,272 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-05-07 17:27:03,272 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,272 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 77 transitions.
[2025-05-07 17:27:03,273 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 77 transitions. Word has length 41
[2025-05-07 17:27:03,273 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,273 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 77 transitions.
[2025-05-07 17:27:03,273 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,273 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 77 transitions.
[2025-05-07 17:27:03,273 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,273 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,273 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,273 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:27:03,273 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,274 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,274 INFO  L85        PathProgramCache]: Analyzing trace with hash -1190139046, now seen corresponding path program 1 times
[2025-05-07 17:27:03,274 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,274 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [226902361]
[2025-05-07 17:27:03,274 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,274 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,287 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,292 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,292 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,292 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,341 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,341 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,341 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [226902361]
[2025-05-07 17:27:03,341 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [226902361] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,341 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,341 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,341 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [78281192]
[2025-05-07 17:27:03,341 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,341 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,341 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,342 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,342 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,342 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,371 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,371 INFO  L93              Difference]: Finished difference Result 72 states and 82 transitions.
[2025-05-07 17:27:03,371 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,371 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,372 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,372 INFO  L225             Difference]: With dead ends: 72
[2025-05-07 17:27:03,372 INFO  L226             Difference]: Without dead ends: 62
[2025-05-07 17:27:03,372 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,373 INFO  L437           NwaCegarLoop]: 79 mSDtfsCounter, 1 mSDsluCounter, 380 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 459 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,373 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 459 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,373 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-05-07 17:27:03,374 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 62.
[2025-05-07 17:27:03,374 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,375 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 71 transitions.
[2025-05-07 17:27:03,375 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 71 transitions. Word has length 41
[2025-05-07 17:27:03,375 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,375 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 71 transitions.
[2025-05-07 17:27:03,375 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,375 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 71 transitions.
[2025-05-07 17:27:03,375 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,375 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,375 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,375 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:27:03,375 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,376 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,376 INFO  L85        PathProgramCache]: Analyzing trace with hash 2024645462, now seen corresponding path program 1 times
[2025-05-07 17:27:03,376 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,376 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [174187053]
[2025-05-07 17:27:03,376 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,376 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,390 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,397 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,397 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,397 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,446 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,447 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,447 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [174187053]
[2025-05-07 17:27:03,447 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [174187053] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,447 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,447 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,447 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [151565378]
[2025-05-07 17:27:03,447 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,447 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,447 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,448 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,448 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,448 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,476 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,476 INFO  L93              Difference]: Finished difference Result 68 states and 76 transitions.
[2025-05-07 17:27:03,476 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,476 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,476 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,477 INFO  L225             Difference]: With dead ends: 68
[2025-05-07 17:27:03,477 INFO  L226             Difference]: Without dead ends: 58
[2025-05-07 17:27:03,477 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,477 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,477 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,478 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-05-07 17:27:03,479 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 58.
[2025-05-07 17:27:03,480 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,480 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 65 transitions.
[2025-05-07 17:27:03,480 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 65 transitions. Word has length 41
[2025-05-07 17:27:03,480 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,480 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 65 transitions.
[2025-05-07 17:27:03,480 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,481 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 65 transitions.
[2025-05-07 17:27:03,481 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,481 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,481 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,481 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:27:03,481 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,481 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,481 INFO  L85        PathProgramCache]: Analyzing trace with hash -984384698, now seen corresponding path program 1 times
[2025-05-07 17:27:03,481 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,481 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [710911915]
[2025-05-07 17:27:03,481 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,482 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,494 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,500 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,500 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,500 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,585 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,586 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,586 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [710911915]
[2025-05-07 17:27:03,586 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [710911915] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,586 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,586 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,586 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1192208265]
[2025-05-07 17:27:03,586 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,586 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,586 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,587 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,587 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,587 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,610 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,611 INFO  L93              Difference]: Finished difference Result 64 states and 70 transitions.
[2025-05-07 17:27:03,611 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,611 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,611 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,612 INFO  L225             Difference]: With dead ends: 64
[2025-05-07 17:27:03,612 INFO  L226             Difference]: Without dead ends: 54
[2025-05-07 17:27:03,612 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,612 INFO  L437           NwaCegarLoop]: 67 mSDtfsCounter, 1 mSDsluCounter, 322 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 389 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:03,612 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 389 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:03,613 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-05-07 17:27:03,614 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 54.
[2025-05-07 17:27:03,615 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,615 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 59 transitions.
[2025-05-07 17:27:03,615 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 59 transitions. Word has length 41
[2025-05-07 17:27:03,615 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,615 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 59 transitions.
[2025-05-07 17:27:03,615 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,615 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 59 transitions.
[2025-05-07 17:27:03,616 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,616 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,616 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,616 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:27:03,616 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,616 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,617 INFO  L85        PathProgramCache]: Analyzing trace with hash 886568828, now seen corresponding path program 1 times
[2025-05-07 17:27:03,617 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,617 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2080403377]
[2025-05-07 17:27:03,617 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,617 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,632 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,640 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,641 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,641 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,704 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,704 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,704 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2080403377]
[2025-05-07 17:27:03,704 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2080403377] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,704 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,704 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,704 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [448999908]
[2025-05-07 17:27:03,704 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,705 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,705 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,705 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,705 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,705 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,731 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,731 INFO  L93              Difference]: Finished difference Result 60 states and 64 transitions.
[2025-05-07 17:27:03,731 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,732 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,732 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,732 INFO  L225             Difference]: With dead ends: 60
[2025-05-07 17:27:03,732 INFO  L226             Difference]: Without dead ends: 50
[2025-05-07 17:27:03,732 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,733 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,733 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,733 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-05-07 17:27:03,734 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 50.
[2025-05-07 17:27:03,734 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,735 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 53 transitions.
[2025-05-07 17:27:03,735 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 53 transitions. Word has length 41
[2025-05-07 17:27:03,735 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,735 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 53 transitions.
[2025-05-07 17:27:03,735 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,735 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 53 transitions.
[2025-05-07 17:27:03,736 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,736 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,736 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,736 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:27:03,736 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,736 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,736 INFO  L85        PathProgramCache]: Analyzing trace with hash 2086170576, now seen corresponding path program 1 times
[2025-05-07 17:27:03,736 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,736 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1009877647]
[2025-05-07 17:27:03,736 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,737 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,755 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,761 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,761 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,761 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,820 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,820 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,820 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1009877647]
[2025-05-07 17:27:03,820 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1009877647] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,820 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,820 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,820 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [115222096]
[2025-05-07 17:27:03,820 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,821 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,821 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,821 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,821 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,821 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,852 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,852 INFO  L93              Difference]: Finished difference Result 56 states and 58 transitions.
[2025-05-07 17:27:03,852 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,852 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,852 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,853 INFO  L225             Difference]: With dead ends: 56
[2025-05-07 17:27:03,853 INFO  L226             Difference]: Without dead ends: 46
[2025-05-07 17:27:03,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:03,853 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,853 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,854 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-05-07 17:27:03,855 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 46.
[2025-05-07 17:27:03,855 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,855 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 47 transitions.
[2025-05-07 17:27:03,855 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 47 transitions. Word has length 41
[2025-05-07 17:27:03,855 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,855 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 47 transitions.
[2025-05-07 17:27:03,856 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,856 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 47 transitions.
[2025-05-07 17:27:03,856 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,856 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,856 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,856 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:27:03,857 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,857 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,857 INFO  L85        PathProgramCache]: Analyzing trace with hash 281620304, now seen corresponding path program 1 times
[2025-05-07 17:27:03,857 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,857 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [607238853]
[2025-05-07 17:27:03,857 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,857 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,872 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,876 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,876 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,876 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:03,924 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,924 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:03,924 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [607238853]
[2025-05-07 17:27:03,924 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [607238853] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:03,924 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:03,924 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:03,924 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [702009520]
[2025-05-07 17:27:03,924 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:03,924 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:03,925 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:03,925 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:03,925 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:03,925 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:03,949 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:03,949 INFO  L93              Difference]: Finished difference Result 52 states and 52 transitions.
[2025-05-07 17:27:03,950 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:03,950 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,950 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:03,950 INFO  L225             Difference]: With dead ends: 52
[2025-05-07 17:27:03,950 INFO  L226             Difference]: Without dead ends: 42
[2025-05-07 17:27:03,951 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,952 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:03,952 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:03,952 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-05-07 17:27:03,953 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-05-07 17:27:03,953 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:03,953 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 41 transitions.
[2025-05-07 17:27:03,953 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 41 transitions. Word has length 41
[2025-05-07 17:27:03,953 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:03,953 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 41 transitions.
[2025-05-07 17:27:03,953 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,954 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 41 transitions.
[2025-05-07 17:27:03,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:03,954 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:03,954 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,954 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:27:03,954 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:03,954 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:03,955 INFO  L85        PathProgramCache]: Analyzing trace with hash 678671206, now seen corresponding path program 1 times
[2025-05-07 17:27:03,955 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:03,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1570465055]
[2025-05-07 17:27:03,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:03,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:03,969 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:03,974 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,974 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:03,974 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:04,022 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,022 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:04,022 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1570465055]
[2025-05-07 17:27:04,022 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1570465055] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:04,022 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:04,022 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:04,022 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [527180379]
[2025-05-07 17:27:04,022 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:04,023 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:04,023 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:04,023 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:04,023 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:04,023 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,050 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:04,051 INFO  L93              Difference]: Finished difference Result 36 states and 35 transitions.
[2025-05-07 17:27:04,051 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:04,051 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,051 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:04,051 INFO  L225             Difference]: With dead ends: 36
[2025-05-07 17:27:04,051 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:04,052 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,052 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,052 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,052 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:04,053 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:04,053 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,053 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:04,053 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 41
[2025-05-07 17:27:04,053 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:04,053 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:04,053 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,053 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:04,053 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:04,055 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:04,056 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:27:04,059 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,061 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:04,064 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,064 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:04,065 INFO  L158              Benchmark]: Toolchain (without parser) took 4404.90ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 181.7MB in the beginning and 86.0MB in the end (delta: 95.7MB). Peak memory consumption was 147.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,065 INFO  L158              Benchmark]: SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 174.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:04,065 INFO  L158              Benchmark]: ChcToBoogie took 47.55ms. Allocated memory is still 234.9MB. Free memory was 181.7MB in the beginning and 172.8MB in the end (delta: 9.0MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,065 INFO  L158              Benchmark]: Boogie Preprocessor took 69.26ms. Allocated memory is still 234.9MB. Free memory was 172.8MB in the beginning and 168.1MB in the end (delta: 4.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:04,065 INFO  L158              Benchmark]: RCFGBuilder took 770.25ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 168.1MB in the beginning and 232.2MB in the end (delta: -64.2MB). Peak memory consumption was 75.3MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,065 INFO  L158              Benchmark]: TraceAbstraction took 3514.42ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 231.3MB in the beginning and 86.0MB in the end (delta: 145.3MB). Peak memory consumption was 107.4MB. Max. memory is 33.6GB.
[2025-05-07 17:27:04,066 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 174.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 47.55ms. Allocated memory is still 234.9MB. Free memory was 181.7MB in the beginning and 172.8MB in the end (delta: 9.0MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 69.26ms. Allocated memory is still 234.9MB. Free memory was 172.8MB in the beginning and 168.1MB in the end (delta: 4.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 770.25ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 168.1MB in the beginning and 232.2MB in the end (delta: -64.2MB). Peak memory consumption was 75.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3514.42ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 231.3MB in the beginning and 86.0MB in the end (delta: 145.3MB). Peak memory consumption was 107.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: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 44 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 22 mSDsluCounter, 13507 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 11027 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 508 IncrementalHoareTripleChecker+Invalid, 508 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 2480 mSDtfsCounter, 508 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.7s InterpolantComputationTime, 943 NumberOfCodeBlocks, 943 NumberOfCodeBlocksAsserted, 23 NumberOfCheckSat, 920 ConstructedInterpolants, 0 QuantifiedInterpolants, 1384 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,076 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
