./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_data.sol_6_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:28:36,333 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:28:36,382 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_36ad548a-b4c7-4422-8bda-42dcb1c3c1cc/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:28:36,386 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:28:36,386 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:28:36,405 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:28:36,406 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:28:36,406 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:28:36,406 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:28:36,406 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:28:36,407 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:28:36,407 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:28:36,407 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:28:36,407 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:28:36,407 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:28:36,407 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:28:36,407 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:36,408 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:28:36,408 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:28:36,409 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:28:36,409 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:28:36,606 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:28:36,612 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:28:36,614 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:28:36,615 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:28:36,615 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:28:36,616 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_36ad548a-b4c7-4422-8bda-42dcb1c3c1cc/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_data.sol_6_no_adts_000.smt2
[2025-05-07 17:28:36,617 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:28:36,619 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:28:36,940 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_36ad548a-b4c7-4422-8bda-42dcb1c3c1cc/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_data.sol_6_no_adts_000.smt2
[2025-05-07 17:28:36,942 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:28:36,943 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:28:36,943 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:28:36,943 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:28:36,943 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:28:36,945 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:36,998 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36 Unit
[2025-05-07 17:28:36,998 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:28:36,999 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:28:36,999 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:28:36,999 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:28:37,009 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,009 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,032 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,032 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,039 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,040 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,042 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,045 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,046 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,059 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:28:37,060 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:28:37,060 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:28:37,060 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:28:37,061 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (1/1) ...
[2025-05-07 17:28:37,062 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:28:37,070 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:37,079 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-05-07 17:28:37,081 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:28:37,090 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:28:37,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_21_0 given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_21_0
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_21_0
[2025-05-07 17:28:37,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_f_55_97_0 given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_f_55_97_0
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_f_55_97_0
[2025-05-07 17:28:37,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,091 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_function_f__56_97_0
[2025-05-07 17:28:37,091 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_16_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_16_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_16_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_return_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_return_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_return_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,092 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__56_97_0
[2025-05-07 17:28:37,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_function_f__56_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_function_f__56_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_36_C_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_36_C_97_0
[2025-05-07 17:28:37,093 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_36_C_97_0
[2025-05-07 17:28:37,093 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_33_C_97_0 given in one single declaration
[2025-05-07 17:28:37,093 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_33_C_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_33_C_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_35_C_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_35_C_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_35_C_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_34_C_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_34_C_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_34_C_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_6_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_6_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_6_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_32_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure block_32_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_32_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_22_g_95_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure block_22_g_95_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_22_g_95_97_0
[2025-05-07 17:28:37,094 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_21_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,094 INFO  L130     BoogieDeclarations]: Found specification of procedure block_21_function_g__96_97_0
[2025-05-07 17:28:37,094 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_21_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_30_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_30_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_30_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_29_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_29_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_29_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_27_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_27_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_27_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_31_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_31_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_31_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_28_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_28_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_28_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_23_return_function_g__96_97_0 given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure block_23_return_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_23_return_function_g__96_97_0
[2025-05-07 17:28:37,095 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:28:37,095 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:28:37,095 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:28:37,322 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:28:37,324 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:28:37,644 INFO  L?                        ?]: Removed 608 outVars from TransFormulas that were not future-live.
[2025-05-07 17:28:37,644 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:28:37,654 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:28:37,654 INFO  L312             CfgBuilder]: Removed 27 assume(true) statements.
[2025-05-07 17:28:37,654 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:37 BoogieIcfgContainer
[2025-05-07 17:28:37,654 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:28:37,656 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:28:37,656 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:28:37,658 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:28:37,658 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:28:36" (1/3) ...
[2025-05-07 17:28:37,659 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3b4e00e1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:28:37, skipping insertion in model container
[2025-05-07 17:28:37,659 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:28:36" (2/3) ...
[2025-05-07 17:28:37,659 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3b4e00e1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:28:37, skipping insertion in model container
[2025-05-07 17:28:37,659 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:28:37" (3/3) ...
[2025-05-07 17:28:37,660 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:28:37,670 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:28:37,673 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 39 procedures, 152 locations, 256 edges, 39 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:28:37,711 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:28:37,719 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;@7eff61d8, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:28:37,719 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:28:37,723 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 152 states, 69 states have (on average 1.0579710144927537) internal successors, (73), 73 states have internal predecessors, (73), 43 states have call successors, (61), 38 states have call predecessors, (61), 38 states have return successors, (61), 40 states have call predecessors, (61), 43 states have call successors, (61)
[2025-05-07 17:28:37,730 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:37,731 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:37,731 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:37,731 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:37,735 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:37,735 INFO  L85        PathProgramCache]: Analyzing trace with hash 1176249821, now seen corresponding path program 1 times
[2025-05-07 17:28:37,740 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:37,741 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1738662472]
[2025-05-07 17:28:37,741 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:37,741 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:37,795 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:37,813 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:37,813 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:37,813 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:37,999 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:38,000 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,000 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1738662472]
[2025-05-07 17:28:38,000 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1738662472] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,001 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,003 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:38,004 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1910217228]
[2025-05-07 17:28:38,004 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,007 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:38,007 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,025 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:38,025 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:38,027 INFO  L87              Difference]: Start difference. First operand  has 152 states, 69 states have (on average 1.0579710144927537) internal successors, (73), 73 states have internal predecessors, (73), 43 states have call successors, (61), 38 states have call predecessors, (61), 38 states have return successors, (61), 40 states have call predecessors, (61), 43 states have call successors, (61) Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:38,085 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,085 INFO  L93              Difference]: Finished difference Result 154 states and 198 transitions.
[2025-05-07 17:28:38,087 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:38,089 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:28:38,089 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,095 INFO  L225             Difference]: With dead ends: 154
[2025-05-07 17:28:38,095 INFO  L226             Difference]: Without dead ends: 150
[2025-05-07 17:28:38,097 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:38,099 INFO  L437           NwaCegarLoop]: 194 mSDtfsCounter, 1 mSDsluCounter, 380 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 574 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,099 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 574 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:38,111 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 150 states.
[2025-05-07 17:28:38,130 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 150 to 148.
[2025-05-07 17:28:38,131 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 148 states, 68 states have (on average 1.0294117647058822) internal successors, (70), 70 states have internal predecessors, (70), 41 states have call successors, (59), 38 states have call predecessors, (59), 38 states have return successors, (59), 39 states have call predecessors, (59), 41 states have call successors, (59)
[2025-05-07 17:28:38,134 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 148 states to 148 states and 188 transitions.
[2025-05-07 17:28:38,135 INFO  L79                 Accepts]: Start accepts. Automaton has 148 states and 188 transitions. Word has length 51
[2025-05-07 17:28:38,135 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,135 INFO  L485      AbstractCegarLoop]: Abstraction has 148 states and 188 transitions.
[2025-05-07 17:28:38,135 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 3 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:38,136 INFO  L278                IsEmpty]: Start isEmpty. Operand 148 states and 188 transitions.
[2025-05-07 17:28:38,137 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:38,137 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,138 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,138 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:38,138 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,138 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,139 INFO  L85        PathProgramCache]: Analyzing trace with hash 1148583905, now seen corresponding path program 1 times
[2025-05-07 17:28:38,139 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,139 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1273181447]
[2025-05-07 17:28:38,139 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,139 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,162 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:38,186 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:38,187 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,187 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,367 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:38,367 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,367 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1273181447]
[2025-05-07 17:28:38,367 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1273181447] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,367 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,368 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:38,368 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [75140529]
[2025-05-07 17:28:38,368 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,369 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:38,369 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,369 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:38,369 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:38,370 INFO  L87              Difference]: Start difference. First operand 148 states and 188 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:38,410 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,410 INFO  L93              Difference]: Finished difference Result 150 states and 189 transitions.
[2025-05-07 17:28:38,411 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:38,411 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:38,412 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,413 INFO  L225             Difference]: With dead ends: 150
[2025-05-07 17:28:38,413 INFO  L226             Difference]: Without dead ends: 144
[2025-05-07 17:28:38,413 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:38,414 INFO  L437           NwaCegarLoop]: 185 mSDtfsCounter, 1 mSDsluCounter, 544 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 729 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,414 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 729 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:38,414 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 144 states.
[2025-05-07 17:28:38,421 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 144 to 144.
[2025-05-07 17:28:38,421 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 144 states, 66 states have (on average 1.0303030303030303) internal successors, (68), 68 states have internal predecessors, (68), 40 states have call successors, (57), 37 states have call predecessors, (57), 37 states have return successors, (57), 38 states have call predecessors, (57), 40 states have call successors, (57)
[2025-05-07 17:28:38,422 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 144 states to 144 states and 182 transitions.
[2025-05-07 17:28:38,422 INFO  L79                 Accepts]: Start accepts. Automaton has 144 states and 182 transitions. Word has length 51
[2025-05-07 17:28:38,423 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,423 INFO  L485      AbstractCegarLoop]: Abstraction has 144 states and 182 transitions.
[2025-05-07 17:28:38,423 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:38,423 INFO  L278                IsEmpty]: Start isEmpty. Operand 144 states and 182 transitions.
[2025-05-07 17:28:38,424 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:38,425 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,425 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,425 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:38,425 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,425 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,425 INFO  L85        PathProgramCache]: Analyzing trace with hash -1773561513, now seen corresponding path program 1 times
[2025-05-07 17:28:38,425 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,425 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1491827909]
[2025-05-07 17:28:38,425 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,426 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,444 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:38,456 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:38,456 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,456 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,568 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:38,568 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,568 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1491827909]
[2025-05-07 17:28:38,568 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1491827909] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,568 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,568 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:38,568 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [170640169]
[2025-05-07 17:28:38,568 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,569 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:38,569 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,569 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:38,569 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:38,569 INFO  L87              Difference]: Start difference. First operand 144 states and 182 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:38,605 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,605 INFO  L93              Difference]: Finished difference Result 146 states and 183 transitions.
[2025-05-07 17:28:38,606 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:38,606 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:38,606 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,607 INFO  L225             Difference]: With dead ends: 146
[2025-05-07 17:28:38,608 INFO  L226             Difference]: Without dead ends: 140
[2025-05-07 17:28:38,608 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:38,608 INFO  L437           NwaCegarLoop]: 180 mSDtfsCounter, 1 mSDsluCounter, 528 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 708 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,609 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 708 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:38,610 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-05-07 17:28:38,619 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 140.
[2025-05-07 17:28:38,619 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 39 states have call successors, (55), 36 states have call predecessors, (55), 36 states have return successors, (55), 37 states have call predecessors, (55), 39 states have call successors, (55)
[2025-05-07 17:28:38,621 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 176 transitions.
[2025-05-07 17:28:38,621 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 176 transitions. Word has length 51
[2025-05-07 17:28:38,621 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,621 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 176 transitions.
[2025-05-07 17:28:38,622 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:38,622 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 176 transitions.
[2025-05-07 17:28:38,624 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:38,624 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,624 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,624 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:38,624 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,624 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,625 INFO  L85        PathProgramCache]: Analyzing trace with hash -1374722599, now seen corresponding path program 1 times
[2025-05-07 17:28:38,625 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,625 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [297530019]
[2025-05-07 17:28:38,625 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,625 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,658 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:38,672 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:38,673 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,673 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,803 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:38,803 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,803 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [297530019]
[2025-05-07 17:28:38,803 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [297530019] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,803 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,803 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:38,804 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [160105509]
[2025-05-07 17:28:38,804 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,804 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:38,804 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,804 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:38,805 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:38,805 INFO  L87              Difference]: Start difference. First operand 140 states and 176 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:38,838 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:38,838 INFO  L93              Difference]: Finished difference Result 142 states and 177 transitions.
[2025-05-07 17:28:38,839 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:38,839 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:38,839 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:38,841 INFO  L225             Difference]: With dead ends: 142
[2025-05-07 17:28:38,841 INFO  L226             Difference]: Without dead ends: 136
[2025-05-07 17:28:38,841 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:38,842 INFO  L437           NwaCegarLoop]: 174 mSDtfsCounter, 1 mSDsluCounter, 510 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 684 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:38,842 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 684 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:38,843 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 136 states.
[2025-05-07 17:28:38,850 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 136 to 136.
[2025-05-07 17:28:38,850 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 136 states, 62 states have (on average 1.032258064516129) internal successors, (64), 64 states have internal predecessors, (64), 38 states have call successors, (53), 35 states have call predecessors, (53), 35 states have return successors, (53), 36 states have call predecessors, (53), 38 states have call successors, (53)
[2025-05-07 17:28:38,851 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 136 states to 136 states and 170 transitions.
[2025-05-07 17:28:38,851 INFO  L79                 Accepts]: Start accepts. Automaton has 136 states and 170 transitions. Word has length 51
[2025-05-07 17:28:38,852 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:38,852 INFO  L485      AbstractCegarLoop]: Abstraction has 136 states and 170 transitions.
[2025-05-07 17:28:38,852 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:38,852 INFO  L278                IsEmpty]: Start isEmpty. Operand 136 states and 170 transitions.
[2025-05-07 17:28:38,853 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:38,853 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:38,853 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:38,853 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:38,853 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:38,854 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:38,854 INFO  L85        PathProgramCache]: Analyzing trace with hash -1484763833, now seen corresponding path program 1 times
[2025-05-07 17:28:38,854 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:38,854 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1203711505]
[2025-05-07 17:28:38,854 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:38,854 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:38,876 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:38,889 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:38,889 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:38,889 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:38,994 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:38,994 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:38,994 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1203711505]
[2025-05-07 17:28:38,994 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1203711505] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:38,994 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:38,994 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:38,994 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [724161849]
[2025-05-07 17:28:38,994 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:38,995 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:38,995 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:38,995 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:38,995 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:38,995 INFO  L87              Difference]: Start difference. First operand 136 states and 170 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,026 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,026 INFO  L93              Difference]: Finished difference Result 138 states and 171 transitions.
[2025-05-07 17:28:39,027 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:39,027 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,027 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,028 INFO  L225             Difference]: With dead ends: 138
[2025-05-07 17:28:39,028 INFO  L226             Difference]: Without dead ends: 132
[2025-05-07 17:28:39,028 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:39,028 INFO  L437           NwaCegarLoop]: 168 mSDtfsCounter, 1 mSDsluCounter, 492 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 660 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,029 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 660 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,029 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-05-07 17:28:39,032 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 132.
[2025-05-07 17:28:39,033 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 132 states, 60 states have (on average 1.0333333333333334) internal successors, (62), 62 states have internal predecessors, (62), 37 states have call successors, (51), 34 states have call predecessors, (51), 34 states have return successors, (51), 35 states have call predecessors, (51), 37 states have call successors, (51)
[2025-05-07 17:28:39,033 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 132 states to 132 states and 164 transitions.
[2025-05-07 17:28:39,034 INFO  L79                 Accepts]: Start accepts. Automaton has 132 states and 164 transitions. Word has length 51
[2025-05-07 17:28:39,034 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,034 INFO  L485      AbstractCegarLoop]: Abstraction has 132 states and 164 transitions.
[2025-05-07 17:28:39,034 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,034 INFO  L278                IsEmpty]: Start isEmpty. Operand 132 states and 164 transitions.
[2025-05-07 17:28:39,034 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,035 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,035 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,035 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:39,035 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,035 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,035 INFO  L85        PathProgramCache]: Analyzing trace with hash 108599557, now seen corresponding path program 1 times
[2025-05-07 17:28:39,035 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,035 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1337198928]
[2025-05-07 17:28:39,035 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,035 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,054 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,061 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,061 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,061 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,166 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,166 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,166 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1337198928]
[2025-05-07 17:28:39,166 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1337198928] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,166 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,166 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:39,166 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [487763195]
[2025-05-07 17:28:39,166 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,166 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:39,166 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,167 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:39,167 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:39,167 INFO  L87              Difference]: Start difference. First operand 132 states and 164 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,196 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,196 INFO  L93              Difference]: Finished difference Result 134 states and 165 transitions.
[2025-05-07 17:28:39,196 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:39,196 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,197 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,197 INFO  L225             Difference]: With dead ends: 134
[2025-05-07 17:28:39,197 INFO  L226             Difference]: Without dead ends: 128
[2025-05-07 17:28:39,197 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:39,198 INFO  L437           NwaCegarLoop]: 162 mSDtfsCounter, 1 mSDsluCounter, 474 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 636 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,198 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 636 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,198 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 128 states.
[2025-05-07 17:28:39,201 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 128 to 128.
[2025-05-07 17:28:39,201 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 58 states have (on average 1.0344827586206897) internal successors, (60), 60 states have internal predecessors, (60), 36 states have call successors, (49), 33 states have call predecessors, (49), 33 states have return successors, (49), 34 states have call predecessors, (49), 36 states have call successors, (49)
[2025-05-07 17:28:39,202 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 158 transitions.
[2025-05-07 17:28:39,202 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 158 transitions. Word has length 51
[2025-05-07 17:28:39,202 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,202 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 158 transitions.
[2025-05-07 17:28:39,202 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,202 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 158 transitions.
[2025-05-07 17:28:39,203 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,203 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,203 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,203 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:39,203 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,203 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,203 INFO  L85        PathProgramCache]: Analyzing trace with hash -63275755, now seen corresponding path program 1 times
[2025-05-07 17:28:39,203 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,203 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1207851069]
[2025-05-07 17:28:39,203 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,203 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,221 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,227 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,227 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,227 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,319 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,319 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,319 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1207851069]
[2025-05-07 17:28:39,319 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1207851069] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,320 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,320 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:39,320 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [126991106]
[2025-05-07 17:28:39,320 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,320 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:39,320 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,320 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:39,320 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:39,321 INFO  L87              Difference]: Start difference. First operand 128 states and 158 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,349 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,349 INFO  L93              Difference]: Finished difference Result 130 states and 159 transitions.
[2025-05-07 17:28:39,349 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:39,349 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,350 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,351 INFO  L225             Difference]: With dead ends: 130
[2025-05-07 17:28:39,351 INFO  L226             Difference]: Without dead ends: 124
[2025-05-07 17:28:39,351 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:39,351 INFO  L437           NwaCegarLoop]: 156 mSDtfsCounter, 1 mSDsluCounter, 456 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 612 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,351 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 612 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,352 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-05-07 17:28:39,354 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 124.
[2025-05-07 17:28:39,355 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 124 states, 56 states have (on average 1.0357142857142858) internal successors, (58), 58 states have internal predecessors, (58), 35 states have call successors, (47), 32 states have call predecessors, (47), 32 states have return successors, (47), 33 states have call predecessors, (47), 35 states have call successors, (47)
[2025-05-07 17:28:39,355 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 124 states to 124 states and 152 transitions.
[2025-05-07 17:28:39,355 INFO  L79                 Accepts]: Start accepts. Automaton has 124 states and 152 transitions. Word has length 51
[2025-05-07 17:28:39,355 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,355 INFO  L485      AbstractCegarLoop]: Abstraction has 124 states and 152 transitions.
[2025-05-07 17:28:39,356 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,356 INFO  L278                IsEmpty]: Start isEmpty. Operand 124 states and 152 transitions.
[2025-05-07 17:28:39,356 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,356 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,356 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,356 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:28:39,356 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,357 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,357 INFO  L85        PathProgramCache]: Analyzing trace with hash -2077253225, now seen corresponding path program 1 times
[2025-05-07 17:28:39,357 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,357 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [81162979]
[2025-05-07 17:28:39,357 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,357 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,373 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,380 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,380 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,380 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,482 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,483 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,483 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [81162979]
[2025-05-07 17:28:39,483 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [81162979] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,483 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,483 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:39,483 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [334247086]
[2025-05-07 17:28:39,483 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,483 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:39,484 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,484 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:39,484 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:39,484 INFO  L87              Difference]: Start difference. First operand 124 states and 152 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,511 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,511 INFO  L93              Difference]: Finished difference Result 126 states and 153 transitions.
[2025-05-07 17:28:39,512 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:39,512 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,512 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,513 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:28:39,513 INFO  L226             Difference]: Without dead ends: 120
[2025-05-07 17:28:39,513 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:39,513 INFO  L437           NwaCegarLoop]: 150 mSDtfsCounter, 1 mSDsluCounter, 438 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 588 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,513 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 588 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,514 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-05-07 17:28:39,516 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 120.
[2025-05-07 17:28:39,516 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 120 states, 54 states have (on average 1.037037037037037) internal successors, (56), 56 states have internal predecessors, (56), 34 states have call successors, (45), 31 states have call predecessors, (45), 31 states have return successors, (45), 32 states have call predecessors, (45), 34 states have call successors, (45)
[2025-05-07 17:28:39,517 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 120 states to 120 states and 146 transitions.
[2025-05-07 17:28:39,517 INFO  L79                 Accepts]: Start accepts. Automaton has 120 states and 146 transitions. Word has length 51
[2025-05-07 17:28:39,517 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,517 INFO  L485      AbstractCegarLoop]: Abstraction has 120 states and 146 transitions.
[2025-05-07 17:28:39,517 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,517 INFO  L278                IsEmpty]: Start isEmpty. Operand 120 states and 146 transitions.
[2025-05-07 17:28:39,518 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,518 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,518 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,518 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:28:39,518 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,518 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,518 INFO  L85        PathProgramCache]: Analyzing trace with hash -1132405921, now seen corresponding path program 1 times
[2025-05-07 17:28:39,518 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,518 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1291671369]
[2025-05-07 17:28:39,518 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,519 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,535 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,541 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,541 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,541 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,592 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,592 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,592 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1291671369]
[2025-05-07 17:28:39,592 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1291671369] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,592 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,592 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:39,592 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [306859006]
[2025-05-07 17:28:39,592 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,592 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:39,592 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,593 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:39,593 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:39,593 INFO  L87              Difference]: Start difference. First operand 120 states and 146 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,622 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,622 INFO  L93              Difference]: Finished difference Result 124 states and 150 transitions.
[2025-05-07 17:28:39,623 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:39,623 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,623 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,624 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:28:39,624 INFO  L226             Difference]: Without dead ends: 124
[2025-05-07 17:28:39,624 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:39,624 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 571 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 717 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-05-07 17:28:39,625 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 717 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,625 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-05-07 17:28:39,628 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 124.
[2025-05-07 17:28:39,628 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 124 states, 56 states have (on average 1.0357142857142858) internal successors, (58), 58 states have internal predecessors, (58), 34 states have call successors, (45), 31 states have call predecessors, (45), 33 states have return successors, (47), 34 states have call predecessors, (47), 34 states have call successors, (47)
[2025-05-07 17:28:39,629 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 124 states to 124 states and 150 transitions.
[2025-05-07 17:28:39,629 INFO  L79                 Accepts]: Start accepts. Automaton has 124 states and 150 transitions. Word has length 51
[2025-05-07 17:28:39,629 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,629 INFO  L485      AbstractCegarLoop]: Abstraction has 124 states and 150 transitions.
[2025-05-07 17:28:39,629 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,629 INFO  L278                IsEmpty]: Start isEmpty. Operand 124 states and 150 transitions.
[2025-05-07 17:28:39,630 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,630 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,630 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,630 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:28:39,630 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,630 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,630 INFO  L85        PathProgramCache]: Analyzing trace with hash -329103911, now seen corresponding path program 1 times
[2025-05-07 17:28:39,630 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,630 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1652870143]
[2025-05-07 17:28:39,630 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,630 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,649 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,655 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,655 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,656 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,774 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,774 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,774 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1652870143]
[2025-05-07 17:28:39,774 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1652870143] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,774 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,774 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-05-07 17:28:39,774 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [85799044]
[2025-05-07 17:28:39,774 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,774 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:28:39,775 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,775 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:28:39,775 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:28:39,775 INFO  L87              Difference]: Start difference. First operand 124 states and 150 transitions. Second operand  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,803 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,803 INFO  L93              Difference]: Finished difference Result 126 states and 151 transitions.
[2025-05-07 17:28:39,803 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:28:39,803 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,804 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,804 INFO  L225             Difference]: With dead ends: 126
[2025-05-07 17:28:39,804 INFO  L226             Difference]: Without dead ends: 120
[2025-05-07 17:28:39,804 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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-05-07 17:28:39,805 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 1 mSDsluCounter, 420 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 564 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:39,805 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 564 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,806 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-05-07 17:28:39,809 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 120.
[2025-05-07 17:28:39,810 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 120 states, 54 states have (on average 1.037037037037037) internal successors, (56), 56 states have internal predecessors, (56), 33 states have call successors, (43), 30 states have call predecessors, (43), 32 states have return successors, (45), 33 states have call predecessors, (45), 33 states have call successors, (45)
[2025-05-07 17:28:39,810 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 120 states to 120 states and 144 transitions.
[2025-05-07 17:28:39,811 INFO  L79                 Accepts]: Start accepts. Automaton has 120 states and 144 transitions. Word has length 51
[2025-05-07 17:28:39,811 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,811 INFO  L485      AbstractCegarLoop]: Abstraction has 120 states and 144 transitions.
[2025-05-07 17:28:39,811 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 5.75) internal successors, (23), 5 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 4 states have return successors, (14), 5 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,811 INFO  L278                IsEmpty]: Start isEmpty. Operand 120 states and 144 transitions.
[2025-05-07 17:28:39,812 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,812 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,812 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,812 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:28:39,812 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,812 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,813 INFO  L85        PathProgramCache]: Analyzing trace with hash -883011583, now seen corresponding path program 1 times
[2025-05-07 17:28:39,813 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,813 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1267093032]
[2025-05-07 17:28:39,813 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,813 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,832 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,838 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,838 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,838 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:39,886 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:39,886 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:39,886 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1267093032]
[2025-05-07 17:28:39,886 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1267093032] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:39,886 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:39,887 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:39,887 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1373531684]
[2025-05-07 17:28:39,887 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:39,887 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:39,887 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:39,887 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:39,887 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:39,888 INFO  L87              Difference]: Start difference. First operand 120 states and 144 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,916 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:39,916 INFO  L93              Difference]: Finished difference Result 124 states and 148 transitions.
[2025-05-07 17:28:39,917 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:39,917 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 3 states have call successors, (14) Word has length 51
[2025-05-07 17:28:39,917 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:39,918 INFO  L225             Difference]: With dead ends: 124
[2025-05-07 17:28:39,918 INFO  L226             Difference]: Without dead ends: 124
[2025-05-07 17:28:39,918 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:39,918 INFO  L437           NwaCegarLoop]: 138 mSDtfsCounter, 1 mSDsluCounter, 542 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 680 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-05-07 17:28:39,918 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 680 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:39,919 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-05-07 17:28:39,923 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 120.
[2025-05-07 17:28:39,923 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 120 states, 54 states have (on average 1.037037037037037) internal successors, (56), 56 states have internal predecessors, (56), 33 states have call successors, (43), 30 states have call predecessors, (43), 32 states have return successors, (45), 33 states have call predecessors, (45), 33 states have call successors, (45)
[2025-05-07 17:28:39,924 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 120 states to 120 states and 144 transitions.
[2025-05-07 17:28:39,924 INFO  L79                 Accepts]: Start accepts. Automaton has 120 states and 144 transitions. Word has length 51
[2025-05-07 17:28:39,924 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:39,924 INFO  L485      AbstractCegarLoop]: Abstraction has 120 states and 144 transitions.
[2025-05-07 17:28:39,924 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 3 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 3 states have call successors, (14)
[2025-05-07 17:28:39,925 INFO  L278                IsEmpty]: Start isEmpty. Operand 120 states and 144 transitions.
[2025-05-07 17:28:39,926 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:28:39,926 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:39,926 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:39,926 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:28:39,926 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:39,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:39,926 INFO  L85        PathProgramCache]: Analyzing trace with hash -1234185295, now seen corresponding path program 1 times
[2025-05-07 17:28:39,926 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:39,926 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1275788426]
[2025-05-07 17:28:39,926 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:39,927 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:39,948 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:28:39,958 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:28:39,958 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:39,958 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:40,126 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:28:40,127 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:40,127 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1275788426]
[2025-05-07 17:28:40,127 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1275788426] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:40,127 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:40,127 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-05-07 17:28:40,127 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [332810518]
[2025-05-07 17:28:40,127 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:40,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-05-07 17:28:40,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:40,128 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-05-07 17:28:40,128 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:40,128 INFO  L87              Difference]: Start difference. First operand 120 states and 144 transitions. Second operand  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:40,188 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:40,188 INFO  L93              Difference]: Finished difference Result 114 states and 138 transitions.
[2025-05-07 17:28:40,188 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-05-07 17:28:40,189 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 4 states have call successors, (14) Word has length 51
[2025-05-07 17:28:40,189 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:40,189 INFO  L225             Difference]: With dead ends: 114
[2025-05-07 17:28:40,189 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:40,189 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:28:40,190 INFO  L437           NwaCegarLoop]: 132 mSDtfsCounter, 0 mSDsluCounter, 644 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 776 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:40,190 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 776 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:40,190 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:40,190 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:40,190 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-05-07 17:28:40,190 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:40,190 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 51
[2025-05-07 17:28:40,190 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:40,190 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:40,191 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 3.8333333333333335) internal successors, (23), 8 states have internal predecessors, (23), 4 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 4 states have call successors, (14)
[2025-05-07 17:28:40,191 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:40,191 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:40,193 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:40,194 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:28:40,197 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:40,199 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:40,202 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:40 BoogieIcfgContainer
[2025-05-07 17:28:40,202 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:40,203 INFO  L158              Benchmark]: Toolchain (without parser) took 3259.94ms. Allocated memory is still 234.9MB. Free memory was 125.9MB in the beginning and 166.0MB in the end (delta: -40.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:40,203 INFO  L158              Benchmark]: SmtParser took 0.20ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:40,203 INFO  L158              Benchmark]: ChcToBoogie took 54.94ms. Allocated memory is still 234.9MB. Free memory was 125.9MB in the beginning and 193.6MB in the end (delta: -67.7MB). Peak memory consumption was 25.6MB. Max. memory is 33.6GB.
[2025-05-07 17:28:40,203 INFO  L158              Benchmark]: Boogie Preprocessor took 60.92ms. Allocated memory is still 234.9MB. Free memory was 193.0MB in the beginning and 188.6MB in the end (delta: 4.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:40,203 INFO  L158              Benchmark]: RCFGBuilder took 594.51ms. Allocated memory is still 234.9MB. Free memory was 188.6MB in the beginning and 120.9MB in the end (delta: 67.7MB). Peak memory consumption was 67.1MB. Max. memory is 33.6GB.
[2025-05-07 17:28:40,204 INFO  L158              Benchmark]: TraceAbstraction took 2546.53ms. Allocated memory is still 234.9MB. Free memory was 120.3MB in the beginning and 166.0MB in the end (delta: -45.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:40,205 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.20ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 54.94ms. Allocated memory is still 234.9MB. Free memory was 125.9MB in the beginning and 193.6MB in the end (delta: -67.7MB). Peak memory consumption was 25.6MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 60.92ms. Allocated memory is still 234.9MB. Free memory was 193.0MB in the beginning and 188.6MB in the end (delta: 4.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 594.51ms. Allocated memory is still 234.9MB. Free memory was 188.6MB in the beginning and 120.9MB in the end (delta: 67.7MB). Peak memory consumption was 67.1MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2546.53ms. Allocated memory is still 234.9MB. Free memory was 120.3MB in the beginning and 166.0MB in the end (delta: -45.8MB). 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 39 procedures, 152 locations, 256 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.5s, OverallIterations: 12, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 22 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 11 mSDsluCounter, 7928 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 5999 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 197 IncrementalHoareTripleChecker+Invalid, 197 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 1929 mSDtfsCounter, 197 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 64 GetRequests, 24 SyntacticMatches, 0 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=152occurred in iteration=0, InterpolantAutomatonStates: 64, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 12 MinimizatonAttempts, 6 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 1.4s InterpolantComputationTime, 612 NumberOfCodeBlocks, 612 NumberOfCodeBlocksAsserted, 12 NumberOfCheckSat, 600 ConstructedInterpolants, 0 QuantifiedInterpolants, 863 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 12 InterpolantComputations, 12 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:28:40,216 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
