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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:05,655 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:05,692 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c717e01-3f37-46d9-bb6f-72fda8358c0a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:05,695 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:05,695 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:05,708 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:05,709 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:05,709 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:05,709 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:05,709 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:05,709 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:05,709 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:05,710 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:05,710 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:05,710 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:05,710 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:05,710 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:05,710 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:05,710 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:05,710 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:05,711 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:05,711 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:05,711 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:05,711 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:05,711 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:05,712 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:05,712 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:05,889 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:05,895 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:05,897 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:05,898 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:05,898 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:05,899 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c717e01-3f37-46d9-bb6f-72fda8358c0a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_26_no_adts_000.smt2
[2025-05-07 17:27:05,900 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:05,902 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:06,268 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c717e01-3f37-46d9-bb6f-72fda8358c0a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_26_no_adts_000.smt2
[2025-05-07 17:27:06,270 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:06,271 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:06,271 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:06,271 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:06,271 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:06,273 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,319 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06 Unit
[2025-05-07 17:27:06,319 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:06,320 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:06,320 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:06,320 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:06,330 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,331 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,357 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,357 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,366 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,367 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,369 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,372 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,374 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,391 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:06,392 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:06,392 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:06,392 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:06,392 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (1/1) ...
[2025-05-07 17:27:06,394 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:06,402 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:06,411 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:27:06,414 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:27:06,422 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:06,422 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:06,422 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:06,422 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_69_0 given in one single declaration
[2025-05-07 17:27:06,422 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_69_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_69_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_6_D_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_6_D_407_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_6_D_407_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_58_D_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_58_D_407_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_58_D_407_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_7_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_7_constructor_406_407_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_7_constructor_406_407_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_constructor_406_407_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_constructor_406_407_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36__405_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36__405_407_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36__405_407_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_constructor_406_407_0
[2025-05-07 17:27:06,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_constructor_406_407_0
[2025-05-07 17:27:06,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,423 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,424 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_constructor_406_407_0
[2025-05-07 17:27:06,424 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,425 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_constructor_406_407_0
[2025-05-07 17:27:06,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_return_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_constructor_406_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_constructor_406_407_0
[2025-05-07 17:27:06,426 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:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_59_D_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_61_D_407_0 given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:27:06,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:06,426 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:06,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:06,707 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:06,708 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:07,174 INFO  L?                        ?]: Removed 1077 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:07,174 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:07,183 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:07,184 INFO  L312             CfgBuilder]: Removed 24 assume(true) statements.
[2025-05-07 17:27:07,184 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:07 BoogieIcfgContainer
[2025-05-07 17:27:07,184 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:07,185 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:07,186 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:07,188 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:07,188 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:06" (1/3) ...
[2025-05-07 17:27:07,189 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5f677a9e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:07, skipping insertion in model container
[2025-05-07 17:27:07,189 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:06" (2/3) ...
[2025-05-07 17:27:07,189 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5f677a9e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:07, skipping insertion in model container
[2025-05-07 17:27:07,189 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:07" (3/3) ...
[2025-05-07 17:27:07,190 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:07,201 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:07,202 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:07,232 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:07,241 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;@46ffa062, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:07,241 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:07,244 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:07,251 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:07,251 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:07,252 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:07,252 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:07,256 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:07,256 INFO  L85        PathProgramCache]: Analyzing trace with hash -1320596194, now seen corresponding path program 1 times
[2025-05-07 17:27:07,261 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:07,262 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1488542063]
[2025-05-07 17:27:07,262 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:07,262 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:07,305 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:07,335 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:07,335 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:07,335 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:07,510 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:07,510 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:07,510 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1488542063]
[2025-05-07 17:27:07,511 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1488542063] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:07,511 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:07,513 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:07,514 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [82287016]
[2025-05-07 17:27:07,515 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:07,517 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:07,517 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:07,547 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:07,548 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:07,550 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:07,618 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:07,618 INFO  L93              Difference]: Finished difference Result 130 states and 175 transitions.
[2025-05-07 17:27:07,620 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:07,621 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:07,621 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:07,630 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:07,630 INFO  L226             Difference]: Without dead ends: 130
[2025-05-07 17:27:07,632 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:07,634 INFO  L437           NwaCegarLoop]: 171 mSDtfsCounter, 1 mSDsluCounter, 330 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 501 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:07,635 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 501 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:07,650 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-05-07 17:27:07,672 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 128.
[2025-05-07 17:27:07,673 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:07,677 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 173 transitions.
[2025-05-07 17:27:07,678 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 173 transitions. Word has length 41
[2025-05-07 17:27:07,679 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:07,679 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 173 transitions.
[2025-05-07 17:27:07,679 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:07,680 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 173 transitions.
[2025-05-07 17:27:07,682 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:07,682 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:07,682 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:07,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:07,683 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:07,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:07,684 INFO  L85        PathProgramCache]: Analyzing trace with hash -348517754, now seen corresponding path program 1 times
[2025-05-07 17:27:07,684 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:07,684 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [826052060]
[2025-05-07 17:27:07,684 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:07,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:07,707 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:07,716 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:07,716 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:07,716 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:07,832 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:07,832 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:07,833 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [826052060]
[2025-05-07 17:27:07,833 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [826052060] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:07,833 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:07,833 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:07,833 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1926200242]
[2025-05-07 17:27:07,833 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:07,834 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:07,834 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:07,835 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:07,835 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:07,835 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:07,856 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:07,856 INFO  L93              Difference]: Finished difference Result 130 states and 174 transitions.
[2025-05-07 17:27:07,857 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:07,857 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:07,857 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:07,859 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:07,859 INFO  L226             Difference]: Without dead ends: 122
[2025-05-07 17:27:07,859 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:07,860 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:07,860 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:07,861 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 122 states.
[2025-05-07 17:27:07,870 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 122 to 122.
[2025-05-07 17:27:07,870 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:07,872 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 161 transitions.
[2025-05-07 17:27:07,872 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 161 transitions. Word has length 41
[2025-05-07 17:27:07,872 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:07,872 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 161 transitions.
[2025-05-07 17:27:07,872 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:07,872 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 161 transitions.
[2025-05-07 17:27:07,874 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:07,874 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:07,874 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:07,874 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:07,875 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:07,875 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:07,875 INFO  L85        PathProgramCache]: Analyzing trace with hash -554624698, now seen corresponding path program 1 times
[2025-05-07 17:27:07,875 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:07,875 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [230200243]
[2025-05-07 17:27:07,875 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:07,875 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:07,894 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:07,916 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:07,916 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:07,916 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,030 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:08,030 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,030 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [230200243]
[2025-05-07 17:27:08,030 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [230200243] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,030 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,030 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,031 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1742491422]
[2025-05-07 17:27:08,031 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,031 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,031 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,031 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,031 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,031 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:08,083 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,083 INFO  L93              Difference]: Finished difference Result 128 states and 166 transitions.
[2025-05-07 17:27:08,084 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:08,084 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:08,084 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,085 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:27:08,085 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:27:08,086 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:08,086 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:08,086 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:08,087 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:27:08,091 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 118.
[2025-05-07 17:27:08,091 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:08,092 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 155 transitions.
[2025-05-07 17:27:08,092 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 155 transitions. Word has length 41
[2025-05-07 17:27:08,092 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,092 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 155 transitions.
[2025-05-07 17:27:08,092 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:08,092 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 155 transitions.
[2025-05-07 17:27:08,093 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:08,093 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,093 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:08,093 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:08,093 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,094 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,094 INFO  L85        PathProgramCache]: Analyzing trace with hash -59871912, now seen corresponding path program 1 times
[2025-05-07 17:27:08,094 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,094 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1066654397]
[2025-05-07 17:27:08,094 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,094 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,111 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:08,121 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:08,121 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,121 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,198 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:08,199 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,199 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1066654397]
[2025-05-07 17:27:08,199 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1066654397] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,199 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,199 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,199 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [684860464]
[2025-05-07 17:27:08,199 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,199 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,199 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,200 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,200 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,200 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:08,236 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,236 INFO  L93              Difference]: Finished difference Result 124 states and 160 transitions.
[2025-05-07 17:27:08,237 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:08,237 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:08,237 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,238 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:27:08,238 INFO  L226             Difference]: Without dead ends: 114
[2025-05-07 17:27:08,238 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:08,238 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:08,238 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:08,239 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-05-07 17:27:08,243 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 114.
[2025-05-07 17:27:08,243 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:08,244 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 149 transitions.
[2025-05-07 17:27:08,244 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 149 transitions. Word has length 41
[2025-05-07 17:27:08,244 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,244 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 149 transitions.
[2025-05-07 17:27:08,244 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:08,244 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 149 transitions.
[2025-05-07 17:27:08,245 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:08,245 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,245 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:08,245 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:08,245 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,245 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,245 INFO  L85        PathProgramCache]: Analyzing trace with hash 1312343432, now seen corresponding path program 1 times
[2025-05-07 17:27:08,245 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,245 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [615937407]
[2025-05-07 17:27:08,245 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,246 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,260 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:08,269 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:08,269 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,269 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,366 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:08,367 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,367 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [615937407]
[2025-05-07 17:27:08,367 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [615937407] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,367 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,367 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,367 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1609812635]
[2025-05-07 17:27:08,367 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,367 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,368 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,368 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,368 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,368 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:08,407 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,407 INFO  L93              Difference]: Finished difference Result 120 states and 154 transitions.
[2025-05-07 17:27:08,407 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:08,408 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:08,408 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,409 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:27:08,409 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:27:08,409 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:08,410 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:08,410 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:08,411 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:27:08,418 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 110.
[2025-05-07 17:27:08,418 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:08,419 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 110 states to 110 states and 143 transitions.
[2025-05-07 17:27:08,419 INFO  L79                 Accepts]: Start accepts. Automaton has 110 states and 143 transitions. Word has length 41
[2025-05-07 17:27:08,419 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,419 INFO  L485      AbstractCegarLoop]: Abstraction has 110 states and 143 transitions.
[2025-05-07 17:27:08,419 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:08,419 INFO  L278                IsEmpty]: Start isEmpty. Operand 110 states and 143 transitions.
[2025-05-07 17:27:08,420 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:08,421 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,421 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:08,421 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:08,421 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,421 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,421 INFO  L85        PathProgramCache]: Analyzing trace with hash 730898826, now seen corresponding path program 1 times
[2025-05-07 17:27:08,421 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,421 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [522607464]
[2025-05-07 17:27:08,421 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,422 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,438 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:08,450 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:08,450 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,450 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,537 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:08,537 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,537 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [522607464]
[2025-05-07 17:27:08,537 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [522607464] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,537 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,537 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [805038366]
[2025-05-07 17:27:08,537 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,538 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,538 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,538 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,538 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,538 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:08,574 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,575 INFO  L93              Difference]: Finished difference Result 116 states and 148 transitions.
[2025-05-07 17:27:08,575 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:08,575 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:08,576 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,576 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:08,576 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:27:08,577 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:08,577 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:08,578 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:08,578 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:27:08,584 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:27:08,584 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:08,585 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 137 transitions.
[2025-05-07 17:27:08,585 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 137 transitions. Word has length 41
[2025-05-07 17:27:08,586 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,586 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 137 transitions.
[2025-05-07 17:27:08,586 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:08,586 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 137 transitions.
[2025-05-07 17:27:08,587 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:08,587 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,587 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:08,587 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:08,587 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,588 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,588 INFO  L85        PathProgramCache]: Analyzing trace with hash -2006865526, now seen corresponding path program 1 times
[2025-05-07 17:27:08,588 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,588 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1409118481]
[2025-05-07 17:27:08,588 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,588 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,605 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:08,615 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:08,615 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,615 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,678 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:08,679 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,679 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1409118481]
[2025-05-07 17:27:08,679 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1409118481] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,679 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,679 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,679 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1733732330]
[2025-05-07 17:27:08,679 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,679 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,679 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,680 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,680 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,680 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:08,710 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,711 INFO  L93              Difference]: Finished difference Result 112 states and 142 transitions.
[2025-05-07 17:27:08,711 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:08,711 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:08,711 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,712 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:27:08,712 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:27:08,712 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:08,712 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:08,713 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:08,713 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:27:08,716 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:27:08,717 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:08,717 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 131 transitions.
[2025-05-07 17:27:08,717 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 131 transitions. Word has length 41
[2025-05-07 17:27:08,717 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,717 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 131 transitions.
[2025-05-07 17:27:08,717 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:08,717 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 131 transitions.
[2025-05-07 17:27:08,718 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:08,718 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,718 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:08,718 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:08,718 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,718 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,719 INFO  L85        PathProgramCache]: Analyzing trace with hash -242122342, now seen corresponding path program 1 times
[2025-05-07 17:27:08,719 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,719 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [54678769]
[2025-05-07 17:27:08,719 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,719 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,734 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:08,742 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:08,743 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,743 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,824 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:08,825 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [54678769]
[2025-05-07 17:27:08,825 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [54678769] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,825 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,825 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,825 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [330653308]
[2025-05-07 17:27:08,825 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,825 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,825 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,826 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,826 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,826 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:08,860 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:08,860 INFO  L93              Difference]: Finished difference Result 108 states and 136 transitions.
[2025-05-07 17:27:08,860 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:08,861 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:08,861 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:08,862 INFO  L225             Difference]: With dead ends: 108
[2025-05-07 17:27:08,862 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:27:08,862 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:08,863 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:08,863 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:08,864 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:27:08,868 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:27:08,869 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:08,869 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 125 transitions.
[2025-05-07 17:27:08,870 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 125 transitions. Word has length 41
[2025-05-07 17:27:08,870 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:08,870 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 125 transitions.
[2025-05-07 17:27:08,870 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:08,870 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 125 transitions.
[2025-05-07 17:27:08,871 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:08,871 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:08,871 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:08,871 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:08,871 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:08,871 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:08,872 INFO  L85        PathProgramCache]: Analyzing trace with hash 297672104, now seen corresponding path program 1 times
[2025-05-07 17:27:08,872 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:08,872 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1584332373]
[2025-05-07 17:27:08,872 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:08,872 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:08,888 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:08,898 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:08,898 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:08,898 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:08,966 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:08,966 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:08,966 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1584332373]
[2025-05-07 17:27:08,966 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1584332373] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:08,966 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:08,966 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:08,966 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [436050858]
[2025-05-07 17:27:08,966 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:08,967 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:08,967 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:08,967 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:08,967 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:08,968 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:09,002 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,003 INFO  L93              Difference]: Finished difference Result 104 states and 130 transitions.
[2025-05-07 17:27:09,003 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,003 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:09,003 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,004 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:27:09,004 INFO  L226             Difference]: Without dead ends: 94
[2025-05-07 17:27:09,005 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:09,005 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:09,005 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:09,006 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-05-07 17:27:09,010 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 94.
[2025-05-07 17:27:09,010 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:09,011 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 119 transitions.
[2025-05-07 17:27:09,011 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 119 transitions. Word has length 41
[2025-05-07 17:27:09,012 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,012 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 119 transitions.
[2025-05-07 17:27:09,012 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:09,012 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 119 transitions.
[2025-05-07 17:27:09,013 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,013 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,013 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:09,013 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:09,013 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,013 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,013 INFO  L85        PathProgramCache]: Analyzing trace with hash -821423674, now seen corresponding path program 1 times
[2025-05-07 17:27:09,013 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,013 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1527324173]
[2025-05-07 17:27:09,013 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,014 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,031 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,040 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,041 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,041 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,103 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:09,103 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1527324173]
[2025-05-07 17:27:09,103 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1527324173] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,103 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,104 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,104 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1429788859]
[2025-05-07 17:27:09,104 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,104 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,104 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,104 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,104 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,105 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:09,138 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,138 INFO  L93              Difference]: Finished difference Result 100 states and 124 transitions.
[2025-05-07 17:27:09,138 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,138 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:09,139 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,139 INFO  L225             Difference]: With dead ends: 100
[2025-05-07 17:27:09,139 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:27:09,140 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:09,140 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:09,141 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:09,141 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:27:09,144 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:27:09,145 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:09,146 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 113 transitions.
[2025-05-07 17:27:09,146 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 113 transitions. Word has length 41
[2025-05-07 17:27:09,146 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,146 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 113 transitions.
[2025-05-07 17:27:09,146 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:09,146 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 113 transitions.
[2025-05-07 17:27:09,147 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,147 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,147 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:09,147 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:09,147 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,147 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,148 INFO  L85        PathProgramCache]: Analyzing trace with hash 1087250846, now seen corresponding path program 1 times
[2025-05-07 17:27:09,148 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,148 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1800031271]
[2025-05-07 17:27:09,148 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,148 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,165 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,174 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,174 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,174 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,239 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:09,239 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,239 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1800031271]
[2025-05-07 17:27:09,239 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1800031271] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,239 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,239 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,239 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1084100821]
[2025-05-07 17:27:09,239 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,239 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,240 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,240 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,240 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,240 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:09,272 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,273 INFO  L93              Difference]: Finished difference Result 96 states and 118 transitions.
[2025-05-07 17:27:09,273 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,273 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:09,273 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,274 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:27:09,274 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:27:09,274 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:09,275 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:09,275 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:09,276 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:27:09,279 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:27:09,279 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:09,280 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 107 transitions.
[2025-05-07 17:27:09,280 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 107 transitions. Word has length 41
[2025-05-07 17:27:09,280 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,280 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 107 transitions.
[2025-05-07 17:27:09,281 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:09,281 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 107 transitions.
[2025-05-07 17:27:09,281 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,281 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,282 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:09,282 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:27:09,282 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,282 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,282 INFO  L85        PathProgramCache]: Analyzing trace with hash -868788892, now seen corresponding path program 1 times
[2025-05-07 17:27:09,282 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,282 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1824310937]
[2025-05-07 17:27:09,282 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,282 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,301 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,308 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,308 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,308 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,358 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:09,359 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,359 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1824310937]
[2025-05-07 17:27:09,359 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1824310937] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,359 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,359 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,359 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2064031771]
[2025-05-07 17:27:09,359 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,359 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,359 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,360 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,360 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,360 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:09,386 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,386 INFO  L93              Difference]: Finished difference Result 92 states and 112 transitions.
[2025-05-07 17:27:09,387 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,387 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:09,387 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,387 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:27:09,387 INFO  L226             Difference]: Without dead ends: 82
[2025-05-07 17:27:09,388 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:09,388 INFO  L437           NwaCegarLoop]: 104 mSDtfsCounter, 1 mSDsluCounter, 510 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 614 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:09,388 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 614 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:09,388 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-05-07 17:27:09,390 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 82.
[2025-05-07 17:27:09,390 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:09,391 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 101 transitions.
[2025-05-07 17:27:09,391 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 101 transitions. Word has length 41
[2025-05-07 17:27:09,391 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,391 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 101 transitions.
[2025-05-07 17:27:09,391 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:09,391 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 101 transitions.
[2025-05-07 17:27:09,391 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,392 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,392 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:09,392 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:27:09,392 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,392 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,392 INFO  L85        PathProgramCache]: Analyzing trace with hash 1169005992, now seen corresponding path program 1 times
[2025-05-07 17:27:09,392 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,392 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1052490544]
[2025-05-07 17:27:09,392 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,392 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,403 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,407 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,407 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,454 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:09,454 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,454 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1052490544]
[2025-05-07 17:27:09,454 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1052490544] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,454 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,454 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,455 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [474520783]
[2025-05-07 17:27:09,455 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,455 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,455 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,455 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,455 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,455 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:09,484 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,484 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:27:09,484 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,484 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:09,484 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,485 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:27:09,485 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:27:09,485 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:09,485 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:09,486 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:09,486 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:27:09,488 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:27:09,488 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:09,488 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 95 transitions.
[2025-05-07 17:27:09,488 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 95 transitions. Word has length 41
[2025-05-07 17:27:09,489 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,489 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 95 transitions.
[2025-05-07 17:27:09,489 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:09,489 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 95 transitions.
[2025-05-07 17:27:09,489 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,489 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,489 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:09,490 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:27:09,490 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,490 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,490 INFO  L85        PathProgramCache]: Analyzing trace with hash 1709394334, now seen corresponding path program 1 times
[2025-05-07 17:27:09,490 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,490 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1636564845]
[2025-05-07 17:27:09,490 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,490 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,503 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,510 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,510 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,510 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,564 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:09,564 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,564 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1636564845]
[2025-05-07 17:27:09,564 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1636564845] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,564 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,564 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,565 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [701132034]
[2025-05-07 17:27:09,565 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,565 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,565 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,565 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,565 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,566 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:09,592 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,592 INFO  L93              Difference]: Finished difference Result 84 states and 100 transitions.
[2025-05-07 17:27:09,592 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,593 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:09,593 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,593 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:27:09,593 INFO  L226             Difference]: Without dead ends: 74
[2025-05-07 17:27:09,593 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,594 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:09,594 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:09,594 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-05-07 17:27:09,596 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 74.
[2025-05-07 17:27:09,596 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:09,596 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 89 transitions.
[2025-05-07 17:27:09,596 INFO  L79                 Accepts]: Start accepts. Automaton has 74 states and 89 transitions. Word has length 41
[2025-05-07 17:27:09,597 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,597 INFO  L485      AbstractCegarLoop]: Abstraction has 74 states and 89 transitions.
[2025-05-07 17:27:09,597 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:09,597 INFO  L278                IsEmpty]: Start isEmpty. Operand 74 states and 89 transitions.
[2025-05-07 17:27:09,597 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,597 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,598 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:09,598 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:27:09,598 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,598 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,598 INFO  L85        PathProgramCache]: Analyzing trace with hash -885983856, now seen corresponding path program 1 times
[2025-05-07 17:27:09,598 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,598 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [830162207]
[2025-05-07 17:27:09,598 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,598 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,610 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,616 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,616 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,616 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,686 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:09,686 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,686 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [830162207]
[2025-05-07 17:27:09,687 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [830162207] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,687 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,687 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,687 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [243139038]
[2025-05-07 17:27:09,687 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,687 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,687 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,687 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,688 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,688 INFO  L87              Difference]: Start difference. First operand 74 states and 89 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:09,716 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,716 INFO  L93              Difference]: Finished difference Result 80 states and 94 transitions.
[2025-05-07 17:27:09,716 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,716 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:09,716 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,717 INFO  L225             Difference]: With dead ends: 80
[2025-05-07 17:27:09,717 INFO  L226             Difference]: Without dead ends: 70
[2025-05-07 17:27:09,717 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:09,717 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 1 mSDsluCounter, 440 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 531 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,717 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 531 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,718 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-05-07 17:27:09,719 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-05-07 17:27:09,719 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:09,720 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 83 transitions.
[2025-05-07 17:27:09,720 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 83 transitions. Word has length 41
[2025-05-07 17:27:09,720 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,720 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 83 transitions.
[2025-05-07 17:27:09,720 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:09,720 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 83 transitions.
[2025-05-07 17:27:09,721 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,721 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,721 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:09,721 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:27:09,721 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,721 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,721 INFO  L85        PathProgramCache]: Analyzing trace with hash 980446608, now seen corresponding path program 1 times
[2025-05-07 17:27:09,721 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,721 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [586736954]
[2025-05-07 17:27:09,721 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,722 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,735 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,740 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,740 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,740 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,833 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:09,833 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,833 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [586736954]
[2025-05-07 17:27:09,833 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [586736954] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,833 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,834 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,834 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1868843635]
[2025-05-07 17:27:09,834 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,834 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,834 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,834 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,834 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,835 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:09,863 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,863 INFO  L93              Difference]: Finished difference Result 76 states and 88 transitions.
[2025-05-07 17:27:09,864 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,864 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:09,864 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,864 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:27:09,865 INFO  L226             Difference]: Without dead ends: 66
[2025-05-07 17:27:09,865 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:09,865 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 1 mSDsluCounter, 412 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 497 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:09,865 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 497 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:09,866 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-05-07 17:27:09,867 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-05-07 17:27:09,868 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:09,868 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 77 transitions.
[2025-05-07 17:27:09,868 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 77 transitions. Word has length 41
[2025-05-07 17:27:09,868 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,868 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 77 transitions.
[2025-05-07 17:27:09,868 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:09,868 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 77 transitions.
[2025-05-07 17:27:09,869 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,869 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,869 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:09,869 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:27:09,869 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:09,869 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:09,870 INFO  L85        PathProgramCache]: Analyzing trace with hash 649501062, now seen corresponding path program 1 times
[2025-05-07 17:27:09,870 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:09,870 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1565836212]
[2025-05-07 17:27:09,870 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:09,870 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:09,885 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:09,893 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:09,893 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:09,893 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:09,961 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:09,961 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:09,961 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1565836212]
[2025-05-07 17:27:09,961 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1565836212] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:09,961 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:09,961 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:09,962 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1264051787]
[2025-05-07 17:27:09,962 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:09,962 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:09,962 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:09,962 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:09,962 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:09,963 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:09,994 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:09,994 INFO  L93              Difference]: Finished difference Result 72 states and 82 transitions.
[2025-05-07 17:27:09,995 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:09,995 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:09,995 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:09,995 INFO  L225             Difference]: With dead ends: 72
[2025-05-07 17:27:09,995 INFO  L226             Difference]: Without dead ends: 62
[2025-05-07 17:27:09,996 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:09,996 INFO  L437           NwaCegarLoop]: 74 mSDtfsCounter, 1 mSDsluCounter, 360 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 434 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:09,996 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 434 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:09,996 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-05-07 17:27:09,998 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 62.
[2025-05-07 17:27:09,998 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:09,998 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 71 transitions.
[2025-05-07 17:27:09,998 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 71 transitions. Word has length 41
[2025-05-07 17:27:09,998 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:09,998 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 71 transitions.
[2025-05-07 17:27:09,999 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:09,999 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 71 transitions.
[2025-05-07 17:27:09,999 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:09,999 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:09,999 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:09,999 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:27:10,000 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:10,000 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:10,000 INFO  L85        PathProgramCache]: Analyzing trace with hash -1924159102, now seen corresponding path program 1 times
[2025-05-07 17:27:10,000 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:10,000 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [320531982]
[2025-05-07 17:27:10,000 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:10,000 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:10,015 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:10,030 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:10,030 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:10,030 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:10,243 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:10,243 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:10,243 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [320531982]
[2025-05-07 17:27:10,243 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [320531982] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:10,243 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:10,243 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:10,243 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [927428029]
[2025-05-07 17:27:10,243 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:10,243 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:10,243 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:10,244 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:10,244 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:10,244 INFO  L87              Difference]: Start difference. First operand 62 states and 71 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:10,315 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:10,315 INFO  L93              Difference]: Finished difference Result 64 states and 72 transitions.
[2025-05-07 17:27:10,316 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:10,316 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:10,316 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:10,316 INFO  L225             Difference]: With dead ends: 64
[2025-05-07 17:27:10,316 INFO  L226             Difference]: Without dead ends: 58
[2025-05-07 17:27:10,317 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:10,317 INFO  L437           NwaCegarLoop]: 64 mSDtfsCounter, 1 mSDsluCounter, 298 mSDsCounter, 0 mSdLazyCounter, 56 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 362 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 56 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:10,317 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 362 Invalid, 56 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 56 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:10,317 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-05-07 17:27:10,318 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 58.
[2025-05-07 17:27:10,318 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:10,319 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 65 transitions.
[2025-05-07 17:27:10,319 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 65 transitions. Word has length 41
[2025-05-07 17:27:10,319 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,319 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 65 transitions.
[2025-05-07 17:27:10,319 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:10,319 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 65 transitions.
[2025-05-07 17:27:10,319 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:10,319 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:10,320 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:10,320 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:27:10,320 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:10,320 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:10,320 INFO  L85        PathProgramCache]: Analyzing trace with hash -157630026, now seen corresponding path program 1 times
[2025-05-07 17:27:10,320 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:10,320 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1586730478]
[2025-05-07 17:27:10,320 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:10,320 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:10,335 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:10,341 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:10,341 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:10,341 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:10,394 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:10,394 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:10,394 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1586730478]
[2025-05-07 17:27:10,394 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1586730478] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:10,394 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:10,394 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:10,394 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [682874979]
[2025-05-07 17:27:10,394 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:10,395 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:10,395 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:10,395 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:10,395 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:10,396 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:10,427 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:10,427 INFO  L93              Difference]: Finished difference Result 64 states and 70 transitions.
[2025-05-07 17:27:10,427 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:10,427 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:10,427 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:10,428 INFO  L225             Difference]: With dead ends: 64
[2025-05-07 17:27:10,428 INFO  L226             Difference]: Without dead ends: 54
[2025-05-07 17:27:10,428 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:10,428 INFO  L437           NwaCegarLoop]: 67 mSDtfsCounter, 1 mSDsluCounter, 320 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 387 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:10,428 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 387 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:10,429 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-05-07 17:27:10,430 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 54.
[2025-05-07 17:27:10,430 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:10,430 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 59 transitions.
[2025-05-07 17:27:10,430 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 59 transitions. Word has length 41
[2025-05-07 17:27:10,430 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,430 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 59 transitions.
[2025-05-07 17:27:10,430 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:10,431 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 59 transitions.
[2025-05-07 17:27:10,431 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:10,431 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:10,431 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:10,431 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:27:10,431 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:10,431 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:10,431 INFO  L85        PathProgramCache]: Analyzing trace with hash 46338430, now seen corresponding path program 1 times
[2025-05-07 17:27:10,431 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:10,431 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1913595321]
[2025-05-07 17:27:10,431 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:10,431 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:10,447 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:10,454 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:10,454 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:10,454 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:10,517 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:10,517 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:10,517 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1913595321]
[2025-05-07 17:27:10,518 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1913595321] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:10,518 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:10,518 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:10,518 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1675682529]
[2025-05-07 17:27:10,518 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:10,518 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:10,518 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:10,518 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:10,518 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:10,518 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:10,546 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:10,546 INFO  L93              Difference]: Finished difference Result 60 states and 64 transitions.
[2025-05-07 17:27:10,546 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:10,547 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:10,547 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:10,547 INFO  L225             Difference]: With dead ends: 60
[2025-05-07 17:27:10,547 INFO  L226             Difference]: Without dead ends: 50
[2025-05-07 17:27:10,547 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:10,548 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:10,548 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:10,548 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-05-07 17:27:10,549 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 50.
[2025-05-07 17:27:10,549 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:10,549 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 53 transitions.
[2025-05-07 17:27:10,550 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 53 transitions. Word has length 41
[2025-05-07 17:27:10,550 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,550 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 53 transitions.
[2025-05-07 17:27:10,550 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:10,550 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 53 transitions.
[2025-05-07 17:27:10,550 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:10,550 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:10,550 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:10,550 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:27:10,550 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:10,551 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:10,551 INFO  L85        PathProgramCache]: Analyzing trace with hash 1041971722, now seen corresponding path program 1 times
[2025-05-07 17:27:10,551 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:10,551 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1602974688]
[2025-05-07 17:27:10,551 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:10,551 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:10,566 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:10,572 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:10,572 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:10,572 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:10,623 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:10,624 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:10,624 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1602974688]
[2025-05-07 17:27:10,624 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1602974688] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:10,624 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:10,624 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:10,624 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [270245725]
[2025-05-07 17:27:10,624 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:10,624 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:10,624 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:10,625 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:10,625 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:10,625 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:10,654 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:10,654 INFO  L93              Difference]: Finished difference Result 56 states and 58 transitions.
[2025-05-07 17:27:10,655 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:10,655 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:10,655 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:10,655 INFO  L225             Difference]: With dead ends: 56
[2025-05-07 17:27:10,655 INFO  L226             Difference]: Without dead ends: 46
[2025-05-07 17:27:10,655 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:10,656 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:10,656 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:10,656 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-05-07 17:27:10,657 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 46.
[2025-05-07 17:27:10,657 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:10,657 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 47 transitions.
[2025-05-07 17:27:10,658 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 47 transitions. Word has length 41
[2025-05-07 17:27:10,658 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,658 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 47 transitions.
[2025-05-07 17:27:10,658 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:10,658 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 47 transitions.
[2025-05-07 17:27:10,658 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:10,658 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:10,658 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:10,658 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:27:10,658 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:10,659 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:10,659 INFO  L85        PathProgramCache]: Analyzing trace with hash -1945283232, now seen corresponding path program 1 times
[2025-05-07 17:27:10,659 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:10,659 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1612522573]
[2025-05-07 17:27:10,659 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:10,659 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:10,673 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:10,678 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:10,678 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:10,678 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:10,730 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:10,730 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:10,730 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1612522573]
[2025-05-07 17:27:10,730 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1612522573] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:10,730 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:10,730 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:10,730 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1959650429]
[2025-05-07 17:27:10,730 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:10,731 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:10,731 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:10,731 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:10,731 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:10,731 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:10,764 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:10,764 INFO  L93              Difference]: Finished difference Result 52 states and 52 transitions.
[2025-05-07 17:27:10,764 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:10,764 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:10,764 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:10,765 INFO  L225             Difference]: With dead ends: 52
[2025-05-07 17:27:10,765 INFO  L226             Difference]: Without dead ends: 42
[2025-05-07 17:27:10,765 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:10,766 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 1 mSDsluCounter, 210 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 254 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:10,766 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 254 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:10,766 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-05-07 17:27:10,767 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-05-07 17:27:10,767 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:10,767 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 41 transitions.
[2025-05-07 17:27:10,768 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 41 transitions. Word has length 41
[2025-05-07 17:27:10,768 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,768 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 41 transitions.
[2025-05-07 17:27:10,768 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:10,768 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 41 transitions.
[2025-05-07 17:27:10,768 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:10,768 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:10,768 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:10,768 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:27:10,768 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:10,769 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:10,769 INFO  L85        PathProgramCache]: Analyzing trace with hash 2060629396, now seen corresponding path program 1 times
[2025-05-07 17:27:10,769 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:10,769 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1210585296]
[2025-05-07 17:27:10,769 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:10,769 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:10,782 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:10,786 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:10,786 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:10,786 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:10,830 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:10,830 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:10,830 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1210585296]
[2025-05-07 17:27:10,831 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1210585296] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:10,831 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:10,831 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:10,831 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2022251078]
[2025-05-07 17:27:10,831 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:10,831 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:10,831 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:10,831 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:10,832 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:10,832 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:10,860 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:10,860 INFO  L93              Difference]: Finished difference Result 36 states and 35 transitions.
[2025-05-07 17:27:10,860 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:10,861 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:10,861 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:10,861 INFO  L225             Difference]: With dead ends: 36
[2025-05-07 17:27:10,861 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:10,861 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:10,861 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:10,862 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:10,862 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:10,862 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:10,862 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:10,862 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:10,862 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 41
[2025-05-07 17:27:10,862 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,862 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:10,862 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:10,862 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:10,863 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:10,864 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:10,865 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:27:10,867 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:10,869 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:10,871 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:10 BoogieIcfgContainer
[2025-05-07 17:27:10,871 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:10,872 INFO  L158              Benchmark]: Toolchain (without parser) took 4601.18ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 179.6MB in the beginning and 137.4MB in the end (delta: 42.2MB). Peak memory consumption was 87.4MB. Max. memory is 33.6GB.
[2025-05-07 17:27:10,872 INFO  L158              Benchmark]: SmtParser took 0.19ms. Allocated memory is still 234.9MB. Free memory is still 173.6MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:10,872 INFO  L158              Benchmark]: ChcToBoogie took 48.08ms. Allocated memory is still 234.9MB. Free memory was 179.6MB in the beginning and 170.9MB in the end (delta: 8.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:10,872 INFO  L158              Benchmark]: Boogie Preprocessor took 71.65ms. Allocated memory is still 234.9MB. Free memory was 170.9MB in the beginning and 166.2MB in the end (delta: 4.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:10,873 INFO  L158              Benchmark]: RCFGBuilder took 792.37ms. Allocated memory was 234.9MB in the beginning and 302.0MB in the end (delta: 67.1MB). Free memory was 166.2MB in the beginning and 213.3MB in the end (delta: -47.1MB). Peak memory consumption was 74.9MB. Max. memory is 33.6GB.
[2025-05-07 17:27:10,873 INFO  L158              Benchmark]: TraceAbstraction took 3686.03ms. Allocated memory was 302.0MB in the beginning and 285.2MB in the end (delta: -16.8MB). Free memory was 212.5MB in the beginning and 137.4MB in the end (delta: 75.1MB). Peak memory consumption was 63.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:10,873 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.19ms. Allocated memory is still 234.9MB. Free memory is still 173.6MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 48.08ms. Allocated memory is still 234.9MB. Free memory was 179.6MB in the beginning and 170.9MB in the end (delta: 8.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 71.65ms. Allocated memory is still 234.9MB. Free memory was 170.9MB in the beginning and 166.2MB in the end (delta: 4.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 792.37ms. Allocated memory was 234.9MB in the beginning and 302.0MB in the end (delta: 67.1MB). Free memory was 166.2MB in the beginning and 213.3MB in the end (delta: -47.1MB). Peak memory consumption was 74.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3686.03ms. Allocated memory was 302.0MB in the beginning and 285.2MB in the end (delta: -16.8MB). Free memory was 212.5MB in the beginning and 137.4MB in the end (delta: 75.1MB). Peak memory consumption was 63.8MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 32 procedures, 128 locations, 228 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.6s, 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, 13473 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 11002 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 487 IncrementalHoareTripleChecker+Invalid, 487 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 2471 mSDtfsCounter, 487 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.9s 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:10,884 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
