./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-149.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:11,545 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:11,625 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c0bd9995-42d6-488a-ba24-e365f27a48c0/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:11,629 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:11,630 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:11,664 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:11,665 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:11,666 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:11,666 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:11,667 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:11,668 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:11,668 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:11,668 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:11,668 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:11,669 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:11,669 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:11,670 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:11,670 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:11,670 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:11,671 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:11,671 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:11,671 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:11,671 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:11,671 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:11,671 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:11,672 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:11,672 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:12,024 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:12,033 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:12,036 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:12,037 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:12,038 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:12,039 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c0bd9995-42d6-488a-ba24-e365f27a48c0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-149.smt2
[2025-04-28 21:21:12,041 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:12,045 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:12,832 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c0bd9995-42d6-488a-ba24-e365f27a48c0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-149.smt2
[2025-04-28 21:21:12,836 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:12,838 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:12,839 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:12,840 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:12,840 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:12,843 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,957 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12 Unit
[2025-04-28 21:21:12,957 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:12,958 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,960 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:12,960 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:12,984 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,984 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,045 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,045 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,063 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,066 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,074 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,086 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,096 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,150 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:13,151 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:13,151 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:13,151 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:13,152 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:13,159 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,178 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:13,193 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-04-28 21:21:13,198 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:13,213 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:13,214 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:13,214 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:13,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_27_0 given in one single declaration
[2025-04-28 21:21:13,214 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_27_0
[2025-04-28 21:21:13,214 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_27_0
[2025-04-28 21:21:13,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_15_D_78_0 given in one single declaration
[2025-04-28 21:21:13,214 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_15_D_78_0
[2025-04-28 21:21:13,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_15_D_78_0
[2025-04-28 21:21:13,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_D_78_0 given in one single declaration
[2025-04-28 21:21:13,215 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_D_78_0
[2025-04-28 21:21:13,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_D_78_0
[2025-04-28 21:21:13,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_79_B_50_0 given in one single declaration
[2025-04-28 21:21:13,215 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_79_B_50_0
[2025-04-28 21:21:13,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_79_B_50_0
[2025-04-28 21:21:13,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_81_B_50_0 given in one single declaration
[2025-04-28 21:21:13,215 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_81_B_50_0
[2025-04-28 21:21:13,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_81_B_50_0
[2025-04-28 21:21:13,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_80_B_50_0 given in one single declaration
[2025-04-28 21:21:13,215 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_80_B_50_0
[2025-04-28 21:21:13,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_80_B_50_0
[2025-04-28 21:21:13,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_73_D_78_0 given in one single declaration
[2025-04-28 21:21:13,216 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_73_D_78_0
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_73_D_78_0
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_75_D_78_0 given in one single declaration
[2025-04-28 21:21:13,216 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_75_D_78_0
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_75_D_78_0
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_74_D_78_0 given in one single declaration
[2025-04-28 21:21:13,216 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_74_D_78_0
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_74_D_78_0
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_85_D_78_0 given in one single declaration
[2025-04-28 21:21:13,219 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_85_D_78_0
[2025-04-28 21:21:13,219 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_85_D_78_0
[2025-04-28 21:21:13,219 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_82_A_38_0 given in one single declaration
[2025-04-28 21:21:13,220 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_82_A_38_0
[2025-04-28 21:21:13,220 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_82_A_38_0
[2025-04-28 21:21:13,220 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_84_A_38_0 given in one single declaration
[2025-04-28 21:21:13,220 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_84_A_38_0
[2025-04-28 21:21:13,220 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_84_A_38_0
[2025-04-28 21:21:13,220 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_83_A_38_0 given in one single declaration
[2025-04-28 21:21:13,220 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_83_A_38_0
[2025-04-28 21:21:13,220 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_83_A_38_0
[2025-04-28 21:21:13,220 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_76_C_62_0 given in one single declaration
[2025-04-28 21:21:13,220 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_76_C_62_0
[2025-04-28 21:21:13,220 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_76_C_62_0
[2025-04-28 21:21:13,220 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_78_C_62_0 given in one single declaration
[2025-04-28 21:21:13,220 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_78_C_62_0
[2025-04-28 21:21:13,220 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_78_C_62_0
[2025-04-28 21:21:13,220 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_77_C_62_0 given in one single declaration
[2025-04-28 21:21:13,221 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_77_C_62_0
[2025-04-28 21:21:13,221 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_77_C_62_0
[2025-04-28 21:21:13,221 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,221 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_function_f__33_78_0
[2025-04-28 21:21:13,221 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_function_f__33_78_0
[2025-04-28 21:21:13,221 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,221 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_function_f__33_78_0
[2025-04-28 21:21:13,221 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_function_f__33_78_0
[2025-04-28 21:21:13,221 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,221 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_function_f__33_78_0
[2025-04-28 21:21:13,221 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_function_f__33_78_0
[2025-04-28 21:21:13,221 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_65_f_32_78_0 given in one single declaration
[2025-04-28 21:21:13,221 INFO  L130     BoogieDeclarations]: Found specification of procedure block_65_f_32_78_0
[2025-04-28 21:21:13,221 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_65_f_32_78_0
[2025-04-28 21:21:13,222 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_64_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,222 INFO  L130     BoogieDeclarations]: Found specification of procedure block_64_function_f__33_78_0
[2025-04-28 21:21:13,222 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_64_function_f__33_78_0
[2025-04-28 21:21:13,222 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_71_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,222 INFO  L130     BoogieDeclarations]: Found specification of procedure block_71_function_f__33_78_0
[2025-04-28 21:21:13,222 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_71_function_f__33_78_0
[2025-04-28 21:21:13,222 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,222 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_function_f__33_78_0
[2025-04-28 21:21:13,222 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_function_f__33_78_0
[2025-04-28 21:21:13,223 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_66_return_f_77_78_0 given in one single declaration
[2025-04-28 21:21:13,224 INFO  L130     BoogieDeclarations]: Found specification of procedure block_66_return_f_77_78_0
[2025-04-28 21:21:13,224 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_66_return_f_77_78_0
[2025-04-28 21:21:13,224 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_return_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,224 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_return_function_f__33_78_0
[2025-04-28 21:21:13,224 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_return_function_f__33_78_0
[2025-04-28 21:21:13,224 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,225 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_function_f__33_78_0
[2025-04-28 21:21:13,225 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_function_f__33_78_0
[2025-04-28 21:21:13,225 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_72_function_f__33_78_0 given in one single declaration
[2025-04-28 21:21:13,225 INFO  L130     BoogieDeclarations]: Found specification of procedure block_72_function_f__33_78_0
[2025-04-28 21:21:13,225 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_72_function_f__33_78_0
[2025-04-28 21:21:13,225 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_14_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,225 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_14_function_f__33_62_0
[2025-04-28 21:21:13,225 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_14_function_f__33_62_0
[2025-04-28 21:21:13,226 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,226 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_function_f__33_62_0
[2025-04-28 21:21:13,226 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_function_f__33_62_0
[2025-04-28 21:21:13,226 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_54_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,226 INFO  L130     BoogieDeclarations]: Found specification of procedure block_54_function_f__33_62_0
[2025-04-28 21:21:13,226 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_54_function_f__33_62_0
[2025-04-28 21:21:13,226 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49_f_32_62_0 given in one single declaration
[2025-04-28 21:21:13,226 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49_f_32_62_0
[2025-04-28 21:21:13,226 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49_f_32_62_0
[2025-04-28 21:21:13,226 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,226 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_function_f__33_62_0
[2025-04-28 21:21:13,226 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_function_f__33_62_0
[2025-04-28 21:21:13,227 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_return_f_61_62_0 given in one single declaration
[2025-04-28 21:21:13,227 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_return_f_61_62_0
[2025-04-28 21:21:13,227 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_return_f_61_62_0
[2025-04-28 21:21:13,227 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_51_return_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,227 INFO  L130     BoogieDeclarations]: Found specification of procedure block_51_return_function_f__33_62_0
[2025-04-28 21:21:13,228 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_51_return_function_f__33_62_0
[2025-04-28 21:21:13,228 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_52_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,228 INFO  L130     BoogieDeclarations]: Found specification of procedure block_52_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_52_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_55_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,229 INFO  L130     BoogieDeclarations]: Found specification of procedure block_55_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_55_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_53_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,229 INFO  L130     BoogieDeclarations]: Found specification of procedure block_53_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_53_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_56_function_f__33_62_0 given in one single declaration
[2025-04-28 21:21:13,229 INFO  L130     BoogieDeclarations]: Found specification of procedure block_56_function_f__33_62_0
[2025-04-28 21:21:13,229 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_56_function_f__33_62_0
[2025-04-28 21:21:13,230 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_10_C_62_0 given in one single declaration
[2025-04-28 21:21:13,230 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_10_C_62_0
[2025-04-28 21:21:13,230 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_10_C_62_0
[2025-04-28 21:21:13,230 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_12_C_62_0 given in one single declaration
[2025-04-28 21:21:13,230 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_12_C_62_0
[2025-04-28 21:21:13,230 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_12_C_62_0
[2025-04-28 21:21:13,230 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_63_C_62_0 given in one single declaration
[2025-04-28 21:21:13,230 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_63_C_62_0
[2025-04-28 21:21:13,231 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_63_C_62_0
[2025-04-28 21:21:13,231 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_60_A_38_0 given in one single declaration
[2025-04-28 21:21:13,232 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_60_A_38_0
[2025-04-28 21:21:13,233 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_60_A_38_0
[2025-04-28 21:21:13,233 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_62_A_38_0 given in one single declaration
[2025-04-28 21:21:13,233 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_62_A_38_0
[2025-04-28 21:21:13,233 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_62_A_38_0
[2025-04-28 21:21:13,233 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_61_A_38_0 given in one single declaration
[2025-04-28 21:21:13,233 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_61_A_38_0
[2025-04-28 21:21:13,233 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_61_A_38_0
[2025-04-28 21:21:13,233 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_57_C_62_0 given in one single declaration
[2025-04-28 21:21:13,233 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_57_C_62_0
[2025-04-28 21:21:13,233 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_57_C_62_0
[2025-04-28 21:21:13,233 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_59_C_62_0 given in one single declaration
[2025-04-28 21:21:13,233 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_59_C_62_0
[2025-04-28 21:21:13,233 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_59_C_62_0
[2025-04-28 21:21:13,234 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_58_C_62_0 given in one single declaration
[2025-04-28 21:21:13,234 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_58_C_62_0
[2025-04-28 21:21:13,234 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_58_C_62_0
[2025-04-28 21:21:13,234 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_5_B_50_0 given in one single declaration
[2025-04-28 21:21:13,234 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_5_B_50_0
[2025-04-28 21:21:13,234 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_5_B_50_0
[2025-04-28 21:21:13,234 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_7_B_50_0 given in one single declaration
[2025-04-28 21:21:13,234 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_7_B_50_0
[2025-04-28 21:21:13,234 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_7_B_50_0
[2025-04-28 21:21:13,234 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_44_A_38_0 given in one single declaration
[2025-04-28 21:21:13,234 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_44_A_38_0
[2025-04-28 21:21:13,234 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_44_A_38_0
[2025-04-28 21:21:13,236 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_46_A_38_0 given in one single declaration
[2025-04-28 21:21:13,236 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_46_A_38_0
[2025-04-28 21:21:13,236 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_46_A_38_0
[2025-04-28 21:21:13,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_45_A_38_0 given in one single declaration
[2025-04-28 21:21:13,237 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_45_A_38_0
[2025-04-28 21:21:13,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_45_A_38_0
[2025-04-28 21:21:13,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_47_B_50_0 given in one single declaration
[2025-04-28 21:21:13,237 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_47_B_50_0
[2025-04-28 21:21:13,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_47_B_50_0
[2025-04-28 21:21:13,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_41_B_50_0 given in one single declaration
[2025-04-28 21:21:13,237 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_41_B_50_0
[2025-04-28 21:21:13,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_41_B_50_0
[2025-04-28 21:21:13,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_43_B_50_0 given in one single declaration
[2025-04-28 21:21:13,237 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_43_B_50_0
[2025-04-28 21:21:13,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_43_B_50_0
[2025-04-28 21:21:13,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_42_B_50_0 given in one single declaration
[2025-04-28 21:21:13,237 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_42_B_50_0
[2025-04-28 21:21:13,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_42_B_50_0
[2025-04-28 21:21:13,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_9_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,238 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_9_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_9_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_40_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,238 INFO  L130     BoogieDeclarations]: Found specification of procedure block_40_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_40_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_8_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,238 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_8_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_8_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_39_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,238 INFO  L130     BoogieDeclarations]: Found specification of procedure block_39_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_39_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_33_f_32_50_0 given in one single declaration
[2025-04-28 21:21:13,238 INFO  L130     BoogieDeclarations]: Found specification of procedure block_33_f_32_50_0
[2025-04-28 21:21:13,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_33_f_32_50_0
[2025-04-28 21:21:13,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,238 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_function_f__33_50_0
[2025-04-28 21:21:13,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,239 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36_function_f__33_50_0
[2025-04-28 21:21:13,239 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36_function_f__33_50_0
[2025-04-28 21:21:13,239 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,239 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_function_f__33_50_0
[2025-04-28 21:21:13,239 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_function_f__33_50_0
[2025-04-28 21:21:13,239 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_34_return_f_49_50_0 given in one single declaration
[2025-04-28 21:21:13,239 INFO  L130     BoogieDeclarations]: Found specification of procedure block_34_return_f_49_50_0
[2025-04-28 21:21:13,239 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_34_return_f_49_50_0
[2025-04-28 21:21:13,239 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_return_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,239 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_return_function_f__33_50_0
[2025-04-28 21:21:13,239 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_return_function_f__33_50_0
[2025-04-28 21:21:13,239 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_function_f__33_50_0 given in one single declaration
[2025-04-28 21:21:13,240 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_function_f__33_50_0
[2025-04-28 21:21:13,240 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_function_f__33_50_0
[2025-04-28 21:21:13,241 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:13,241 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:13,241 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:13,816 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:13,820 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:14,790 INFO  L?                        ?]: Removed 628 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:14,791 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:14,819 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:14,819 INFO  L312             CfgBuilder]: Removed 38 assume(true) statements.
[2025-04-28 21:21:14,824 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14 BoogieIcfgContainer
[2025-04-28 21:21:14,824 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:14,826 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:14,826 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:14,835 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:14,836 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:12" (1/3) ...
[2025-04-28 21:21:14,836 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@acc4952 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,837 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (2/3) ...
[2025-04-28 21:21:14,837 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@acc4952 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,837 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14" (3/3) ...
[2025-04-28 21:21:14,841 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:14,857 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:14,862 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 69 procedures, 280 locations, 456 edges, 69 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:14,941 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:14,960 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;@458e8299, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:14,960 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:14,968 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 280 states, 112 states have (on average 1.125) internal successors, (126), 126 states have internal predecessors, (126), 98 states have call successors, (110), 68 states have call predecessors, (110), 68 states have return successors, (110), 85 states have call predecessors, (110), 98 states have call successors, (110)
[2025-04-28 21:21:14,995 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:14,995 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,999 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,000 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,006 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,006 INFO  L85        PathProgramCache]: Analyzing trace with hash 1389378231, now seen corresponding path program 1 times
[2025-04-28 21:21:15,015 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,015 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [677735328]
[2025-04-28 21:21:15,015 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,016 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,102 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:15,236 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:15,236 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,238 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,710 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:15,710 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,711 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [677735328]
[2025-04-28 21:21:15,711 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [677735328] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,711 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,714 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:15,717 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1027082601]
[2025-04-28 21:21:15,718 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,722 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:15,723 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,779 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:15,780 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:15,783 INFO  L87              Difference]: Start difference. First operand  has 280 states, 112 states have (on average 1.125) internal successors, (126), 126 states have internal predecessors, (126), 98 states have call successors, (110), 68 states have call predecessors, (110), 68 states have return successors, (110), 85 states have call predecessors, (110), 98 states have call successors, (110) Second operand  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:15,923 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:15,924 INFO  L93              Difference]: Finished difference Result 255 states and 303 transitions.
[2025-04-28 21:21:15,925 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:15,926 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14) Word has length 52
[2025-04-28 21:21:15,927 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:15,940 INFO  L225             Difference]: With dead ends: 255
[2025-04-28 21:21:15,941 INFO  L226             Difference]: Without dead ends: 230
[2025-04-28 21:21:15,943 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-04-28 21:21:15,946 INFO  L437           NwaCegarLoop]: 299 mSDtfsCounter, 1 mSDsluCounter, 576 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 875 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:15,947 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 875 Invalid, 5 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:15,962 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 230 states.
[2025-04-28 21:21:16,005 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 230 to 228.
[2025-04-28 21:21:16,008 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 228 states, 93 states have (on average 1.096774193548387) internal successors, (102), 102 states have internal predecessors, (102), 75 states have call successors, (78), 59 states have call predecessors, (78), 59 states have return successors, (78), 66 states have call predecessors, (78), 75 states have call successors, (78)
[2025-04-28 21:21:16,020 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 228 states to 228 states and 258 transitions.
[2025-04-28 21:21:16,025 INFO  L79                 Accepts]: Start accepts. Automaton has 228 states and 258 transitions. Word has length 52
[2025-04-28 21:21:16,026 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,026 INFO  L485      AbstractCegarLoop]: Abstraction has 228 states and 258 transitions.
[2025-04-28 21:21:16,026 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:16,026 INFO  L278                IsEmpty]: Start isEmpty. Operand 228 states and 258 transitions.
[2025-04-28 21:21:16,029 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:16,033 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,033 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]
[2025-04-28 21:21:16,034 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:16,034 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,035 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,035 INFO  L85        PathProgramCache]: Analyzing trace with hash -1261651843, now seen corresponding path program 1 times
[2025-04-28 21:21:16,035 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,035 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1432758211]
[2025-04-28 21:21:16,035 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,035 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,087 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:16,149 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:16,150 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,150 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,487 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:16,488 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,488 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1432758211]
[2025-04-28 21:21:16,488 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1432758211] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,488 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,488 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:16,489 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [491188833]
[2025-04-28 21:21:16,489 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,490 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:16,493 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,494 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:16,494 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:16,494 INFO  L87              Difference]: Start difference. First operand 228 states and 258 transitions. Second operand  has 5 states, 4 states have (on average 6.0) internal successors, (24), 5 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 4 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:16,586 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,589 INFO  L93              Difference]: Finished difference Result 232 states and 262 transitions.
[2025-04-28 21:21:16,589 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:16,590 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.0) internal successors, (24), 5 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 4 states have call predecessors, (14), 4 states have call successors, (14) Word has length 52
[2025-04-28 21:21:16,590 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,593 INFO  L225             Difference]: With dead ends: 232
[2025-04-28 21:21:16,596 INFO  L226             Difference]: Without dead ends: 225
[2025-04-28 21:21:16,597 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:16,597 INFO  L437           NwaCegarLoop]: 256 mSDtfsCounter, 1 mSDsluCounter, 751 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1007 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,600 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1007 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,601 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 225 states.
[2025-04-28 21:21:16,627 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 225 to 223.
[2025-04-28 21:21:16,630 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 223 states, 93 states have (on average 1.075268817204301) internal successors, (100), 100 states have internal predecessors, (100), 70 states have call successors, (73), 59 states have call predecessors, (73), 59 states have return successors, (73), 63 states have call predecessors, (73), 70 states have call successors, (73)
[2025-04-28 21:21:16,634 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 223 states to 223 states and 246 transitions.
[2025-04-28 21:21:16,635 INFO  L79                 Accepts]: Start accepts. Automaton has 223 states and 246 transitions. Word has length 52
[2025-04-28 21:21:16,636 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,636 INFO  L485      AbstractCegarLoop]: Abstraction has 223 states and 246 transitions.
[2025-04-28 21:21:16,636 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.0) internal successors, (24), 5 states have internal predecessors, (24), 4 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 4 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:16,638 INFO  L278                IsEmpty]: Start isEmpty. Operand 223 states and 246 transitions.
[2025-04-28 21:21:16,641 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:16,642 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,642 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]
[2025-04-28 21:21:16,643 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:16,643 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,644 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,644 INFO  L85        PathProgramCache]: Analyzing trace with hash 830234133, now seen corresponding path program 1 times
[2025-04-28 21:21:16,646 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,646 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1842832701]
[2025-04-28 21:21:16,646 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,646 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,694 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:16,703 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:16,704 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,704 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,850 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:16,850 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,851 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1842832701]
[2025-04-28 21:21:16,851 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1842832701] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,851 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,851 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,851 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1877237068]
[2025-04-28 21:21:16,851 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,851 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,852 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,852 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,852 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,852 INFO  L87              Difference]: Start difference. First operand 223 states and 246 transitions. Second operand  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 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-04-28 21:21:16,875 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,875 INFO  L93              Difference]: Finished difference Result 227 states and 250 transitions.
[2025-04-28 21:21:16,875 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,876 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 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 52
[2025-04-28 21:21:16,876 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,878 INFO  L225             Difference]: With dead ends: 227
[2025-04-28 21:21:16,878 INFO  L226             Difference]: Without dead ends: 220
[2025-04-28 21:21:16,878 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-04-28 21:21:16,879 INFO  L437           NwaCegarLoop]: 246 mSDtfsCounter, 1 mSDsluCounter, 481 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 727 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,880 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 727 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,881 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 220 states.
[2025-04-28 21:21:16,891 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 220 to 218.
[2025-04-28 21:21:16,896 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 93 states have (on average 1.053763440860215) internal successors, (98), 98 states have internal predecessors, (98), 65 states have call successors, (68), 59 states have call predecessors, (68), 59 states have return successors, (68), 60 states have call predecessors, (68), 65 states have call successors, (68)
[2025-04-28 21:21:16,898 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 234 transitions.
[2025-04-28 21:21:16,898 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 234 transitions. Word has length 52
[2025-04-28 21:21:16,898 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,898 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 234 transitions.
[2025-04-28 21:21:16,898 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.0) internal successors, (24), 4 states have internal predecessors, (24), 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-04-28 21:21:16,898 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 234 transitions.
[2025-04-28 21:21:16,905 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-04-28 21:21:16,905 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,905 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]
[2025-04-28 21:21:16,905 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:16,905 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,906 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,906 INFO  L85        PathProgramCache]: Analyzing trace with hash -1164109246, now seen corresponding path program 1 times
[2025-04-28 21:21:16,906 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,906 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1735210397]
[2025-04-28 21:21:16,906 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,906 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,985 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-04-28 21:21:17,009 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-04-28 21:21:17,009 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,010 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,225 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:17,225 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,225 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1735210397]
[2025-04-28 21:21:17,226 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1735210397] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,226 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,227 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:17,227 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1093366383]
[2025-04-28 21:21:17,227 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,227 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:17,227 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,228 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:17,229 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:17,230 INFO  L87              Difference]: Start difference. First operand 218 states and 234 transitions. Second operand  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 5 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 5 states have call successors, (17)
[2025-04-28 21:21:17,314 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,315 INFO  L93              Difference]: Finished difference Result 223 states and 240 transitions.
[2025-04-28 21:21:17,316 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:17,316 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 5 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 5 states have call successors, (17) Word has length 62
[2025-04-28 21:21:17,316 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,318 INFO  L225             Difference]: With dead ends: 223
[2025-04-28 21:21:17,318 INFO  L226             Difference]: Without dead ends: 223
[2025-04-28 21:21:17,319 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:17,322 INFO  L437           NwaCegarLoop]: 231 mSDtfsCounter, 1 mSDsluCounter, 908 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1139 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,323 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1139 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,324 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 223 states.
[2025-04-28 21:21:17,347 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 223 to 223.
[2025-04-28 21:21:17,348 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 223 states, 95 states have (on average 1.0526315789473684) internal successors, (100), 100 states have internal predecessors, (100), 66 states have call successors, (69), 59 states have call predecessors, (69), 61 states have return successors, (71), 63 states have call predecessors, (71), 66 states have call successors, (71)
[2025-04-28 21:21:17,353 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 223 states to 223 states and 240 transitions.
[2025-04-28 21:21:17,353 INFO  L79                 Accepts]: Start accepts. Automaton has 223 states and 240 transitions. Word has length 62
[2025-04-28 21:21:17,353 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,354 INFO  L485      AbstractCegarLoop]: Abstraction has 223 states and 240 transitions.
[2025-04-28 21:21:17,354 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 5 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 5 states have call predecessors, (17), 5 states have call successors, (17)
[2025-04-28 21:21:17,354 INFO  L278                IsEmpty]: Start isEmpty. Operand 223 states and 240 transitions.
[2025-04-28 21:21:17,358 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-04-28 21:21:17,358 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,359 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,359 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:17,359 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,359 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,360 INFO  L85        PathProgramCache]: Analyzing trace with hash -1015357740, now seen corresponding path program 1 times
[2025-04-28 21:21:17,360 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,360 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1054928250]
[2025-04-28 21:21:17,360 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,360 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,407 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-04-28 21:21:17,444 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-04-28 21:21:17,445 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,445 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,630 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:17,630 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,630 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1054928250]
[2025-04-28 21:21:17,631 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1054928250] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,631 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,631 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:17,631 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1844941424]
[2025-04-28 21:21:17,631 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,631 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:17,631 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,632 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:17,632 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:17,632 INFO  L87              Difference]: Start difference. First operand 223 states and 240 transitions. Second operand  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 6 states have call predecessors, (17), 3 states have call successors, (17)
[2025-04-28 21:21:17,701 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,702 INFO  L93              Difference]: Finished difference Result 227 states and 244 transitions.
[2025-04-28 21:21:17,702 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:17,702 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 6 states have call predecessors, (17), 3 states have call successors, (17) Word has length 62
[2025-04-28 21:21:17,703 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,704 INFO  L225             Difference]: With dead ends: 227
[2025-04-28 21:21:17,704 INFO  L226             Difference]: Without dead ends: 227
[2025-04-28 21:21:17,704 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:17,705 INFO  L437           NwaCegarLoop]: 231 mSDtfsCounter, 1 mSDsluCounter, 908 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1139 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,711 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1139 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:17,712 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 227 states.
[2025-04-28 21:21:17,727 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 227 to 227.
[2025-04-28 21:21:17,728 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 227 states, 97 states have (on average 1.0515463917525774) internal successors, (102), 102 states have internal predecessors, (102), 66 states have call successors, (69), 59 states have call predecessors, (69), 63 states have return successors, (73), 65 states have call predecessors, (73), 66 states have call successors, (73)
[2025-04-28 21:21:17,732 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 227 states to 227 states and 244 transitions.
[2025-04-28 21:21:17,732 INFO  L79                 Accepts]: Start accepts. Automaton has 227 states and 244 transitions. Word has length 62
[2025-04-28 21:21:17,732 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,732 INFO  L485      AbstractCegarLoop]: Abstraction has 227 states and 244 transitions.
[2025-04-28 21:21:17,733 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.6) internal successors, (28), 6 states have internal predecessors, (28), 3 states have call successors, (17), 1 states have call predecessors, (17), 5 states have return successors, (17), 6 states have call predecessors, (17), 3 states have call successors, (17)
[2025-04-28 21:21:17,733 INFO  L278                IsEmpty]: Start isEmpty. Operand 227 states and 244 transitions.
[2025-04-28 21:21:17,734 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-04-28 21:21:17,734 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,734 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]
[2025-04-28 21:21:17,734 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:17,735 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,735 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,735 INFO  L85        PathProgramCache]: Analyzing trace with hash 1725687933, now seen corresponding path program 1 times
[2025-04-28 21:21:17,735 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,735 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1218537685]
[2025-04-28 21:21:17,737 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,737 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,775 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-04-28 21:21:17,855 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:21:17,855 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,855 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:18,190 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,190 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1218537685]
[2025-04-28 21:21:18,191 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1218537685] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,191 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,191 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:18,191 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1263714748]
[2025-04-28 21:21:18,191 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,191 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:18,192 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,192 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:18,192 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:18,193 INFO  L87              Difference]: Start difference. First operand 227 states and 244 transitions. Second operand  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 6 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 7 states have call predecessors, (18), 6 states have call successors, (18)
[2025-04-28 21:21:18,335 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,335 INFO  L93              Difference]: Finished difference Result 192 states and 204 transitions.
[2025-04-28 21:21:18,336 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:18,336 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 6 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 7 states have call predecessors, (18), 6 states have call successors, (18) Word has length 65
[2025-04-28 21:21:18,339 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,340 INFO  L225             Difference]: With dead ends: 192
[2025-04-28 21:21:18,340 INFO  L226             Difference]: Without dead ends: 159
[2025-04-28 21:21:18,340 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:18,341 INFO  L437           NwaCegarLoop]: 195 mSDtfsCounter, 2 mSDsluCounter, 1339 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1534 SdHoareTripleChecker+Invalid, 45 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,342 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1534 Invalid, 45 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,344 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 159 states.
[2025-04-28 21:21:18,357 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 159 to 159.
[2025-04-28 21:21:18,359 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 68 states have (on average 1.0441176470588236) internal successors, (71), 71 states have internal predecessors, (71), 46 states have call successors, (48), 42 states have call predecessors, (48), 44 states have return successors, (50), 45 states have call predecessors, (50), 46 states have call successors, (50)
[2025-04-28 21:21:18,361 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 169 transitions.
[2025-04-28 21:21:18,362 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 169 transitions. Word has length 65
[2025-04-28 21:21:18,363 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,363 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 169 transitions.
[2025-04-28 21:21:18,363 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 6 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 7 states have call predecessors, (18), 6 states have call successors, (18)
[2025-04-28 21:21:18,364 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 169 transitions.
[2025-04-28 21:21:18,365 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-04-28 21:21:18,365 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,365 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]
[2025-04-28 21:21:18,365 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:18,366 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,366 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,366 INFO  L85        PathProgramCache]: Analyzing trace with hash -1392170714, now seen corresponding path program 1 times
[2025-04-28 21:21:18,366 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,366 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [875947701]
[2025-04-28 21:21:18,366 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,367 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,420 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-04-28 21:21:18,458 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:21:18,458 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,458 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,806 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:18,808 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,808 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [875947701]
[2025-04-28 21:21:18,808 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [875947701] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,808 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,808 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:18,808 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1426066100]
[2025-04-28 21:21:18,808 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,809 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:18,809 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,810 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:18,810 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:18,810 INFO  L87              Difference]: Start difference. First operand 159 states and 169 transitions. Second operand  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 8 states have call predecessors, (18), 4 states have call successors, (18)
[2025-04-28 21:21:18,936 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,937 INFO  L93              Difference]: Finished difference Result 159 states and 168 transitions.
[2025-04-28 21:21:18,937 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:18,937 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 8 states have call predecessors, (18), 4 states have call successors, (18) Word has length 65
[2025-04-28 21:21:18,938 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,939 INFO  L225             Difference]: With dead ends: 159
[2025-04-28 21:21:18,939 INFO  L226             Difference]: Without dead ends: 92
[2025-04-28 21:21:18,939 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:18,940 INFO  L437           NwaCegarLoop]: 161 mSDtfsCounter, 1 mSDsluCounter, 1103 mSDsCounter, 0 mSdLazyCounter, 52 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1264 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 52 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,940 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1264 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 52 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,941 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-04-28 21:21:18,947 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-04-28 21:21:18,948 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 39 states have (on average 1.0256410256410255) internal successors, (40), 40 states have internal predecessors, (40), 27 states have call successors, (28), 25 states have call predecessors, (28), 25 states have return successors, (28), 26 states have call predecessors, (28), 27 states have call successors, (28)
[2025-04-28 21:21:18,949 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 96 transitions.
[2025-04-28 21:21:18,949 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 96 transitions. Word has length 65
[2025-04-28 21:21:18,949 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,953 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 96 transitions.
[2025-04-28 21:21:18,953 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 4.142857142857143) internal successors, (29), 9 states have internal predecessors, (29), 4 states have call successors, (18), 1 states have call predecessors, (18), 7 states have return successors, (18), 8 states have call predecessors, (18), 4 states have call successors, (18)
[2025-04-28 21:21:18,953 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 96 transitions.
[2025-04-28 21:21:18,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 83
[2025-04-28 21:21:18,954 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,954 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,954 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:18,954 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,955 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,955 INFO  L85        PathProgramCache]: Analyzing trace with hash 1588678405, now seen corresponding path program 1 times
[2025-04-28 21:21:18,955 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [760595914]
[2025-04-28 21:21:18,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,024 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 82 statements into 1 equivalence classes.
[2025-04-28 21:21:19,053 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 82 of 82 statements.
[2025-04-28 21:21:19,054 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,054 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,210 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:19,210 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,210 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [760595914]
[2025-04-28 21:21:19,210 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [760595914] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,210 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,210 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:19,210 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [625718067]
[2025-04-28 21:21:19,211 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,211 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:19,211 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,212 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:19,212 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:19,212 INFO  L87              Difference]: Start difference. First operand 92 states and 96 transitions. Second operand  has 6 states, 5 states have (on average 7.2) internal successors, (36), 6 states have internal predecessors, (36), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-04-28 21:21:19,259 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,259 INFO  L93              Difference]: Finished difference Result 96 states and 100 transitions.
[2025-04-28 21:21:19,260 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:19,260 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.2) internal successors, (36), 6 states have internal predecessors, (36), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23) Word has length 82
[2025-04-28 21:21:19,260 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,261 INFO  L225             Difference]: With dead ends: 96
[2025-04-28 21:21:19,261 INFO  L226             Difference]: Without dead ends: 96
[2025-04-28 21:21:19,261 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:19,262 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 1 mSDsluCounter, 362 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 455 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,262 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 455 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:19,263 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-04-28 21:21:19,266 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 96.
[2025-04-28 21:21:19,269 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 96 states, 41 states have (on average 1.024390243902439) internal successors, (42), 42 states have internal predecessors, (42), 27 states have call successors, (28), 25 states have call predecessors, (28), 27 states have return successors, (30), 28 states have call predecessors, (30), 27 states have call successors, (30)
[2025-04-28 21:21:19,270 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 96 states to 96 states and 100 transitions.
[2025-04-28 21:21:19,270 INFO  L79                 Accepts]: Start accepts. Automaton has 96 states and 100 transitions. Word has length 82
[2025-04-28 21:21:19,270 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,270 INFO  L485      AbstractCegarLoop]: Abstraction has 96 states and 100 transitions.
[2025-04-28 21:21:19,271 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.2) internal successors, (36), 6 states have internal predecessors, (36), 4 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-04-28 21:21:19,271 INFO  L278                IsEmpty]: Start isEmpty. Operand 96 states and 100 transitions.
[2025-04-28 21:21:19,272 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 86
[2025-04-28 21:21:19,273 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,273 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,274 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:19,274 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,274 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,274 INFO  L85        PathProgramCache]: Analyzing trace with hash 456343453, now seen corresponding path program 1 times
[2025-04-28 21:21:19,274 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,274 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1608191654]
[2025-04-28 21:21:19,274 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,275 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,323 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 85 statements into 1 equivalence classes.
[2025-04-28 21:21:19,346 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 85 of 85 statements.
[2025-04-28 21:21:19,346 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,346 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,684 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:19,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1608191654]
[2025-04-28 21:21:19,685 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1608191654] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,685 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,685 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:19,685 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1735835176]
[2025-04-28 21:21:19,685 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,685 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:19,686 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,686 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:19,687 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:19,687 INFO  L87              Difference]: Start difference. First operand 96 states and 100 transitions. Second operand  has 9 states, 7 states have (on average 5.285714285714286) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 7 states have return successors, (24), 7 states have call predecessors, (24), 5 states have call successors, (24)
[2025-04-28 21:21:19,782 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,783 INFO  L93              Difference]: Finished difference Result 35 states and 35 transitions.
[2025-04-28 21:21:19,783 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:19,783 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 5.285714285714286) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 7 states have return successors, (24), 7 states have call predecessors, (24), 5 states have call successors, (24) Word has length 85
[2025-04-28 21:21:19,784 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,784 INFO  L225             Difference]: With dead ends: 35
[2025-04-28 21:21:19,784 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:19,784 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:19,784 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 0 mSDsluCounter, 192 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 222 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,785 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 222 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,785 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:19,785 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:19,785 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-04-28 21:21:19,786 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:19,786 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 85
[2025-04-28 21:21:19,786 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,786 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:19,786 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 5.285714285714286) internal successors, (37), 9 states have internal predecessors, (37), 5 states have call successors, (24), 1 states have call predecessors, (24), 7 states have return successors, (24), 7 states have call predecessors, (24), 5 states have call successors, (24)
[2025-04-28 21:21:19,786 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:19,786 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:19,789 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:19,790 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:19,793 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,795 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:19,799 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:19 BoogieIcfgContainer
[2025-04-28 21:21:19,799 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:19,800 INFO  L158              Benchmark]: Toolchain (without parser) took 6962.29ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 108.6MB in the beginning and 232.1MB in the end (delta: -123.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:19,800 INFO  L158              Benchmark]: SmtParser took 0.50ms. Allocated memory is still 234.9MB. Free memory is still 169.7MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:19,800 INFO  L158              Benchmark]: ChcToBoogie took 118.09ms. Allocated memory is still 234.9MB. Free memory was 108.6MB in the beginning and 101.0MB in the end (delta: 7.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:19,800 INFO  L158              Benchmark]: Boogie Preprocessor took 191.93ms. Allocated memory is still 234.9MB. Free memory was 101.0MB in the beginning and 95.9MB in the end (delta: 5.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:19,800 INFO  L158              Benchmark]: RCFGBuilder took 1673.35ms. Allocated memory is still 234.9MB. Free memory was 95.9MB in the beginning and 163.7MB in the end (delta: -67.7MB). Peak memory consumption was 40.1MB. Max. memory is 33.6GB.
[2025-04-28 21:21:19,801 INFO  L158              Benchmark]: TraceAbstraction took 4972.83ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 162.8MB in the beginning and 232.1MB in the end (delta: -69.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:19,802 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.50ms. Allocated memory is still 234.9MB. Free memory is still 169.7MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 118.09ms. Allocated memory is still 234.9MB. Free memory was 108.6MB in the beginning and 101.0MB in the end (delta: 7.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 191.93ms. Allocated memory is still 234.9MB. Free memory was 101.0MB in the beginning and 95.9MB in the end (delta: 5.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 1673.35ms. Allocated memory is still 234.9MB. Free memory was 95.9MB in the beginning and 163.7MB in the end (delta: -67.7MB). Peak memory consumption was 40.1MB. Max. memory is 33.6GB.
 * TraceAbstraction took 4972.83ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 162.8MB in the beginning and 232.1MB in the end (delta: -69.3MB). There was no memory consumed. 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 69 procedures, 280 locations, 456 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 4.9s, OverallIterations: 9, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.1s, AutomataDifference: 1.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 50 SdHoareTripleChecker+Valid, 0.5s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 9 mSDsluCounter, 8362 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 6620 mSDsCounter, 12 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 205 IncrementalHoareTripleChecker+Invalid, 217 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 12 mSolverCounterUnsat, 1742 mSDtfsCounter, 205 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 61 GetRequests, 20 SyntacticMatches, 0 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=280occurred in iteration=0, InterpolantAutomatonStates: 58, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 9 MinimizatonAttempts, 6 StatesRemovedByMinimization, 3 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.5s SatisfiabilityAnalysisTime, 2.5s InterpolantComputationTime, 577 NumberOfCodeBlocks, 577 NumberOfCodeBlocksAsserted, 9 NumberOfCheckSat, 568 ConstructedInterpolants, 0 QuantifiedInterpolants, 754 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 9 InterpolantComputations, 9 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:19,817 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
