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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:03,352 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:03,395 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ee229699-cc3c-49a7-b632-6e5decc16a39/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:03,398 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:03,398 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:03,411 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:03,411 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:03,412 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:03,412 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:03,412 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:03,412 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:03,412 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:03,412 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:03,413 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:03,413 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:03,413 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:03,413 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:03,413 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:03,413 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:03,413 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:03,413 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:03,414 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:03,414 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:03,414 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:03,414 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:03,414 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:03,414 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:03,611 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:03,617 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:03,619 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:03,620 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:03,620 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:03,621 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ee229699-cc3c-49a7-b632-6e5decc16a39/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/implicit_only_constructor_hierarchy.sol_0_no_adts_000.smt2
[2025-05-07 17:26:03,622 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:03,624 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:03,855 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ee229699-cc3c-49a7-b632-6e5decc16a39/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/implicit_only_constructor_hierarchy.sol_0_no_adts_000.smt2
[2025-05-07 17:26:03,857 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:03,858 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:03,859 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:03,859 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:03,859 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:03,861 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,893 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03 Unit
[2025-05-07 17:26:03,893 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:03,894 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:03,894 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:03,894 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:03,905 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,905 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,927 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,927 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,932 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,933 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,934 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,936 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,937 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,951 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:03,951 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:03,951 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:03,951 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:03,952 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,954 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:03,963 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:03,971 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:26:03,973 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:26:03,980 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:03,981 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:03,981 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:03,981 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_18_0 given in one single declaration
[2025-05-07 17:26:03,981 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_18_0
[2025-05-07 17:26:03,981 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_18_0
[2025-05-07 17:26:03,981 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_f__38_39_0 given in one single declaration
[2025-05-07 17:26:03,981 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_f__38_39_0
[2025-05-07 17:26:03,981 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_f__38_39_0
[2025-05-07 17:26:03,981 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_f__38_39_0 given in one single declaration
[2025-05-07 17:26:03,981 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_f__38_39_0
[2025-05-07 17:26:03,981 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_f__38_39_0
[2025-05-07 17:26:03,982 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:26:03,982 INFO  L130     BoogieDeclarations]: Found specification of procedure block_59_return_function_f__38_39_0
[2025-05-07 17:26:03,982 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_59_return_function_f__38_39_0
[2025-05-07 17:26:03,982 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_58_f_37_39_0 given in one single declaration
[2025-05-07 17:26:03,982 INFO  L130     BoogieDeclarations]: Found specification of procedure block_58_f_37_39_0
[2025-05-07 17:26:03,982 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_58_f_37_39_0
[2025-05-07 17:26:03,982 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_57_function_f__38_39_0 given in one single declaration
[2025-05-07 17:26:03,982 INFO  L130     BoogieDeclarations]: Found specification of procedure block_57_function_f__38_39_0
[2025-05-07 17:26:03,982 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_57_function_f__38_39_0
[2025-05-07 17:26:03,982 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_60_function_f__38_39_0 given in one single declaration
[2025-05-07 17:26:03,983 INFO  L130     BoogieDeclarations]: Found specification of procedure block_60_function_f__38_39_0
[2025-05-07 17:26:03,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_60_function_f__38_39_0
[2025-05-07 17:26:03,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_61_function_f__38_39_0 given in one single declaration
[2025-05-07 17:26:03,983 INFO  L130     BoogieDeclarations]: Found specification of procedure block_61_function_f__38_39_0
[2025-05-07 17:26:03,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_61_function_f__38_39_0
[2025-05-07 17:26:03,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_12_C_39_0 given in one single declaration
[2025-05-07 17:26:03,983 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_12_C_39_0
[2025-05-07 17:26:03,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_12_C_39_0
[2025-05-07 17:26:03,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_14_C_39_0 given in one single declaration
[2025-05-07 17:26:03,983 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_14_C_39_0
[2025-05-07 17:26:03,983 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_14_C_39_0
[2025-05-07 17:26:03,983 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_65_B_26_0 given in one single declaration
[2025-05-07 17:26:03,983 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_65_B_26_0
[2025-05-07 17:26:03,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_65_B_26_0
[2025-05-07 17:26:03,984 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:26:03,984 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_67_B_26_0
[2025-05-07 17:26:03,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_67_B_26_0
[2025-05-07 17:26:03,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_66_B_26_0 given in one single declaration
[2025-05-07 17:26:03,984 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_66_B_26_0
[2025-05-07 17:26:03,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_66_B_26_0
[2025-05-07 17:26:03,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_62_C_39_0 given in one single declaration
[2025-05-07 17:26:03,984 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_62_C_39_0
[2025-05-07 17:26:03,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_62_C_39_0
[2025-05-07 17:26:03,984 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:26:03,984 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_64_C_39_0
[2025-05-07 17:26:03,984 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_64_C_39_0
[2025-05-07 17:26:03,984 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_63_C_39_0 given in one single declaration
[2025-05-07 17:26:03,985 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_63_C_39_0
[2025-05-07 17:26:03,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_63_C_39_0
[2025-05-07 17:26:03,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_68_A_13_0 given in one single declaration
[2025-05-07 17:26:03,985 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_68_A_13_0
[2025-05-07 17:26:03,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_68_A_13_0
[2025-05-07 17:26:03,985 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:26:03,985 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_70_A_13_0
[2025-05-07 17:26:03,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_70_A_13_0
[2025-05-07 17:26:03,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_69_A_13_0 given in one single declaration
[2025-05-07 17:26:03,985 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_69_A_13_0
[2025-05-07 17:26:03,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_69_A_13_0
[2025-05-07 17:26:03,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_71_C_39_0 given in one single declaration
[2025-05-07 17:26:03,985 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_71_C_39_0
[2025-05-07 17:26:03,985 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_71_C_39_0
[2025-05-07 17:26:03,985 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_g__25_39_0 given in one single declaration
[2025-05-07 17:26:03,986 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_function_g__25_39_0 given in one single declaration
[2025-05-07 17:26:03,986 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_17_function_g__25_39_0 given in one single declaration
[2025-05-07 17:26:03,986 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_17_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_17_function_g__25_39_0
[2025-05-07 17:26:03,986 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:26:03,986 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_return_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_return_function_g__25_39_0
[2025-05-07 17:26:03,986 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_g_24_39_0 given in one single declaration
[2025-05-07 17:26:03,986 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_g_24_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_g_24_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_function_g__25_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_function_g__25_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_function_g__25_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_function_g__25_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_function_g__25_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_function_g__25_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_16_function_h__12_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_16_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_16_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_function_h__12_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_15_function_h__12_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_15_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_15_function_h__12_39_0
[2025-05-07 17:26:03,987 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:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_return_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_return_function_h__12_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_h_11_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_h_11_39_0
[2025-05-07 17:26:03,987 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_h_11_39_0
[2025-05-07 17:26:03,987 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_47_function_h__12_39_0 given in one single declaration
[2025-05-07 17:26:03,987 INFO  L130     BoogieDeclarations]: Found specification of procedure block_47_function_h__12_39_0
[2025-05-07 17:26:03,988 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_47_function_h__12_39_0
[2025-05-07 17:26:03,988 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_function_h__12_39_0 given in one single declaration
[2025-05-07 17:26:03,988 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_function_h__12_39_0
[2025-05-07 17:26:03,988 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_function_h__12_39_0
[2025-05-07 17:26:03,988 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:03,988 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:03,988 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:26:04,153 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:26:04,155 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:26:04,422 INFO  L?                        ?]: Removed 303 outVars from TransFormulas that were not future-live.
[2025-05-07 17:26:04,422 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:26:04,437 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:26:04,437 INFO  L312             CfgBuilder]: Removed 19 assume(true) statements.
[2025-05-07 17:26:04,437 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:04 BoogieIcfgContainer
[2025-05-07 17:26:04,437 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:26:04,439 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:26:04,440 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:26:04,443 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:26:04,443 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:03" (1/3) ...
[2025-05-07 17:26:04,444 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@29ab09e4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:26:04, skipping insertion in model container
[2025-05-07 17:26:04,444 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (2/3) ...
[2025-05-07 17:26:04,444 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@29ab09e4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:26:04, skipping insertion in model container
[2025-05-07 17:26:04,444 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:04" (3/3) ...
[2025-05-07 17:26:04,445 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:26:04,458 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:26:04,460 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 36 procedures, 141 locations, 216 edges, 36 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:26:04,501 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:26:04,509 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;@7de0e7ef, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:26:04,510 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:26:04,513 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 141 states, 56 states have (on average 1.125) internal successors, (63), 63 states have internal predecessors, (63), 48 states have call successors, (51), 35 states have call predecessors, (51), 35 states have return successors, (51), 42 states have call predecessors, (51), 48 states have call successors, (51)
[2025-05-07 17:26:04,520 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:26:04,520 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:04,521 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:26:04,521 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:04,524 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:04,525 INFO  L85        PathProgramCache]: Analyzing trace with hash -880987820, now seen corresponding path program 1 times
[2025-05-07 17:26:04,530 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:04,530 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1444603374]
[2025-05-07 17:26:04,530 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:04,531 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:04,574 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:26:04,592 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:26:04,593 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:04,593 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:04,756 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:26:04,756 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:04,756 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1444603374]
[2025-05-07 17:26:04,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1444603374] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:04,757 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:04,759 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:04,760 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [540930470]
[2025-05-07 17:26:04,760 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:04,763 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:04,764 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:04,782 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:04,783 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:04,784 INFO  L87              Difference]: Start difference. First operand  has 141 states, 56 states have (on average 1.125) internal successors, (63), 63 states have internal predecessors, (63), 48 states have call successors, (51), 35 states have call predecessors, (51), 35 states have return successors, (51), 42 states have call predecessors, (51), 48 states have call successors, (51) 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:26:04,839 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:04,839 INFO  L93              Difference]: Finished difference Result 143 states and 169 transitions.
[2025-05-07 17:26:04,840 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:04,841 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:26:04,842 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:04,848 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:26:04,848 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:26:04,850 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:26:04,852 INFO  L437           NwaCegarLoop]: 163 mSDtfsCounter, 1 mSDsluCounter, 310 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 473 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:26:04,852 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 473 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:04,868 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:26:04,893 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 130.
[2025-05-07 17:26:04,895 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:26:04,904 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 142 transitions.
[2025-05-07 17:26:04,906 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 142 transitions. Word has length 51
[2025-05-07 17:26:04,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:04,907 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 142 transitions.
[2025-05-07 17:26:04,907 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:26:04,907 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 142 transitions.
[2025-05-07 17:26:04,909 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 72
[2025-05-07 17:26:04,909 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:04,909 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:26:04,909 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:26:04,909 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:04,910 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:04,910 INFO  L85        PathProgramCache]: Analyzing trace with hash 690674958, now seen corresponding path program 1 times
[2025-05-07 17:26:04,910 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:04,910 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1148139848]
[2025-05-07 17:26:04,910 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:04,910 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:04,949 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 71 statements into 1 equivalence classes.
[2025-05-07 17:26:04,986 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 71 of 71 statements.
[2025-05-07 17:26:04,986 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:04,986 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:05,150 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:26:05,150 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:05,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1148139848]
[2025-05-07 17:26:05,150 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1148139848] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:05,150 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:05,151 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:26:05,151 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1540409446]
[2025-05-07 17:26:05,151 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:05,151 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:26:05,152 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:05,152 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:26:05,152 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:26:05,152 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), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:26:05,227 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:05,228 INFO  L93              Difference]: Finished difference Result 134 states and 146 transitions.
[2025-05-07 17:26:05,228 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:26:05,228 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), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20) Word has length 71
[2025-05-07 17:26:05,228 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:05,229 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:26:05,229 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:26:05,229 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:26:05,230 INFO  L437           NwaCegarLoop]: 137 mSDtfsCounter, 2 mSDsluCounter, 805 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 942 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:26:05,230 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 942 Invalid, 39 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:05,231 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:26:05,236 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 134.
[2025-05-07 17:26:05,236 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 57 states have (on average 1.0526315789473684) internal successors, (60), 60 states have internal predecessors, (60), 39 states have call successors, (42), 35 states have call predecessors, (42), 37 states have return successors, (44), 38 states have call predecessors, (44), 39 states have call successors, (44)
[2025-05-07 17:26:05,238 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 146 transitions.
[2025-05-07 17:26:05,238 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 146 transitions. Word has length 71
[2025-05-07 17:26:05,238 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:05,238 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 146 transitions.
[2025-05-07 17:26:05,238 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), 4 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (20), 7 states have call predecessors, (20), 4 states have call successors, (20)
[2025-05-07 17:26:05,239 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 146 transitions.
[2025-05-07 17:26:05,240 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 72
[2025-05-07 17:26:05,240 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:05,240 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:26:05,240 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:26:05,240 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:05,241 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:05,241 INFO  L85        PathProgramCache]: Analyzing trace with hash -1645330406, now seen corresponding path program 1 times
[2025-05-07 17:26:05,241 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:05,241 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [456416026]
[2025-05-07 17:26:05,241 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:05,241 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:05,263 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 71 statements into 1 equivalence classes.
[2025-05-07 17:26:05,277 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 71 of 71 statements.
[2025-05-07 17:26:05,277 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:05,277 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:05,869 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:26:05,869 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:05,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [456416026]
[2025-05-07 17:26:05,869 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [456416026] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:05,869 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:05,869 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [24] imperfect sequences [] total 24
[2025-05-07 17:26:05,869 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1157715093]
[2025-05-07 17:26:05,869 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:05,870 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-05-07 17:26:05,870 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:05,870 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-05-07 17:26:05,871 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=506, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:26:05,871 INFO  L87              Difference]: Start difference. First operand 134 states and 146 transitions. Second operand  has 24 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 20 states have internal predecessors, (31), 8 states have call successors, (20), 1 states have call predecessors, (20), 18 states have return successors, (20), 18 states have call predecessors, (20), 8 states have call successors, (20)
[2025-05-07 17:26:06,242 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:06,242 INFO  L93              Difference]: Finished difference Result 137 states and 152 transitions.
[2025-05-07 17:26:06,242 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-05-07 17:26:06,242 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), 8 states have call successors, (20), 1 states have call predecessors, (20), 18 states have return successors, (20), 18 states have call predecessors, (20), 8 states have call successors, (20) Word has length 71
[2025-05-07 17:26:06,243 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:06,244 INFO  L225             Difference]: With dead ends: 137
[2025-05-07 17:26:06,244 INFO  L226             Difference]: Without dead ends: 136
[2025-05-07 17:26:06,245 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 29 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=72, Invalid=740, Unknown=0, NotChecked=0, Total=812
[2025-05-07 17:26:06,245 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 5 mSDsluCounter, 2546 mSDsCounter, 0 mSdLazyCounter, 471 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 2670 SdHoareTripleChecker+Invalid, 475 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 471 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:06,245 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 2670 Invalid, 475 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 471 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:26:06,246 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 136 states.
[2025-05-07 17:26:06,254 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 136 to 136.
[2025-05-07 17:26:06,254 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 136 states, 58 states have (on average 1.0517241379310345) internal successors, (61), 61 states have internal predecessors, (61), 39 states have call successors, (42), 35 states have call predecessors, (42), 38 states have return successors, (47), 39 states have call predecessors, (47), 39 states have call successors, (47)
[2025-05-07 17:26:06,256 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 136 states to 136 states and 150 transitions.
[2025-05-07 17:26:06,256 INFO  L79                 Accepts]: Start accepts. Automaton has 136 states and 150 transitions. Word has length 71
[2025-05-07 17:26:06,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:06,256 INFO  L485      AbstractCegarLoop]: Abstraction has 136 states and 150 transitions.
[2025-05-07 17:26:06,257 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), 8 states have call successors, (20), 1 states have call predecessors, (20), 18 states have return successors, (20), 18 states have call predecessors, (20), 8 states have call successors, (20)
[2025-05-07 17:26:06,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 136 states and 150 transitions.
[2025-05-07 17:26:06,259 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:06,259 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:06,259 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:26:06,260 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:26:06,260 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:06,260 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:06,260 INFO  L85        PathProgramCache]: Analyzing trace with hash 632278255, now seen corresponding path program 1 times
[2025-05-07 17:26:06,260 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:06,261 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1108228510]
[2025-05-07 17:26:06,261 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:06,261 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:06,300 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:06,321 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:06,321 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:06,321 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:07,238 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:26:07,238 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:07,238 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1108228510]
[2025-05-07 17:26:07,238 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1108228510] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:07,238 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:07,238 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [30] imperfect sequences [] total 30
[2025-05-07 17:26:07,238 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [286973951]
[2025-05-07 17:26:07,238 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:07,239 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-05-07 17:26:07,239 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:07,240 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-05-07 17:26:07,241 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=812, Unknown=0, NotChecked=0, Total=870
[2025-05-07 17:26:07,241 INFO  L87              Difference]: Start difference. First operand 136 states and 150 transitions. Second operand  has 30 states, 22 states have (on average 1.8636363636363635) internal successors, (41), 25 states have internal predecessors, (41), 12 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 12 states have call successors, (27)
[2025-05-07 17:26:07,877 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:07,877 INFO  L93              Difference]: Finished difference Result 147 states and 172 transitions.
[2025-05-07 17:26:07,877 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 31 states. 
[2025-05-07 17:26:07,878 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), 12 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 12 states have call successors, (27) Word has length 96
[2025-05-07 17:26:07,878 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:07,879 INFO  L225             Difference]: With dead ends: 147
[2025-05-07 17:26:07,879 INFO  L226             Difference]: Without dead ends: 146
[2025-05-07 17:26:07,879 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 35 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 34 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=92, Invalid=1240, Unknown=0, NotChecked=0, Total=1332
[2025-05-07 17:26:07,880 INFO  L437           NwaCegarLoop]: 123 mSDtfsCounter, 9 mSDsluCounter, 3214 mSDsCounter, 0 mSdLazyCounter, 913 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 3337 SdHoareTripleChecker+Invalid, 918 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 913 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:07,880 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 3337 Invalid, 918 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 913 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-05-07 17:26:07,881 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-05-07 17:26:07,886 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 142.
[2025-05-07 17:26:07,887 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 41 states have call successors, (44), 35 states have call predecessors, (44), 40 states have return successors, (52), 43 states have call predecessors, (52), 41 states have call successors, (52)
[2025-05-07 17:26:07,887 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 159 transitions.
[2025-05-07 17:26:07,888 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 159 transitions. Word has length 96
[2025-05-07 17:26:07,888 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:07,888 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 159 transitions.
[2025-05-07 17:26:07,888 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), 12 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 12 states have call successors, (27)
[2025-05-07 17:26:07,888 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 159 transitions.
[2025-05-07 17:26:07,889 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:07,889 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:07,889 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:26:07,890 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:26:07,890 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:07,890 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:07,890 INFO  L85        PathProgramCache]: Analyzing trace with hash 1949266537, now seen corresponding path program 1 times
[2025-05-07 17:26:07,890 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:07,890 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [441190694]
[2025-05-07 17:26:07,890 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:07,890 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:07,924 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:07,935 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:07,935 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:07,935 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:08,416 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:26:08,416 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:08,416 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [441190694]
[2025-05-07 17:26:08,417 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [441190694] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:08,417 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:08,417 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [24] imperfect sequences [] total 24
[2025-05-07 17:26:08,417 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1876969638]
[2025-05-07 17:26:08,417 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:08,417 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-05-07 17:26:08,417 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:08,418 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-05-07 17:26:08,418 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=506, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:26:08,418 INFO  L87              Difference]: Start difference. First operand 142 states and 159 transitions. Second operand  has 24 states, 18 states have (on average 2.3333333333333335) internal successors, (42), 20 states have internal predecessors, (42), 10 states have call successors, (27), 1 states have call predecessors, (27), 18 states have return successors, (27), 18 states have call predecessors, (27), 10 states have call successors, (27)
[2025-05-07 17:26:08,720 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:08,720 INFO  L93              Difference]: Finished difference Result 146 states and 169 transitions.
[2025-05-07 17:26:08,720 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-05-07 17:26:08,721 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 18 states have (on average 2.3333333333333335) internal successors, (42), 20 states have internal predecessors, (42), 10 states have call successors, (27), 1 states have call predecessors, (27), 18 states have return successors, (27), 18 states have call predecessors, (27), 10 states have call successors, (27) Word has length 96
[2025-05-07 17:26:08,721 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:08,722 INFO  L225             Difference]: With dead ends: 146
[2025-05-07 17:26:08,722 INFO  L226             Difference]: Without dead ends: 146
[2025-05-07 17:26:08,723 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:26:08,723 INFO  L437           NwaCegarLoop]: 135 mSDtfsCounter, 6 mSDsluCounter, 2773 mSDsCounter, 0 mSdLazyCounter, 448 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 2908 SdHoareTripleChecker+Invalid, 452 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 448 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:08,724 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 2908 Invalid, 452 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 448 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:26:08,725 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-05-07 17:26:08,733 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 144.
[2025-05-07 17:26:08,733 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 144 states, 61 states have (on average 1.0491803278688525) internal successors, (64), 64 states have internal predecessors, (64), 41 states have call successors, (44), 35 states have call predecessors, (44), 41 states have return successors, (55), 44 states have call predecessors, (55), 41 states have call successors, (55)
[2025-05-07 17:26:08,734 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 144 states to 144 states and 163 transitions.
[2025-05-07 17:26:08,734 INFO  L79                 Accepts]: Start accepts. Automaton has 144 states and 163 transitions. Word has length 96
[2025-05-07 17:26:08,735 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:08,735 INFO  L485      AbstractCegarLoop]: Abstraction has 144 states and 163 transitions.
[2025-05-07 17:26:08,735 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 18 states have (on average 2.3333333333333335) internal successors, (42), 20 states have internal predecessors, (42), 10 states have call successors, (27), 1 states have call predecessors, (27), 18 states have return successors, (27), 18 states have call predecessors, (27), 10 states have call successors, (27)
[2025-05-07 17:26:08,735 INFO  L278                IsEmpty]: Start isEmpty. Operand 144 states and 163 transitions.
[2025-05-07 17:26:08,736 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:08,737 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:08,737 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:26:08,737 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:26:08,737 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:08,737 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:08,737 INFO  L85        PathProgramCache]: Analyzing trace with hash -562177690, now seen corresponding path program 1 times
[2025-05-07 17:26:08,738 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:08,738 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [507601474]
[2025-05-07 17:26:08,738 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:08,738 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:08,762 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:08,772 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:08,772 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:08,772 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:09,419 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:26:09,419 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:09,419 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [507601474]
[2025-05-07 17:26:09,419 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [507601474] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:09,419 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:09,419 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [30] imperfect sequences [] total 30
[2025-05-07 17:26:09,419 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [166782250]
[2025-05-07 17:26:09,419 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:09,420 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-05-07 17:26:09,420 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:09,420 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-05-07 17:26:09,421 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=812, Unknown=0, NotChecked=0, Total=870
[2025-05-07 17:26:09,421 INFO  L87              Difference]: Start difference. First operand 144 states and 163 transitions. Second operand  has 30 states, 22 states have (on average 1.8636363636363635) internal successors, (41), 25 states have internal predecessors, (41), 12 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 12 states have call successors, (27)
[2025-05-07 17:26:09,924 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:09,924 INFO  L93              Difference]: Finished difference Result 155 states and 188 transitions.
[2025-05-07 17:26:09,924 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 31 states. 
[2025-05-07 17:26:09,924 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), 12 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 12 states have call successors, (27) Word has length 96
[2025-05-07 17:26:09,924 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:09,925 INFO  L225             Difference]: With dead ends: 155
[2025-05-07 17:26:09,925 INFO  L226             Difference]: Without dead ends: 154
[2025-05-07 17:26:09,925 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 35 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 34 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=92, Invalid=1240, Unknown=0, NotChecked=0, Total=1332
[2025-05-07 17:26:09,926 INFO  L437           NwaCegarLoop]: 126 mSDtfsCounter, 7 mSDsluCounter, 3412 mSDsCounter, 0 mSdLazyCounter, 973 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 3538 SdHoareTripleChecker+Invalid, 976 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 973 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:09,926 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 3538 Invalid, 976 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 973 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:26:09,927 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 154 states.
[2025-05-07 17:26:09,931 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 154 to 152.
[2025-05-07 17:26:09,931 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 152 states, 64 states have (on average 1.046875) internal successors, (67), 67 states have internal predecessors, (67), 43 states have call successors, (46), 35 states have call predecessors, (46), 44 states have return successors, (66), 49 states have call predecessors, (66), 43 states have call successors, (66)
[2025-05-07 17:26:09,932 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 152 states to 152 states and 179 transitions.
[2025-05-07 17:26:09,932 INFO  L79                 Accepts]: Start accepts. Automaton has 152 states and 179 transitions. Word has length 96
[2025-05-07 17:26:09,932 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:09,932 INFO  L485      AbstractCegarLoop]: Abstraction has 152 states and 179 transitions.
[2025-05-07 17:26:09,933 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), 12 states have call successors, (27), 1 states have call predecessors, (27), 22 states have return successors, (27), 23 states have call predecessors, (27), 12 states have call successors, (27)
[2025-05-07 17:26:09,933 INFO  L278                IsEmpty]: Start isEmpty. Operand 152 states and 179 transitions.
[2025-05-07 17:26:09,933 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:09,933 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:09,934 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:26:09,934 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:26:09,934 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:09,934 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:09,934 INFO  L85        PathProgramCache]: Analyzing trace with hash -1857439606, now seen corresponding path program 1 times
[2025-05-07 17:26:09,934 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:09,934 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1410118152]
[2025-05-07 17:26:09,934 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:09,934 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:09,959 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:09,966 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:09,966 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:09,966 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:10,380 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:26:10,380 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:10,380 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1410118152]
[2025-05-07 17:26:10,380 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1410118152] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:10,380 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:10,380 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [24] imperfect sequences [] total 24
[2025-05-07 17:26:10,380 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1102320097]
[2025-05-07 17:26:10,380 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:10,381 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-05-07 17:26:10,381 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:10,381 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-05-07 17:26:10,382 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=506, Unknown=0, NotChecked=0, Total=552
[2025-05-07 17:26:10,382 INFO  L87              Difference]: Start difference. First operand 152 states and 179 transitions. Second operand  has 24 states, 18 states have (on average 2.3333333333333335) internal successors, (42), 20 states have internal predecessors, (42), 10 states have call successors, (27), 1 states have call predecessors, (27), 18 states have return successors, (27), 18 states have call predecessors, (27), 10 states have call successors, (27)
[2025-05-07 17:26:10,732 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:10,732 INFO  L93              Difference]: Finished difference Result 154 states and 185 transitions.
[2025-05-07 17:26:10,732 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-05-07 17:26:10,732 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 18 states have (on average 2.3333333333333335) internal successors, (42), 20 states have internal predecessors, (42), 10 states have call successors, (27), 1 states have call predecessors, (27), 18 states have return successors, (27), 18 states have call predecessors, (27), 10 states have call successors, (27) Word has length 96
[2025-05-07 17:26:10,733 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:10,733 INFO  L225             Difference]: With dead ends: 154
[2025-05-07 17:26:10,733 INFO  L226             Difference]: Without dead ends: 154
[2025-05-07 17:26:10,734 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:26:10,735 INFO  L437           NwaCegarLoop]: 132 mSDtfsCounter, 6 mSDsluCounter, 2712 mSDsCounter, 0 mSdLazyCounter, 448 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 2844 SdHoareTripleChecker+Invalid, 452 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 448 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:10,735 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 2844 Invalid, 452 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 448 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:26:10,735 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 154 states.
[2025-05-07 17:26:10,742 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 154 to 152.
[2025-05-07 17:26:10,743 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 152 states, 64 states have (on average 1.046875) internal successors, (67), 67 states have internal predecessors, (67), 43 states have call successors, (46), 35 states have call predecessors, (46), 44 states have return successors, (65), 49 states have call predecessors, (65), 43 states have call successors, (65)
[2025-05-07 17:26:10,744 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 152 states to 152 states and 178 transitions.
[2025-05-07 17:26:10,744 INFO  L79                 Accepts]: Start accepts. Automaton has 152 states and 178 transitions. Word has length 96
[2025-05-07 17:26:10,745 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:10,745 INFO  L485      AbstractCegarLoop]: Abstraction has 152 states and 178 transitions.
[2025-05-07 17:26:10,745 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 18 states have (on average 2.3333333333333335) internal successors, (42), 20 states have internal predecessors, (42), 10 states have call successors, (27), 1 states have call predecessors, (27), 18 states have return successors, (27), 18 states have call predecessors, (27), 10 states have call successors, (27)
[2025-05-07 17:26:10,745 INFO  L278                IsEmpty]: Start isEmpty. Operand 152 states and 178 transitions.
[2025-05-07 17:26:10,746 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:10,747 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:10,747 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:10,747 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:26:10,747 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:10,747 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:10,747 INFO  L85        PathProgramCache]: Analyzing trace with hash -687700344, now seen corresponding path program 1 times
[2025-05-07 17:26:10,748 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:10,748 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [208564478]
[2025-05-07 17:26:10,748 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:10,748 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:10,791 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:10,804 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:10,805 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:10,805 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:11,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-05-07 17:26:11,465 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:11,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [208564478]
[2025-05-07 17:26:11,465 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [208564478] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:11,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1914524106]
[2025-05-07 17:26:11,465 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:11,465 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:11,467 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:11,468 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:26:11,469 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:26:11,745 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:11,893 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:11,893 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:11,893 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:11,898 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1629 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:11,905 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:12,019 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 19 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:26:12,019 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:26:12,019 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1914524106] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:12,019 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:26:12,020 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [28] total 32
[2025-05-07 17:26:12,020 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [999620741]
[2025-05-07 17:26:12,020 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:12,020 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:12,020 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:12,020 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:12,021 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-05-07 17:26:12,021 INFO  L87              Difference]: Start difference. First operand 152 states and 178 transitions. Second operand  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 5 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:26:12,044 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:12,044 INFO  L93              Difference]: Finished difference Result 151 states and 173 transitions.
[2025-05-07 17:26:12,045 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:12,045 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 5 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33) Word has length 121
[2025-05-07 17:26:12,045 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:12,046 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:26:12,046 INFO  L226             Difference]: Without dead ends: 142
[2025-05-07 17:26:12,047 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 151 GetRequests, 121 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:26:12,047 INFO  L437           NwaCegarLoop]: 149 mSDtfsCounter, 1 mSDsluCounter, 573 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 722 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:26:12,047 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 722 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:12,048 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-05-07 17:26:12,053 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 142.
[2025-05-07 17:26:12,054 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 40 states have call successors, (42), 34 states have call predecessors, (42), 41 states have return successors, (57), 44 states have call predecessors, (57), 40 states have call successors, (57)
[2025-05-07 17:26:12,055 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 162 transitions.
[2025-05-07 17:26:12,055 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 162 transitions. Word has length 121
[2025-05-07 17:26:12,055 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:12,055 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 162 transitions.
[2025-05-07 17:26:12,055 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 5 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:26:12,055 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 162 transitions.
[2025-05-07 17:26:12,057 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:12,057 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:12,057 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:12,063 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:26:12,258 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:12,258 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:12,259 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:12,259 INFO  L85        PathProgramCache]: Analyzing trace with hash -1313321201, now seen corresponding path program 1 times
[2025-05-07 17:26:12,260 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:12,260 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1078944018]
[2025-05-07 17:26:12,260 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:12,260 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:12,329 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:12,337 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:12,338 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:12,338 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:12,944 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:26:12,944 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:12,944 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1078944018]
[2025-05-07 17:26:12,944 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1078944018] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:12,944 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:12,944 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [30] imperfect sequences [] total 30
[2025-05-07 17:26:12,944 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [232172709]
[2025-05-07 17:26:12,944 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:12,945 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-05-07 17:26:12,945 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:12,945 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-05-07 17:26:12,945 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=812, Unknown=0, NotChecked=0, Total=870
[2025-05-07 17:26:12,946 INFO  L87              Difference]: Start difference. First operand 142 states and 162 transitions. Second operand  has 30 states, 22 states have (on average 2.3636363636363638) internal successors, (52), 25 states have internal predecessors, (52), 14 states have call successors, (34), 1 states have call predecessors, (34), 22 states have return successors, (34), 23 states have call predecessors, (34), 14 states have call successors, (34)
[2025-05-07 17:26:13,460 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:13,461 INFO  L93              Difference]: Finished difference Result 146 states and 173 transitions.
[2025-05-07 17:26:13,461 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 31 states. 
[2025-05-07 17:26:13,461 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 22 states have (on average 2.3636363636363638) internal successors, (52), 25 states have internal predecessors, (52), 14 states have call successors, (34), 1 states have call predecessors, (34), 22 states have return successors, (34), 23 states have call predecessors, (34), 14 states have call successors, (34) Word has length 121
[2025-05-07 17:26:13,461 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:13,462 INFO  L225             Difference]: With dead ends: 146
[2025-05-07 17:26:13,462 INFO  L226             Difference]: Without dead ends: 146
[2025-05-07 17:26:13,463 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:26:13,463 INFO  L437           NwaCegarLoop]: 120 mSDtfsCounter, 9 mSDsluCounter, 3250 mSDsCounter, 0 mSdLazyCounter, 851 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 3370 SdHoareTripleChecker+Invalid, 856 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 851 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:13,463 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 3370 Invalid, 856 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 851 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:26:13,464 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-05-07 17:26:13,468 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 142.
[2025-05-07 17:26:13,469 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 40 states have call successors, (42), 34 states have call predecessors, (42), 41 states have return successors, (56), 44 states have call predecessors, (56), 40 states have call successors, (56)
[2025-05-07 17:26:13,469 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 161 transitions.
[2025-05-07 17:26:13,469 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 161 transitions. Word has length 121
[2025-05-07 17:26:13,470 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:13,470 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 161 transitions.
[2025-05-07 17:26:13,470 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 22 states have (on average 2.3636363636363638) internal successors, (52), 25 states have internal predecessors, (52), 14 states have call successors, (34), 1 states have call predecessors, (34), 22 states have return successors, (34), 23 states have call predecessors, (34), 14 states have call successors, (34)
[2025-05-07 17:26:13,470 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 161 transitions.
[2025-05-07 17:26:13,471 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:13,471 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:13,471 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:13,471 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:26:13,471 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:13,471 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:13,472 INFO  L85        PathProgramCache]: Analyzing trace with hash -1473536589, now seen corresponding path program 1 times
[2025-05-07 17:26:13,472 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:13,472 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1474877036]
[2025-05-07 17:26:13,472 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:13,472 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:13,511 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:13,524 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:13,524 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:13,524 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:14,304 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-05-07 17:26:14,304 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:14,304 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1474877036]
[2025-05-07 17:26:14,305 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1474877036] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:14,305 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:14,305 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [35] imperfect sequences [] total 35
[2025-05-07 17:26:14,305 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [605684105]
[2025-05-07 17:26:14,305 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:14,305 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 35 states
[2025-05-07 17:26:14,305 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:14,306 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 35 interpolants.
[2025-05-07 17:26:14,306 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=68, Invalid=1122, Unknown=0, NotChecked=0, Total=1190
[2025-05-07 17:26:14,307 INFO  L87              Difference]: Start difference. First operand 142 states and 161 transitions. Second operand  has 35 states, 26 states have (on average 1.9615384615384615) internal successors, (51), 30 states have internal predecessors, (51), 15 states have call successors, (34), 1 states have call predecessors, (34), 26 states have return successors, (34), 27 states have call predecessors, (34), 15 states have call successors, (34)
[2025-05-07 17:26:14,914 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:14,914 INFO  L93              Difference]: Finished difference Result 147 states and 174 transitions.
[2025-05-07 17:26:14,914 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 36 states. 
[2025-05-07 17:26:14,914 INFO  L79                 Accepts]: Start accepts. Automaton has  has 35 states, 26 states have (on average 1.9615384615384615) internal successors, (51), 30 states have internal predecessors, (51), 15 states have call successors, (34), 1 states have call predecessors, (34), 26 states have return successors, (34), 27 states have call predecessors, (34), 15 states have call successors, (34) Word has length 121
[2025-05-07 17:26:14,915 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:14,915 INFO  L225             Difference]: With dead ends: 147
[2025-05-07 17:26:14,915 INFO  L226             Difference]: Without dead ends: 146
[2025-05-07 17:26:14,916 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 46 GetRequests, 5 SyntacticMatches, 0 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 42 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=106, Invalid=1700, Unknown=0, NotChecked=0, Total=1806
[2025-05-07 17:26:14,916 INFO  L437           NwaCegarLoop]: 107 mSDtfsCounter, 10 mSDsluCounter, 3376 mSDsCounter, 0 mSdLazyCounter, 1202 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 3483 SdHoareTripleChecker+Invalid, 1207 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 1202 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:14,916 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 3483 Invalid, 1207 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 1202 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-05-07 17:26:14,917 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-05-07 17:26:14,921 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 140.
[2025-05-07 17:26:14,921 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 59 states have (on average 1.0508474576271187) internal successors, (62), 62 states have internal predecessors, (62), 40 states have call successors, (42), 34 states have call predecessors, (42), 40 states have return successors, (53), 43 states have call predecessors, (53), 40 states have call successors, (53)
[2025-05-07 17:26:14,922 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 157 transitions.
[2025-05-07 17:26:14,922 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 157 transitions. Word has length 121
[2025-05-07 17:26:14,922 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:14,922 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 157 transitions.
[2025-05-07 17:26:14,922 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 35 states, 26 states have (on average 1.9615384615384615) internal successors, (51), 30 states have internal predecessors, (51), 15 states have call successors, (34), 1 states have call predecessors, (34), 26 states have return successors, (34), 27 states have call predecessors, (34), 15 states have call successors, (34)
[2025-05-07 17:26:14,922 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 157 transitions.
[2025-05-07 17:26:14,923 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:14,923 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:14,923 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:14,923 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:26:14,923 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:14,924 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:14,924 INFO  L85        PathProgramCache]: Analyzing trace with hash 1865750982, now seen corresponding path program 1 times
[2025-05-07 17:26:14,924 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:14,924 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2033470964]
[2025-05-07 17:26:14,924 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:14,924 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:14,958 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:14,971 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:14,971 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:14,971 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:15,552 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-05-07 17:26:15,552 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:15,552 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2033470964]
[2025-05-07 17:26:15,552 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2033470964] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:15,552 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [825829027]
[2025-05-07 17:26:15,552 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:15,552 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:15,554 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:15,555 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:26:15,559 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:26:15,785 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:15,892 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:15,892 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:15,892 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:15,897 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1629 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:15,900 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:15,968 INFO  L134       CoverageAnalysis]: Checked inductivity of 27 backedges. 19 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:26:15,968 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:26:15,968 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [825829027] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:15,968 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:26:15,968 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [28] total 32
[2025-05-07 17:26:15,968 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1312500229]
[2025-05-07 17:26:15,968 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:15,969 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:15,969 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:15,969 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:15,970 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-05-07 17:26:15,970 INFO  L87              Difference]: Start difference. First operand 140 states and 157 transitions. Second operand  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 5 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:26:15,986 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:15,986 INFO  L93              Difference]: Finished difference Result 141 states and 157 transitions.
[2025-05-07 17:26:15,986 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:15,986 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 5 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33) Word has length 121
[2025-05-07 17:26:15,987 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:15,987 INFO  L225             Difference]: With dead ends: 141
[2025-05-07 17:26:15,987 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:26:15,987 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 151 GetRequests, 121 SyntacticMatches, 0 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-05-07 17:26:15,988 INFO  L437           NwaCegarLoop]: 138 mSDtfsCounter, 1 mSDsluCounter, 533 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 671 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:26:15,988 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 671 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:15,988 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:26:15,990 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 128.
[2025-05-07 17:26:15,991 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 54 states have (on average 1.0555555555555556) internal successors, (57), 57 states have internal predecessors, (57), 37 states have call successors, (38), 33 states have call predecessors, (38), 36 states have return successors, (43), 37 states have call predecessors, (43), 37 states have call successors, (43)
[2025-05-07 17:26:15,991 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 138 transitions.
[2025-05-07 17:26:15,991 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 138 transitions. Word has length 121
[2025-05-07 17:26:15,991 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:15,991 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 138 transitions.
[2025-05-07 17:26:15,991 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.2) internal successors, (51), 6 states have internal predecessors, (51), 5 states have call successors, (33), 2 states have call predecessors, (33), 5 states have return successors, (33), 5 states have call predecessors, (33), 5 states have call successors, (33)
[2025-05-07 17:26:15,992 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 138 transitions.
[2025-05-07 17:26:15,992 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-05-07 17:26:15,992 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:15,993 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:26:15,999 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:26:16,193 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:16,194 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:16,195 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:16,195 INFO  L85        PathProgramCache]: Analyzing trace with hash 1452358840, now seen corresponding path program 1 times
[2025-05-07 17:26:16,195 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:16,195 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [258675989]
[2025-05-07 17:26:16,195 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:16,196 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:16,271 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:16,278 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:16,278 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:16,278 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:16,797 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:26:16,797 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:16,797 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [258675989]
[2025-05-07 17:26:16,797 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [258675989] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:16,797 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1782981240]
[2025-05-07 17:26:16,797 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:16,797 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:16,799 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:16,800 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:26:16,801 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:26:17,030 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-05-07 17:26:17,134 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-05-07 17:26:17,134 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:17,134 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:17,139 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1277 conjuncts, 92 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:17,142 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:17,219 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:26:17,219 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:18,858 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-05-07 17:26:18,858 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1782981240] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:18,858 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:18,858 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [28, 28, 30] total 46
[2025-05-07 17:26:18,858 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1202685628]
[2025-05-07 17:26:18,859 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:18,859 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 46 states
[2025-05-07 17:26:18,859 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:18,859 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 46 interpolants.
[2025-05-07 17:26:18,860 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=118, Invalid=1952, Unknown=0, NotChecked=0, Total=2070
[2025-05-07 17:26:18,860 INFO  L87              Difference]: Start difference. First operand 128 states and 138 transitions. Second operand  has 46 states, 32 states have (on average 1.6875) internal successors, (54), 37 states have internal predecessors, (54), 18 states have call successors, (35), 1 states have call predecessors, (35), 32 states have return successors, (44), 37 states have call predecessors, (44), 18 states have call successors, (44)
[2025-05-07 17:26:19,369 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:19,369 INFO  L93              Difference]: Finished difference Result 134 states and 150 transitions.
[2025-05-07 17:26:19,369 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 29 states. 
[2025-05-07 17:26:19,369 INFO  L79                 Accepts]: Start accepts. Automaton has  has 46 states, 32 states have (on average 1.6875) internal successors, (54), 37 states have internal predecessors, (54), 18 states have call successors, (35), 1 states have call predecessors, (35), 32 states have return successors, (44), 37 states have call predecessors, (44), 18 states have call successors, (44) Word has length 96
[2025-05-07 17:26:19,370 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:19,370 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:26:19,370 INFO  L226             Difference]: Without dead ends: 133
[2025-05-07 17:26:19,371 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 229 GetRequests, 178 SyntacticMatches, 0 SemanticMatches, 51 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 223 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=167, Invalid=2589, Unknown=0, NotChecked=0, Total=2756
[2025-05-07 17:26:19,371 INFO  L437           NwaCegarLoop]: 111 mSDtfsCounter, 6 mSDsluCounter, 3676 mSDsCounter, 0 mSdLazyCounter, 953 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 3787 SdHoareTripleChecker+Invalid, 957 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 953 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:19,371 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 3787 Invalid, 957 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 953 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:26:19,371 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-05-07 17:26:19,374 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 133.
[2025-05-07 17:26:19,374 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), 38 states have call successors, (39), 33 states have call predecessors, (39), 38 states have return successors, (50), 40 states have call predecessors, (50), 38 states have call successors, (50)
[2025-05-07 17:26:19,374 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 148 transitions.
[2025-05-07 17:26:19,374 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 148 transitions. Word has length 96
[2025-05-07 17:26:19,375 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:19,375 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 148 transitions.
[2025-05-07 17:26:19,375 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 46 states, 32 states have (on average 1.6875) internal successors, (54), 37 states have internal predecessors, (54), 18 states have call successors, (35), 1 states have call predecessors, (35), 32 states have return successors, (44), 37 states have call predecessors, (44), 18 states have call successors, (44)
[2025-05-07 17:26:19,375 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 148 transitions.
[2025-05-07 17:26:19,375 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:19,375 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:19,375 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:19,380 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:26:19,576 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:19,577 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:19,578 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:19,578 INFO  L85        PathProgramCache]: Analyzing trace with hash 1552426203, now seen corresponding path program 1 times
[2025-05-07 17:26:19,578 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:19,578 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1060021031]
[2025-05-07 17:26:19,578 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:19,579 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:19,618 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:19,629 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:19,629 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:19,629 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:20,304 INFO  L134       CoverageAnalysis]: Checked inductivity of 29 backedges. 4 proven. 12 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:26:20,304 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:20,304 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1060021031]
[2025-05-07 17:26:20,304 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1060021031] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:20,304 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [325314194]
[2025-05-07 17:26:20,304 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:20,304 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:20,306 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:20,307 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:20,308 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:26:20,706 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:20,883 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:20,884 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:20,884 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:20,888 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1629 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:20,891 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:20,982 INFO  L134       CoverageAnalysis]: Checked inductivity of 29 backedges. 24 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-05-07 17:26:20,983 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:26:20,983 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [325314194] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:20,983 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:26:20,983 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [30] total 34
[2025-05-07 17:26:20,983 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1653834399]
[2025-05-07 17:26:20,983 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:20,983 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:20,983 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:20,983 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:20,984 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=1056, Unknown=0, NotChecked=0, Total=1122
[2025-05-07 17:26:20,984 INFO  L87              Difference]: Start difference. First operand 133 states and 148 transitions. Second operand  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 2 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:26:21,012 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:21,012 INFO  L93              Difference]: Finished difference Result 133 states and 147 transitions.
[2025-05-07 17:26:21,012 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:21,012 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 2 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34) Word has length 121
[2025-05-07 17:26:21,013 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:21,013 INFO  L225             Difference]: With dead ends: 133
[2025-05-07 17:26:21,013 INFO  L226             Difference]: Without dead ends: 133
[2025-05-07 17:26:21,013 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 151 GetRequests, 119 SyntacticMatches, 0 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=66, Invalid=1056, Unknown=0, NotChecked=0, Total=1122
[2025-05-07 17:26:21,014 INFO  L437           NwaCegarLoop]: 134 mSDtfsCounter, 1 mSDsluCounter, 513 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 647 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:21,014 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 647 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:21,014 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-05-07 17:26:21,016 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 133.
[2025-05-07 17:26:21,016 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), 38 states have call successors, (39), 33 states have call predecessors, (39), 38 states have return successors, (49), 40 states have call predecessors, (49), 38 states have call successors, (49)
[2025-05-07 17:26:21,017 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 147 transitions.
[2025-05-07 17:26:21,017 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 147 transitions. Word has length 121
[2025-05-07 17:26:21,017 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:21,017 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 147 transitions.
[2025-05-07 17:26:21,017 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 10.4) internal successors, (52), 6 states have internal predecessors, (52), 4 states have call successors, (34), 2 states have call predecessors, (34), 5 states have return successors, (34), 6 states have call predecessors, (34), 4 states have call successors, (34)
[2025-05-07 17:26:21,017 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 147 transitions.
[2025-05-07 17:26:21,018 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:21,018 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:21,018 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 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:26:21,023 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:26:21,218 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable13
[2025-05-07 17:26:21,219 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:21,220 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:21,220 INFO  L85        PathProgramCache]: Analyzing trace with hash -1992944880, now seen corresponding path program 1 times
[2025-05-07 17:26:21,220 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:21,221 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2107093122]
[2025-05-07 17:26:21,221 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:21,221 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:21,347 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:21,358 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:21,358 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:21,359 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:22,123 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-05-07 17:26:22,123 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:22,123 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2107093122]
[2025-05-07 17:26:22,123 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2107093122] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:22,123 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2122965084]
[2025-05-07 17:26:22,123 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:22,123 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:22,125 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:22,126 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:22,127 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-05-07 17:26:22,409 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:22,532 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:22,532 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:22,532 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:22,538 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1628 conjuncts, 114 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:22,541 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:22,601 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-05-07 17:26:22,601 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:25,259 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:26:25,259 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2122965084] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:25,259 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:25,259 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [34, 34, 36] total 58
[2025-05-07 17:26:25,259 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1803962276]
[2025-05-07 17:26:25,259 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:25,260 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 58 states
[2025-05-07 17:26:25,260 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:25,261 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 58 interpolants.
[2025-05-07 17:26:25,261 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=151, Invalid=3155, Unknown=0, NotChecked=0, Total=3306
[2025-05-07 17:26:25,261 INFO  L87              Difference]: Start difference. First operand 133 states and 147 transitions. Second operand  has 58 states, 40 states have (on average 1.75) internal successors, (70), 47 states have internal predecessors, (70), 26 states have call successors, (46), 1 states have call predecessors, (46), 40 states have return successors, (58), 47 states have call predecessors, (58), 26 states have call successors, (58)
[2025-05-07 17:26:25,955 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:25,956 INFO  L93              Difference]: Finished difference Result 145 states and 173 transitions.
[2025-05-07 17:26:25,956 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 36 states. 
[2025-05-07 17:26:25,956 INFO  L79                 Accepts]: Start accepts. Automaton has  has 58 states, 40 states have (on average 1.75) internal successors, (70), 47 states have internal predecessors, (70), 26 states have call successors, (46), 1 states have call predecessors, (46), 40 states have return successors, (58), 47 states have call predecessors, (58), 26 states have call successors, (58) Word has length 121
[2025-05-07 17:26:25,957 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:25,957 INFO  L225             Difference]: With dead ends: 145
[2025-05-07 17:26:25,957 INFO  L226             Difference]: Without dead ends: 144
[2025-05-07 17:26:25,958 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 288 GetRequests, 223 SyntacticMatches, 0 SemanticMatches, 65 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 376 ImplicationChecksByTransitivity, 1.1s TimeCoverageRelationStatistics Valid=213, Invalid=4209, Unknown=0, NotChecked=0, Total=4422
[2025-05-07 17:26:25,958 INFO  L437           NwaCegarLoop]: 108 mSDtfsCounter, 12 mSDsluCounter, 3958 mSDsCounter, 0 mSdLazyCounter, 1375 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 4066 SdHoareTripleChecker+Invalid, 1384 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 1375 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:25,958 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 4066 Invalid, 1384 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 1375 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-05-07 17:26:25,959 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 144 states.
[2025-05-07 17:26:25,961 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 144 to 133.
[2025-05-07 17:26:25,962 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), 38 states have call successors, (39), 33 states have call predecessors, (39), 38 states have return successors, (49), 40 states have call predecessors, (49), 38 states have call successors, (49)
[2025-05-07 17:26:25,962 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 147 transitions.
[2025-05-07 17:26:25,962 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 147 transitions. Word has length 121
[2025-05-07 17:26:25,962 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:25,962 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 147 transitions.
[2025-05-07 17:26:25,963 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 58 states, 40 states have (on average 1.75) internal successors, (70), 47 states have internal predecessors, (70), 26 states have call successors, (46), 1 states have call predecessors, (46), 40 states have return successors, (58), 47 states have call predecessors, (58), 26 states have call successors, (58)
[2025-05-07 17:26:25,963 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 147 transitions.
[2025-05-07 17:26:25,963 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 122
[2025-05-07 17:26:25,963 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:25,963 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 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:26:25,969 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-05-07 17:26:26,164 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:26,164 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:26,165 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:26,166 INFO  L85        PathProgramCache]: Analyzing trace with hash 307770727, now seen corresponding path program 1 times
[2025-05-07 17:26:26,166 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:26,166 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2035612424]
[2025-05-07 17:26:26,166 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:26,167 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:26,239 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:26,247 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:26,247 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:26,247 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:27,037 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-05-07 17:26:27,037 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:27,037 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2035612424]
[2025-05-07 17:26:27,037 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2035612424] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:27,037 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1571097660]
[2025-05-07 17:26:27,037 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:27,037 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:27,040 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:27,041 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:27,042 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-05-07 17:26:27,371 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 121 statements into 1 equivalence classes.
[2025-05-07 17:26:27,484 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 121 of 121 statements.
[2025-05-07 17:26:27,485 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:27,485 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:27,491 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1628 conjuncts, 114 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:27,494 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:27,555 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-05-07 17:26:27,555 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:29,754 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:26:29,754 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1571097660] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:29,754 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:29,754 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [34, 34, 36] total 58
[2025-05-07 17:26:29,754 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [258693696]
[2025-05-07 17:26:29,754 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:29,755 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 58 states
[2025-05-07 17:26:29,755 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:29,755 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 58 interpolants.
[2025-05-07 17:26:29,756 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=151, Invalid=3155, Unknown=0, NotChecked=0, Total=3306
[2025-05-07 17:26:29,756 INFO  L87              Difference]: Start difference. First operand 133 states and 147 transitions. Second operand  has 58 states, 40 states have (on average 1.75) internal successors, (70), 47 states have internal predecessors, (70), 26 states have call successors, (46), 1 states have call predecessors, (46), 40 states have return successors, (58), 47 states have call predecessors, (58), 26 states have call successors, (58)
[2025-05-07 17:26:30,392 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:30,393 INFO  L93              Difference]: Finished difference Result 150 states and 183 transitions.
[2025-05-07 17:26:30,393 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 36 states. 
[2025-05-07 17:26:30,393 INFO  L79                 Accepts]: Start accepts. Automaton has  has 58 states, 40 states have (on average 1.75) internal successors, (70), 47 states have internal predecessors, (70), 26 states have call successors, (46), 1 states have call predecessors, (46), 40 states have return successors, (58), 47 states have call predecessors, (58), 26 states have call successors, (58) Word has length 121
[2025-05-07 17:26:30,393 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:30,394 INFO  L225             Difference]: With dead ends: 150
[2025-05-07 17:26:30,394 INFO  L226             Difference]: Without dead ends: 149
[2025-05-07 17:26:30,395 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 288 GetRequests, 223 SyntacticMatches, 0 SemanticMatches, 65 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 376 ImplicationChecksByTransitivity, 1.0s TimeCoverageRelationStatistics Valid=213, Invalid=4209, Unknown=0, NotChecked=0, Total=4422
[2025-05-07 17:26:30,395 INFO  L437           NwaCegarLoop]: 108 mSDtfsCounter, 11 mSDsluCounter, 3339 mSDsCounter, 0 mSdLazyCounter, 1171 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 3447 SdHoareTripleChecker+Invalid, 1179 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 1171 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:30,395 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 3447 Invalid, 1179 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 1171 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-05-07 17:26:30,395 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-05-07 17:26:30,398 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 143.
[2025-05-07 17:26:30,399 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 143 states, 60 states have (on average 1.05) internal successors, (63), 63 states have internal predecessors, (63), 40 states have call successors, (41), 33 states have call predecessors, (41), 42 states have return successors, (63), 46 states have call predecessors, (63), 40 states have call successors, (63)
[2025-05-07 17:26:30,399 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 143 states to 143 states and 167 transitions.
[2025-05-07 17:26:30,399 INFO  L79                 Accepts]: Start accepts. Automaton has 143 states and 167 transitions. Word has length 121
[2025-05-07 17:26:30,399 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:30,399 INFO  L485      AbstractCegarLoop]: Abstraction has 143 states and 167 transitions.
[2025-05-07 17:26:30,400 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 58 states, 40 states have (on average 1.75) internal successors, (70), 47 states have internal predecessors, (70), 26 states have call successors, (46), 1 states have call predecessors, (46), 40 states have return successors, (58), 47 states have call predecessors, (58), 26 states have call successors, (58)
[2025-05-07 17:26:30,400 INFO  L278                IsEmpty]: Start isEmpty. Operand 143 states and 167 transitions.
[2025-05-07 17:26:30,400 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 147
[2025-05-07 17:26:30,400 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:30,400 INFO  L218           NwaCegarLoop]: trace histogram [4, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:26:30,406 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-05-07 17:26:30,601 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-05-07 17:26:30,602 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:30,603 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:30,603 INFO  L85        PathProgramCache]: Analyzing trace with hash 135592185, now seen corresponding path program 1 times
[2025-05-07 17:26:30,603 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:30,603 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [110412100]
[2025-05-07 17:26:30,603 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:30,604 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:30,735 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 146 statements into 1 equivalence classes.
[2025-05-07 17:26:30,745 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 146 of 146 statements.
[2025-05-07 17:26:30,745 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:30,745 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:31,723 INFO  L134       CoverageAnalysis]: Checked inductivity of 34 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-05-07 17:26:31,723 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:31,723 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [110412100]
[2025-05-07 17:26:31,723 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [110412100] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:31,723 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2015814450]
[2025-05-07 17:26:31,723 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:31,723 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:31,724 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:31,726 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:31,727 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-05-07 17:26:32,145 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 146 statements into 1 equivalence classes.
[2025-05-07 17:26:32,294 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 146 of 146 statements.
[2025-05-07 17:26:32,294 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:32,294 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:32,302 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1979 conjuncts, 136 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:32,306 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:32,385 INFO  L134       CoverageAnalysis]: Checked inductivity of 34 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-05-07 17:26:32,385 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:35,486 INFO  L134       CoverageAnalysis]: Checked inductivity of 34 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-05-07 17:26:35,486 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2015814450] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:35,486 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:35,487 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [39, 39, 41] total 68
[2025-05-07 17:26:35,487 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [345367081]
[2025-05-07 17:26:35,487 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:35,487 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 68 states
[2025-05-07 17:26:35,487 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:35,488 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 68 interpolants.
[2025-05-07 17:26:35,488 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=178, Invalid=4378, Unknown=0, NotChecked=0, Total=4556
[2025-05-07 17:26:35,488 INFO  L87              Difference]: Start difference. First operand 143 states and 167 transitions. Second operand  has 68 states, 48 states have (on average 1.7916666666666667) internal successors, (86), 57 states have internal predecessors, (86), 32 states have call successors, (57), 1 states have call predecessors, (57), 48 states have return successors, (72), 55 states have call predecessors, (72), 32 states have call successors, (72)
[2025-05-07 17:26:36,566 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:36,566 INFO  L93              Difference]: Finished difference Result 143 states and 174 transitions.
[2025-05-07 17:26:36,566 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 41 states. 
[2025-05-07 17:26:36,567 INFO  L79                 Accepts]: Start accepts. Automaton has  has 68 states, 48 states have (on average 1.7916666666666667) internal successors, (86), 57 states have internal predecessors, (86), 32 states have call successors, (57), 1 states have call predecessors, (57), 48 states have return successors, (72), 55 states have call predecessors, (72), 32 states have call successors, (72) Word has length 146
[2025-05-07 17:26:36,567 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:36,567 INFO  L225             Difference]: With dead ends: 143
[2025-05-07 17:26:36,567 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:26:36,568 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 346 GetRequests, 270 SyntacticMatches, 0 SemanticMatches, 76 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 526 ImplicationChecksByTransitivity, 1.4s TimeCoverageRelationStatistics Valid=246, Invalid=5760, Unknown=0, NotChecked=0, Total=6006
[2025-05-07 17:26:36,569 INFO  L437           NwaCegarLoop]: 99 mSDtfsCounter, 9 mSDsluCounter, 4980 mSDsCounter, 0 mSdLazyCounter, 2101 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 5079 SdHoareTripleChecker+Invalid, 2106 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 2101 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:36,569 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 5079 Invalid, 2106 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 2101 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:26:36,569 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:26:36,569 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:26:36,569 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:26:36,569 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:26:36,569 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 146
[2025-05-07 17:26:36,569 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:36,569 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:26:36,569 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 68 states, 48 states have (on average 1.7916666666666667) internal successors, (86), 57 states have internal predecessors, (86), 32 states have call successors, (57), 1 states have call predecessors, (57), 48 states have return successors, (72), 55 states have call predecessors, (72), 32 states have call successors, (72)
[2025-05-07 17:26:36,569 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:26:36,570 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:26:36,571 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:26:36,577 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-05-07 17:26:36,772 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable16
[2025-05-07 17:26:36,781 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:36,786 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:26:36,793 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:26:36 BoogieIcfgContainer
[2025-05-07 17:26:36,794 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:26:36,795 INFO  L158              Benchmark]: Toolchain (without parser) took 32936.21ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 143.2MB in the beginning and 252.1MB in the end (delta: -108.9MB). Peak memory consumption was 88.9MB. Max. memory is 33.6GB.
[2025-05-07 17:26:36,796 INFO  L158              Benchmark]: SmtParser took 0.21ms. Allocated memory is still 234.9MB. Free memory was 173.4MB in the beginning and 172.1MB in the end (delta: 1.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:36,796 INFO  L158              Benchmark]: ChcToBoogie took 35.08ms. Allocated memory is still 234.9MB. Free memory was 143.2MB in the beginning and 139.8MB in the end (delta: 3.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:36,797 INFO  L158              Benchmark]: Boogie Preprocessor took 56.60ms. Allocated memory is still 234.9MB. Free memory was 139.8MB in the beginning and 136.1MB in the end (delta: 3.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:26:36,798 INFO  L158              Benchmark]: RCFGBuilder took 486.36ms. Allocated memory is still 234.9MB. Free memory was 136.1MB in the beginning and 162.4MB in the end (delta: -26.2MB). Peak memory consumption was 26.1MB. Max. memory is 33.6GB.
[2025-05-07 17:26:36,798 INFO  L158              Benchmark]: TraceAbstraction took 32354.18ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 161.6MB in the beginning and 252.1MB in the end (delta: -90.6MB). Peak memory consumption was 113.1MB. Max. memory is 33.6GB.
[2025-05-07 17:26:36,801 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.21ms. Allocated memory is still 234.9MB. Free memory was 173.4MB in the beginning and 172.1MB in the end (delta: 1.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 35.08ms. Allocated memory is still 234.9MB. Free memory was 143.2MB in the beginning and 139.8MB in the end (delta: 3.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 56.60ms. Allocated memory is still 234.9MB. Free memory was 139.8MB in the beginning and 136.1MB in the end (delta: 3.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 486.36ms. Allocated memory is still 234.9MB. Free memory was 136.1MB in the beginning and 162.4MB in the end (delta: -26.2MB). Peak memory consumption was 26.1MB. Max. memory is 33.6GB.
 * TraceAbstraction took 32354.18ms. Allocated memory was 234.9MB in the beginning and 436.2MB in the end (delta: 201.3MB). Free memory was 161.6MB in the beginning and 252.1MB in the end (delta: -90.6MB). Peak memory consumption was 113.1MB. 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 36 procedures, 141 locations, 216 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 32.3s, OverallIterations: 16, TraceHistogramMax: 4, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 6.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 202 SdHoareTripleChecker+Valid, 4.9s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 96 mSDsluCounter, 41984 SdHoareTripleChecker+Invalid, 4.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 39970 mSDsCounter, 64 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 10989 IncrementalHoareTripleChecker+Invalid, 11053 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 64 mSolverCounterUnsat, 2014 mSDtfsCounter, 10989 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 1864 GetRequests, 1279 SyntacticMatches, 0 SemanticMatches, 585 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1721 ImplicationChecksByTransitivity, 7.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=152occurred in iteration=6, InterpolantAutomatonStates: 373, 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, 16 MinimizatonAttempts, 43 StatesRemovedByMinimization, 10 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.7s SsaConstructionTime, 1.2s SatisfiabilityAnalysisTime, 19.9s InterpolantComputationTime, 2513 NumberOfCodeBlocks, 2513 NumberOfCodeBlocksAsserted, 23 NumberOfCheckSat, 2970 ConstructedInterpolants, 0 QuantifiedInterpolants, 6826 SizeOfPredicates, 48 NumberOfNonLiveVariables, 11399 ConjunctsInSsa, 471 ConjunctsInUnsatCore, 27 InterpolantComputations, 12 PerfectInterpolantSequences, 413/505 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:26:36,822 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
