./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/implicit_only_constructor_hierarchy.sol_4_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:25:20,406 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:25:20,446 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c60d308-1e91-410a-a8ed-5b67a1ef00ca/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:25:20,449 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:25:20,449 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:25:20,462 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:25:20,463 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:25:20,463 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:25:20,463 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:25:20,463 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:25:20,463 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:25:20,463 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:25:20,463 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:25:20,463 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:25:20,463 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:25:20,463 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:20,464 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:25:20,464 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:25:20,465 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:25:20,465 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:25:20,648 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:25:20,656 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:25:20,658 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:25:20,659 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:25:20,659 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:25:20,660 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c60d308-1e91-410a-a8ed-5b67a1ef00ca/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/implicit_only_constructor_hierarchy.sol_4_no_adts_000.smt2
[2025-05-07 17:25:20,662 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:25:20,665 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:25:21,018 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c60d308-1e91-410a-a8ed-5b67a1ef00ca/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/implicit_only_constructor_hierarchy.sol_4_no_adts_000.smt2
[2025-05-07 17:25:21,020 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:25:21,021 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:25:21,021 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:25:21,021 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:25:21,021 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:25:21,024 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,087 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21 Unit
[2025-05-07 17:25:21,088 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:25:21,089 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:25:21,089 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:25:21,089 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:25:21,099 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,099 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,124 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,125 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,132 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,133 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,135 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,139 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,141 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,156 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:25:21,156 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:25:21,156 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:25:21,156 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:25:21,157 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (1/1) ...
[2025-05-07 17:25:21,159 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:21,168 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:21,177 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:25:21,179 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:25:21,186 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:25:21,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:25:21,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_13_0 given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_13_0
[2025-05-07 17:25:21,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_13_0
[2025-05-07 17:25:21,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_12_C_39_0 given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_12_C_39_0
[2025-05-07 17:25:21,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_12_C_39_0
[2025-05-07 17:25:21,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_f__38_39_0 given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_f__38_39_0
[2025-05-07 17:25:21,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_f__38_39_0
[2025-05-07 17:25:21,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_f__38_39_0 given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_f__38_39_0
[2025-05-07 17:25:21,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_f__38_39_0
[2025-05-07 17:25:21,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_59_return_function_f__38_39_0 given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure block_59_return_function_f__38_39_0
[2025-05-07 17:25:21,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_59_return_function_f__38_39_0
[2025-05-07 17:25:21,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_58_f_37_39_0 given in one single declaration
[2025-05-07 17:25:21,187 INFO  L130     BoogieDeclarations]: Found specification of procedure block_58_f_37_39_0
[2025-05-07 17:25:21,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_58_f_37_39_0
[2025-05-07 17:25:21,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_function_f__38_39_0 given in one single declaration
[2025-05-07 17:25:21,188 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_function_f__38_39_0
[2025-05-07 17:25:21,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_function_f__38_39_0
[2025-05-07 17:25:21,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_60_function_f__38_39_0 given in one single declaration
[2025-05-07 17:25:21,188 INFO  L130     BoogieDeclarations]: Found specification of procedure block_60_function_f__38_39_0
[2025-05-07 17:25:21,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_60_function_f__38_39_0
[2025-05-07 17:25:21,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_61_function_f__38_39_0 given in one single declaration
[2025-05-07 17:25:21,188 INFO  L130     BoogieDeclarations]: Found specification of procedure block_61_function_f__38_39_0
[2025-05-07 17:25:21,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_61_function_f__38_39_0
[2025-05-07 17:25:21,188 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_14_C_39_0 given in one single declaration
[2025-05-07 17:25:21,188 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_14_C_39_0
[2025-05-07 17:25:21,188 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_14_C_39_0
[2025-05-07 17:25:21,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_65_B_26_0 given in one single declaration
[2025-05-07 17:25:21,189 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_65_B_26_0
[2025-05-07 17:25:21,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_65_B_26_0
[2025-05-07 17:25:21,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_67_B_26_0 given in one single declaration
[2025-05-07 17:25:21,189 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_67_B_26_0
[2025-05-07 17:25:21,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_67_B_26_0
[2025-05-07 17:25:21,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_66_B_26_0 given in one single declaration
[2025-05-07 17:25:21,189 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_66_B_26_0
[2025-05-07 17:25:21,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_66_B_26_0
[2025-05-07 17:25:21,189 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_62_C_39_0 given in one single declaration
[2025-05-07 17:25:21,189 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_62_C_39_0
[2025-05-07 17:25:21,189 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_62_C_39_0
[2025-05-07 17:25:21,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_64_C_39_0 given in one single declaration
[2025-05-07 17:25:21,190 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_64_C_39_0
[2025-05-07 17:25:21,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_64_C_39_0
[2025-05-07 17:25:21,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_63_C_39_0 given in one single declaration
[2025-05-07 17:25:21,190 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_63_C_39_0
[2025-05-07 17:25:21,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_63_C_39_0
[2025-05-07 17:25:21,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_68_A_13_0 given in one single declaration
[2025-05-07 17:25:21,190 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_68_A_13_0
[2025-05-07 17:25:21,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_68_A_13_0
[2025-05-07 17:25:21,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_70_A_13_0 given in one single declaration
[2025-05-07 17:25:21,190 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_70_A_13_0
[2025-05-07 17:25:21,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_70_A_13_0
[2025-05-07 17:25:21,190 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_69_A_13_0 given in one single declaration
[2025-05-07 17:25:21,190 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_69_A_13_0
[2025-05-07 17:25:21,190 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_69_A_13_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_71_C_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_71_C_39_0
[2025-05-07 17:25:21,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_71_C_39_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_g__25_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_function_g__25_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_17_function_g__25_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_17_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_17_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_return_function_g__25_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_return_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_return_function_g__25_39_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_g_24_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_g_24_39_0
[2025-05-07 17:25:21,191 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_g_24_39_0
[2025-05-07 17:25:21,191 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_function_g__25_39_0 given in one single declaration
[2025-05-07 17:25:21,191 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_function_g__25_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_function_g__25_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_function_g__25_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_function_g__25_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_function_g__25_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_16_function_h__12_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_16_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_16_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_function_h__12_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_15_function_h__12_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_15_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_15_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_return_function_h__12_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_return_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_return_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_h_11_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_h_11_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_h_11_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_function_h__12_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_function_h__12_39_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_function_h__12_39_0
[2025-05-07 17:25:21,192 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_A_13_0 given in one single declaration
[2025-05-07 17:25:21,192 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_A_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_A_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_A_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_A_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_A_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_26_A_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_26_A_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_26_A_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_28_A_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_28_A_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_28_A_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_27_A_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_27_A_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_27_A_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_29_A_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_29_A_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_29_A_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_h__12_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_h__12_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_h__12_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_function_h__12_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_function_h__12_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_function_h__12_13_0
[2025-05-07 17:25:21,193 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_h__12_13_0 given in one single declaration
[2025-05-07 17:25:21,193 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_h__12_13_0
[2025-05-07 17:25:21,193 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_h__12_13_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_h_11_13_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_h_11_13_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_h_11_13_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_function_h__12_13_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_return_function_h__12_13_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_return_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_return_function_h__12_13_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_h__12_26_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_h__12_26_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_h__12_26_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_8_function_h__12_26_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_8_function_h__12_26_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_8_function_h__12_26_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_33_function_h__12_26_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure block_33_function_h__12_26_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_33_function_h__12_26_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_31_h_11_26_0 given in one single declaration
[2025-05-07 17:25:21,194 INFO  L130     BoogieDeclarations]: Found specification of procedure block_31_h_11_26_0
[2025-05-07 17:25:21,194 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_31_h_11_26_0
[2025-05-07 17:25:21,194 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_h__12_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_h__12_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_h__12_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_return_function_h__12_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_return_function_h__12_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_return_function_h__12_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_34_function_h__12_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure block_34_function_h__12_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_34_function_h__12_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_5_B_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_5_B_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_5_B_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_7_B_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_7_B_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_7_B_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_40_B_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_40_B_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_40_B_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_42_B_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_42_B_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_42_B_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_41_B_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_41_B_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_41_B_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_46_B_26_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_46_B_26_0
[2025-05-07 17:25:21,195 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_46_B_26_0
[2025-05-07 17:25:21,195 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_43_A_13_0 given in one single declaration
[2025-05-07 17:25:21,195 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_43_A_13_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_43_A_13_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_45_A_13_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_45_A_13_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_45_A_13_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_44_A_13_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_44_A_13_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_44_A_13_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_11_function_g__25_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_11_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_11_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_function_g__25_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_10_function_g__25_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_10_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_10_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_return_function_g__25_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36_g_24_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36_g_24_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36_g_24_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_function_g__25_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_function_g__25_26_0 given in one single declaration
[2025-05-07 17:25:21,196 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_function_g__25_26_0
[2025-05-07 17:25:21,196 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:25:21,197 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:25:21,197 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:25:21,474 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:25:21,476 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:25:21,902 INFO  L?                        ?]: Removed 624 outVars from TransFormulas that were not future-live.
[2025-05-07 17:25:21,902 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:25:21,915 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:25:21,915 INFO  L312             CfgBuilder]: Removed 37 assume(true) statements.
[2025-05-07 17:25:21,915 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:21 BoogieIcfgContainer
[2025-05-07 17:25:21,915 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:25:21,917 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:25:21,917 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:25:21,920 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:25:21,920 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:21" (1/3) ...
[2025-05-07 17:25:21,920 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5c1fc351 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:25:21, skipping insertion in model container
[2025-05-07 17:25:21,921 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:21" (2/3) ...
[2025-05-07 17:25:21,921 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5c1fc351 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:25:21, skipping insertion in model container
[2025-05-07 17:25:21,921 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:21" (3/3) ...
[2025-05-07 17:25:21,922 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:25:21,933 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:25:21,935 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 72 procedures, 282 locations, 434 edges, 72 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:25:21,968 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:25:21,977 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;@71d60870, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:25:21,977 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:25:21,980 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 282 states, 113 states have (on average 1.1327433628318584) internal successors, (128), 128 states have internal predecessors, (128), 96 states have call successors, (102), 71 states have call predecessors, (102), 71 states have return successors, (102), 82 states have call predecessors, (102), 96 states have call successors, (102)
[2025-05-07 17:25:21,990 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:25:21,990 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:21,991 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:21,991 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:21,995 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:21,995 INFO  L85        PathProgramCache]: Analyzing trace with hash 671394068, now seen corresponding path program 1 times
[2025-05-07 17:25:22,000 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,000 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1538702448]
[2025-05-07 17:25:22,001 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,001 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,044 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:25:22,061 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:25:22,061 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,062 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,231 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:25:22,231 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,231 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1538702448]
[2025-05-07 17:25:22,232 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1538702448] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,232 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,234 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:22,235 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [936822527]
[2025-05-07 17:25:22,235 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,239 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:22,239 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,271 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:22,271 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:22,273 INFO  L87              Difference]: Start difference. First operand  has 282 states, 113 states have (on average 1.1327433628318584) internal successors, (128), 128 states have internal predecessors, (128), 96 states have call successors, (102), 71 states have call predecessors, (102), 71 states have return successors, (102), 82 states have call predecessors, (102), 96 states have call successors, (102) Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:25:22,325 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,325 INFO  L93              Difference]: Finished difference Result 284 states and 335 transitions.
[2025-05-07 17:25:22,326 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:22,328 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:25:22,328 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,337 INFO  L225             Difference]: With dead ends: 284
[2025-05-07 17:25:22,337 INFO  L226             Difference]: Without dead ends: 277
[2025-05-07 17:25:22,338 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:25:22,341 INFO  L437           NwaCegarLoop]: 330 mSDtfsCounter, 1 mSDsluCounter, 649 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 979 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,341 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 979 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,352 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 277 states.
[2025-05-07 17:25:22,379 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 277 to 275.
[2025-05-07 17:25:22,380 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 275 states, 112 states have (on average 1.1071428571428572) internal successors, (124), 124 states have internal predecessors, (124), 91 states have call successors, (97), 71 states have call predecessors, (97), 71 states have return successors, (97), 79 states have call predecessors, (97), 91 states have call successors, (97)
[2025-05-07 17:25:22,384 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 275 states to 275 states and 318 transitions.
[2025-05-07 17:25:22,385 INFO  L79                 Accepts]: Start accepts. Automaton has 275 states and 318 transitions. Word has length 51
[2025-05-07 17:25:22,385 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,385 INFO  L485      AbstractCegarLoop]: Abstraction has 275 states and 318 transitions.
[2025-05-07 17:25:22,385 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:25:22,386 INFO  L278                IsEmpty]: Start isEmpty. Operand 275 states and 318 transitions.
[2025-05-07 17:25:22,388 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:25:22,388 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,388 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:22,388 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:25:22,388 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,389 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,389 INFO  L85        PathProgramCache]: Analyzing trace with hash 610567654, now seen corresponding path program 1 times
[2025-05-07 17:25:22,389 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,389 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1021668080]
[2025-05-07 17:25:22,389 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,389 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,415 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:25:22,437 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:25:22,437 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,437 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,536 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:25:22,537 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,537 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1021668080]
[2025-05-07 17:25:22,537 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1021668080] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,537 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,537 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:22,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1086852459]
[2025-05-07 17:25:22,537 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,538 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:22,538 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,538 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:22,538 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:22,539 INFO  L87              Difference]: Start difference. First operand 275 states and 318 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:25:22,566 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,566 INFO  L93              Difference]: Finished difference Result 279 states and 324 transitions.
[2025-05-07 17:25:22,567 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:22,567 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:25:22,567 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,570 INFO  L225             Difference]: With dead ends: 279
[2025-05-07 17:25:22,570 INFO  L226             Difference]: Without dead ends: 268
[2025-05-07 17:25:22,570 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:25:22,571 INFO  L437           NwaCegarLoop]: 318 mSDtfsCounter, 1 mSDsluCounter, 620 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 938 SdHoareTripleChecker+Invalid, 4 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:22,571 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 938 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,572 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 268 states.
[2025-05-07 17:25:22,586 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 268 to 266.
[2025-05-07 17:25:22,587 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 266 states, 112 states have (on average 1.0803571428571428) internal successors, (121), 121 states have internal predecessors, (121), 82 states have call successors, (88), 71 states have call predecessors, (88), 71 states have return successors, (88), 73 states have call predecessors, (88), 82 states have call successors, (88)
[2025-05-07 17:25:22,589 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 266 states to 266 states and 297 transitions.
[2025-05-07 17:25:22,590 INFO  L79                 Accepts]: Start accepts. Automaton has 266 states and 297 transitions. Word has length 51
[2025-05-07 17:25:22,591 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,591 INFO  L485      AbstractCegarLoop]: Abstraction has 266 states and 297 transitions.
[2025-05-07 17:25:22,591 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:25:22,591 INFO  L278                IsEmpty]: Start isEmpty. Operand 266 states and 297 transitions.
[2025-05-07 17:25:22,593 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:25:22,593 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:22,594 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:25:22,594 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,594 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,594 INFO  L85        PathProgramCache]: Analyzing trace with hash 207376137, now seen corresponding path program 1 times
[2025-05-07 17:25:22,594 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,594 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [505776114]
[2025-05-07 17:25:22,594 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,594 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,618 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:25:22,627 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:25:22,628 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,628 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:22,716 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:25:22,716 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:22,716 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [505776114]
[2025-05-07 17:25:22,716 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [505776114] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:22,716 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:22,716 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:22,716 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1200470856]
[2025-05-07 17:25:22,716 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:22,717 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:22,717 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:22,717 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:22,717 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:22,717 INFO  L87              Difference]: Start difference. First operand 266 states and 297 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:25:22,735 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:22,736 INFO  L93              Difference]: Finished difference Result 270 states and 301 transitions.
[2025-05-07 17:25:22,736 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:22,736 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:25:22,736 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:22,738 INFO  L225             Difference]: With dead ends: 270
[2025-05-07 17:25:22,739 INFO  L226             Difference]: Without dead ends: 266
[2025-05-07 17:25:22,739 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:25:22,739 INFO  L437           NwaCegarLoop]: 298 mSDtfsCounter, 1 mSDsluCounter, 588 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 886 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:25:22,740 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 886 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:22,741 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 266 states.
[2025-05-07 17:25:22,750 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 266 to 264.
[2025-05-07 17:25:22,751 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 264 states, 112 states have (on average 1.0714285714285714) internal successors, (120), 120 states have internal predecessors, (120), 80 states have call successors, (86), 71 states have call predecessors, (86), 71 states have return successors, (86), 72 states have call predecessors, (86), 80 states have call successors, (86)
[2025-05-07 17:25:22,753 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 264 states to 264 states and 292 transitions.
[2025-05-07 17:25:22,753 INFO  L79                 Accepts]: Start accepts. Automaton has 264 states and 292 transitions. Word has length 51
[2025-05-07 17:25:22,753 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:22,753 INFO  L485      AbstractCegarLoop]: Abstraction has 264 states and 292 transitions.
[2025-05-07 17:25:22,753 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:25:22,754 INFO  L278                IsEmpty]: Start isEmpty. Operand 264 states and 292 transitions.
[2025-05-07 17:25:22,755 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:25:22,755 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:22,755 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:22,755 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:25:22,755 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:22,756 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:22,756 INFO  L85        PathProgramCache]: Analyzing trace with hash 1295583629, now seen corresponding path program 1 times
[2025-05-07 17:25:22,756 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:22,756 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [344746325]
[2025-05-07 17:25:22,756 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:22,756 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:22,775 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:25:22,785 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:25:22,785 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:22,785 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,094 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:25:23,094 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,094 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [344746325]
[2025-05-07 17:25:23,094 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [344746325] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,094 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,094 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [] total 16
[2025-05-07 17:25:23,094 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2123207808]
[2025-05-07 17:25:23,094 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,095 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-05-07 17:25:23,095 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,095 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-05-07 17:25:23,096 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=211, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:25:23,096 INFO  L87              Difference]: Start difference. First operand 264 states and 292 transitions. Second operand  has 16 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 14 states have internal predecessors, (23), 7 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14)
[2025-05-07 17:25:23,329 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,330 INFO  L93              Difference]: Finished difference Result 274 states and 306 transitions.
[2025-05-07 17:25:23,330 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-05-07 17:25:23,330 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 14 states have internal predecessors, (23), 7 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14) Word has length 51
[2025-05-07 17:25:23,331 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,332 INFO  L225             Difference]: With dead ends: 274
[2025-05-07 17:25:23,332 INFO  L226             Difference]: Without dead ends: 274
[2025-05-07 17:25:23,333 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-05-07 17:25:23,333 INFO  L437           NwaCegarLoop]: 285 mSDtfsCounter, 5 mSDsluCounter, 3950 mSDsCounter, 0 mSdLazyCounter, 218 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 4235 SdHoareTripleChecker+Invalid, 219 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 218 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,334 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 4235 Invalid, 219 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 218 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:25:23,334 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 274 states.
[2025-05-07 17:25:23,345 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 274 to 272.
[2025-05-07 17:25:23,346 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 272 states, 115 states have (on average 1.0695652173913044) internal successors, (123), 123 states have internal predecessors, (123), 82 states have call successors, (88), 71 states have call predecessors, (88), 74 states have return successors, (93), 77 states have call predecessors, (93), 82 states have call successors, (93)
[2025-05-07 17:25:23,347 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 272 states to 272 states and 304 transitions.
[2025-05-07 17:25:23,348 INFO  L79                 Accepts]: Start accepts. Automaton has 272 states and 304 transitions. Word has length 51
[2025-05-07 17:25:23,348 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,348 INFO  L485      AbstractCegarLoop]: Abstraction has 272 states and 304 transitions.
[2025-05-07 17:25:23,348 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 14 states have internal predecessors, (23), 7 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (14), 11 states have call predecessors, (14), 7 states have call successors, (14)
[2025-05-07 17:25:23,348 INFO  L278                IsEmpty]: Start isEmpty. Operand 272 states and 304 transitions.
[2025-05-07 17:25:23,350 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:25:23,350 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,350 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:23,350 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:25:23,350 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,351 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,351 INFO  L85        PathProgramCache]: Analyzing trace with hash 1277321195, now seen corresponding path program 1 times
[2025-05-07 17:25:23,351 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,351 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1793834835]
[2025-05-07 17:25:23,351 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,351 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,373 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:25:23,385 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:25:23,386 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,386 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,495 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:25:23,495 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,495 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1793834835]
[2025-05-07 17:25:23,495 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1793834835] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,495 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,495 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:25:23,496 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1724705540]
[2025-05-07 17:25:23,496 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,496 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:25:23,496 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,497 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:25:23,497 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:23,497 INFO  L87              Difference]: Start difference. First operand 272 states and 304 transitions. Second operand  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 6 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 6 states have call predecessors, (14), 6 states have call successors, (14)
[2025-05-07 17:25:23,560 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,560 INFO  L93              Difference]: Finished difference Result 271 states and 300 transitions.
[2025-05-07 17:25:23,561 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:25:23,561 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 6 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 6 states have call predecessors, (14), 6 states have call successors, (14) Word has length 51
[2025-05-07 17:25:23,561 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,562 INFO  L225             Difference]: With dead ends: 271
[2025-05-07 17:25:23,563 INFO  L226             Difference]: Without dead ends: 271
[2025-05-07 17:25:23,563 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:25:23,563 INFO  L437           NwaCegarLoop]: 288 mSDtfsCounter, 2 mSDsluCounter, 1705 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1993 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,564 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1993 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:23,564 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 271 states.
[2025-05-07 17:25:23,571 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 271 to 271.
[2025-05-07 17:25:23,571 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 271 states, 115 states have (on average 1.0695652173913044) internal successors, (123), 123 states have internal predecessors, (123), 81 states have call successors, (87), 71 states have call predecessors, (87), 74 states have return successors, (90), 76 states have call predecessors, (90), 81 states have call successors, (90)
[2025-05-07 17:25:23,573 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 271 states to 271 states and 300 transitions.
[2025-05-07 17:25:23,573 INFO  L79                 Accepts]: Start accepts. Automaton has 271 states and 300 transitions. Word has length 51
[2025-05-07 17:25:23,573 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,573 INFO  L485      AbstractCegarLoop]: Abstraction has 271 states and 300 transitions.
[2025-05-07 17:25:23,573 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 6 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 6 states have call predecessors, (14), 6 states have call successors, (14)
[2025-05-07 17:25:23,574 INFO  L278                IsEmpty]: Start isEmpty. Operand 271 states and 300 transitions.
[2025-05-07 17:25:23,575 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:25:23,575 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,575 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:23,575 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:25:23,576 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,576 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,576 INFO  L85        PathProgramCache]: Analyzing trace with hash 1122267868, now seen corresponding path program 1 times
[2025-05-07 17:25:23,576 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,576 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1209494115]
[2025-05-07 17:25:23,576 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,576 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,600 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:25:23,606 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:25:23,606 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,606 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:23,688 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:25:23,688 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:23,688 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1209494115]
[2025-05-07 17:25:23,688 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1209494115] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:23,688 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:23,688 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:23,689 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1106741331]
[2025-05-07 17:25:23,689 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:23,689 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:23,689 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:23,689 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:23,690 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:23,690 INFO  L87              Difference]: Start difference. First operand 271 states and 300 transitions. Second operand  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (20), 5 states have call predecessors, (20), 5 states have call successors, (20)
[2025-05-07 17:25:23,723 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:23,723 INFO  L93              Difference]: Finished difference Result 271 states and 299 transitions.
[2025-05-07 17:25:23,724 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:23,724 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (20), 5 states have call predecessors, (20), 5 states have call successors, (20) Word has length 76
[2025-05-07 17:25:23,724 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:23,725 INFO  L225             Difference]: With dead ends: 271
[2025-05-07 17:25:23,725 INFO  L226             Difference]: Without dead ends: 271
[2025-05-07 17:25:23,725 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:23,726 INFO  L437           NwaCegarLoop]: 291 mSDtfsCounter, 1 mSDsluCounter, 1152 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1443 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:23,726 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1443 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:23,727 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 271 states.
[2025-05-07 17:25:23,733 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 271 to 271.
[2025-05-07 17:25:23,733 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 271 states, 115 states have (on average 1.0695652173913044) internal successors, (123), 123 states have internal predecessors, (123), 81 states have call successors, (87), 71 states have call predecessors, (87), 74 states have return successors, (89), 76 states have call predecessors, (89), 81 states have call successors, (89)
[2025-05-07 17:25:23,734 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 271 states to 271 states and 299 transitions.
[2025-05-07 17:25:23,734 INFO  L79                 Accepts]: Start accepts. Automaton has 271 states and 299 transitions. Word has length 76
[2025-05-07 17:25:23,735 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:23,735 INFO  L485      AbstractCegarLoop]: Abstraction has 271 states and 299 transitions.
[2025-05-07 17:25:23,735 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.8) internal successors, (29), 6 states have internal predecessors, (29), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (20), 5 states have call predecessors, (20), 5 states have call successors, (20)
[2025-05-07 17:25:23,735 INFO  L278                IsEmpty]: Start isEmpty. Operand 271 states and 299 transitions.
[2025-05-07 17:25:23,736 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:25:23,736 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:23,736 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:23,736 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:25:23,736 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:23,736 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:23,736 INFO  L85        PathProgramCache]: Analyzing trace with hash 751937978, now seen corresponding path program 1 times
[2025-05-07 17:25:23,736 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:23,736 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [451678024]
[2025-05-07 17:25:23,737 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:23,737 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:23,764 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:25:23,774 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:25:23,775 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:23,775 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:24,221 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:25:24,221 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:24,221 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [451678024]
[2025-05-07 17:25:24,221 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [451678024] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:24,221 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [11870690]
[2025-05-07 17:25:24,222 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:24,222 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:24,223 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:24,225 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:24,226 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:25:24,573 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:25:24,679 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:25:24,679 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:24,679 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:24,685 INFO  L256         TraceCheckSpWp]: Trace formula consists of 987 conjuncts, 64 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:24,695 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:24,791 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:25:24,791 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:25:26,114 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 3 proven. 6 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:25:26,114 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [11870690] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:25:26,114 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:25:26,114 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [20, 20, 22] total 33
[2025-05-07 17:25:26,114 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [500292450]
[2025-05-07 17:25:26,114 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:25:26,114 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-05-07 17:25:26,114 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:26,115 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-05-07 17:25:26,115 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=86, Invalid=970, Unknown=0, NotChecked=0, Total=1056
[2025-05-07 17:25:26,116 INFO  L87              Difference]: Start difference. First operand 271 states and 299 transitions. Second operand  has 33 states, 23 states have (on average 1.826086956521739) internal successors, (42), 28 states have internal predecessors, (42), 17 states have call successors, (27), 1 states have call predecessors, (27), 23 states have return successors, (34), 24 states have call predecessors, (34), 17 states have call successors, (34)
[2025-05-07 17:25:26,388 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:26,389 INFO  L93              Difference]: Finished difference Result 271 states and 298 transitions.
[2025-05-07 17:25:26,389 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-05-07 17:25:26,389 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 23 states have (on average 1.826086956521739) internal successors, (42), 28 states have internal predecessors, (42), 17 states have call successors, (27), 1 states have call predecessors, (27), 23 states have return successors, (34), 24 states have call predecessors, (34), 17 states have call successors, (34) Word has length 76
[2025-05-07 17:25:26,390 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:26,390 INFO  L225             Difference]: With dead ends: 271
[2025-05-07 17:25:26,390 INFO  L226             Difference]: Without dead ends: 215
[2025-05-07 17:25:26,391 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 179 GetRequests, 143 SyntacticMatches, 0 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 91 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=115, Invalid=1291, Unknown=0, NotChecked=0, Total=1406
[2025-05-07 17:25:26,391 INFO  L437           NwaCegarLoop]: 283 mSDtfsCounter, 6 mSDsluCounter, 5858 mSDsCounter, 0 mSdLazyCounter, 363 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 6141 SdHoareTripleChecker+Invalid, 367 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 363 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:26,391 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 6141 Invalid, 367 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 363 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:25:26,392 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 215 states.
[2025-05-07 17:25:26,395 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 215 to 215.
[2025-05-07 17:25:26,395 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 215 states, 91 states have (on average 1.065934065934066) internal successors, (97), 97 states have internal predecessors, (97), 65 states have call successors, (70), 58 states have call predecessors, (70), 58 states have return successors, (70), 59 states have call predecessors, (70), 65 states have call successors, (70)
[2025-05-07 17:25:26,396 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 215 states to 215 states and 237 transitions.
[2025-05-07 17:25:26,397 INFO  L79                 Accepts]: Start accepts. Automaton has 215 states and 237 transitions. Word has length 76
[2025-05-07 17:25:26,397 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:26,397 INFO  L485      AbstractCegarLoop]: Abstraction has 215 states and 237 transitions.
[2025-05-07 17:25:26,397 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 23 states have (on average 1.826086956521739) internal successors, (42), 28 states have internal predecessors, (42), 17 states have call successors, (27), 1 states have call predecessors, (27), 23 states have return successors, (34), 24 states have call predecessors, (34), 17 states have call successors, (34)
[2025-05-07 17:25:26,397 INFO  L278                IsEmpty]: Start isEmpty. Operand 215 states and 237 transitions.
[2025-05-07 17:25:26,398 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 62
[2025-05-07 17:25:26,398 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:26,398 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:26,405 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:25:26,599 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-05-07 17:25:26,599 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:26,599 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:26,599 INFO  L85        PathProgramCache]: Analyzing trace with hash 450582390, now seen corresponding path program 1 times
[2025-05-07 17:25:26,599 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:26,599 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1418148074]
[2025-05-07 17:25:26,600 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:26,600 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:26,623 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-05-07 17:25:26,631 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-05-07 17:25:26,632 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:26,632 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:26,714 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:25:26,714 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:26,714 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1418148074]
[2025-05-07 17:25:26,714 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1418148074] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:26,714 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:26,715 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:25:26,715 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1800458478]
[2025-05-07 17:25:26,715 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:26,715 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:25:26,715 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:26,716 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:25:26,716 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:26,716 INFO  L87              Difference]: Start difference. First operand 215 states and 237 transitions. Second operand  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 4 states have call successors, (17), 1 states have call predecessors, (17), 6 states have return successors, (17), 7 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:25:26,768 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:26,768 INFO  L93              Difference]: Finished difference Result 219 states and 241 transitions.
[2025-05-07 17:25:26,769 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:25:26,769 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 4 states have call successors, (17), 1 states have call predecessors, (17), 6 states have return successors, (17), 7 states have call predecessors, (17), 4 states have call successors, (17) Word has length 61
[2025-05-07 17:25:26,769 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:26,770 INFO  L225             Difference]: With dead ends: 219
[2025-05-07 17:25:26,770 INFO  L226             Difference]: Without dead ends: 219
[2025-05-07 17:25:26,771 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:25:26,771 INFO  L437           NwaCegarLoop]: 235 mSDtfsCounter, 2 mSDsluCounter, 1387 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1622 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:26,771 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1622 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:26,772 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 219 states.
[2025-05-07 17:25:26,778 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 219 to 219.
[2025-05-07 17:25:26,778 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 219 states, 93 states have (on average 1.064516129032258) internal successors, (99), 99 states have internal predecessors, (99), 65 states have call successors, (70), 58 states have call predecessors, (70), 60 states have return successors, (72), 61 states have call predecessors, (72), 65 states have call successors, (72)
[2025-05-07 17:25:26,780 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 219 states to 219 states and 241 transitions.
[2025-05-07 17:25:26,780 INFO  L79                 Accepts]: Start accepts. Automaton has 219 states and 241 transitions. Word has length 61
[2025-05-07 17:25:26,780 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:26,780 INFO  L485      AbstractCegarLoop]: Abstraction has 219 states and 241 transitions.
[2025-05-07 17:25:26,780 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 4 states have call successors, (17), 1 states have call predecessors, (17), 6 states have return successors, (17), 7 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:25:26,780 INFO  L278                IsEmpty]: Start isEmpty. Operand 219 states and 241 transitions.
[2025-05-07 17:25:26,781 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 62
[2025-05-07 17:25:26,782 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:26,782 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:26,782 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:25:26,782 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:26,782 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:26,782 INFO  L85        PathProgramCache]: Analyzing trace with hash 590943484, now seen corresponding path program 1 times
[2025-05-07 17:25:26,782 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:26,782 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2002692556]
[2025-05-07 17:25:26,782 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:26,783 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:26,806 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-05-07 17:25:26,813 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-05-07 17:25:26,814 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:26,814 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:27,131 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:25:27,132 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:27,132 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2002692556]
[2025-05-07 17:25:27,132 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2002692556] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:27,132 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:27,132 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [20] imperfect sequences [] total 20
[2025-05-07 17:25:27,132 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1823629119]
[2025-05-07 17:25:27,132 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:27,132 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-05-07 17:25:27,132 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:27,133 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-05-07 17:25:27,133 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=343, Unknown=0, NotChecked=0, Total=380
[2025-05-07 17:25:27,133 INFO  L87              Difference]: Start difference. First operand 219 states and 241 transitions. Second operand  has 20 states, 15 states have (on average 1.8) internal successors, (27), 17 states have internal predecessors, (27), 7 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (17), 15 states have call predecessors, (17), 7 states have call successors, (17)
[2025-05-07 17:25:27,426 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:27,426 INFO  L93              Difference]: Finished difference Result 222 states and 246 transitions.
[2025-05-07 17:25:27,426 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-05-07 17:25:27,427 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 15 states have (on average 1.8) internal successors, (27), 17 states have internal predecessors, (27), 7 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (17), 15 states have call predecessors, (17), 7 states have call successors, (17) Word has length 61
[2025-05-07 17:25:27,427 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:27,428 INFO  L225             Difference]: With dead ends: 222
[2025-05-07 17:25:27,428 INFO  L226             Difference]: Without dead ends: 221
[2025-05-07 17:25:27,429 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 24 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=55, Invalid=497, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:25:27,429 INFO  L437           NwaCegarLoop]: 220 mSDtfsCounter, 5 mSDsluCounter, 3917 mSDsCounter, 0 mSdLazyCounter, 348 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 4137 SdHoareTripleChecker+Invalid, 350 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 348 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:27,429 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 4137 Invalid, 350 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 348 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:25:27,430 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 221 states.
[2025-05-07 17:25:27,436 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 221 to 221.
[2025-05-07 17:25:27,436 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 221 states, 94 states have (on average 1.0638297872340425) internal successors, (100), 100 states have internal predecessors, (100), 65 states have call successors, (70), 58 states have call predecessors, (70), 61 states have return successors, (74), 62 states have call predecessors, (74), 65 states have call successors, (74)
[2025-05-07 17:25:27,437 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 221 states to 221 states and 244 transitions.
[2025-05-07 17:25:27,437 INFO  L79                 Accepts]: Start accepts. Automaton has 221 states and 244 transitions. Word has length 61
[2025-05-07 17:25:27,438 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:27,438 INFO  L485      AbstractCegarLoop]: Abstraction has 221 states and 244 transitions.
[2025-05-07 17:25:27,438 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 15 states have (on average 1.8) internal successors, (27), 17 states have internal predecessors, (27), 7 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (17), 15 states have call predecessors, (17), 7 states have call successors, (17)
[2025-05-07 17:25:27,438 INFO  L278                IsEmpty]: Start isEmpty. Operand 221 states and 244 transitions.
[2025-05-07 17:25:27,439 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:25:27,439 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:27,439 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:27,439 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:25:27,439 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:27,440 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:27,440 INFO  L85        PathProgramCache]: Analyzing trace with hash -572901632, now seen corresponding path program 1 times
[2025-05-07 17:25:27,440 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:27,440 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2112062704]
[2025-05-07 17:25:27,440 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:27,440 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:27,466 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:25:27,474 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:25:27,475 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:27,475 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:27,956 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-05-07 17:25:27,957 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:27,957 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2112062704]
[2025-05-07 17:25:27,957 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2112062704] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:27,957 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1404668710]
[2025-05-07 17:25:27,957 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:27,957 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:27,959 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:27,961 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:27,962 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:25:28,236 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:25:28,320 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:25:28,321 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:28,321 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:28,324 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1132 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:28,326 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:28,420 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-05-07 17:25:28,421 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:28,421 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1404668710] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:28,421 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:28,421 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [24] total 28
[2025-05-07 17:25:28,421 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1240906622]
[2025-05-07 17:25:28,421 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:28,421 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:28,421 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:28,422 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:28,422 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=703, Unknown=0, NotChecked=0, Total=756
[2025-05-07 17:25:28,422 INFO  L87              Difference]: Start difference. First operand 221 states and 244 transitions. Second operand  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 3 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (22), 6 states have call predecessors, (22), 3 states have call successors, (22)
[2025-05-07 17:25:28,452 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:28,452 INFO  L93              Difference]: Finished difference Result 221 states and 243 transitions.
[2025-05-07 17:25:28,452 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:28,453 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 3 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (22), 6 states have call predecessors, (22), 3 states have call successors, (22) Word has length 86
[2025-05-07 17:25:28,453 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:28,453 INFO  L225             Difference]: With dead ends: 221
[2025-05-07 17:25:28,453 INFO  L226             Difference]: Without dead ends: 130
[2025-05-07 17:25:28,454 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 112 GetRequests, 86 SyntacticMatches, 0 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=53, Invalid=703, Unknown=0, NotChecked=0, Total=756
[2025-05-07 17:25:28,454 INFO  L437           NwaCegarLoop]: 233 mSDtfsCounter, 1 mSDsluCounter, 920 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1153 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:28,454 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1153 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:28,454 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-05-07 17:25:28,457 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 130.
[2025-05-07 17:25:28,457 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 55 states have (on average 1.0545454545454545) internal successors, (58), 58 states have internal predecessors, (58), 39 states have call successors, (42), 35 states have call predecessors, (42), 35 states have return successors, (42), 36 states have call predecessors, (42), 39 states have call successors, (42)
[2025-05-07 17:25:28,458 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 142 transitions.
[2025-05-07 17:25:28,458 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 142 transitions. Word has length 86
[2025-05-07 17:25:28,458 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:28,458 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 142 transitions.
[2025-05-07 17:25:28,458 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.4) internal successors, (32), 6 states have internal predecessors, (32), 3 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (22), 6 states have call predecessors, (22), 3 states have call successors, (22)
[2025-05-07 17:25:28,458 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 142 transitions.
[2025-05-07 17:25:28,458 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 72
[2025-05-07 17:25:28,459 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:28,459 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, 1, 1, 1, 1, 1, 1, 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:25:28,466 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:25:28,659 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:28,660 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:28,661 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:28,661 INFO  L85        PathProgramCache]: Analyzing trace with hash 355656228, now seen corresponding path program 1 times
[2025-05-07 17:25:28,661 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:28,661 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1796492837]
[2025-05-07 17:25:28,661 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:28,662 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:28,739 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 71 statements into 1 equivalence classes.
[2025-05-07 17:25:28,745 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 71 of 71 statements.
[2025-05-07 17:25:28,745 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:28,745 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:28,838 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:25:28,839 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:28,839 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1796492837]
[2025-05-07 17:25:28,839 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1796492837] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:28,839 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:28,839 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:25:28,839 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1240723159]
[2025-05-07 17:25:28,839 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:28,839 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:25:28,839 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:28,840 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:25:28,840 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:25:28,840 INFO  L87              Difference]: Start difference. First operand 130 states and 142 transitions. Second operand  has 8 states, 6 states have (on average 5.166666666666667) internal successors, (31), 8 states have internal predecessors, (31), 6 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 6 states have call successors, (20)
[2025-05-07 17:25:28,889 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:28,889 INFO  L93              Difference]: Finished difference Result 135 states and 148 transitions.
[2025-05-07 17:25:28,889 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:25:28,889 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 5.166666666666667) internal successors, (31), 8 states have internal predecessors, (31), 6 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 6 states have call successors, (20) Word has length 71
[2025-05-07 17:25:28,889 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:28,890 INFO  L225             Difference]: With dead ends: 135
[2025-05-07 17:25:28,890 INFO  L226             Difference]: Without dead ends: 135
[2025-05-07 17:25:28,890 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-05-07 17:25:28,890 INFO  L437           NwaCegarLoop]: 139 mSDtfsCounter, 2 mSDsluCounter, 815 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 954 SdHoareTripleChecker+Invalid, 39 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:28,890 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 954 Invalid, 39 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:28,891 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 135 states.
[2025-05-07 17:25:28,894 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 135 to 135.
[2025-05-07 17:25:28,894 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 135 states, 57 states have (on average 1.0526315789473684) internal successors, (60), 60 states have internal predecessors, (60), 40 states have call successors, (43), 35 states have call predecessors, (43), 37 states have return successors, (45), 39 states have call predecessors, (45), 40 states have call successors, (45)
[2025-05-07 17:25:28,895 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 135 states to 135 states and 148 transitions.
[2025-05-07 17:25:28,895 INFO  L79                 Accepts]: Start accepts. Automaton has 135 states and 148 transitions. Word has length 71
[2025-05-07 17:25:28,896 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:28,896 INFO  L485      AbstractCegarLoop]: Abstraction has 135 states and 148 transitions.
[2025-05-07 17:25:28,896 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 5.166666666666667) internal successors, (31), 8 states have internal predecessors, (31), 6 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 6 states have call predecessors, (20), 6 states have call successors, (20)
[2025-05-07 17:25:28,896 INFO  L278                IsEmpty]: Start isEmpty. Operand 135 states and 148 transitions.
[2025-05-07 17:25:28,897 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 72
[2025-05-07 17:25:28,897 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:28,897 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:28,897 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:25:28,897 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:28,897 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:28,897 INFO  L85        PathProgramCache]: Analyzing trace with hash -63200152, now seen corresponding path program 1 times
[2025-05-07 17:25:28,897 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:28,897 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1374617575]
[2025-05-07 17:25:28,898 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:28,898 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:28,921 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 71 statements into 1 equivalence classes.
[2025-05-07 17:25:28,926 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 71 of 71 statements.
[2025-05-07 17:25:28,927 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:28,927 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:29,327 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:25:29,327 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:29,328 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1374617575]
[2025-05-07 17:25:29,328 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1374617575] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:29,328 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:29,328 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [24] imperfect sequences [] total 24
[2025-05-07 17:25:29,328 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [972777674]
[2025-05-07 17:25:29,328 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:29,328 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-05-07 17:25:29,328 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:29,329 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-05-07 17:25:29,329 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=506, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:25:29,329 INFO  L87              Difference]: Start difference. First operand 135 states and 148 transitions. Second operand  has 24 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 20 states have internal predecessors, (31), 9 states have call successors, (20), 1 states have call predecessors, (20), 18 states have return successors, (20), 17 states have call predecessors, (20), 9 states have call successors, (20)
[2025-05-07 17:25:29,648 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:29,648 INFO  L93              Difference]: Finished difference Result 137 states and 152 transitions.
[2025-05-07 17:25:29,648 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-05-07 17:25:29,649 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 20 states have internal predecessors, (31), 9 states have call successors, (20), 1 states have call predecessors, (20), 18 states have return successors, (20), 17 states have call predecessors, (20), 9 states have call successors, (20) Word has length 71
[2025-05-07 17:25:29,649 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:29,650 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:25:29,650 INFO  L226             Difference]: Without dead ends: 137
[2025-05-07 17:25:29,650 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 29 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 14 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=72, Invalid=740, Unknown=0, NotChecked=0, Total=812
[2025-05-07 17:25:29,650 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 5 mSDsluCounter, 2666 mSDsCounter, 0 mSdLazyCounter, 467 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 2790 SdHoareTripleChecker+Invalid, 470 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 467 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:29,651 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 2790 Invalid, 470 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 467 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:25:29,651 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-05-07 17:25:29,654 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 137.
[2025-05-07 17:25:29,655 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 58 states have (on average 1.0517241379310345) internal successors, (61), 61 states have internal predecessors, (61), 40 states have call successors, (43), 35 states have call predecessors, (43), 38 states have return successors, (48), 40 states have call predecessors, (48), 40 states have call successors, (48)
[2025-05-07 17:25:29,655 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 152 transitions.
[2025-05-07 17:25:29,656 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 152 transitions. Word has length 71
[2025-05-07 17:25:29,656 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:29,656 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 152 transitions.
[2025-05-07 17:25:29,656 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 20 states have internal predecessors, (31), 9 states have call successors, (20), 1 states have call predecessors, (20), 18 states have return successors, (20), 17 states have call predecessors, (20), 9 states have call successors, (20)
[2025-05-07 17:25:29,656 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 152 transitions.
[2025-05-07 17:25:29,657 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:25:29,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:29,657 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:29,657 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:25:29,657 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:29,658 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:29,658 INFO  L85        PathProgramCache]: Analyzing trace with hash -284538677, now seen corresponding path program 1 times
[2025-05-07 17:25:29,658 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:29,658 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [695397055]
[2025-05-07 17:25:29,658 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:29,658 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:29,690 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:25:29,694 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:25:29,694 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:29,694 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:29,772 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:29,772 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:29,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [695397055]
[2025-05-07 17:25:29,772 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [695397055] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:29,772 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:29,772 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:29,772 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [794443012]
[2025-05-07 17:25:29,772 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:29,773 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:29,773 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:29,773 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:29,773 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:29,774 INFO  L87              Difference]: Start difference. First operand 137 states and 152 transitions. Second operand  has 6 states, 5 states have (on average 8.4) internal successors, (42), 6 states have internal predecessors, (42), 5 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 5 states have call predecessors, (27), 5 states have call successors, (27)
[2025-05-07 17:25:29,792 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:29,792 INFO  L93              Difference]: Finished difference Result 142 states and 157 transitions.
[2025-05-07 17:25:29,793 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:29,793 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.4) internal successors, (42), 6 states have internal predecessors, (42), 5 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 5 states have call predecessors, (27), 5 states have call successors, (27) Word has length 96
[2025-05-07 17:25:29,793 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:29,793 INFO  L225             Difference]: With dead ends: 142
[2025-05-07 17:25:29,793 INFO  L226             Difference]: Without dead ends: 133
[2025-05-07 17:25:29,794 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:29,794 INFO  L437           NwaCegarLoop]: 147 mSDtfsCounter, 1 mSDsluCounter, 567 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 714 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:29,794 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 714 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:29,794 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-05-07 17:25:29,796 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 133.
[2025-05-07 17:25:29,796 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 56 states have (on average 1.0535714285714286) internal successors, (59), 59 states have internal predecessors, (59), 39 states have call successors, (41), 34 states have call predecessors, (41), 37 states have return successors, (46), 39 states have call predecessors, (46), 39 states have call successors, (46)
[2025-05-07 17:25:29,797 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 146 transitions.
[2025-05-07 17:25:29,797 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 146 transitions. Word has length 96
[2025-05-07 17:25:29,797 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:29,797 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 146 transitions.
[2025-05-07 17:25:29,797 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.4) internal successors, (42), 6 states have internal predecessors, (42), 5 states have call successors, (27), 1 states have call predecessors, (27), 5 states have return successors, (27), 5 states have call predecessors, (27), 5 states have call successors, (27)
[2025-05-07 17:25:29,797 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 146 transitions.
[2025-05-07 17:25:29,798 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:25:29,798 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:29,798 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:29,798 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:25:29,798 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:29,798 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:29,798 INFO  L85        PathProgramCache]: Analyzing trace with hash -1902139771, now seen corresponding path program 1 times
[2025-05-07 17:25:29,798 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:29,798 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1088603287]
[2025-05-07 17:25:29,798 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:29,798 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:29,824 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:25:29,831 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:25:29,831 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:29,831 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:30,412 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:30,412 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:30,413 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1088603287]
[2025-05-07 17:25:30,413 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1088603287] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:30,413 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:30,413 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [30] imperfect sequences [] total 30
[2025-05-07 17:25:30,413 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1144531764]
[2025-05-07 17:25:30,413 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:30,413 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-05-07 17:25:30,413 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:30,413 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-05-07 17:25:30,413 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=812, Unknown=0, NotChecked=0, Total=870
[2025-05-07 17:25:30,414 INFO  L87              Difference]: Start difference. First operand 133 states and 146 transitions. Second operand  has 30 states, 22 states have (on average 1.8636363636363635) internal successors, (41), 25 states have internal predecessors, (41), 13 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 22 states have call predecessors, (27), 13 states have call successors, (27)
[2025-05-07 17:25:30,887 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:30,887 INFO  L93              Difference]: Finished difference Result 137 states and 155 transitions.
[2025-05-07 17:25:30,888 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 31 states. 
[2025-05-07 17:25:30,888 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 22 states have (on average 1.8636363636363635) internal successors, (41), 25 states have internal predecessors, (41), 13 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 22 states have call predecessors, (27), 13 states have call successors, (27) Word has length 96
[2025-05-07 17:25:30,888 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:30,889 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:25:30,889 INFO  L226             Difference]: Without dead ends: 137
[2025-05-07 17:25:30,889 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 35 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 27 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=92, Invalid=1240, Unknown=0, NotChecked=0, Total=1332
[2025-05-07 17:25:30,890 INFO  L437           NwaCegarLoop]: 118 mSDtfsCounter, 8 mSDsluCounter, 3191 mSDsCounter, 0 mSdLazyCounter, 906 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 3309 SdHoareTripleChecker+Invalid, 910 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 906 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:30,890 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 3309 Invalid, 910 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 906 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:25:30,890 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-05-07 17:25:30,892 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 133.
[2025-05-07 17:25:30,892 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 56 states have (on average 1.0535714285714286) internal successors, (59), 59 states have internal predecessors, (59), 39 states have call successors, (41), 34 states have call predecessors, (41), 37 states have return successors, (46), 39 states have call predecessors, (46), 39 states have call successors, (46)
[2025-05-07 17:25:30,893 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 146 transitions.
[2025-05-07 17:25:30,893 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 146 transitions. Word has length 96
[2025-05-07 17:25:30,893 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:30,893 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 146 transitions.
[2025-05-07 17:25:30,893 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 22 states have (on average 1.8636363636363635) internal successors, (41), 25 states have internal predecessors, (41), 13 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 22 states have call predecessors, (27), 13 states have call successors, (27)
[2025-05-07 17:25:30,893 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 146 transitions.
[2025-05-07 17:25:30,893 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:25:30,893 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:30,894 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:25:30,894 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:25:30,894 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:30,894 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:30,894 INFO  L85        PathProgramCache]: Analyzing trace with hash -414918472, now seen corresponding path program 1 times
[2025-05-07 17:25:30,894 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:30,894 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [396919153]
[2025-05-07 17:25:30,894 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:30,894 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:30,922 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:25:30,928 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:25:30,929 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:30,929 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:31,478 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:25:31,478 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:31,478 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [396919153]
[2025-05-07 17:25:31,479 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [396919153] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:31,479 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1404387649]
[2025-05-07 17:25:31,479 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:31,479 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:31,481 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:31,483 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:31,483 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:25:31,780 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:25:31,864 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:25:31,864 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:31,864 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:31,868 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1277 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:31,870 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:31,939 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 16 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:31,939 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:25:31,939 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1404387649] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:31,939 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:25:31,939 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [28] total 32
[2025-05-07 17:25:31,939 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [925876875]
[2025-05-07 17:25:31,939 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:31,939 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:31,940 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:31,940 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:31,940 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-05-07 17:25:31,940 INFO  L87              Difference]: Start difference. First operand 133 states and 146 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 5 states have call successors, (27), 2 states have call predecessors, (27), 5 states have return successors, (27), 5 states have call predecessors, (27), 5 states have call successors, (27)
[2025-05-07 17:25:31,957 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:31,958 INFO  L93              Difference]: Finished difference Result 33 states and 34 transitions.
[2025-05-07 17:25:31,958 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:31,958 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 5 states have call successors, (27), 2 states have call predecessors, (27), 5 states have return successors, (27), 5 states have call predecessors, (27), 5 states have call successors, (27) Word has length 96
[2025-05-07 17:25:31,958 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:31,958 INFO  L225             Difference]: With dead ends: 33
[2025-05-07 17:25:31,958 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:25:31,958 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 126 GetRequests, 96 SyntacticMatches, 0 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-05-07 17:25:31,959 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 0 mSDsluCounter, 102 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 129 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:25:31,959 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 129 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:31,959 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:25:31,959 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:25:31,960 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:25:31,960 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:25:31,960 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 96
[2025-05-07 17:25:31,960 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:31,960 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:25:31,960 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 5 states have call successors, (27), 2 states have call predecessors, (27), 5 states have return successors, (27), 5 states have call predecessors, (27), 5 states have call successors, (27)
[2025-05-07 17:25:31,960 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:25:31,960 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:25:31,962 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:25:31,967 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:25:32,163 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:32,172 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:32,177 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:25:32,186 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:25:32 BoogieIcfgContainer
[2025-05-07 17:25:32,187 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:25:32,188 INFO  L158              Benchmark]: Toolchain (without parser) took 11166.65ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 121.6MB in the beginning and 291.4MB in the end (delta: -169.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:32,189 INFO  L158              Benchmark]: SmtParser took 0.29ms. Allocated memory is still 234.9MB. Free memory is still 171.7MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:32,189 INFO  L158              Benchmark]: ChcToBoogie took 66.87ms. Allocated memory is still 234.9MB. Free memory was 121.5MB in the beginning and 190.0MB in the end (delta: -68.5MB). Peak memory consumption was 24.5MB. Max. memory is 33.6GB.
[2025-05-07 17:25:32,190 INFO  L158              Benchmark]: Boogie Preprocessor took 67.27ms. Allocated memory is still 234.9MB. Free memory was 190.0MB in the beginning and 184.8MB in the end (delta: 5.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:32,191 INFO  L158              Benchmark]: RCFGBuilder took 759.08ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 184.4MB in the beginning and 256.9MB in the end (delta: -72.6MB). Peak memory consumption was 92.8MB. Max. memory is 33.6GB.
[2025-05-07 17:25:32,191 INFO  L158              Benchmark]: TraceAbstraction took 10269.65ms. Allocated memory was 318.8MB in the beginning and 352.3MB in the end (delta: 33.6MB). Free memory was 256.1MB in the beginning and 291.4MB in the end (delta: -35.3MB). Peak memory consumption was 8.3MB. Max. memory is 33.6GB.
[2025-05-07 17:25:32,195 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.29ms. Allocated memory is still 234.9MB. Free memory is still 171.7MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 66.87ms. Allocated memory is still 234.9MB. Free memory was 121.5MB in the beginning and 190.0MB in the end (delta: -68.5MB). Peak memory consumption was 24.5MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 67.27ms. Allocated memory is still 234.9MB. Free memory was 190.0MB in the beginning and 184.8MB in the end (delta: 5.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 759.08ms. Allocated memory was 234.9MB in the beginning and 318.8MB in the end (delta: 83.9MB). Free memory was 184.4MB in the beginning and 256.9MB in the end (delta: -72.6MB). Peak memory consumption was 92.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 10269.65ms. Allocated memory was 318.8MB in the beginning and 352.3MB in the end (delta: 33.6MB). Free memory was 256.1MB in the beginning and 291.4MB in the end (delta: -35.3MB). Peak memory consumption was 8.3MB. 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 72 procedures, 282 locations, 434 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 10.2s, OverallIterations: 15, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 2.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 106 SdHoareTripleChecker+Valid, 1.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 41 mSDsluCounter, 31423 SdHoareTripleChecker+Invalid, 1.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 28087 mSDsCounter, 23 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 2483 IncrementalHoareTripleChecker+Invalid, 2506 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 23 mSolverCounterUnsat, 3336 mSDtfsCounter, 2483 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 578 GetRequests, 350 SyntacticMatches, 0 SemanticMatches, 228 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 149 ImplicationChecksByTransitivity, 1.8s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=282occurred in iteration=0, InterpolantAutomatonStates: 172, 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, 15 MinimizatonAttempts, 12 StatesRemovedByMinimization, 5 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.2s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 5.5s InterpolantComputationTime, 1303 NumberOfCodeBlocks, 1303 NumberOfCodeBlocksAsserted, 18 NumberOfCheckSat, 1360 ConstructedInterpolants, 0 QuantifiedInterpolants, 2490 SizeOfPredicates, 5 NumberOfNonLiveVariables, 3396 ConjunctsInSsa, 74 ConjunctsInUnsatCore, 19 InterpolantComputations, 14 PerfectInterpolantSequences, 137/162 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:25:32,213 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
