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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:56,167 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:56,203 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df0b503-4314-4b63-85a8-d8b280cc946f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:56,206 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:56,206 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:56,219 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:56,220 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:56,220 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:56,220 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:56,220 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:56,221 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:56,221 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:56,221 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:56,221 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:56,221 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:56,222 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:56,222 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:56,222 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:56,222 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:56,222 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:56,222 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:56,222 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:56,222 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:56,223 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:56,223 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:56,223 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:56,223 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:56,445 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:56,453 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:56,455 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:56,456 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:56,456 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:56,457 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df0b503-4314-4b63-85a8-d8b280cc946f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_10_no_adts_000.smt2
[2025-05-07 17:27:56,459 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:56,462 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:56,890 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df0b503-4314-4b63-85a8-d8b280cc946f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/range_check.sol_10_no_adts_000.smt2
[2025-05-07 17:27:56,893 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:56,894 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:56,894 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:56,894 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:56,894 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:56,896 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,943 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56 Unit
[2025-05-07 17:27:56,944 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:56,944 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:56,944 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:56,944 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:56,955 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,955 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,980 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,980 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,990 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,991 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,993 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,997 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:56,999 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:57,015 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:57,016 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:57,016 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:57,016 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:57,016 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (1/1) ...
[2025-05-07 17:27:57,018 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:57,026 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:57,035 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:27:57,037 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:27:57,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:57,045 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:57,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:57,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_70_0 given in one single declaration
[2025-05-07 17:27:57,045 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_70_0
[2025-05-07 17:27:57,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_70_0
[2025-05-07 17:27:57,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_6_D_407_0 given in one single declaration
[2025-05-07 17:27:57,045 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_6_D_407_0
[2025-05-07 17:27:57,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_6_D_407_0
[2025-05-07 17:27:57,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_58_D_407_0 given in one single declaration
[2025-05-07 17:27:57,045 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_58_D_407_0
[2025-05-07 17:27:57,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_58_D_407_0
[2025-05-07 17:27:57,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_7_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,045 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_7_constructor_406_407_0
[2025-05-07 17:27:57,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_7_constructor_406_407_0
[2025-05-07 17:27:57,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,045 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36__405_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36__405_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36__405_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43_constructor_406_407_0
[2025-05-07 17:27:57,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,046 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_45_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_45_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_45_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_46_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_46_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_46_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,047 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_constructor_406_407_0
[2025-05-07 17:27:57,047 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_41_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_41_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_41_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_return_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_constructor_406_407_0 given in one single declaration
[2025-05-07 17:27:57,048 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_constructor_406_407_0
[2025-05-07 17:27:57,048 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_60_D_407_0 given in one single declaration
[2025-05-07 17:27:57,049 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:27:57,049 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_60_D_407_0
[2025-05-07 17:27:57,049 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_59_D_407_0 given in one single declaration
[2025-05-07 17:27:57,049 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:27:57,049 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_59_D_407_0
[2025-05-07 17:27:57,049 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_61_D_407_0 given in one single declaration
[2025-05-07 17:27:57,049 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:27:57,049 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_61_D_407_0
[2025-05-07 17:27:57,049 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:57,049 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:57,049 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:57,300 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:57,302 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:57,765 INFO  L?                        ?]: Removed 1077 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:57,765 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:57,774 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:57,774 INFO  L312             CfgBuilder]: Removed 24 assume(true) statements.
[2025-05-07 17:27:57,774 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:57 BoogieIcfgContainer
[2025-05-07 17:27:57,775 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:57,776 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:57,776 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:57,779 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:57,779 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:56" (1/3) ...
[2025-05-07 17:27:57,779 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35748a02 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:57, skipping insertion in model container
[2025-05-07 17:27:57,780 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:56" (2/3) ...
[2025-05-07 17:27:57,780 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35748a02 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:57, skipping insertion in model container
[2025-05-07 17:27:57,780 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:57" (3/3) ...
[2025-05-07 17:27:57,781 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:57,791 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:57,793 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 32 procedures, 128 locations, 228 edges, 32 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:57,824 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:57,833 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;@3b5f4622, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:57,833 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:57,836 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 128 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 35 states have call successors, (55), 31 states have call predecessors, (55), 31 states have return successors, (55), 33 states have call predecessors, (55), 35 states have call successors, (55)
[2025-05-07 17:27:57,844 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:57,844 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:57,844 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:57,845 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:57,849 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:57,849 INFO  L85        PathProgramCache]: Analyzing trace with hash 884425312, now seen corresponding path program 1 times
[2025-05-07 17:27:57,855 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:57,855 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [453481472]
[2025-05-07 17:27:57,855 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:57,856 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:57,898 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:57,926 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:57,927 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:57,927 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:58,092 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:58,092 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:58,092 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [453481472]
[2025-05-07 17:27:58,093 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [453481472] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:58,093 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:58,095 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:58,096 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1994511772]
[2025-05-07 17:27:58,097 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:58,100 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:58,101 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:58,118 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:58,118 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:58,120 INFO  L87              Difference]: Start difference. First operand  has 128 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 35 states have call successors, (55), 31 states have call predecessors, (55), 31 states have return successors, (55), 33 states have call predecessors, (55), 35 states have call successors, (55) Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,189 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:58,189 INFO  L93              Difference]: Finished difference Result 130 states and 175 transitions.
[2025-05-07 17:27:58,191 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:58,192 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:58,192 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:58,198 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:58,198 INFO  L226             Difference]: Without dead ends: 130
[2025-05-07 17:27:58,199 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:58,201 INFO  L437           NwaCegarLoop]: 172 mSDtfsCounter, 1 mSDsluCounter, 331 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 503 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:58,202 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 503 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:58,211 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-05-07 17:27:58,231 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 128.
[2025-05-07 17:27:58,232 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 60 states have (on average 1.0333333333333334) internal successors, (62), 62 states have internal predecessors, (62), 35 states have call successors, (55), 31 states have call predecessors, (55), 32 states have return successors, (56), 34 states have call predecessors, (56), 35 states have call successors, (56)
[2025-05-07 17:27:58,235 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 173 transitions.
[2025-05-07 17:27:58,236 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 173 transitions. Word has length 41
[2025-05-07 17:27:58,236 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:58,237 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 173 transitions.
[2025-05-07 17:27:58,237 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,237 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 173 transitions.
[2025-05-07 17:27:58,241 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:58,241 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:58,241 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:58,241 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:58,242 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:58,242 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:58,243 INFO  L85        PathProgramCache]: Analyzing trace with hash 941376430, now seen corresponding path program 1 times
[2025-05-07 17:27:58,243 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:58,243 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2039384859]
[2025-05-07 17:27:58,243 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:58,243 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:58,264 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:58,273 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:58,273 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:58,273 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:58,364 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:58,365 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:58,365 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2039384859]
[2025-05-07 17:27:58,365 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2039384859] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:58,365 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:58,365 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:58,365 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1784800980]
[2025-05-07 17:27:58,365 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:58,366 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:58,366 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:58,367 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:58,367 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:58,367 INFO  L87              Difference]: Start difference. First operand 128 states and 173 transitions. Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,386 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:58,386 INFO  L93              Difference]: Finished difference Result 130 states and 174 transitions.
[2025-05-07 17:27:58,387 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:58,387 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:58,387 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:58,389 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:27:58,389 INFO  L226             Difference]: Without dead ends: 122
[2025-05-07 17:27:58,389 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:58,390 INFO  L437           NwaCegarLoop]: 172 mSDtfsCounter, 1 mSDsluCounter, 335 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 507 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:58,390 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 507 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:58,391 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 122 states.
[2025-05-07 17:27:58,401 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 122 to 122.
[2025-05-07 17:27:58,402 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 59 states have (on average 1.0) internal successors, (59), 59 states have internal predecessors, (59), 31 states have call successors, (51), 31 states have call predecessors, (51), 31 states have return successors, (51), 31 states have call predecessors, (51), 31 states have call successors, (51)
[2025-05-07 17:27:58,403 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 161 transitions.
[2025-05-07 17:27:58,403 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 161 transitions. Word has length 41
[2025-05-07 17:27:58,403 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:58,404 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 161 transitions.
[2025-05-07 17:27:58,404 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,404 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 161 transitions.
[2025-05-07 17:27:58,405 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:58,406 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:58,406 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:58,406 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:58,406 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:58,407 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:58,407 INFO  L85        PathProgramCache]: Analyzing trace with hash -777602358, now seen corresponding path program 1 times
[2025-05-07 17:27:58,407 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:58,407 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1039874672]
[2025-05-07 17:27:58,407 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:58,407 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:58,428 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:58,450 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:58,450 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:58,450 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:58,546 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:58,546 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:58,546 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1039874672]
[2025-05-07 17:27:58,546 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1039874672] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:58,546 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:58,546 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:58,546 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1780348082]
[2025-05-07 17:27:58,546 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:58,547 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:58,547 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:58,547 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:58,548 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:58,548 INFO  L87              Difference]: Start difference. First operand 122 states and 161 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,590 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:58,590 INFO  L93              Difference]: Finished difference Result 128 states and 166 transitions.
[2025-05-07 17:27:58,591 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:58,591 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:58,591 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:58,593 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:27:58,593 INFO  L226             Difference]: Without dead ends: 118
[2025-05-07 17:27:58,593 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:58,594 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 1 mSDsluCounter, 800 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 963 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:58,594 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 963 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:58,595 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 118 states.
[2025-05-07 17:27:58,602 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 118 to 118.
[2025-05-07 17:27:58,602 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 118 states, 57 states have (on average 1.0) internal successors, (57), 57 states have internal predecessors, (57), 30 states have call successors, (49), 30 states have call predecessors, (49), 30 states have return successors, (49), 30 states have call predecessors, (49), 30 states have call successors, (49)
[2025-05-07 17:27:58,604 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 155 transitions.
[2025-05-07 17:27:58,604 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 155 transitions. Word has length 41
[2025-05-07 17:27:58,604 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:58,604 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 155 transitions.
[2025-05-07 17:27:58,604 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,604 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 155 transitions.
[2025-05-07 17:27:58,606 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:58,606 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:58,606 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:58,606 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:58,606 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:58,607 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:58,607 INFO  L85        PathProgramCache]: Analyzing trace with hash -1359046964, now seen corresponding path program 1 times
[2025-05-07 17:27:58,607 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:58,607 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [336046182]
[2025-05-07 17:27:58,607 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:58,607 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:58,625 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:58,639 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:58,639 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:58,639 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:58,754 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:58,754 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:58,754 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [336046182]
[2025-05-07 17:27:58,754 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [336046182] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:58,754 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:58,754 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:58,754 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1235621416]
[2025-05-07 17:27:58,754 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:58,755 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:58,755 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:58,755 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:58,755 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:58,756 INFO  L87              Difference]: Start difference. First operand 118 states and 155 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,796 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:58,797 INFO  L93              Difference]: Finished difference Result 124 states and 160 transitions.
[2025-05-07 17:27:58,797 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:58,797 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:58,798 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:58,799 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:27:58,799 INFO  L226             Difference]: Without dead ends: 114
[2025-05-07 17:27:58,799 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:58,800 INFO  L437           NwaCegarLoop]: 157 mSDtfsCounter, 1 mSDsluCounter, 770 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 927 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:58,800 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 927 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:58,801 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-05-07 17:27:58,807 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 114.
[2025-05-07 17:27:58,807 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 114 states, 55 states have (on average 1.0) internal successors, (55), 55 states have internal predecessors, (55), 29 states have call successors, (47), 29 states have call predecessors, (47), 29 states have return successors, (47), 29 states have call predecessors, (47), 29 states have call successors, (47)
[2025-05-07 17:27:58,808 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 114 states to 114 states and 149 transitions.
[2025-05-07 17:27:58,808 INFO  L79                 Accepts]: Start accepts. Automaton has 114 states and 149 transitions. Word has length 41
[2025-05-07 17:27:58,809 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:58,809 INFO  L485      AbstractCegarLoop]: Abstraction has 114 states and 149 transitions.
[2025-05-07 17:27:58,809 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,809 INFO  L278                IsEmpty]: Start isEmpty. Operand 114 states and 149 transitions.
[2025-05-07 17:27:58,810 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:58,810 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:58,810 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:58,810 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:58,810 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:58,811 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:58,811 INFO  L85        PathProgramCache]: Analyzing trace with hash 2145149594, now seen corresponding path program 1 times
[2025-05-07 17:27:58,811 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:58,811 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1663318052]
[2025-05-07 17:27:58,811 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:58,811 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:58,829 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:58,842 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:58,842 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:58,842 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:58,931 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:58,931 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:58,931 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1663318052]
[2025-05-07 17:27:58,931 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1663318052] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:58,931 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:58,931 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:58,931 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1537987966]
[2025-05-07 17:27:58,931 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:58,932 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:58,932 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:58,932 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:58,932 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:58,932 INFO  L87              Difference]: Start difference. First operand 114 states and 149 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,963 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:58,963 INFO  L93              Difference]: Finished difference Result 120 states and 154 transitions.
[2025-05-07 17:27:58,963 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:58,964 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:58,964 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:58,964 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:27:58,964 INFO  L226             Difference]: Without dead ends: 110
[2025-05-07 17:27:58,965 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:58,965 INFO  L437           NwaCegarLoop]: 151 mSDtfsCounter, 1 mSDsluCounter, 740 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 891 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:58,965 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 891 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:58,966 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-05-07 17:27:58,969 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 110.
[2025-05-07 17:27:58,969 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 110 states, 53 states have (on average 1.0) internal successors, (53), 53 states have internal predecessors, (53), 28 states have call successors, (45), 28 states have call predecessors, (45), 28 states have return successors, (45), 28 states have call predecessors, (45), 28 states have call successors, (45)
[2025-05-07 17:27:58,970 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 110 states to 110 states and 143 transitions.
[2025-05-07 17:27:58,970 INFO  L79                 Accepts]: Start accepts. Automaton has 110 states and 143 transitions. Word has length 41
[2025-05-07 17:27:58,970 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:58,970 INFO  L485      AbstractCegarLoop]: Abstraction has 110 states and 143 transitions.
[2025-05-07 17:27:58,970 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:58,970 INFO  L278                IsEmpty]: Start isEmpty. Operand 110 states and 143 transitions.
[2025-05-07 17:27:58,971 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:58,971 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:58,971 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:58,971 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:58,971 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:58,971 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:58,971 INFO  L85        PathProgramCache]: Analyzing trace with hash 1026947914, now seen corresponding path program 1 times
[2025-05-07 17:27:58,971 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:58,971 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1629245015]
[2025-05-07 17:27:58,971 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:58,972 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:58,986 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:58,996 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:58,996 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:58,996 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,065 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,065 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,066 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1629245015]
[2025-05-07 17:27:59,066 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1629245015] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,066 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,066 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,066 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2012185707]
[2025-05-07 17:27:59,066 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,066 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,066 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,067 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,067 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,067 INFO  L87              Difference]: Start difference. First operand 110 states and 143 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,101 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,101 INFO  L93              Difference]: Finished difference Result 116 states and 148 transitions.
[2025-05-07 17:27:59,102 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,102 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,102 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,103 INFO  L225             Difference]: With dead ends: 116
[2025-05-07 17:27:59,103 INFO  L226             Difference]: Without dead ends: 106
[2025-05-07 17:27:59,103 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,104 INFO  L437           NwaCegarLoop]: 145 mSDtfsCounter, 1 mSDsluCounter, 710 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 855 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,104 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 855 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,105 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-05-07 17:27:59,110 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 106.
[2025-05-07 17:27:59,111 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 51 states have (on average 1.0) internal successors, (51), 51 states have internal predecessors, (51), 27 states have call successors, (43), 27 states have call predecessors, (43), 27 states have return successors, (43), 27 states have call predecessors, (43), 27 states have call successors, (43)
[2025-05-07 17:27:59,111 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 137 transitions.
[2025-05-07 17:27:59,112 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 137 transitions. Word has length 41
[2025-05-07 17:27:59,112 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,112 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 137 transitions.
[2025-05-07 17:27:59,112 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,112 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 137 transitions.
[2025-05-07 17:27:59,113 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,113 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,113 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,113 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:59,113 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,114 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,114 INFO  L85        PathProgramCache]: Analyzing trace with hash 1650396808, now seen corresponding path program 1 times
[2025-05-07 17:27:59,114 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,114 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1120398472]
[2025-05-07 17:27:59,114 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,114 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,129 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,135 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,135 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,135 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,189 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,189 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1120398472]
[2025-05-07 17:27:59,189 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1120398472] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,189 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,189 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,189 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1116075506]
[2025-05-07 17:27:59,189 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,190 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,190 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,190 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,190 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,190 INFO  L87              Difference]: Start difference. First operand 106 states and 137 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,223 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,223 INFO  L93              Difference]: Finished difference Result 112 states and 142 transitions.
[2025-05-07 17:27:59,224 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,224 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,224 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,225 INFO  L225             Difference]: With dead ends: 112
[2025-05-07 17:27:59,225 INFO  L226             Difference]: Without dead ends: 102
[2025-05-07 17:27:59,225 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,225 INFO  L437           NwaCegarLoop]: 139 mSDtfsCounter, 1 mSDsluCounter, 680 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 819 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,226 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 819 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,226 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-05-07 17:27:59,229 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 102.
[2025-05-07 17:27:59,229 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 49 states have (on average 1.0) internal successors, (49), 49 states have internal predecessors, (49), 26 states have call successors, (41), 26 states have call predecessors, (41), 26 states have return successors, (41), 26 states have call predecessors, (41), 26 states have call successors, (41)
[2025-05-07 17:27:59,230 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 131 transitions.
[2025-05-07 17:27:59,230 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 131 transitions. Word has length 41
[2025-05-07 17:27:59,230 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,230 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 131 transitions.
[2025-05-07 17:27:59,230 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,231 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 131 transitions.
[2025-05-07 17:27:59,231 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,231 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,231 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,232 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:59,232 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,232 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,232 INFO  L85        PathProgramCache]: Analyzing trace with hash 965422800, now seen corresponding path program 1 times
[2025-05-07 17:27:59,232 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,232 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1164819352]
[2025-05-07 17:27:59,232 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,232 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,246 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,252 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,252 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,252 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,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:27:59,318 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,318 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1164819352]
[2025-05-07 17:27:59,318 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1164819352] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,318 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,318 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,318 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [148214116]
[2025-05-07 17:27:59,319 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,319 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,319 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,319 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,319 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,320 INFO  L87              Difference]: Start difference. First operand 102 states and 131 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,349 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,350 INFO  L93              Difference]: Finished difference Result 108 states and 136 transitions.
[2025-05-07 17:27:59,350 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,350 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,350 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,351 INFO  L225             Difference]: With dead ends: 108
[2025-05-07 17:27:59,351 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:27:59,351 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,352 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 650 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 783 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,352 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 783 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,353 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:27:59,356 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:27:59,357 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 47 states have (on average 1.0) internal successors, (47), 47 states have internal predecessors, (47), 25 states have call successors, (39), 25 states have call predecessors, (39), 25 states have return successors, (39), 25 states have call predecessors, (39), 25 states have call successors, (39)
[2025-05-07 17:27:59,358 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 125 transitions.
[2025-05-07 17:27:59,358 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 125 transitions. Word has length 41
[2025-05-07 17:27:59,358 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,358 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 125 transitions.
[2025-05-07 17:27:59,358 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,358 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 125 transitions.
[2025-05-07 17:27:59,359 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,359 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,359 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,359 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:59,359 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,360 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,360 INFO  L85        PathProgramCache]: Analyzing trace with hash -172653834, now seen corresponding path program 1 times
[2025-05-07 17:27:59,360 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,360 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1177351314]
[2025-05-07 17:27:59,360 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,360 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,376 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,385 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,385 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,385 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,447 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,447 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,447 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1177351314]
[2025-05-07 17:27:59,447 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1177351314] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,447 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,447 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,447 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [349672070]
[2025-05-07 17:27:59,447 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,448 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,448 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,448 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,448 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,448 INFO  L87              Difference]: Start difference. First operand 98 states and 125 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,483 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,483 INFO  L93              Difference]: Finished difference Result 104 states and 130 transitions.
[2025-05-07 17:27:59,483 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,483 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,483 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,484 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:27:59,484 INFO  L226             Difference]: Without dead ends: 94
[2025-05-07 17:27:59,484 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,484 INFO  L437           NwaCegarLoop]: 127 mSDtfsCounter, 1 mSDsluCounter, 620 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 747 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,485 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 747 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,485 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-05-07 17:27:59,487 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 94.
[2025-05-07 17:27:59,487 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 45 states have (on average 1.0) internal successors, (45), 45 states have internal predecessors, (45), 24 states have call successors, (37), 24 states have call predecessors, (37), 24 states have return successors, (37), 24 states have call predecessors, (37), 24 states have call successors, (37)
[2025-05-07 17:27:59,488 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 119 transitions.
[2025-05-07 17:27:59,488 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 119 transitions. Word has length 41
[2025-05-07 17:27:59,488 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,488 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 119 transitions.
[2025-05-07 17:27:59,488 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,488 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 119 transitions.
[2025-05-07 17:27:59,489 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,489 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,489 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,489 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:59,489 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,489 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,489 INFO  L85        PathProgramCache]: Analyzing trace with hash 1336232614, now seen corresponding path program 1 times
[2025-05-07 17:27:59,489 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,489 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [768842578]
[2025-05-07 17:27:59,489 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,489 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,501 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,506 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,506 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,506 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,558 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,558 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,558 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [768842578]
[2025-05-07 17:27:59,558 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [768842578] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,559 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,559 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,559 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [470104079]
[2025-05-07 17:27:59,559 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,559 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,559 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,559 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,560 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,560 INFO  L87              Difference]: Start difference. First operand 94 states and 119 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,587 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,587 INFO  L93              Difference]: Finished difference Result 100 states and 124 transitions.
[2025-05-07 17:27:59,587 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,587 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,587 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,588 INFO  L225             Difference]: With dead ends: 100
[2025-05-07 17:27:59,588 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:27:59,588 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,589 INFO  L437           NwaCegarLoop]: 121 mSDtfsCounter, 1 mSDsluCounter, 590 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 711 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,589 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 711 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,589 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:27:59,591 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:27:59,591 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 43 states have (on average 1.0) internal successors, (43), 43 states have internal predecessors, (43), 23 states have call successors, (35), 23 states have call predecessors, (35), 23 states have return successors, (35), 23 states have call predecessors, (35), 23 states have call successors, (35)
[2025-05-07 17:27:59,592 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 113 transitions.
[2025-05-07 17:27:59,592 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 113 transitions. Word has length 41
[2025-05-07 17:27:59,592 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,592 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 113 transitions.
[2025-05-07 17:27:59,592 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,592 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 113 transitions.
[2025-05-07 17:27:59,593 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,593 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,593 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,593 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:59,593 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,593 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,593 INFO  L85        PathProgramCache]: Analyzing trace with hash 282648296, now seen corresponding path program 1 times
[2025-05-07 17:27:59,593 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,593 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [886658261]
[2025-05-07 17:27:59,593 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,594 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,608 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,617 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,617 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,617 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,726 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,726 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,726 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [886658261]
[2025-05-07 17:27:59,726 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [886658261] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,726 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,726 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,726 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1091732019]
[2025-05-07 17:27:59,726 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,726 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,726 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,727 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,727 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,727 INFO  L87              Difference]: Start difference. First operand 90 states and 113 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,755 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,755 INFO  L93              Difference]: Finished difference Result 96 states and 118 transitions.
[2025-05-07 17:27:59,756 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,756 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,756 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,756 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:27:59,757 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:27:59,757 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,757 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 1 mSDsluCounter, 562 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 677 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,757 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 677 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,758 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:27:59,761 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-05-07 17:27:59,761 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 41 states have (on average 1.0) internal successors, (41), 41 states have internal predecessors, (41), 22 states have call successors, (33), 22 states have call predecessors, (33), 22 states have return successors, (33), 22 states have call predecessors, (33), 22 states have call successors, (33)
[2025-05-07 17:27:59,762 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 107 transitions.
[2025-05-07 17:27:59,762 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 107 transitions. Word has length 41
[2025-05-07 17:27:59,762 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,762 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 107 transitions.
[2025-05-07 17:27:59,762 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,762 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 107 transitions.
[2025-05-07 17:27:59,763 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,763 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,763 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,763 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:27:59,763 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,763 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,763 INFO  L85        PathProgramCache]: Analyzing trace with hash -836447482, now seen corresponding path program 1 times
[2025-05-07 17:27:59,763 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,764 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1931285732]
[2025-05-07 17:27:59,764 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,764 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,780 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,790 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,790 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,790 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,853 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,854 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,854 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1931285732]
[2025-05-07 17:27:59,854 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1931285732] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,854 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,854 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,854 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1230084699]
[2025-05-07 17:27:59,854 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,854 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,854 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,855 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,855 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,855 INFO  L87              Difference]: Start difference. First operand 86 states and 107 transitions. Second operand  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,885 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,885 INFO  L93              Difference]: Finished difference Result 92 states and 112 transitions.
[2025-05-07 17:27:59,886 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:59,886 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11) Word has length 41
[2025-05-07 17:27:59,886 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:59,887 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:27:59,887 INFO  L226             Difference]: Without dead ends: 82
[2025-05-07 17:27:59,887 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,887 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 530 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 639 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:59,888 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 639 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:59,888 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-05-07 17:27:59,891 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 82.
[2025-05-07 17:27:59,891 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 39 states have (on average 1.0) internal successors, (39), 39 states have internal predecessors, (39), 21 states have call successors, (31), 21 states have call predecessors, (31), 21 states have return successors, (31), 21 states have call predecessors, (31), 21 states have call successors, (31)
[2025-05-07 17:27:59,891 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 101 transitions.
[2025-05-07 17:27:59,892 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 101 transitions. Word has length 41
[2025-05-07 17:27:59,892 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:59,892 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 101 transitions.
[2025-05-07 17:27:59,892 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:27:59,892 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 101 transitions.
[2025-05-07 17:27:59,893 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:59,893 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:59,893 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:59,893 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:27:59,893 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:59,893 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:59,893 INFO  L85        PathProgramCache]: Analyzing trace with hash -1002694944, now seen corresponding path program 1 times
[2025-05-07 17:27:59,894 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:59,894 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1919583704]
[2025-05-07 17:27:59,894 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:59,894 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:59,906 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:59,912 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:59,912 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:59,912 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:59,970 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:27:59,970 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:59,970 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1919583704]
[2025-05-07 17:27:59,970 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1919583704] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:59,970 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:59,970 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:59,971 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1308416518]
[2025-05-07 17:27:59,971 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:59,971 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:59,971 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:59,971 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:59,971 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:59,971 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:28:00,001 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,001 INFO  L93              Difference]: Finished difference Result 88 states and 106 transitions.
[2025-05-07 17:28:00,002 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,002 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:28:00,002 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,003 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:28:00,003 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:28:00,003 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:28:00,003 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:28:00,004 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:28:00,004 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:28:00,007 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:28:00,007 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:28:00,008 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 95 transitions.
[2025-05-07 17:28:00,008 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 95 transitions. Word has length 41
[2025-05-07 17:28:00,008 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,008 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 95 transitions.
[2025-05-07 17:28:00,008 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:28:00,008 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 95 transitions.
[2025-05-07 17:28:00,009 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,009 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,009 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:28:00,009 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:28:00,009 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,009 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,009 INFO  L85        PathProgramCache]: Analyzing trace with hash -380551456, now seen corresponding path program 1 times
[2025-05-07 17:28:00,009 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,010 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [521419935]
[2025-05-07 17:28:00,010 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,010 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,022 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,028 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,028 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,028 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,092 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:28:00,092 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,092 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [521419935]
[2025-05-07 17:28:00,092 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [521419935] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,092 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,092 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,092 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1528426407]
[2025-05-07 17:28:00,092 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,092 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,093 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,093 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,093 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,093 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:28:00,124 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,124 INFO  L93              Difference]: Finished difference Result 84 states and 100 transitions.
[2025-05-07 17:28:00,124 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,125 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:28:00,125 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,125 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:28:00,125 INFO  L226             Difference]: Without dead ends: 74
[2025-05-07 17:28:00,125 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:28:00,126 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:28:00,126 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:28:00,127 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-05-07 17:28:00,129 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 74.
[2025-05-07 17:28:00,129 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:28:00,130 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 89 transitions.
[2025-05-07 17:28:00,130 INFO  L79                 Accepts]: Start accepts. Automaton has 74 states and 89 transitions. Word has length 41
[2025-05-07 17:28:00,130 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,130 INFO  L485      AbstractCegarLoop]: Abstraction has 74 states and 89 transitions.
[2025-05-07 17:28:00,130 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:28:00,130 INFO  L278                IsEmpty]: Start isEmpty. Operand 74 states and 89 transitions.
[2025-05-07 17:28:00,131 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,131 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,131 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:28:00,131 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:28:00,131 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,132 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,132 INFO  L85        PathProgramCache]: Analyzing trace with hash 634477254, now seen corresponding path program 1 times
[2025-05-07 17:28:00,132 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,132 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [947470002]
[2025-05-07 17:28:00,132 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,132 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,150 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,160 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,160 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,160 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,236 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:28:00,236 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,236 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [947470002]
[2025-05-07 17:28:00,236 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [947470002] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,236 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,236 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,236 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [886473985]
[2025-05-07 17:28:00,236 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,236 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,237 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,237 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,237 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,237 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:28:00,266 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,266 INFO  L93              Difference]: Finished difference Result 80 states and 94 transitions.
[2025-05-07 17:28:00,266 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,266 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:28:00,267 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,267 INFO  L225             Difference]: With dead ends: 80
[2025-05-07 17:28:00,267 INFO  L226             Difference]: Without dead ends: 70
[2025-05-07 17:28:00,267 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:28:00,268 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:28:00,268 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:28:00,268 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-05-07 17:28:00,270 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-05-07 17:28:00,270 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:28:00,271 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 83 transitions.
[2025-05-07 17:28:00,271 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 83 transitions. Word has length 41
[2025-05-07 17:28:00,271 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,271 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 83 transitions.
[2025-05-07 17:28:00,271 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:28:00,271 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 83 transitions.
[2025-05-07 17:28:00,272 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,272 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,272 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:28:00,272 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:28:00,272 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,272 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,273 INFO  L85        PathProgramCache]: Analyzing trace with hash -920939798, now seen corresponding path program 1 times
[2025-05-07 17:28:00,273 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,273 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [98458527]
[2025-05-07 17:28:00,273 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,273 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,290 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,294 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,294 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,294 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,342 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:28:00,342 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,342 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [98458527]
[2025-05-07 17:28:00,342 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [98458527] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,342 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,342 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,343 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [828309846]
[2025-05-07 17:28:00,343 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,343 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,343 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,343 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,344 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,344 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:28:00,377 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,377 INFO  L93              Difference]: Finished difference Result 76 states and 88 transitions.
[2025-05-07 17:28:00,377 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,377 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:28:00,378 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,378 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:28:00,378 INFO  L226             Difference]: Without dead ends: 66
[2025-05-07 17:28:00,378 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:28:00,379 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:28:00,379 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:28:00,380 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-05-07 17:28:00,382 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-05-07 17:28:00,383 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:28:00,383 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 77 transitions.
[2025-05-07 17:28:00,383 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 77 transitions. Word has length 41
[2025-05-07 17:28:00,383 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,384 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 77 transitions.
[2025-05-07 17:28:00,384 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:28:00,384 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 77 transitions.
[2025-05-07 17:28:00,384 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,384 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,385 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:28:00,385 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:28:00,385 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,385 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,385 INFO  L85        PathProgramCache]: Analyzing trace with hash -1939182910, now seen corresponding path program 1 times
[2025-05-07 17:28:00,385 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,385 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [902295551]
[2025-05-07 17:28:00,385 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,386 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,409 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,420 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,420 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,420 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,584 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:28:00,584 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,584 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [902295551]
[2025-05-07 17:28:00,585 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [902295551] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,585 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,585 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,585 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1904473693]
[2025-05-07 17:28:00,585 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,585 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,585 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,585 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,586 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,586 INFO  L87              Difference]: Start difference. First operand 66 states and 77 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:28:00,655 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,655 INFO  L93              Difference]: Finished difference Result 68 states and 78 transitions.
[2025-05-07 17:28:00,655 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,655 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:28:00,655 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,656 INFO  L225             Difference]: With dead ends: 68
[2025-05-07 17:28:00,656 INFO  L226             Difference]: Without dead ends: 62
[2025-05-07 17:28:00,656 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:28:00,657 INFO  L437           NwaCegarLoop]: 69 mSDtfsCounter, 1 mSDsluCounter, 256 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 325 SdHoareTripleChecker+Invalid, 54 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:00,657 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 325 Invalid, 54 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:00,657 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-05-07 17:28:00,659 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 62.
[2025-05-07 17:28:00,659 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:28:00,660 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 71 transitions.
[2025-05-07 17:28:00,660 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 71 transitions. Word has length 41
[2025-05-07 17:28:00,660 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,660 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 71 transitions.
[2025-05-07 17:28:00,660 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:28:00,660 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 71 transitions.
[2025-05-07 17:28:00,661 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,661 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,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:28:00,661 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:28:00,661 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,662 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,662 INFO  L85        PathProgramCache]: Analyzing trace with hash -2043607360, now seen corresponding path program 1 times
[2025-05-07 17:28:00,662 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,662 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1193189076]
[2025-05-07 17:28:00,662 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,662 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,678 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,687 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,687 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,687 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,757 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:28:00,757 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,757 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1193189076]
[2025-05-07 17:28:00,758 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1193189076] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,758 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,758 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,758 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [775415374]
[2025-05-07 17:28:00,758 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,758 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,758 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,758 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,759 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,759 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:28:00,786 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,786 INFO  L93              Difference]: Finished difference Result 68 states and 76 transitions.
[2025-05-07 17:28:00,787 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,787 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:28:00,787 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,787 INFO  L225             Difference]: With dead ends: 68
[2025-05-07 17:28:00,787 INFO  L226             Difference]: Without dead ends: 58
[2025-05-07 17:28:00,788 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,788 INFO  L437           NwaCegarLoop]: 73 mSDtfsCounter, 1 mSDsluCounter, 350 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 423 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:00,788 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 423 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:00,789 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-05-07 17:28:00,791 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 58.
[2025-05-07 17:28:00,791 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:28:00,791 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 65 transitions.
[2025-05-07 17:28:00,791 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 65 transitions. Word has length 41
[2025-05-07 17:28:00,791 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,791 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 65 transitions.
[2025-05-07 17:28:00,791 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 7 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 6 states have call predecessors, (11), 3 states have call successors, (11)
[2025-05-07 17:28:00,792 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 65 transitions.
[2025-05-07 17:28:00,792 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,792 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,792 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:28:00,792 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:28:00,792 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,792 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,792 INFO  L85        PathProgramCache]: Analyzing trace with hash 1319037650, now seen corresponding path program 1 times
[2025-05-07 17:28:00,792 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,792 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1760523500]
[2025-05-07 17:28:00,792 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,792 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,807 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,812 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,812 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,812 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,868 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:28:00,868 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,868 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1760523500]
[2025-05-07 17:28:00,868 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1760523500] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,868 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,868 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,868 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1290081409]
[2025-05-07 17:28:00,868 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,868 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,868 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,869 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,869 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,869 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:28:00,894 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,894 INFO  L93              Difference]: Finished difference Result 64 states and 70 transitions.
[2025-05-07 17:28:00,894 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,895 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:28:00,895 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,895 INFO  L225             Difference]: With dead ends: 64
[2025-05-07 17:28:00,895 INFO  L226             Difference]: Without dead ends: 54
[2025-05-07 17:28:00,895 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:28:00,895 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:28:00,896 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:28:00,896 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-05-07 17:28:00,897 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 54.
[2025-05-07 17:28:00,897 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:28:00,897 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 59 transitions.
[2025-05-07 17:28:00,898 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 59 transitions. Word has length 41
[2025-05-07 17:28:00,898 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,898 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 59 transitions.
[2025-05-07 17:28:00,898 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:28:00,898 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 59 transitions.
[2025-05-07 17:28:00,898 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,898 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,898 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:28:00,898 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:28:00,898 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,899 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,899 INFO  L85        PathProgramCache]: Analyzing trace with hash 198155980, now seen corresponding path program 1 times
[2025-05-07 17:28:00,899 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,899 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [376521325]
[2025-05-07 17:28:00,899 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,899 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,911 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:00,916 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:00,916 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,916 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,962 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:28:00,962 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,962 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [376521325]
[2025-05-07 17:28:00,963 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [376521325] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,963 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,963 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:00,963 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [794191573]
[2025-05-07 17:28:00,963 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,963 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:00,963 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,964 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:00,964 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:00,964 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:28:00,989 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,989 INFO  L93              Difference]: Finished difference Result 60 states and 64 transitions.
[2025-05-07 17:28:00,989 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:00,990 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:28:00,990 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,990 INFO  L225             Difference]: With dead ends: 60
[2025-05-07 17:28:00,990 INFO  L226             Difference]: Without dead ends: 50
[2025-05-07 17:28:00,990 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:28:00,991 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 1 mSDsluCounter, 290 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 351 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:00,991 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 351 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:00,991 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-05-07 17:28:00,993 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 50.
[2025-05-07 17:28:00,993 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:28:00,993 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 53 transitions.
[2025-05-07 17:28:00,993 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 53 transitions. Word has length 41
[2025-05-07 17:28:00,993 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,993 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 53 transitions.
[2025-05-07 17:28:00,994 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:28:00,994 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 53 transitions.
[2025-05-07 17:28:00,994 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:00,994 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,994 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:28:00,994 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:28:00,994 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,995 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,995 INFO  L85        PathProgramCache]: Analyzing trace with hash 2045605588, now seen corresponding path program 1 times
[2025-05-07 17:28:00,995 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,995 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1236051275]
[2025-05-07 17:28:00,995 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,995 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:01,009 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:01,014 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:01,014 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:01,014 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:01,068 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:28:01,069 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:01,069 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1236051275]
[2025-05-07 17:28:01,069 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1236051275] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:01,069 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:01,069 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:01,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [82733999]
[2025-05-07 17:28:01,069 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:01,069 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:01,069 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:01,070 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:01,070 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:01,070 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:28:01,099 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:01,099 INFO  L93              Difference]: Finished difference Result 56 states and 58 transitions.
[2025-05-07 17:28:01,099 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:01,099 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:28:01,100 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:01,100 INFO  L225             Difference]: With dead ends: 56
[2025-05-07 17:28:01,100 INFO  L226             Difference]: Without dead ends: 46
[2025-05-07 17:28:01,100 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:28:01,101 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:28:01,101 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:28:01,101 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-05-07 17:28:01,102 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 46.
[2025-05-07 17:28:01,103 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:28:01,103 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 47 transitions.
[2025-05-07 17:28:01,103 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 47 transitions. Word has length 41
[2025-05-07 17:28:01,103 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:01,103 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 47 transitions.
[2025-05-07 17:28:01,103 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:28:01,103 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 47 transitions.
[2025-05-07 17:28:01,103 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:01,104 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:01,104 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:28:01,104 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:28:01,104 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:01,104 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:01,104 INFO  L85        PathProgramCache]: Analyzing trace with hash 259738274, now seen corresponding path program 1 times
[2025-05-07 17:28:01,104 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:01,104 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [75817908]
[2025-05-07 17:28:01,104 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:01,104 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:01,116 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:01,121 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:01,121 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:01,121 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:01,179 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:28:01,179 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:01,179 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [75817908]
[2025-05-07 17:28:01,179 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [75817908] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:01,179 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:01,179 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:01,180 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1528808989]
[2025-05-07 17:28:01,180 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:01,180 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:01,180 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:01,180 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:01,180 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:01,180 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:28:01,208 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:01,208 INFO  L93              Difference]: Finished difference Result 52 states and 52 transitions.
[2025-05-07 17:28:01,208 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:01,208 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:28:01,209 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:01,209 INFO  L225             Difference]: With dead ends: 52
[2025-05-07 17:28:01,209 INFO  L226             Difference]: Without dead ends: 42
[2025-05-07 17:28:01,209 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:28:01,211 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 1 mSDsluCounter, 210 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 254 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:01,211 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 254 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:01,211 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-05-07 17:28:01,212 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-05-07 17:28:01,212 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:28:01,213 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 41 transitions.
[2025-05-07 17:28:01,213 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 41 transitions. Word has length 41
[2025-05-07 17:28:01,213 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:01,213 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 41 transitions.
[2025-05-07 17:28:01,213 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:28:01,213 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 41 transitions.
[2025-05-07 17:28:01,213 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:28:01,213 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:01,213 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:28:01,213 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:28:01,214 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:01,214 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:01,214 INFO  L85        PathProgramCache]: Analyzing trace with hash 1962899164, now seen corresponding path program 1 times
[2025-05-07 17:28:01,214 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:01,214 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1982782772]
[2025-05-07 17:28:01,214 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:01,214 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:01,226 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:28:01,232 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:28:01,232 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:01,232 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:01,285 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:28:01,285 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:01,285 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1982782772]
[2025-05-07 17:28:01,285 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1982782772] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:01,286 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:01,286 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:28:01,286 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1587360234]
[2025-05-07 17:28:01,286 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:01,286 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:28:01,286 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:01,286 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:28:01,286 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:01,287 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:28:01,313 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:01,313 INFO  L93              Difference]: Finished difference Result 36 states and 35 transitions.
[2025-05-07 17:28:01,313 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:28:01,313 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:28:01,314 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:01,314 INFO  L225             Difference]: With dead ends: 36
[2025-05-07 17:28:01,314 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:01,314 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:28:01,314 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:28:01,315 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:28:01,315 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:01,315 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:01,315 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:28:01,315 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:01,315 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 41
[2025-05-07 17:28:01,315 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:01,315 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:01,315 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:28:01,315 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:01,316 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:01,318 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:01,318 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-05-07 17:28:01,321 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:28:01,323 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:01,326 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:01 BoogieIcfgContainer
[2025-05-07 17:28:01,326 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:01,327 INFO  L158              Benchmark]: Toolchain (without parser) took 4433.18ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 181.5MB in the beginning and 155.3MB in the end (delta: 26.2MB). Peak memory consumption was 80.5MB. Max. memory is 33.6GB.
[2025-05-07 17:28:01,327 INFO  L158              Benchmark]: SmtParser took 0.34ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:01,327 INFO  L158              Benchmark]: ChcToBoogie took 49.54ms. Allocated memory is still 234.9MB. Free memory was 181.5MB in the beginning and 173.4MB in the end (delta: 8.2MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:28:01,327 INFO  L158              Benchmark]: Boogie Preprocessor took 71.06ms. Allocated memory is still 234.9MB. Free memory was 173.4MB in the beginning and 168.0MB in the end (delta: 5.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:01,328 INFO  L158              Benchmark]: RCFGBuilder took 759.02ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 168.0MB in the beginning and 233.6MB in the end (delta: -65.6MB). Peak memory consumption was 74.3MB. Max. memory is 33.6GB.
[2025-05-07 17:28:01,328 INFO  L158              Benchmark]: TraceAbstraction took 3550.37ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 232.6MB in the beginning and 155.3MB in the end (delta: 77.3MB). Peak memory consumption was 40.4MB. Max. memory is 33.6GB.
[2025-05-07 17:28:01,329 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.34ms. Allocated memory is still 234.9MB. Free memory is still 172.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 49.54ms. Allocated memory is still 234.9MB. Free memory was 181.5MB in the beginning and 173.4MB in the end (delta: 8.2MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 71.06ms. Allocated memory is still 234.9MB. Free memory was 173.4MB in the beginning and 168.0MB in the end (delta: 5.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 759.02ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 168.0MB in the beginning and 233.6MB in the end (delta: -65.6MB). Peak memory consumption was 74.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3550.37ms. Allocated memory was 318.8MB in the beginning and 285.2MB in the end (delta: -33.6MB). Free memory was 232.6MB in the beginning and 155.3MB in the end (delta: 77.3MB). Peak memory consumption was 40.4MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 32 procedures, 128 locations, 228 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.5s, OverallIterations: 23, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 44 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 22 mSDsluCounter, 13427 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 10951 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 485 IncrementalHoareTripleChecker+Invalid, 485 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 2476 mSDtfsCounter, 485 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 155 GetRequests, 46 SyntacticMatches, 0 SemanticMatches, 109 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.4s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=128occurred in iteration=0, InterpolantAutomatonStates: 155, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 23 MinimizatonAttempts, 2 StatesRemovedByMinimization, 1 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.8s InterpolantComputationTime, 943 NumberOfCodeBlocks, 943 NumberOfCodeBlocksAsserted, 23 NumberOfCheckSat, 920 ConstructedInterpolants, 0 QuantifiedInterpolants, 1366 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 23 InterpolantComputations, 23 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:28:01,341 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
