./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_4.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:29:26,493 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:29:26,543 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2157b465-5f86-42e4-862d-dc0da104ec8a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:29:26,547 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:29:26,547 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:29:26,564 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:29:26,565 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:29:26,565 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:29:26,565 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:29:26,565 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:29:26,566 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:29:26,566 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:29:26,566 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:29:26,566 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:29:26,566 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:29:26,566 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:29:26,566 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:29:26,566 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:29:26,566 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:26,567 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:29:26,567 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:29:26,567 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:29:26,567 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:29:26,567 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:29:26,567 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:29:26,568 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:29:26,568 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:29:26,767 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:29:26,775 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:29:26,777 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:29:26,778 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:29:26,778 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:29:26,779 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2157b465-5f86-42e4-862d-dc0da104ec8a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_4.sol_0_no_adts_000.smt2
[2025-05-07 17:29:26,780 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:29:26,784 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:29:27,126 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2157b465-5f86-42e4-862d-dc0da104ec8a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_4.sol_0_no_adts_000.smt2
[2025-05-07 17:29:27,128 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:29:27,130 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:29:27,130 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:29:27,130 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:29:27,131 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:29:27,133 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,174 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27 Unit
[2025-05-07 17:29:27,175 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:29:27,175 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:29:27,176 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:29:27,176 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:29:27,190 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,190 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,212 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,212 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,216 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,217 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,219 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,223 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,226 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,247 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:29:27,248 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:29:27,248 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:29:27,248 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:29:27,249 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (1/1) ...
[2025-05-07 17:29:27,252 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:27,266 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:27,276 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:29:27,278 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:29:27,293 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:29:27,293 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:29:27,293 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:29:27,293 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_2_0 given in one single declaration
[2025-05-07 17:29:27,293 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_2_0
[2025-05-07 17:29:27,293 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_2_0
[2025-05-07 17:29:27,293 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_11_A_53_0 given in one single declaration
[2025-05-07 17:29:27,293 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_11_A_53_0
[2025-05-07 17:29:27,293 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_11_A_53_0
[2025-05-07 17:29:27,294 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_45_B_26_0 given in one single declaration
[2025-05-07 17:29:27,294 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_45_B_26_0
[2025-05-07 17:29:27,294 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_45_B_26_0
[2025-05-07 17:29:27,294 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_13_constructor_25_53_0 given in one single declaration
[2025-05-07 17:29:27,294 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_13_constructor_25_53_0
[2025-05-07 17:29:27,294 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_13_constructor_25_53_0
[2025-05-07 17:29:27,294 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_44_return_constructor_25_53_0 given in one single declaration
[2025-05-07 17:29:27,294 INFO  L130     BoogieDeclarations]: Found specification of procedure block_44_return_constructor_25_53_0
[2025-05-07 17:29:27,294 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_44_return_constructor_25_53_0
[2025-05-07 17:29:27,294 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_43__24_53_0 given in one single declaration
[2025-05-07 17:29:27,294 INFO  L130     BoogieDeclarations]: Found specification of procedure block_43__24_53_0
[2025-05-07 17:29:27,294 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_43__24_53_0
[2025-05-07 17:29:27,295 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_42_constructor_25_53_0 given in one single declaration
[2025-05-07 17:29:27,295 INFO  L130     BoogieDeclarations]: Found specification of procedure block_42_constructor_25_53_0
[2025-05-07 17:29:27,295 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_42_constructor_25_53_0
[2025-05-07 17:29:27,295 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_47_B_26_0 given in one single declaration
[2025-05-07 17:29:27,295 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_47_B_26_0
[2025-05-07 17:29:27,295 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_47_B_26_0
[2025-05-07 17:29:27,295 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_46_B_26_0 given in one single declaration
[2025-05-07 17:29:27,295 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_46_B_26_0
[2025-05-07 17:29:27,295 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_46_B_26_0
[2025-05-07 17:29:27,295 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_39_A_53_0 given in one single declaration
[2025-05-07 17:29:27,295 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_39_A_53_0
[2025-05-07 17:29:27,295 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_39_A_53_0
[2025-05-07 17:29:27,295 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_41_A_53_0 given in one single declaration
[2025-05-07 17:29:27,295 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_41_A_53_0
[2025-05-07 17:29:27,295 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_41_A_53_0
[2025-05-07 17:29:27,295 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_40_A_53_0 given in one single declaration
[2025-05-07 17:29:27,296 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_40_A_53_0
[2025-05-07 17:29:27,296 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_40_A_53_0
[2025-05-07 17:29:27,296 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_14_constructor_52_53_0 given in one single declaration
[2025-05-07 17:29:27,296 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_14_constructor_52_53_0
[2025-05-07 17:29:27,296 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_14_constructor_52_53_0
[2025-05-07 17:29:27,296 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_38_constructor_52_53_0 given in one single declaration
[2025-05-07 17:29:27,296 INFO  L130     BoogieDeclarations]: Found specification of procedure block_38_constructor_52_53_0
[2025-05-07 17:29:27,296 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_38_constructor_52_53_0
[2025-05-07 17:29:27,296 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_36__51_53_0 given in one single declaration
[2025-05-07 17:29:27,296 INFO  L130     BoogieDeclarations]: Found specification of procedure block_36__51_53_0
[2025-05-07 17:29:27,296 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_36__51_53_0
[2025-05-07 17:29:27,296 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_35_constructor_52_53_0 given in one single declaration
[2025-05-07 17:29:27,296 INFO  L130     BoogieDeclarations]: Found specification of procedure block_35_constructor_52_53_0
[2025-05-07 17:29:27,297 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_35_constructor_52_53_0
[2025-05-07 17:29:27,297 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_37_return_constructor_52_53_0 given in one single declaration
[2025-05-07 17:29:27,297 INFO  L130     BoogieDeclarations]: Found specification of procedure block_37_return_constructor_52_53_0
[2025-05-07 17:29:27,297 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_37_return_constructor_52_53_0
[2025-05-07 17:29:27,297 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_54_A_53_0 given in one single declaration
[2025-05-07 17:29:27,297 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_54_A_53_0
[2025-05-07 17:29:27,297 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_54_A_53_0
[2025-05-07 17:29:27,297 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_51_C_13_0 given in one single declaration
[2025-05-07 17:29:27,297 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_51_C_13_0
[2025-05-07 17:29:27,297 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_51_C_13_0
[2025-05-07 17:29:27,297 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_53_C_13_0 given in one single declaration
[2025-05-07 17:29:27,297 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_53_C_13_0
[2025-05-07 17:29:27,297 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_53_C_13_0
[2025-05-07 17:29:27,297 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_52_C_13_0 given in one single declaration
[2025-05-07 17:29:27,297 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_52_C_13_0
[2025-05-07 17:29:27,298 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_52_C_13_0
[2025-05-07 17:29:27,298 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_12_constructor_12_53_0 given in one single declaration
[2025-05-07 17:29:27,298 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_12_constructor_12_53_0
[2025-05-07 17:29:27,298 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_12_constructor_12_53_0
[2025-05-07 17:29:27,298 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_50_return_constructor_12_53_0 given in one single declaration
[2025-05-07 17:29:27,298 INFO  L130     BoogieDeclarations]: Found specification of procedure block_50_return_constructor_12_53_0
[2025-05-07 17:29:27,298 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_50_return_constructor_12_53_0
[2025-05-07 17:29:27,298 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_49__11_53_0 given in one single declaration
[2025-05-07 17:29:27,298 INFO  L130     BoogieDeclarations]: Found specification of procedure block_49__11_53_0
[2025-05-07 17:29:27,298 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_49__11_53_0
[2025-05-07 17:29:27,298 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_48_constructor_12_53_0 given in one single declaration
[2025-05-07 17:29:27,298 INFO  L130     BoogieDeclarations]: Found specification of procedure block_48_constructor_12_53_0
[2025-05-07 17:29:27,298 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_48_constructor_12_53_0
[2025-05-07 17:29:27,298 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:29:27,299 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:29:27,299 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:29:27,451 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:29:27,452 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:29:27,677 INFO  L?                        ?]: Removed 254 outVars from TransFormulas that were not future-live.
[2025-05-07 17:29:27,677 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:29:27,687 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:29:27,687 INFO  L312             CfgBuilder]: Removed 11 assume(true) statements.
[2025-05-07 17:29:27,687 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:27 BoogieIcfgContainer
[2025-05-07 17:29:27,687 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:29:27,689 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:29:27,689 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:29:27,691 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:29:27,692 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:27" (1/3) ...
[2025-05-07 17:29:27,692 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@72316d93 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:29:27, skipping insertion in model container
[2025-05-07 17:29:27,692 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:27" (2/3) ...
[2025-05-07 17:29:27,692 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@72316d93 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:29:27, skipping insertion in model container
[2025-05-07 17:29:27,692 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:27" (3/3) ...
[2025-05-07 17:29:27,693 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:29:27,703 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:29:27,705 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 27 procedures, 113 locations, 177 edges, 27 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:29:27,739 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:29:27,750 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;@71608eed, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:29:27,751 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:29:27,754 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 113 states, 44 states have (on average 1.1590909090909092) internal successors, (51), 51 states have internal predecessors, (51), 41 states have call successors, (42), 26 states have call predecessors, (42), 26 states have return successors, (42), 35 states have call predecessors, (42), 41 states have call successors, (42)
[2025-05-07 17:29:27,763 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:27,763 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:27,763 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:27,764 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:27,767 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:27,767 INFO  L85        PathProgramCache]: Analyzing trace with hash 1019045098, now seen corresponding path program 1 times
[2025-05-07 17:29:27,773 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:27,773 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1355283382]
[2025-05-07 17:29:27,773 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:27,774 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:27,813 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:27,888 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:27,888 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:27,888 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,089 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:29:28,090 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,090 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1355283382]
[2025-05-07 17:29:28,090 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1355283382] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,090 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,092 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:28,094 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1580998988]
[2025-05-07 17:29:28,094 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,097 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:28,097 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,130 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:28,131 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:28,132 INFO  L87              Difference]: Start difference. First operand  has 113 states, 44 states have (on average 1.1590909090909092) internal successors, (51), 51 states have internal predecessors, (51), 41 states have call successors, (42), 26 states have call predecessors, (42), 26 states have return successors, (42), 35 states have call predecessors, (42), 41 states have call successors, (42) Second operand  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:29:28,224 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,225 INFO  L93              Difference]: Finished difference Result 110 states and 130 transitions.
[2025-05-07 17:29:28,226 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:28,228 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:29:28,228 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,235 INFO  L225             Difference]: With dead ends: 110
[2025-05-07 17:29:28,236 INFO  L226             Difference]: Without dead ends: 109
[2025-05-07 17:29:28,237 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:29:28,240 INFO  L437           NwaCegarLoop]: 127 mSDtfsCounter, 0 mSDsluCounter, 493 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 620 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,241 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 620 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,255 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 109 states.
[2025-05-07 17:29:28,276 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 109 to 109.
[2025-05-07 17:29:28,277 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 109 states, 43 states have (on average 1.1162790697674418) internal successors, (48), 48 states have internal predecessors, (48), 39 states have call successors, (40), 26 states have call predecessors, (40), 26 states have return successors, (40), 34 states have call predecessors, (40), 39 states have call successors, (40)
[2025-05-07 17:29:28,282 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 109 states to 109 states and 128 transitions.
[2025-05-07 17:29:28,283 INFO  L79                 Accepts]: Start accepts. Automaton has 109 states and 128 transitions. Word has length 41
[2025-05-07 17:29:28,283 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,284 INFO  L485      AbstractCegarLoop]: Abstraction has 109 states and 128 transitions.
[2025-05-07 17:29:28,284 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.8) internal successors, (19), 6 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:29:28,284 INFO  L278                IsEmpty]: Start isEmpty. Operand 109 states and 128 transitions.
[2025-05-07 17:29:28,286 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:29:28,286 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,286 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,286 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:29:28,287 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,287 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,287 INFO  L85        PathProgramCache]: Analyzing trace with hash 1417215854, now seen corresponding path program 1 times
[2025-05-07 17:29:28,287 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,287 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [518245615]
[2025-05-07 17:29:28,288 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,288 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,309 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:29:28,319 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:29:28,319 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,319 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,398 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:29:28,399 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,399 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [518245615]
[2025-05-07 17:29:28,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [518245615] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,399 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:28,399 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1649072230]
[2025-05-07 17:29:28,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,400 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:28,400 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,401 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:28,401 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:28,401 INFO  L87              Difference]: Start difference. First operand 109 states and 128 transitions. Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:29:28,454 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,454 INFO  L93              Difference]: Finished difference Result 110 states and 127 transitions.
[2025-05-07 17:29:28,455 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:28,455 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:29:28,455 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,457 INFO  L225             Difference]: With dead ends: 110
[2025-05-07 17:29:28,457 INFO  L226             Difference]: Without dead ends: 109
[2025-05-07 17:29:28,457 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:29:28,458 INFO  L437           NwaCegarLoop]: 121 mSDtfsCounter, 1 mSDsluCounter, 224 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 345 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,458 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 345 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,459 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 109 states.
[2025-05-07 17:29:28,468 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 109 to 107.
[2025-05-07 17:29:28,468 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 43 states have (on average 1.0930232558139534) internal successors, (47), 47 states have internal predecessors, (47), 37 states have call successors, (38), 26 states have call predecessors, (38), 26 states have return successors, (38), 33 states have call predecessors, (38), 37 states have call successors, (38)
[2025-05-07 17:29:28,470 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 123 transitions.
[2025-05-07 17:29:28,470 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 123 transitions. Word has length 41
[2025-05-07 17:29:28,471 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,471 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 123 transitions.
[2025-05-07 17:29:28,471 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:29:28,471 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 123 transitions.
[2025-05-07 17:29:28,473 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:29:28,473 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,473 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,473 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:28,474 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,474 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,474 INFO  L85        PathProgramCache]: Analyzing trace with hash -1971175304, now seen corresponding path program 1 times
[2025-05-07 17:29:28,474 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,474 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1127395696]
[2025-05-07 17:29:28,474 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,474 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,498 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:29:28,520 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:29:28,520 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,520 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,620 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:29:28,620 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,620 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1127395696]
[2025-05-07 17:29:28,620 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1127395696] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,620 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,620 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:29:28,620 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1890191213]
[2025-05-07 17:29:28,620 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,621 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:29:28,621 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,621 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:29:28,621 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:29:28,622 INFO  L87              Difference]: Start difference. First operand 107 states and 123 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:28,668 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,668 INFO  L93              Difference]: Finished difference Result 107 states and 122 transitions.
[2025-05-07 17:29:28,668 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:28,669 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:29:28,669 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,670 INFO  L225             Difference]: With dead ends: 107
[2025-05-07 17:29:28,670 INFO  L226             Difference]: Without dead ends: 105
[2025-05-07 17:29:28,670 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:29:28,671 INFO  L437           NwaCegarLoop]: 119 mSDtfsCounter, 0 mSDsluCounter, 461 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 580 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,671 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 580 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,672 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 105 states.
[2025-05-07 17:29:28,678 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 105 to 105.
[2025-05-07 17:29:28,678 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 43 states have (on average 1.069767441860465) internal successors, (46), 46 states have internal predecessors, (46), 35 states have call successors, (36), 26 states have call predecessors, (36), 26 states have return successors, (36), 32 states have call predecessors, (36), 35 states have call successors, (36)
[2025-05-07 17:29:28,680 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 118 transitions.
[2025-05-07 17:29:28,680 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 118 transitions. Word has length 66
[2025-05-07 17:29:28,681 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,681 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 118 transitions.
[2025-05-07 17:29:28,681 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:28,681 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 118 transitions.
[2025-05-07 17:29:28,682 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:29:28,682 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,683 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:28,683 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,683 INFO  L85        PathProgramCache]: Analyzing trace with hash -895440388, now seen corresponding path program 1 times
[2025-05-07 17:29:28,684 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,684 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2032871033]
[2025-05-07 17:29:28,684 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,709 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:29:28,719 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:29:28,719 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,719 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,783 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:29:28,783 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,783 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2032871033]
[2025-05-07 17:29:28,783 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2032871033] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,783 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,783 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:28,783 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [378056462]
[2025-05-07 17:29:28,783 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,783 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:28,784 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,784 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:28,784 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:28,784 INFO  L87              Difference]: Start difference. First operand 105 states and 118 transitions. Second operand  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 4 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:28,818 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,818 INFO  L93              Difference]: Finished difference Result 106 states and 117 transitions.
[2025-05-07 17:29:28,818 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:28,818 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 4 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:29:28,819 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,820 INFO  L225             Difference]: With dead ends: 106
[2025-05-07 17:29:28,820 INFO  L226             Difference]: Without dead ends: 104
[2025-05-07 17:29:28,820 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:29:28,821 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 1 mSDsluCounter, 209 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 321 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:28,821 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 321 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,822 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 104 states.
[2025-05-07 17:29:28,828 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 104 to 102.
[2025-05-07 17:29:28,829 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 43 states have (on average 1.0465116279069768) internal successors, (45), 45 states have internal predecessors, (45), 32 states have call successors, (33), 26 states have call predecessors, (33), 26 states have return successors, (33), 30 states have call predecessors, (33), 32 states have call successors, (33)
[2025-05-07 17:29:28,829 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 111 transitions.
[2025-05-07 17:29:28,830 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 111 transitions. Word has length 66
[2025-05-07 17:29:28,830 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,830 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 111 transitions.
[2025-05-07 17:29:28,830 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 4 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:28,830 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 111 transitions.
[2025-05-07 17:29:28,831 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:29:28,831 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,831 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,831 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:29:28,832 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,832 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,832 INFO  L85        PathProgramCache]: Analyzing trace with hash -1309905506, now seen corresponding path program 1 times
[2025-05-07 17:29:28,832 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,832 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1138559667]
[2025-05-07 17:29:28,832 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,832 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,868 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:29:28,871 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:29:28,872 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,872 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,952 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:29:28,952 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,952 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1138559667]
[2025-05-07 17:29:28,952 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1138559667] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,952 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,952 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:28,952 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1097381931]
[2025-05-07 17:29:28,952 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,953 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:28,953 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,953 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:28,953 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:28,954 INFO  L87              Difference]: Start difference. First operand 102 states and 111 transitions. Second operand  has 4 states, 3 states have (on average 13.666666666666666) internal successors, (41), 4 states have internal predecessors, (41), 3 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 3 states have call predecessors, (25), 3 states have call successors, (25)
[2025-05-07 17:29:28,962 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:28,962 INFO  L93              Difference]: Finished difference Result 104 states and 112 transitions.
[2025-05-07 17:29:28,962 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:28,962 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 13.666666666666666) internal successors, (41), 4 states have internal predecessors, (41), 3 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 3 states have call predecessors, (25), 3 states have call successors, (25) Word has length 91
[2025-05-07 17:29:28,963 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:28,964 INFO  L225             Difference]: With dead ends: 104
[2025-05-07 17:29:28,964 INFO  L226             Difference]: Without dead ends: 98
[2025-05-07 17:29:28,964 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:29:28,965 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 1 mSDsluCounter, 213 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 325 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:29:28,965 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 325 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:28,965 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-05-07 17:29:28,968 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-05-07 17:29:28,969 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 43 states have (on average 1.0232558139534884) internal successors, (44), 44 states have internal predecessors, (44), 28 states have call successors, (29), 26 states have call predecessors, (29), 26 states have return successors, (29), 27 states have call predecessors, (29), 28 states have call successors, (29)
[2025-05-07 17:29:28,969 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 102 transitions.
[2025-05-07 17:29:28,969 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 102 transitions. Word has length 91
[2025-05-07 17:29:28,969 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,970 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 102 transitions.
[2025-05-07 17:29:28,970 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 13.666666666666666) internal successors, (41), 4 states have internal predecessors, (41), 3 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 3 states have call predecessors, (25), 3 states have call successors, (25)
[2025-05-07 17:29:28,970 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 102 transitions.
[2025-05-07 17:29:28,971 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:29:28,971 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,971 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:29:28,971 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:29:28,971 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,972 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,972 INFO  L85        PathProgramCache]: Analyzing trace with hash -1622924127, now seen corresponding path program 1 times
[2025-05-07 17:29:28,972 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,972 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1197783273]
[2025-05-07 17:29:28,972 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,972 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:29,006 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:29:29,054 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:29:29,054 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:29,054 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:29,913 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:29:29,913 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:29,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1197783273]
[2025-05-07 17:29:29,913 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1197783273] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:29,913 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:29,913 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [20] imperfect sequences [] total 20
[2025-05-07 17:29:29,914 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [173097689]
[2025-05-07 17:29:29,914 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:29,914 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-05-07 17:29:29,914 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:29,915 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-05-07 17:29:29,915 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=343, Unknown=0, NotChecked=0, Total=380
[2025-05-07 17:29:29,915 INFO  L87              Difference]: Start difference. First operand 98 states and 102 transitions. Second operand  has 20 states, 14 states have (on average 2.9285714285714284) internal successors, (41), 17 states have internal predecessors, (41), 9 states have call successors, (25), 1 states have call predecessors, (25), 14 states have return successors, (25), 16 states have call predecessors, (25), 9 states have call successors, (25)
[2025-05-07 17:29:30,284 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:30,284 INFO  L93              Difference]: Finished difference Result 105 states and 112 transitions.
[2025-05-07 17:29:30,284 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-05-07 17:29:30,285 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 14 states have (on average 2.9285714285714284) internal successors, (41), 17 states have internal predecessors, (41), 9 states have call successors, (25), 1 states have call predecessors, (25), 14 states have return successors, (25), 16 states have call predecessors, (25), 9 states have call successors, (25) Word has length 91
[2025-05-07 17:29:30,285 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:30,286 INFO  L225             Difference]: With dead ends: 105
[2025-05-07 17:29:30,286 INFO  L226             Difference]: Without dead ends: 94
[2025-05-07 17:29:30,286 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 25 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=57, Invalid=543, Unknown=0, NotChecked=0, Total=600
[2025-05-07 17:29:30,287 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 5 mSDsluCounter, 1520 mSDsCounter, 0 mSdLazyCounter, 310 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 1607 SdHoareTripleChecker+Invalid, 312 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 310 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:30,287 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 1607 Invalid, 312 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 310 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:29:30,288 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-05-07 17:29:30,292 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 94.
[2025-05-07 17:29:30,293 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 41 states have (on average 1.024390243902439) internal successors, (42), 42 states have internal predecessors, (42), 27 states have call successors, (27), 25 states have call predecessors, (27), 25 states have return successors, (27), 26 states have call predecessors, (27), 27 states have call successors, (27)
[2025-05-07 17:29:30,294 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 96 transitions.
[2025-05-07 17:29:30,294 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 96 transitions. Word has length 91
[2025-05-07 17:29:30,294 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:30,294 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 96 transitions.
[2025-05-07 17:29:30,294 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 14 states have (on average 2.9285714285714284) internal successors, (41), 17 states have internal predecessors, (41), 9 states have call successors, (25), 1 states have call predecessors, (25), 14 states have return successors, (25), 16 states have call predecessors, (25), 9 states have call successors, (25)
[2025-05-07 17:29:30,294 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 96 transitions.
[2025-05-07 17:29:30,295 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:29:30,295 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:30,295 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:30,296 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:29:30,296 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:30,296 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:30,296 INFO  L85        PathProgramCache]: Analyzing trace with hash 826462351, now seen corresponding path program 1 times
[2025-05-07 17:29:30,296 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:30,296 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1638955926]
[2025-05-07 17:29:30,296 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:30,297 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:30,332 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:29:30,359 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:29:30,359 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:30,359 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:30,475 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:29:30,475 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:30,475 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1638955926]
[2025-05-07 17:29:30,475 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1638955926] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:30,476 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:30,476 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:30,476 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1000736391]
[2025-05-07 17:29:30,476 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:30,476 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:30,476 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:30,477 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:30,477 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:30,477 INFO  L87              Difference]: Start difference. First operand 94 states and 96 transitions. Second operand  has 7 states, 5 states have (on average 8.2) internal successors, (41), 7 states have internal predecessors, (41), 5 states have call successors, (25), 1 states have call predecessors, (25), 5 states have return successors, (25), 5 states have call predecessors, (25), 5 states have call successors, (25)
[2025-05-07 17:29:30,515 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:30,515 INFO  L93              Difference]: Finished difference Result 93 states and 93 transitions.
[2025-05-07 17:29:30,516 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:30,516 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 8.2) internal successors, (41), 7 states have internal predecessors, (41), 5 states have call successors, (25), 1 states have call predecessors, (25), 5 states have return successors, (25), 5 states have call predecessors, (25), 5 states have call successors, (25) Word has length 91
[2025-05-07 17:29:30,516 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:30,516 INFO  L225             Difference]: With dead ends: 93
[2025-05-07 17:29:30,517 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:29:30,517 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:29:30,517 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 1 mSDsluCounter, 434 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 524 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:30,518 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 524 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:30,518 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:29:30,522 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-05-07 17:29:30,522 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 41 states have (on average 1.0) internal successors, (41), 41 states have internal predecessors, (41), 25 states have call successors, (25), 25 states have call predecessors, (25), 25 states have return successors, (25), 25 states have call predecessors, (25), 25 states have call successors, (25)
[2025-05-07 17:29:30,522 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 91 transitions.
[2025-05-07 17:29:30,523 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 91 transitions. Word has length 91
[2025-05-07 17:29:30,523 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:30,523 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 91 transitions.
[2025-05-07 17:29:30,523 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 8.2) internal successors, (41), 7 states have internal predecessors, (41), 5 states have call successors, (25), 1 states have call predecessors, (25), 5 states have return successors, (25), 5 states have call predecessors, (25), 5 states have call successors, (25)
[2025-05-07 17:29:30,523 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 91 transitions.
[2025-05-07 17:29:30,524 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:29:30,524 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:30,524 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:30,524 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:29:30,524 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:30,525 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:30,525 INFO  L85        PathProgramCache]: Analyzing trace with hash -1684033397, now seen corresponding path program 1 times
[2025-05-07 17:29:30,525 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:30,525 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2106833245]
[2025-05-07 17:29:30,525 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:30,525 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:30,549 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:29:30,556 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:29:30,556 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:30,556 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:30,605 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:29:30,606 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:30,606 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2106833245]
[2025-05-07 17:29:30,606 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2106833245] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:30,606 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:30,606 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:30,606 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [94497618]
[2025-05-07 17:29:30,606 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:30,607 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:30,607 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:30,607 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:30,607 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:30,607 INFO  L87              Difference]: Start difference. First operand 92 states and 91 transitions. Second operand  has 4 states, 3 states have (on average 13.666666666666666) internal successors, (41), 4 states have internal predecessors, (41), 4 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 4 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:29:30,614 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:30,614 INFO  L93              Difference]: Finished difference Result 59 states and 58 transitions.
[2025-05-07 17:29:30,614 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:30,614 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 13.666666666666666) internal successors, (41), 4 states have internal predecessors, (41), 4 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 4 states have call predecessors, (25), 4 states have call successors, (25) Word has length 91
[2025-05-07 17:29:30,614 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:30,614 INFO  L225             Difference]: With dead ends: 59
[2025-05-07 17:29:30,615 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:29:30,615 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:29:30,615 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 0 mSDsluCounter, 107 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 165 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:29:30,615 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 165 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:30,616 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:29:30,616 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:29:30,616 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:29:30,616 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:29:30,616 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 91
[2025-05-07 17:29:30,616 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:30,616 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:29:30,616 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 13.666666666666666) internal successors, (41), 4 states have internal predecessors, (41), 4 states have call successors, (25), 1 states have call predecessors, (25), 3 states have return successors, (25), 4 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:29:30,616 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:29:30,616 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:29:30,618 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:29:30,619 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:29:30,621 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:30,623 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:29:30,626 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:29:30 BoogieIcfgContainer
[2025-05-07 17:29:30,626 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:29:30,626 INFO  L158              Benchmark]: Toolchain (without parser) took 3496.99ms. Allocated memory is still 234.9MB. Free memory was 147.5MB in the beginning and 99.0MB in the end (delta: 48.6MB). Peak memory consumption was 48.0MB. Max. memory is 33.6GB.
[2025-05-07 17:29:30,626 INFO  L158              Benchmark]: SmtParser took 0.26ms. 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:29:30,627 INFO  L158              Benchmark]: ChcToBoogie took 44.65ms. Allocated memory is still 234.9MB. Free memory was 147.4MB in the beginning and 144.7MB in the end (delta: 2.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:30,627 INFO  L158              Benchmark]: Boogie Preprocessor took 71.30ms. Allocated memory is still 234.9MB. Free memory was 144.6MB in the beginning and 141.3MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:30,627 INFO  L158              Benchmark]: RCFGBuilder took 439.67ms. Allocated memory is still 234.9MB. Free memory was 141.3MB in the beginning and 171.4MB in the end (delta: -30.0MB). Peak memory consumption was 43.7MB. Max. memory is 33.6GB.
[2025-05-07 17:29:30,627 INFO  L158              Benchmark]: TraceAbstraction took 2937.14ms. Allocated memory is still 234.9MB. Free memory was 170.5MB in the beginning and 99.0MB in the end (delta: 71.6MB). Peak memory consumption was 71.4MB. Max. memory is 33.6GB.
[2025-05-07 17:29:30,628 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.26ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 44.65ms. Allocated memory is still 234.9MB. Free memory was 147.4MB in the beginning and 144.7MB in the end (delta: 2.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 71.30ms. Allocated memory is still 234.9MB. Free memory was 144.6MB in the beginning and 141.3MB in the end (delta: 3.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 439.67ms. Allocated memory is still 234.9MB. Free memory was 141.3MB in the beginning and 171.4MB in the end (delta: -30.0MB). Peak memory consumption was 43.7MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2937.14ms. Allocated memory is still 234.9MB. Free memory was 170.5MB in the beginning and 99.0MB in the end (delta: 71.6MB). Peak memory consumption was 71.4MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 27 procedures, 113 locations, 177 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.9s, OverallIterations: 8, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.7s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 30 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 9 mSDsluCounter, 4487 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 3661 mSDsCounter, 5 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 409 IncrementalHoareTripleChecker+Invalid, 414 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 5 mSolverCounterUnsat, 826 mSDtfsCounter, 409 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 61 GetRequests, 16 SyntacticMatches, 0 SemanticMatches, 45 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.3s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=113occurred in iteration=0, InterpolantAutomatonStates: 55, 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, 8 MinimizatonAttempts, 4 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 1.5s InterpolantComputationTime, 578 NumberOfCodeBlocks, 578 NumberOfCodeBlocksAsserted, 8 NumberOfCheckSat, 570 ConstructedInterpolants, 0 QuantifiedInterpolants, 807 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 8 InterpolantComputations, 8 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:29:30,640 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
