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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:29:23,549 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:29:23,587 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_65a8bbe8-0ba9-4320-8ef8-1649db9bda29/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:29:23,590 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:29:23,590 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:29:23,603 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:29:23,604 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:29:23,604 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:29:23,604 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:29:23,604 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:29:23,604 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:29:23,604 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:29:23,604 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:29:23,605 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:29:23,605 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:29:23,605 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:29:23,605 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:29:23,605 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:29:23,605 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:23,605 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:29:23,605 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:29:23,605 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:29:23,606 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:29:23,606 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:29:23,606 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:29:23,606 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:29:23,606 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:29:23,791 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:29:23,797 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:29:23,799 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:29:23,799 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:29:23,800 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:29:23,800 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_65a8bbe8-0ba9-4320-8ef8-1649db9bda29/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_37_no_adts_000.smt2
[2025-05-07 17:29:23,801 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:29:23,804 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:29:24,161 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_65a8bbe8-0ba9-4320-8ef8-1649db9bda29/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_37_no_adts_000.smt2
[2025-05-07 17:29:24,164 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:29:24,164 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:29:24,165 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:29:24,165 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:29:24,165 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:29:24,167 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,212 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24 Unit
[2025-05-07 17:29:24,213 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:29:24,213 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:29:24,213 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:29:24,213 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:29:24,224 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,224 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,249 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,249 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,258 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,259 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,261 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,265 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,267 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,283 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:29:24,283 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:29:24,283 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:29:24,284 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:29:24,284 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (1/1) ...
[2025-05-07 17:29:24,286 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:24,294 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:24,303 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:29:24,305 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:29:24,312 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:29:24,313 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:29:24,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:29:24,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_64_0 given in one single declaration
[2025-05-07 17:29:24,313 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_64_0
[2025-05-07 17:29:24,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_64_0
[2025-05-07 17:29:24,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_6_D_407_0 given in one single declaration
[2025-05-07 17:29:24,313 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_6_D_407_0
[2025-05-07 17:29:24,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_6_D_407_0
[2025-05-07 17:29:24,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_58_D_407_0 given in one single declaration
[2025-05-07 17:29:24,313 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_58_D_407_0
[2025-05-07 17:29:24,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_58_D_407_0
[2025-05-07 17:29:24,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_7_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,313 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_7_constructor_406_407_0
[2025-05-07 17:29:24,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_7_constructor_406_407_0
[2025-05-07 17:29:24,313 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,313 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_constructor_406_407_0
[2025-05-07 17:29:24,313 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36__405_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36__405_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36__405_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,314 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_constructor_406_407_0
[2025-05-07 17:29:24,314 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_constructor_406_407_0
[2025-05-07 17:29:24,315 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,315 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,316 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,316 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,316 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,316 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_return_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,316 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:29:24,316 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,317 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_constructor_406_407_0
[2025-05-07 17:29:24,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_constructor_406_407_0
[2025-05-07 17:29:24,317 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_constructor_406_407_0 given in one single declaration
[2025-05-07 17:29:24,317 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_constructor_406_407_0
[2025-05-07 17:29:24,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_constructor_406_407_0
[2025-05-07 17:29:24,317 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:29:24,317 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:29:24,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:29:24,317 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_59_D_407_0 given in one single declaration
[2025-05-07 17:29:24,317 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:29:24,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:29:24,317 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_61_D_407_0 given in one single declaration
[2025-05-07 17:29:24,317 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:29:24,317 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:29:24,318 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:29:24,318 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:29:24,318 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:29:24,569 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:29:24,570 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:29:25,038 INFO  L?                        ?]: Removed 1077 outVars from TransFormulas that were not future-live.
[2025-05-07 17:29:25,038 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:29:25,051 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:29:25,051 INFO  L312             CfgBuilder]: Removed 24 assume(true) statements.
[2025-05-07 17:29:25,051 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:25 BoogieIcfgContainer
[2025-05-07 17:29:25,052 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:29:25,054 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:29:25,054 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:29:25,057 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:29:25,057 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:24" (1/3) ...
[2025-05-07 17:29:25,057 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@507bfa52 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:29:25, skipping insertion in model container
[2025-05-07 17:29:25,058 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:24" (2/3) ...
[2025-05-07 17:29:25,058 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@507bfa52 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:29:25, skipping insertion in model container
[2025-05-07 17:29:25,058 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:25" (3/3) ...
[2025-05-07 17:29:25,059 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:29:25,069 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:29:25,071 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:29:25,101 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:29:25,110 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;@48d41b1d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:29:25,110 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:29:25,113 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:29:25,120 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:25,120 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:25,121 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:29:25,121 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:25,124 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:25,125 INFO  L85        PathProgramCache]: Analyzing trace with hash 1209627918, now seen corresponding path program 1 times
[2025-05-07 17:29:25,130 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:25,130 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [498094914]
[2025-05-07 17:29:25,131 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,131 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,179 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:25,211 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:25,212 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,212 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,365 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:25,365 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,366 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [498094914]
[2025-05-07 17:29:25,366 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [498094914] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:25,366 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:25,369 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:25,371 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [47993867]
[2025-05-07 17:29:25,371 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:25,375 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:25,375 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:25,405 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:25,406 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:25,408 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:29:25,472 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:25,472 INFO  L93              Difference]: Finished difference Result 130 states and 175 transitions.
[2025-05-07 17:29:25,473 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:25,475 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:29:25,475 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:25,481 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:29:25,481 INFO  L226             Difference]: Without dead ends: 130
[2025-05-07 17:29:25,483 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:29:25,484 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:29:25,485 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:29:25,495 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-05-07 17:29:25,515 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 128.
[2025-05-07 17:29:25,516 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:29:25,519 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 173 transitions.
[2025-05-07 17:29:25,520 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 173 transitions. Word has length 41
[2025-05-07 17:29:25,521 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:25,521 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 173 transitions.
[2025-05-07 17:29:25,521 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:29:25,521 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 173 transitions.
[2025-05-07 17:29:25,523 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:25,523 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:25,523 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:29:25,523 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:29:25,523 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:25,524 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:25,524 INFO  L85        PathProgramCache]: Analyzing trace with hash -885983856, now seen corresponding path program 1 times
[2025-05-07 17:29:25,524 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:25,524 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [367957974]
[2025-05-07 17:29:25,524 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,524 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,547 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:25,578 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:25,578 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,578 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,707 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:25,707 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,707 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [367957974]
[2025-05-07 17:29:25,707 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [367957974] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:25,707 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:25,707 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:25,708 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1791334890]
[2025-05-07 17:29:25,708 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:25,709 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:25,709 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:25,709 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:25,710 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:25,710 INFO  L87              Difference]: Start difference. First operand 128 states and 173 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:29:25,778 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:25,778 INFO  L93              Difference]: Finished difference Result 136 states and 182 transitions.
[2025-05-07 17:29:25,779 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:25,779 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:29:25,779 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:25,780 INFO  L225             Difference]: With dead ends: 136
[2025-05-07 17:29:25,780 INFO  L226             Difference]: Without dead ends: 124
[2025-05-07 17:29:25,780 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:25,781 INFO  L437           NwaCegarLoop]: 173 mSDtfsCounter, 1 mSDsluCounter, 846 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1019 SdHoareTripleChecker+Invalid, 37 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:25,781 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1019 Invalid, 37 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:25,782 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-05-07 17:29:25,788 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 124.
[2025-05-07 17:29:25,788 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 124 states, 58 states have (on average 1.0344827586206897) internal successors, (60), 60 states have internal predecessors, (60), 34 states have call successors, (53), 30 states have call predecessors, (53), 31 states have return successors, (54), 33 states have call predecessors, (54), 34 states have call successors, (54)
[2025-05-07 17:29:25,789 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 124 states to 124 states and 167 transitions.
[2025-05-07 17:29:25,789 INFO  L79                 Accepts]: Start accepts. Automaton has 124 states and 167 transitions. Word has length 41
[2025-05-07 17:29:25,789 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:25,789 INFO  L485      AbstractCegarLoop]: Abstraction has 124 states and 167 transitions.
[2025-05-07 17:29:25,789 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:29:25,789 INFO  L278                IsEmpty]: Start isEmpty. Operand 124 states and 167 transitions.
[2025-05-07 17:29:25,790 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:25,790 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:25,791 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:25,791 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:25,791 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:25,791 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:25,791 INFO  L85        PathProgramCache]: Analyzing trace with hash 1725589390, now seen corresponding path program 1 times
[2025-05-07 17:29:25,791 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:25,791 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2080674522]
[2025-05-07 17:29:25,791 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,791 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,808 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:25,811 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:25,811 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,811 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,858 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:25,859 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,859 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2080674522]
[2025-05-07 17:29:25,859 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2080674522] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:25,859 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:25,859 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:25,859 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1835386454]
[2025-05-07 17:29:25,859 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:25,859 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:25,860 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:25,860 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:25,860 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:25,860 INFO  L87              Difference]: Start difference. First operand 124 states and 167 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:29:25,870 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:25,870 INFO  L93              Difference]: Finished difference Result 126 states and 168 transitions.
[2025-05-07 17:29:25,870 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:25,870 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:29:25,871 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:25,872 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:29:25,872 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:29:25,872 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:29:25,872 INFO  L437           NwaCegarLoop]: 165 mSDtfsCounter, 1 mSDsluCounter, 322 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 487 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:29:25,872 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 487 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:25,873 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:29:25,878 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 118.
[2025-05-07 17:29:25,878 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:29:25,879 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 155 transitions.
[2025-05-07 17:29:25,879 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 155 transitions. Word has length 41
[2025-05-07 17:29:25,879 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:25,879 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 155 transitions.
[2025-05-07 17:29:25,879 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:29:25,879 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 155 transitions.
[2025-05-07 17:29:25,880 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:25,880 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:25,881 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:29:25,881 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:25,881 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:25,881 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:25,881 INFO  L85        PathProgramCache]: Analyzing trace with hash 297672104, now seen corresponding path program 1 times
[2025-05-07 17:29:25,881 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:25,881 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1261945001]
[2025-05-07 17:29:25,881 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:25,882 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:25,898 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:25,911 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:25,911 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:25,912 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:25,985 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:25,985 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:25,985 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1261945001]
[2025-05-07 17:29:25,985 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1261945001] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:25,985 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:25,986 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:25,986 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [870622528]
[2025-05-07 17:29:25,986 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:25,986 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:25,986 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:25,986 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:25,986 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:25,986 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:29:26,021 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,021 INFO  L93              Difference]: Finished difference Result 124 states and 160 transitions.
[2025-05-07 17:29:26,021 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:26,021 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:29:26,022 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,022 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:29:26,023 INFO  L226             Difference]: Without dead ends: 114
[2025-05-07 17:29:26,023 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,023 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:29:26,023 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:29:26,024 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-05-07 17:29:26,029 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 114.
[2025-05-07 17:29:26,029 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:29:26,030 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 149 transitions.
[2025-05-07 17:29:26,030 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 149 transitions. Word has length 41
[2025-05-07 17:29:26,030 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,030 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 149 transitions.
[2025-05-07 17:29:26,031 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:29:26,031 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 149 transitions.
[2025-05-07 17:29:26,031 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:26,032 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,032 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:29:26,032 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:29:26,032 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:26,032 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:26,032 INFO  L85        PathProgramCache]: Analyzing trace with hash -554624698, now seen corresponding path program 1 times
[2025-05-07 17:29:26,032 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:26,032 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2146426127]
[2025-05-07 17:29:26,032 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,033 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:26,057 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:26,063 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:26,064 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:26,064 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,124 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:26,124 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:26,125 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2146426127]
[2025-05-07 17:29:26,125 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2146426127] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:26,125 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:26,125 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:26,125 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1887137216]
[2025-05-07 17:29:26,125 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:26,125 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:26,125 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:26,126 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:26,126 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,126 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:29:26,164 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,165 INFO  L93              Difference]: Finished difference Result 120 states and 154 transitions.
[2025-05-07 17:29:26,165 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:26,165 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:29:26,166 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,166 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:29:26,167 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:29:26,167 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,167 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:29:26,167 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:29:26,168 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:29:26,174 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 110.
[2025-05-07 17:29:26,174 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:29:26,175 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 110 states to 110 states and 143 transitions.
[2025-05-07 17:29:26,175 INFO  L79                 Accepts]: Start accepts. Automaton has 110 states and 143 transitions. Word has length 41
[2025-05-07 17:29:26,176 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,176 INFO  L485      AbstractCegarLoop]: Abstraction has 110 states and 143 transitions.
[2025-05-07 17:29:26,176 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:29:26,176 INFO  L278                IsEmpty]: Start isEmpty. Operand 110 states and 143 transitions.
[2025-05-07 17:29:26,177 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:26,177 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,177 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:29:26,177 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:29:26,177 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:26,178 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:26,178 INFO  L85        PathProgramCache]: Analyzing trace with hash -1924159102, now seen corresponding path program 1 times
[2025-05-07 17:29:26,178 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:26,178 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [295748058]
[2025-05-07 17:29:26,178 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,178 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:26,197 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:26,208 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:26,208 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:26,208 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,428 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:26,428 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:26,428 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [295748058]
[2025-05-07 17:29:26,428 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [295748058] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:26,428 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:26,428 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:26,428 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [910955706]
[2025-05-07 17:29:26,428 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:26,428 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:26,429 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:26,429 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:26,429 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,429 INFO  L87              Difference]: Start difference. First operand 110 states and 143 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:29:26,580 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,580 INFO  L93              Difference]: Finished difference Result 112 states and 144 transitions.
[2025-05-07 17:29:26,580 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:26,581 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:29:26,581 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,582 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:29:26,582 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:29:26,583 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:29:26,583 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 1 mSDsluCounter, 465 mSDsCounter, 0 mSdLazyCounter, 120 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 589 SdHoareTripleChecker+Invalid, 120 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 120 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:26,584 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 589 Invalid, 120 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 120 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:26,584 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:29:26,588 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:29:26,588 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:29:26,588 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 137 transitions.
[2025-05-07 17:29:26,588 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 137 transitions. Word has length 41
[2025-05-07 17:29:26,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,589 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 137 transitions.
[2025-05-07 17:29:26,589 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:29:26,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 137 transitions.
[2025-05-07 17:29:26,589 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:26,589 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,589 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:26,589 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:29:26,590 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:26,590 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:26,590 INFO  L85        PathProgramCache]: Analyzing trace with hash 1312343432, now seen corresponding path program 1 times
[2025-05-07 17:29:26,590 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:26,590 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2130458122]
[2025-05-07 17:29:26,590 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,590 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:26,604 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:26,612 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:26,612 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:26,612 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,669 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:26,669 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:26,669 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2130458122]
[2025-05-07 17:29:26,669 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2130458122] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:26,669 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:26,669 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:26,669 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1875465672]
[2025-05-07 17:29:26,669 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:26,670 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:26,670 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:26,670 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:26,670 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,671 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:29:26,701 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,702 INFO  L93              Difference]: Finished difference Result 112 states and 142 transitions.
[2025-05-07 17:29:26,702 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:26,702 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:29:26,702 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,703 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:29:26,703 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:29:26,703 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,704 INFO  L437           NwaCegarLoop]: 134 mSDtfsCounter, 1 mSDsluCounter, 660 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 794 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:29:26,704 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 794 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:26,704 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:29:26,707 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:29:26,708 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:29:26,708 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 131 transitions.
[2025-05-07 17:29:26,708 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 131 transitions. Word has length 41
[2025-05-07 17:29:26,708 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,708 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 131 transitions.
[2025-05-07 17:29:26,708 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:29:26,709 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 131 transitions.
[2025-05-07 17:29:26,709 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:26,709 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,709 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:29:26,709 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:29:26,709 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:26,709 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:26,710 INFO  L85        PathProgramCache]: Analyzing trace with hash 2060629396, now seen corresponding path program 1 times
[2025-05-07 17:29:26,710 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:26,710 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [143013752]
[2025-05-07 17:29:26,710 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,710 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:26,723 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:26,729 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:26,730 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:26,730 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,781 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:26,782 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:26,782 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [143013752]
[2025-05-07 17:29:26,782 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [143013752] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:26,782 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:26,782 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:26,782 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1847183550]
[2025-05-07 17:29:26,782 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:26,782 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:26,782 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:26,783 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:26,783 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,783 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:29:26,812 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,812 INFO  L93              Difference]: Finished difference Result 108 states and 136 transitions.
[2025-05-07 17:29:26,812 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:26,813 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:29:26,813 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,814 INFO  L225             Difference]: With dead ends: 108
[2025-05-07 17:29:26,814 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:29:26,814 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,814 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:29:26,815 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:29:26,815 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:29:26,819 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:29:26,820 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:29:26,820 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 125 transitions.
[2025-05-07 17:29:26,821 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 125 transitions. Word has length 41
[2025-05-07 17:29:26,821 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,821 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 125 transitions.
[2025-05-07 17:29:26,821 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:29:26,821 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 125 transitions.
[2025-05-07 17:29:26,822 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:26,822 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,822 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:29:26,822 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:29:26,822 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:26,822 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:26,822 INFO  L85        PathProgramCache]: Analyzing trace with hash -868788892, now seen corresponding path program 1 times
[2025-05-07 17:29:26,823 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:26,823 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [962128122]
[2025-05-07 17:29:26,823 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,823 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:26,838 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:26,849 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:26,849 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:26,849 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:26,933 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:26,933 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:26,933 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [962128122]
[2025-05-07 17:29:26,933 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [962128122] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:26,933 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:26,933 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:26,933 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1258639317]
[2025-05-07 17:29:26,933 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:26,934 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:26,934 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:26,934 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:26,934 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,934 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:29:26,967 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:26,967 INFO  L93              Difference]: Finished difference Result 104 states and 130 transitions.
[2025-05-07 17:29:26,968 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:26,968 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:29:26,968 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:26,969 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:29:26,969 INFO  L226             Difference]: Without dead ends: 94
[2025-05-07 17:29:26,969 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:26,970 INFO  L437           NwaCegarLoop]: 127 mSDtfsCounter, 1 mSDsluCounter, 622 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 749 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:29:26,970 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 749 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:26,971 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-05-07 17:29:26,974 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 94.
[2025-05-07 17:29:26,975 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:29:26,975 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 119 transitions.
[2025-05-07 17:29:26,976 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 119 transitions. Word has length 41
[2025-05-07 17:29:26,976 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:26,976 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 119 transitions.
[2025-05-07 17:29:26,976 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:29:26,976 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 119 transitions.
[2025-05-07 17:29:26,977 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:26,977 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:26,977 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:29:26,977 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:29:26,977 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:26,977 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:26,977 INFO  L85        PathProgramCache]: Analyzing trace with hash 46338430, now seen corresponding path program 1 times
[2025-05-07 17:29:26,977 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:26,977 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1945572149]
[2025-05-07 17:29:26,977 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:26,978 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:26,995 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,006 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,006 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,006 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,064 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,064 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,064 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1945572149]
[2025-05-07 17:29:27,064 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1945572149] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,064 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,064 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,064 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [114045542]
[2025-05-07 17:29:27,064 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,065 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,065 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,065 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,065 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,065 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:29:27,092 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,092 INFO  L93              Difference]: Finished difference Result 100 states and 124 transitions.
[2025-05-07 17:29:27,092 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,092 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:29:27,093 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,093 INFO  L225             Difference]: With dead ends: 100
[2025-05-07 17:29:27,093 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:29:27,093 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,094 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:29:27,094 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:29:27,095 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:29:27,098 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:29:27,098 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:29:27,099 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 113 transitions.
[2025-05-07 17:29:27,099 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 113 transitions. Word has length 41
[2025-05-07 17:29:27,099 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,099 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 113 transitions.
[2025-05-07 17:29:27,100 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:29:27,100 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 113 transitions.
[2025-05-07 17:29:27,100 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,100 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,100 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:29:27,100 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:29:27,101 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,101 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,101 INFO  L85        PathProgramCache]: Analyzing trace with hash 1087250846, now seen corresponding path program 1 times
[2025-05-07 17:29:27,101 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,101 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [897298154]
[2025-05-07 17:29:27,101 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,101 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,117 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,124 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,124 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,124 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,184 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,184 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,184 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [897298154]
[2025-05-07 17:29:27,184 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [897298154] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,184 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,184 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,185 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [81342909]
[2025-05-07 17:29:27,185 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,185 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,185 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,185 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,185 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,185 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:29:27,212 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,212 INFO  L93              Difference]: Finished difference Result 96 states and 118 transitions.
[2025-05-07 17:29:27,212 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,212 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:29:27,213 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,213 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:29:27,213 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:29:27,213 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,214 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:29:27,214 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:29:27,215 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:29:27,218 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:29:27,218 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:29:27,219 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 107 transitions.
[2025-05-07 17:29:27,219 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 107 transitions. Word has length 41
[2025-05-07 17:29:27,219 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,219 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 107 transitions.
[2025-05-07 17:29:27,219 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:29:27,219 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 107 transitions.
[2025-05-07 17:29:27,220 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,220 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,220 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:29:27,220 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:29:27,220 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,221 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,221 INFO  L85        PathProgramCache]: Analyzing trace with hash -821423674, now seen corresponding path program 1 times
[2025-05-07 17:29:27,221 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,221 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1322928512]
[2025-05-07 17:29:27,221 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,221 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,238 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,248 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,249 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,249 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,318 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,318 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,318 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1322928512]
[2025-05-07 17:29:27,318 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1322928512] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,318 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,318 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,318 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [994399557]
[2025-05-07 17:29:27,318 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,318 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,318 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,318 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,318 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,319 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:29:27,344 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,344 INFO  L93              Difference]: Finished difference Result 92 states and 112 transitions.
[2025-05-07 17:29:27,344 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,344 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:29:27,344 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,345 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:29:27,345 INFO  L226             Difference]: Without dead ends: 82
[2025-05-07 17:29:27,345 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,345 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 530 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 639 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:27,345 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 639 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:27,346 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-05-07 17:29:27,347 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 82.
[2025-05-07 17:29:27,347 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:29:27,348 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 101 transitions.
[2025-05-07 17:29:27,348 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 101 transitions. Word has length 41
[2025-05-07 17:29:27,348 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,348 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 101 transitions.
[2025-05-07 17:29:27,348 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:29:27,348 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 101 transitions.
[2025-05-07 17:29:27,348 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,348 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,348 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:29:27,348 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:29:27,348 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,349 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,349 INFO  L85        PathProgramCache]: Analyzing trace with hash -59871912, now seen corresponding path program 1 times
[2025-05-07 17:29:27,349 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,349 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1443426038]
[2025-05-07 17:29:27,349 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,349 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,360 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,366 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,366 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,366 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,418 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,418 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,418 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1443426038]
[2025-05-07 17:29:27,418 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1443426038] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,418 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,418 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,418 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1497733116]
[2025-05-07 17:29:27,418 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,418 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,418 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,418 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,418 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,419 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:29:27,443 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,444 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:29:27,444 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,444 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:29:27,444 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,445 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:29:27,445 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:29:27,445 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,445 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:29:27,446 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:29:27,446 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:29:27,449 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:29:27,449 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:29:27,449 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 95 transitions.
[2025-05-07 17:29:27,450 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 95 transitions. Word has length 41
[2025-05-07 17:29:27,450 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,450 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 95 transitions.
[2025-05-07 17:29:27,450 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:29:27,450 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 95 transitions.
[2025-05-07 17:29:27,450 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,450 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,451 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:29:27,451 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:29:27,451 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,451 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,451 INFO  L85        PathProgramCache]: Analyzing trace with hash -157630026, now seen corresponding path program 1 times
[2025-05-07 17:29:27,451 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,451 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1556033264]
[2025-05-07 17:29:27,451 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,451 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,466 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,471 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,471 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,471 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,522 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,522 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,522 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1556033264]
[2025-05-07 17:29:27,522 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1556033264] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,522 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,522 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,522 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1489798291]
[2025-05-07 17:29:27,522 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,523 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,523 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,523 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,523 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,523 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:29:27,554 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,554 INFO  L93              Difference]: Finished difference Result 84 states and 100 transitions.
[2025-05-07 17:29:27,555 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,555 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:29:27,555 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,555 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:29:27,556 INFO  L226             Difference]: Without dead ends: 74
[2025-05-07 17:29:27,556 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,556 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:29:27,556 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:29:27,557 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-05-07 17:29:27,559 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 74.
[2025-05-07 17:29:27,559 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:29:27,559 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 89 transitions.
[2025-05-07 17:29:27,560 INFO  L79                 Accepts]: Start accepts. Automaton has 74 states and 89 transitions. Word has length 41
[2025-05-07 17:29:27,560 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,560 INFO  L485      AbstractCegarLoop]: Abstraction has 74 states and 89 transitions.
[2025-05-07 17:29:27,560 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:29:27,560 INFO  L278                IsEmpty]: Start isEmpty. Operand 74 states and 89 transitions.
[2025-05-07 17:29:27,560 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,560 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,561 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:29:27,561 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:29:27,561 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,561 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,561 INFO  L85        PathProgramCache]: Analyzing trace with hash -2006865526, now seen corresponding path program 1 times
[2025-05-07 17:29:27,561 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,561 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [851323558]
[2025-05-07 17:29:27,561 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,561 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,576 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,581 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,581 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,581 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,627 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,628 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,628 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [851323558]
[2025-05-07 17:29:27,628 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [851323558] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,628 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,628 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,628 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2071117455]
[2025-05-07 17:29:27,628 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,628 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,628 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,628 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,628 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,628 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:29:27,655 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,655 INFO  L93              Difference]: Finished difference Result 80 states and 94 transitions.
[2025-05-07 17:29:27,656 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,656 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:29:27,656 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,657 INFO  L225             Difference]: With dead ends: 80
[2025-05-07 17:29:27,657 INFO  L226             Difference]: Without dead ends: 70
[2025-05-07 17:29:27,657 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,657 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:29:27,657 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:29:27,658 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-05-07 17:29:27,660 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-05-07 17:29:27,660 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:29:27,661 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 83 transitions.
[2025-05-07 17:29:27,661 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 83 transitions. Word has length 41
[2025-05-07 17:29:27,661 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,661 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 83 transitions.
[2025-05-07 17:29:27,661 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:29:27,661 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 83 transitions.
[2025-05-07 17:29:27,661 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,661 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,661 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:29:27,661 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:29:27,661 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,662 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,662 INFO  L85        PathProgramCache]: Analyzing trace with hash 980446608, now seen corresponding path program 1 times
[2025-05-07 17:29:27,662 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,662 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1684804942]
[2025-05-07 17:29:27,662 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,662 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,674 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,683 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,683 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,683 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,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:29:27,730 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,730 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1684804942]
[2025-05-07 17:29:27,730 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1684804942] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,730 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,730 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,731 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1334723790]
[2025-05-07 17:29:27,731 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,731 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,731 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,731 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,731 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,731 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:29:27,757 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,757 INFO  L93              Difference]: Finished difference Result 76 states and 88 transitions.
[2025-05-07 17:29:27,758 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,758 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:29:27,758 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,758 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:29:27,758 INFO  L226             Difference]: Without dead ends: 66
[2025-05-07 17:29:27,758 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,759 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 1 mSDsluCounter, 410 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 495 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:29:27,759 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 495 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:27,759 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-05-07 17:29:27,760 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-05-07 17:29:27,760 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:29:27,761 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 77 transitions.
[2025-05-07 17:29:27,761 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 77 transitions. Word has length 41
[2025-05-07 17:29:27,761 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,761 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 77 transitions.
[2025-05-07 17:29:27,761 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:29:27,761 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 77 transitions.
[2025-05-07 17:29:27,761 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,761 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,761 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:29:27,761 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:29:27,761 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,762 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,762 INFO  L85        PathProgramCache]: Analyzing trace with hash 1169005992, now seen corresponding path program 1 times
[2025-05-07 17:29:27,762 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,762 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [296276570]
[2025-05-07 17:29:27,762 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,762 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,772 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,776 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,776 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,776 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,816 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,816 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,817 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [296276570]
[2025-05-07 17:29:27,817 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [296276570] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,817 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,817 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,817 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1222570205]
[2025-05-07 17:29:27,817 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,817 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,817 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,818 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,818 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,818 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:29:27,842 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,842 INFO  L93              Difference]: Finished difference Result 72 states and 82 transitions.
[2025-05-07 17:29:27,842 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,842 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:29:27,842 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,843 INFO  L225             Difference]: With dead ends: 72
[2025-05-07 17:29:27,843 INFO  L226             Difference]: Without dead ends: 62
[2025-05-07 17:29:27,843 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,843 INFO  L437           NwaCegarLoop]: 79 mSDtfsCounter, 1 mSDsluCounter, 380 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 459 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:27,843 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 459 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:27,844 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-05-07 17:29:27,845 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 62.
[2025-05-07 17:29:27,845 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:29:27,845 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 71 transitions.
[2025-05-07 17:29:27,845 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 71 transitions. Word has length 41
[2025-05-07 17:29:27,845 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,845 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 71 transitions.
[2025-05-07 17:29:27,845 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:29:27,845 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 71 transitions.
[2025-05-07 17:29:27,846 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,846 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,846 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:29:27,846 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:29:27,846 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,846 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,846 INFO  L85        PathProgramCache]: Analyzing trace with hash 649501062, now seen corresponding path program 1 times
[2025-05-07 17:29:27,846 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,846 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1209936002]
[2025-05-07 17:29:27,846 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,846 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,858 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,863 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,863 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,863 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:27,913 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:27,913 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:27,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1209936002]
[2025-05-07 17:29:27,913 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1209936002] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:27,913 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:27,913 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:27,913 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [586890089]
[2025-05-07 17:29:27,913 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:27,913 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:27,914 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:27,914 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:27,914 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,914 INFO  L87              Difference]: Start difference. First operand 62 states and 71 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:29:27,940 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:27,940 INFO  L93              Difference]: Finished difference Result 68 states and 76 transitions.
[2025-05-07 17:29:27,941 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:27,941 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:29:27,941 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:27,942 INFO  L225             Difference]: With dead ends: 68
[2025-05-07 17:29:27,942 INFO  L226             Difference]: Without dead ends: 58
[2025-05-07 17:29:27,942 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:27,942 INFO  L437           NwaCegarLoop]: 68 mSDtfsCounter, 1 mSDsluCounter, 330 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 398 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:29:27,942 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 398 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:27,943 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-05-07 17:29:27,945 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 58.
[2025-05-07 17:29:27,945 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:29:27,945 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 65 transitions.
[2025-05-07 17:29:27,945 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 65 transitions. Word has length 41
[2025-05-07 17:29:27,945 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:27,946 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 65 transitions.
[2025-05-07 17:29:27,946 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:29:27,946 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 65 transitions.
[2025-05-07 17:29:27,946 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,946 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,946 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:29:27,946 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:29:27,947 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,947 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,947 INFO  L85        PathProgramCache]: Analyzing trace with hash -1945283232, now seen corresponding path program 1 times
[2025-05-07 17:29:27,947 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,947 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1035640244]
[2025-05-07 17:29:27,947 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,947 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,963 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,970 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,970 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,970 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,031 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,031 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1035640244]
[2025-05-07 17:29:28,031 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1035640244] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,031 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,031 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:28,031 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1227207228]
[2025-05-07 17:29:28,031 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,031 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:28,031 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,032 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:28,032 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,032 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:29:28,059 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,059 INFO  L93              Difference]: Finished difference Result 64 states and 70 transitions.
[2025-05-07 17:29:28,059 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:28,059 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:29:28,059 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,060 INFO  L225             Difference]: With dead ends: 64
[2025-05-07 17:29:28,060 INFO  L226             Difference]: Without dead ends: 54
[2025-05-07 17:29:28,060 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,061 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:29:28,061 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:29:28,061 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-05-07 17:29:28,062 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 54.
[2025-05-07 17:29:28,062 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:29:28,063 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 59 transitions.
[2025-05-07 17:29:28,063 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 59 transitions. Word has length 41
[2025-05-07 17:29:28,063 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,063 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 59 transitions.
[2025-05-07 17:29:28,063 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:29:28,063 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 59 transitions.
[2025-05-07 17:29:28,063 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:28,063 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,063 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:29:28,063 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:29:28,063 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,064 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,064 INFO  L85        PathProgramCache]: Analyzing trace with hash 730898826, now seen corresponding path program 1 times
[2025-05-07 17:29:28,064 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,064 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [27663072]
[2025-05-07 17:29:28,064 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,064 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,075 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:28,079 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:28,079 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,079 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,125 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,125 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,125 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [27663072]
[2025-05-07 17:29:28,125 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [27663072] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,125 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,125 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:28,125 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1055736143]
[2025-05-07 17:29:28,125 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,126 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:28,126 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,126 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:28,126 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,126 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:29:28,152 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,153 INFO  L93              Difference]: Finished difference Result 60 states and 64 transitions.
[2025-05-07 17:29:28,153 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:28,153 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:29:28,153 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,154 INFO  L225             Difference]: With dead ends: 60
[2025-05-07 17:29:28,154 INFO  L226             Difference]: Without dead ends: 50
[2025-05-07 17:29:28,154 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,154 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 1 mSDsluCounter, 270 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 326 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:29:28,155 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 326 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,155 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-05-07 17:29:28,156 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 50.
[2025-05-07 17:29:28,156 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:29:28,156 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 53 transitions.
[2025-05-07 17:29:28,156 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 53 transitions. Word has length 41
[2025-05-07 17:29:28,156 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,156 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 53 transitions.
[2025-05-07 17:29:28,157 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:29:28,157 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 53 transitions.
[2025-05-07 17:29:28,157 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:28,157 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,157 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:29:28,157 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:29:28,157 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,157 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,157 INFO  L85        PathProgramCache]: Analyzing trace with hash -242122342, now seen corresponding path program 1 times
[2025-05-07 17:29:28,157 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,157 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [466245247]
[2025-05-07 17:29:28,157 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,157 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,171 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:28,176 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:28,176 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,176 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,227 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,227 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,227 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [466245247]
[2025-05-07 17:29:28,227 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [466245247] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,227 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,227 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:28,227 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [566291744]
[2025-05-07 17:29:28,227 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,227 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:28,227 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,228 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:28,228 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,228 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:29:28,254 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,254 INFO  L93              Difference]: Finished difference Result 56 states and 58 transitions.
[2025-05-07 17:29:28,254 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:28,254 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:29:28,254 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,254 INFO  L225             Difference]: With dead ends: 56
[2025-05-07 17:29:28,254 INFO  L226             Difference]: Without dead ends: 46
[2025-05-07 17:29:28,255 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,255 INFO  L437           NwaCegarLoop]: 50 mSDtfsCounter, 1 mSDsluCounter, 240 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 290 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:29:28,255 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 290 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,255 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-05-07 17:29:28,256 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 46.
[2025-05-07 17:29:28,256 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:29:28,256 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 47 transitions.
[2025-05-07 17:29:28,256 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 47 transitions. Word has length 41
[2025-05-07 17:29:28,257 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,257 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 47 transitions.
[2025-05-07 17:29:28,257 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:29:28,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 47 transitions.
[2025-05-07 17:29:28,257 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:28,257 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,257 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,257 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:29:28,257 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,257 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,257 INFO  L85        PathProgramCache]: Analyzing trace with hash 1709394334, now seen corresponding path program 1 times
[2025-05-07 17:29:28,257 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,257 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1787546331]
[2025-05-07 17:29:28,257 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,258 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,271 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:28,276 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:28,276 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,276 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,326 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,327 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,327 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1787546331]
[2025-05-07 17:29:28,327 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1787546331] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,327 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,327 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:28,327 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1539425168]
[2025-05-07 17:29:28,327 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,327 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:28,327 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,328 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:28,328 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,328 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:29:28,361 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,361 INFO  L93              Difference]: Finished difference Result 52 states and 52 transitions.
[2025-05-07 17:29:28,361 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:28,362 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:29:28,362 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,362 INFO  L225             Difference]: With dead ends: 52
[2025-05-07 17:29:28,362 INFO  L226             Difference]: Without dead ends: 42
[2025-05-07 17:29:28,362 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,364 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 1 mSDsluCounter, 230 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 279 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,364 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 279 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,365 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-05-07 17:29:28,366 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-05-07 17:29:28,366 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:29:28,366 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 41 transitions.
[2025-05-07 17:29:28,366 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 41 transitions. Word has length 41
[2025-05-07 17:29:28,367 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,367 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 41 transitions.
[2025-05-07 17:29:28,367 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:29:28,367 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 41 transitions.
[2025-05-07 17:29:28,367 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:28,367 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,367 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:29:28,367 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:29:28,367 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,368 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,368 INFO  L85        PathProgramCache]: Analyzing trace with hash 1041971722, now seen corresponding path program 1 times
[2025-05-07 17:29:28,368 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,368 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [651449199]
[2025-05-07 17:29:28,368 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,368 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,386 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:28,392 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:28,392 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,392 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,455 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:28,455 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,455 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [651449199]
[2025-05-07 17:29:28,455 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [651449199] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,455 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,455 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:28,455 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [896225890]
[2025-05-07 17:29:28,455 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,455 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:28,456 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,456 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:28,456 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:28,456 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:29:28,483 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,484 INFO  L93              Difference]: Finished difference Result 36 states and 35 transitions.
[2025-05-07 17:29:28,484 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:28,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:29:28,484 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,484 INFO  L225             Difference]: With dead ends: 36
[2025-05-07 17:29:28,484 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:29:28,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:29:28,485 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:29:28,485 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:29:28,485 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:29:28,485 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:29:28,486 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:29:28,486 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:29:28,486 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 41
[2025-05-07 17:29:28,486 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,486 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:29:28,486 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:29:28,486 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:29:28,486 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:29:28,488 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:29:28,488 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:29:28,490 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:29:28,492 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:29:28,495 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:29:28 BoogieIcfgContainer
[2025-05-07 17:29:28,495 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:29:28,495 INFO  L158              Benchmark]: Toolchain (without parser) took 4330.81ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 179.4MB in the beginning and 195.8MB in the end (delta: -16.4MB). Peak memory consumption was 28.2MB. Max. memory is 33.6GB.
[2025-05-07 17:29:28,495 INFO  L158              Benchmark]: SmtParser took 0.19ms. Allocated memory is still 234.9MB. Free memory is still 172.8MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:28,495 INFO  L158              Benchmark]: ChcToBoogie took 47.91ms. Allocated memory is still 234.9MB. Free memory was 179.4MB in the beginning and 171.2MB in the end (delta: 8.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:28,496 INFO  L158              Benchmark]: Boogie Preprocessor took 69.90ms. Allocated memory is still 234.9MB. Free memory was 170.8MB in the beginning and 166.1MB in the end (delta: 4.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:28,496 INFO  L158              Benchmark]: RCFGBuilder took 768.16ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 166.1MB in the beginning and 230.4MB in the end (delta: -64.3MB). Peak memory consumption was 75.3MB. Max. memory is 33.6GB.
[2025-05-07 17:29:28,496 INFO  L158              Benchmark]: TraceAbstraction took 3441.06ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 229.5MB in the beginning and 195.8MB in the end (delta: 33.8MB). Peak memory consumption was 4.0MB. Max. memory is 33.6GB.
[2025-05-07 17:29:28,497 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 172.8MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 47.91ms. Allocated memory is still 234.9MB. Free memory was 179.4MB in the beginning and 171.2MB in the end (delta: 8.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 69.90ms. Allocated memory is still 234.9MB. Free memory was 170.8MB in the beginning and 166.1MB in the end (delta: 4.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 768.16ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 166.1MB in the beginning and 230.4MB in the end (delta: -64.3MB). Peak memory consumption was 75.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3441.06ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 229.5MB in the beginning and 195.8MB in the end (delta: 33.8MB). Peak memory consumption was 4.0MB. 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.4s, OverallIterations: 23, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 44 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 22 mSDsluCounter, 13279 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 10822 mSDsCounter, 2 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 565 IncrementalHoareTripleChecker+Invalid, 567 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 2 mSolverCounterUnsat, 2457 mSDtfsCounter, 565 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.6s InterpolantComputationTime, 943 NumberOfCodeBlocks, 943 NumberOfCodeBlocksAsserted, 23 NumberOfCheckSat, 920 ConstructedInterpolants, 0 QuantifiedInterpolants, 1366 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 23 InterpolantComputations, 23 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:29:28,507 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
