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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:41,813 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:41,850 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a226c78-c960-4b73-9d8b-9a998b831098/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:41,853 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:41,853 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:41,867 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:41,868 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:41,868 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:41,868 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:41,868 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:41,868 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:41,868 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:41,868 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:41,868 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:41,869 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:41,869 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:41,869 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:41,870 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:41,870 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:42,048 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:42,055 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:42,057 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:42,058 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:42,058 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:42,059 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a226c78-c960-4b73-9d8b-9a998b831098/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_local_vars.sol_0_no_adts_000.smt2
[2025-05-07 17:27:42,060 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:42,062 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:42,344 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a226c78-c960-4b73-9d8b-9a998b831098/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/functions/constructor_hierarchy_mixed_chain_local_vars.sol_0_no_adts_000.smt2
[2025-05-07 17:27:42,346 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:42,347 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:42,348 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:42,348 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:42,348 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:42,350 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,396 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42 Unit
[2025-05-07 17:27:42,396 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:42,397 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:42,397 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:42,397 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:42,409 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,409 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,440 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,440 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,448 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,450 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,451 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,455 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,457 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,475 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:42,476 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:42,476 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:42,476 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:42,477 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (1/1) ...
[2025-05-07 17:27:42,480 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:42,492 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:42,502 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:27:42,505 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:27:42,515 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:42,516 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:42,516 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:42,516 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_3_0 given in one single declaration
[2025-05-07 17:27:42,516 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_3_0
[2025-05-07 17:27:42,516 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_3_0
[2025-05-07 17:27:42,516 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_26_A_80_0 given in one single declaration
[2025-05-07 17:27:42,516 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_26_A_80_0
[2025-05-07 17:27:42,516 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_26_A_80_0
[2025-05-07 17:27:42,516 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_119_B_51_0 given in one single declaration
[2025-05-07 17:27:42,516 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_119_B_51_0
[2025-05-07 17:27:42,516 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_119_B_51_0
[2025-05-07 17:27:42,517 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_29_constructor_50_80_0 given in one single declaration
[2025-05-07 17:27:42,517 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_29_constructor_50_80_0
[2025-05-07 17:27:42,517 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_29_constructor_50_80_0
[2025-05-07 17:27:42,517 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_118_return_constructor_50_80_0 given in one single declaration
[2025-05-07 17:27:42,517 INFO  L130     BoogieDeclarations]: Found specification of procedure block_118_return_constructor_50_80_0
[2025-05-07 17:27:42,517 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_118_return_constructor_50_80_0
[2025-05-07 17:27:42,517 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_117__49_80_0 given in one single declaration
[2025-05-07 17:27:42,517 INFO  L130     BoogieDeclarations]: Found specification of procedure block_117__49_80_0
[2025-05-07 17:27:42,517 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_117__49_80_0
[2025-05-07 17:27:42,518 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_116_constructor_50_80_0 given in one single declaration
[2025-05-07 17:27:42,518 INFO  L130     BoogieDeclarations]: Found specification of procedure block_116_constructor_50_80_0
[2025-05-07 17:27:42,518 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_116_constructor_50_80_0
[2025-05-07 17:27:42,518 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_121_B_51_0 given in one single declaration
[2025-05-07 17:27:42,518 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_121_B_51_0
[2025-05-07 17:27:42,518 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_121_B_51_0
[2025-05-07 17:27:42,518 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_120_B_51_0 given in one single declaration
[2025-05-07 17:27:42,518 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_120_B_51_0
[2025-05-07 17:27:42,518 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_120_B_51_0
[2025-05-07 17:27:42,519 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_113_A_80_0 given in one single declaration
[2025-05-07 17:27:42,519 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_113_A_80_0
[2025-05-07 17:27:42,519 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_113_A_80_0
[2025-05-07 17:27:42,519 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_30_constructor_79_80_0 given in one single declaration
[2025-05-07 17:27:42,519 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_30_constructor_79_80_0
[2025-05-07 17:27:42,519 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_30_constructor_79_80_0
[2025-05-07 17:27:42,519 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_111_constructor_79_80_0 given in one single declaration
[2025-05-07 17:27:42,519 INFO  L130     BoogieDeclarations]: Found specification of procedure block_111_constructor_79_80_0
[2025-05-07 17:27:42,519 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_111_constructor_79_80_0
[2025-05-07 17:27:42,519 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_109__78_80_0 given in one single declaration
[2025-05-07 17:27:42,519 INFO  L130     BoogieDeclarations]: Found specification of procedure block_109__78_80_0
[2025-05-07 17:27:42,519 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_109__78_80_0
[2025-05-07 17:27:42,520 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_108_constructor_79_80_0 given in one single declaration
[2025-05-07 17:27:42,520 INFO  L130     BoogieDeclarations]: Found specification of procedure block_108_constructor_79_80_0
[2025-05-07 17:27:42,520 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_108_constructor_79_80_0
[2025-05-07 17:27:42,520 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_110_return_constructor_79_80_0 given in one single declaration
[2025-05-07 17:27:42,520 INFO  L130     BoogieDeclarations]: Found specification of procedure block_110_return_constructor_79_80_0
[2025-05-07 17:27:42,520 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_110_return_constructor_79_80_0
[2025-05-07 17:27:42,520 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_112_constructor_79_80_0 given in one single declaration
[2025-05-07 17:27:42,520 INFO  L130     BoogieDeclarations]: Found specification of procedure block_112_constructor_79_80_0
[2025-05-07 17:27:42,520 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_112_constructor_79_80_0
[2025-05-07 17:27:42,520 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_115_A_80_0 given in one single declaration
[2025-05-07 17:27:42,520 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_115_A_80_0
[2025-05-07 17:27:42,520 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_115_A_80_0
[2025-05-07 17:27:42,521 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_114_A_80_0 given in one single declaration
[2025-05-07 17:27:42,521 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_114_A_80_0
[2025-05-07 17:27:42,521 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_114_A_80_0
[2025-05-07 17:27:42,521 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_128_D_33_0 given in one single declaration
[2025-05-07 17:27:42,521 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_128_D_33_0
[2025-05-07 17:27:42,521 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_128_D_33_0
[2025-05-07 17:27:42,521 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_130_D_33_0 given in one single declaration
[2025-05-07 17:27:42,521 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_130_D_33_0
[2025-05-07 17:27:42,521 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_130_D_33_0
[2025-05-07 17:27:42,521 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_129_D_33_0 given in one single declaration
[2025-05-07 17:27:42,521 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_129_D_33_0
[2025-05-07 17:27:42,521 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_129_D_33_0
[2025-05-07 17:27:42,522 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_28_constructor_32_80_0 given in one single declaration
[2025-05-07 17:27:42,522 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_28_constructor_32_80_0
[2025-05-07 17:27:42,522 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_28_constructor_32_80_0
[2025-05-07 17:27:42,522 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_127_return_constructor_32_80_0 given in one single declaration
[2025-05-07 17:27:42,522 INFO  L130     BoogieDeclarations]: Found specification of procedure block_127_return_constructor_32_80_0
[2025-05-07 17:27:42,522 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_127_return_constructor_32_80_0
[2025-05-07 17:27:42,522 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_126__31_80_0 given in one single declaration
[2025-05-07 17:27:42,522 INFO  L130     BoogieDeclarations]: Found specification of procedure block_126__31_80_0
[2025-05-07 17:27:42,522 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_126__31_80_0
[2025-05-07 17:27:42,522 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_125_constructor_32_80_0 given in one single declaration
[2025-05-07 17:27:42,522 INFO  L130     BoogieDeclarations]: Found specification of procedure block_125_constructor_32_80_0
[2025-05-07 17:27:42,522 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_125_constructor_32_80_0
[2025-05-07 17:27:42,522 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_137_F_15_0 given in one single declaration
[2025-05-07 17:27:42,523 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_137_F_15_0
[2025-05-07 17:27:42,523 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_137_F_15_0
[2025-05-07 17:27:42,523 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_27_constructor_14_80_0 given in one single declaration
[2025-05-07 17:27:42,523 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_27_constructor_14_80_0
[2025-05-07 17:27:42,523 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_27_constructor_14_80_0
[2025-05-07 17:27:42,523 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_136_return_constructor_14_80_0 given in one single declaration
[2025-05-07 17:27:42,523 INFO  L130     BoogieDeclarations]: Found specification of procedure block_136_return_constructor_14_80_0
[2025-05-07 17:27:42,523 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_136_return_constructor_14_80_0
[2025-05-07 17:27:42,523 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_135__13_80_0 given in one single declaration
[2025-05-07 17:27:42,523 INFO  L130     BoogieDeclarations]: Found specification of procedure block_135__13_80_0
[2025-05-07 17:27:42,523 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_135__13_80_0
[2025-05-07 17:27:42,523 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_134_constructor_14_80_0 given in one single declaration
[2025-05-07 17:27:42,523 INFO  L130     BoogieDeclarations]: Found specification of procedure block_134_constructor_14_80_0
[2025-05-07 17:27:42,523 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_134_constructor_14_80_0
[2025-05-07 17:27:42,523 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_139_F_15_0 given in one single declaration
[2025-05-07 17:27:42,524 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_139_F_15_0
[2025-05-07 17:27:42,524 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_139_F_15_0
[2025-05-07 17:27:42,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_138_F_15_0 given in one single declaration
[2025-05-07 17:27:42,524 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_138_F_15_0
[2025-05-07 17:27:42,524 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_138_F_15_0
[2025-05-07 17:27:42,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_140_A_80_0 given in one single declaration
[2025-05-07 17:27:42,524 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_140_A_80_0
[2025-05-07 17:27:42,524 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_140_A_80_0
[2025-05-07 17:27:42,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_122_C_36_0 given in one single declaration
[2025-05-07 17:27:42,524 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_122_C_36_0
[2025-05-07 17:27:42,524 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_122_C_36_0
[2025-05-07 17:27:42,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_124_C_36_0 given in one single declaration
[2025-05-07 17:27:42,524 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_124_C_36_0
[2025-05-07 17:27:42,524 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_124_C_36_0
[2025-05-07 17:27:42,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_123_C_36_0 given in one single declaration
[2025-05-07 17:27:42,524 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_123_C_36_0
[2025-05-07 17:27:42,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_123_C_36_0
[2025-05-07 17:27:42,525 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_131_E_18_0 given in one single declaration
[2025-05-07 17:27:42,525 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_131_E_18_0
[2025-05-07 17:27:42,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_131_E_18_0
[2025-05-07 17:27:42,525 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_133_E_18_0 given in one single declaration
[2025-05-07 17:27:42,525 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_133_E_18_0
[2025-05-07 17:27:42,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_133_E_18_0
[2025-05-07 17:27:42,525 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_132_E_18_0 given in one single declaration
[2025-05-07 17:27:42,525 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_132_E_18_0
[2025-05-07 17:27:42,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_132_E_18_0
[2025-05-07 17:27:42,525 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:42,525 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:42,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:42,735 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:42,736 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:43,017 INFO  L?                        ?]: Removed 388 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:43,018 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:43,027 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:43,028 INFO  L312             CfgBuilder]: Removed 19 assume(true) statements.
[2025-05-07 17:27:43,028 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:43 BoogieIcfgContainer
[2025-05-07 17:27:43,028 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:43,029 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:43,030 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:43,032 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:43,032 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:42" (1/3) ...
[2025-05-07 17:27:43,033 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@d93de47 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:43, skipping insertion in model container
[2025-05-07 17:27:43,033 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:42" (2/3) ...
[2025-05-07 17:27:43,033 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@d93de47 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:43, skipping insertion in model container
[2025-05-07 17:27:43,033 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:43" (3/3) ...
[2025-05-07 17:27:43,034 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:43,044 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:43,046 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 41 procedures, 182 locations, 307 edges, 41 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:43,077 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:43,085 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;@43704d7e, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:43,085 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:43,088 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 182 states, 65 states have (on average 1.1692307692307693) internal successors, (76), 76 states have internal predecessors, (76), 75 states have call successors, (77), 40 states have call predecessors, (77), 40 states have return successors, (77), 65 states have call predecessors, (77), 75 states have call successors, (77)
[2025-05-07 17:27:43,098 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:43,098 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:43,099 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:27:43,099 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:43,102 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:43,103 INFO  L85        PathProgramCache]: Analyzing trace with hash -1141559361, now seen corresponding path program 1 times
[2025-05-07 17:27:43,109 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:43,109 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1396041949]
[2025-05-07 17:27:43,109 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:43,109 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:43,149 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:43,198 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:43,199 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:43,199 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:43,393 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:27:43,393 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:43,394 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1396041949]
[2025-05-07 17:27:43,394 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1396041949] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:43,394 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:43,397 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:43,398 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [91454195]
[2025-05-07 17:27:43,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:43,402 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:43,402 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:43,424 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:43,425 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:43,427 INFO  L87              Difference]: Start difference. First operand  has 182 states, 65 states have (on average 1.1692307692307693) internal successors, (76), 76 states have internal predecessors, (76), 75 states have call successors, (77), 40 states have call predecessors, (77), 40 states have return successors, (77), 65 states have call predecessors, (77), 75 states have call successors, (77) 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), 6 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:27:43,531 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:43,532 INFO  L93              Difference]: Finished difference Result 180 states and 227 transitions.
[2025-05-07 17:27:43,533 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:43,534 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), 6 states have call predecessors, (11), 4 states have call successors, (11) Word has length 41
[2025-05-07 17:27:43,534 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:43,540 INFO  L225             Difference]: With dead ends: 180
[2025-05-07 17:27:43,541 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:43,542 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:27:43,544 INFO  L437           NwaCegarLoop]: 224 mSDtfsCounter, 0 mSDsluCounter, 877 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1101 SdHoareTripleChecker+Invalid, 25 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:43,545 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1101 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:43,555 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:43,576 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 178.
[2025-05-07 17:27:43,578 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 178 states, 64 states have (on average 1.140625) internal successors, (73), 73 states have internal predecessors, (73), 73 states have call successors, (75), 40 states have call predecessors, (75), 40 states have return successors, (75), 64 states have call predecessors, (75), 73 states have call successors, (75)
[2025-05-07 17:27:43,582 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 178 states to 178 states and 223 transitions.
[2025-05-07 17:27:43,583 INFO  L79                 Accepts]: Start accepts. Automaton has 178 states and 223 transitions. Word has length 41
[2025-05-07 17:27:43,583 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:43,583 INFO  L485      AbstractCegarLoop]: Abstraction has 178 states and 223 transitions.
[2025-05-07 17:27:43,583 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), 6 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:27:43,584 INFO  L278                IsEmpty]: Start isEmpty. Operand 178 states and 223 transitions.
[2025-05-07 17:27:43,585 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-05-07 17:27:43,585 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:43,586 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:27:43,586 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:27:43,586 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:43,586 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:43,586 INFO  L85        PathProgramCache]: Analyzing trace with hash -65824445, now seen corresponding path program 1 times
[2025-05-07 17:27:43,586 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:43,586 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1801203936]
[2025-05-07 17:27:43,587 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:43,587 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:43,606 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-05-07 17:27:43,612 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-05-07 17:27:43,612 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:43,612 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:43,680 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:27:43,680 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:43,680 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1801203936]
[2025-05-07 17:27:43,680 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1801203936] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:43,680 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:43,681 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:43,681 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [501590776]
[2025-05-07 17:27:43,681 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:43,682 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:43,682 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:43,683 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:43,683 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:43,683 INFO  L87              Difference]: Start difference. First operand 178 states and 223 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:27:43,761 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:43,761 INFO  L93              Difference]: Finished difference Result 179 states and 222 transitions.
[2025-05-07 17:27:43,762 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:43,762 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:27:43,762 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:43,765 INFO  L225             Difference]: With dead ends: 179
[2025-05-07 17:27:43,765 INFO  L226             Difference]: Without dead ends: 178
[2025-05-07 17:27:43,765 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:27:43,766 INFO  L437           NwaCegarLoop]: 213 mSDtfsCounter, 1 mSDsluCounter, 387 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 600 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:43,766 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 600 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:43,767 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-05-07 17:27:43,779 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 176.
[2025-05-07 17:27:43,780 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 176 states, 64 states have (on average 1.125) internal successors, (72), 72 states have internal predecessors, (72), 71 states have call successors, (73), 40 states have call predecessors, (73), 40 states have return successors, (73), 63 states have call predecessors, (73), 71 states have call successors, (73)
[2025-05-07 17:27:43,782 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 176 states to 176 states and 218 transitions.
[2025-05-07 17:27:43,782 INFO  L79                 Accepts]: Start accepts. Automaton has 176 states and 218 transitions. Word has length 41
[2025-05-07 17:27:43,782 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:43,782 INFO  L485      AbstractCegarLoop]: Abstraction has 176 states and 218 transitions.
[2025-05-07 17:27:43,782 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:27:43,782 INFO  L278                IsEmpty]: Start isEmpty. Operand 176 states and 218 transitions.
[2025-05-07 17:27:43,783 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-05-07 17:27:43,783 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:43,784 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:43,784 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:27:43,784 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:43,784 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:43,784 INFO  L85        PathProgramCache]: Analyzing trace with hash 1791928549, now seen corresponding path program 1 times
[2025-05-07 17:27:43,784 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:43,784 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [335459537]
[2025-05-07 17:27:43,784 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:43,784 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:43,807 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-05-07 17:27:43,828 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-05-07 17:27:43,828 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:43,828 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:43,937 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:27:43,937 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:43,937 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [335459537]
[2025-05-07 17:27:43,937 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [335459537] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:43,937 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:43,938 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:43,938 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [14128814]
[2025-05-07 17:27:43,938 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:43,938 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:43,938 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:43,939 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:43,939 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:43,939 INFO  L87              Difference]: Start difference. First operand 176 states and 218 transitions. Second operand  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:27:44,028 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,028 INFO  L93              Difference]: Finished difference Result 178 states and 219 transitions.
[2025-05-07 17:27:44,029 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:44,029 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 2 states have call successors, (14) Word has length 51
[2025-05-07 17:27:44,029 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,030 INFO  L225             Difference]: With dead ends: 178
[2025-05-07 17:27:44,030 INFO  L226             Difference]: Without dead ends: 175
[2025-05-07 17:27:44,030 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:27:44,031 INFO  L437           NwaCegarLoop]: 209 mSDtfsCounter, 1 mSDsluCounter, 797 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 1006 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:44,031 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 1006 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:44,032 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 175 states.
[2025-05-07 17:27:44,038 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 175 to 173.
[2025-05-07 17:27:44,038 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 173 states, 64 states have (on average 1.109375) internal successors, (71), 71 states have internal predecessors, (71), 68 states have call successors, (70), 40 states have call predecessors, (70), 40 states have return successors, (70), 61 states have call predecessors, (70), 68 states have call successors, (70)
[2025-05-07 17:27:44,039 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 173 states to 173 states and 211 transitions.
[2025-05-07 17:27:44,039 INFO  L79                 Accepts]: Start accepts. Automaton has 173 states and 211 transitions. Word has length 51
[2025-05-07 17:27:44,039 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,039 INFO  L485      AbstractCegarLoop]: Abstraction has 173 states and 211 transitions.
[2025-05-07 17:27:44,039 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.6) internal successors, (23), 6 states have internal predecessors, (23), 2 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (14), 5 states have call predecessors, (14), 2 states have call successors, (14)
[2025-05-07 17:27:44,040 INFO  L278                IsEmpty]: Start isEmpty. Operand 173 states and 211 transitions.
[2025-05-07 17:27:44,041 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:27:44,041 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,041 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]
[2025-05-07 17:27:44,041 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:27:44,041 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,042 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,042 INFO  L85        PathProgramCache]: Analyzing trace with hash 1417818145, now seen corresponding path program 1 times
[2025-05-07 17:27:44,042 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,042 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [248025865]
[2025-05-07 17:27:44,042 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,042 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,076 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:27:44,092 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:27:44,093 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,093 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,179 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:27:44,179 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [248025865]
[2025-05-07 17:27:44,180 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [248025865] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,180 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,180 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:44,180 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1422432466]
[2025-05-07 17:27:44,180 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,180 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:44,180 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,181 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:44,181 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:44,181 INFO  L87              Difference]: Start difference. First operand 173 states and 211 transitions. Second operand  has 4 states, 3 states have (on average 12.666666666666666) internal successors, (38), 4 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 3 states have return successors, (24), 4 states have call predecessors, (24), 3 states have call successors, (24)
[2025-05-07 17:27:44,223 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,223 INFO  L93              Difference]: Finished difference Result 175 states and 215 transitions.
[2025-05-07 17:27:44,223 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:44,224 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.666666666666666) internal successors, (38), 4 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 3 states have return successors, (24), 4 states have call predecessors, (24), 3 states have call successors, (24) Word has length 86
[2025-05-07 17:27:44,224 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,225 INFO  L225             Difference]: With dead ends: 175
[2025-05-07 17:27:44,225 INFO  L226             Difference]: Without dead ends: 175
[2025-05-07 17:27:44,226 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:27:44,226 INFO  L437           NwaCegarLoop]: 210 mSDtfsCounter, 1 mSDsluCounter, 377 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 587 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:44,227 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 587 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:44,228 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 175 states.
[2025-05-07 17:27:44,238 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 175 to 175.
[2025-05-07 17:27:44,238 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 175 states, 65 states have (on average 1.1076923076923078) internal successors, (72), 72 states have internal predecessors, (72), 68 states have call successors, (70), 40 states have call predecessors, (70), 41 states have return successors, (73), 62 states have call predecessors, (73), 68 states have call successors, (73)
[2025-05-07 17:27:44,240 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 175 states to 175 states and 215 transitions.
[2025-05-07 17:27:44,240 INFO  L79                 Accepts]: Start accepts. Automaton has 175 states and 215 transitions. Word has length 86
[2025-05-07 17:27:44,241 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,241 INFO  L485      AbstractCegarLoop]: Abstraction has 175 states and 215 transitions.
[2025-05-07 17:27:44,241 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.666666666666666) internal successors, (38), 4 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 3 states have return successors, (24), 4 states have call predecessors, (24), 3 states have call successors, (24)
[2025-05-07 17:27:44,241 INFO  L278                IsEmpty]: Start isEmpty. Operand 175 states and 215 transitions.
[2025-05-07 17:27:44,243 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 87
[2025-05-07 17:27:44,243 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,243 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]
[2025-05-07 17:27:44,244 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:27:44,244 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,244 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,244 INFO  L85        PathProgramCache]: Analyzing trace with hash 1679273125, now seen corresponding path program 1 times
[2025-05-07 17:27:44,244 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,244 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [567345407]
[2025-05-07 17:27:44,244 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,245 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,278 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 86 statements into 1 equivalence classes.
[2025-05-07 17:27:44,296 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 86 of 86 statements.
[2025-05-07 17:27:44,296 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,296 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,382 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:27:44,382 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,382 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [567345407]
[2025-05-07 17:27:44,383 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [567345407] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,383 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,383 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:44,383 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1127749025]
[2025-05-07 17:27:44,383 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,383 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:44,383 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,384 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:44,384 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:44,384 INFO  L87              Difference]: Start difference. First operand 175 states and 215 transitions. Second operand  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 3 states have call successors, (24)
[2025-05-07 17:27:44,447 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,447 INFO  L93              Difference]: Finished difference Result 174 states and 210 transitions.
[2025-05-07 17:27:44,448 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:44,448 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 3 states have call successors, (24) Word has length 86
[2025-05-07 17:27:44,448 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,449 INFO  L225             Difference]: With dead ends: 174
[2025-05-07 17:27:44,449 INFO  L226             Difference]: Without dead ends: 172
[2025-05-07 17:27:44,449 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:27:44,450 INFO  L437           NwaCegarLoop]: 198 mSDtfsCounter, 1 mSDsluCounter, 760 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 958 SdHoareTripleChecker+Invalid, 37 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:44,450 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 958 Invalid, 37 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:44,451 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 172 states.
[2025-05-07 17:27:44,455 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 172 to 170.
[2025-05-07 17:27:44,456 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 170 states, 65 states have (on average 1.0923076923076922) internal successors, (71), 71 states have internal predecessors, (71), 63 states have call successors, (65), 40 states have call predecessors, (65), 41 states have return successors, (68), 58 states have call predecessors, (68), 63 states have call successors, (68)
[2025-05-07 17:27:44,457 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 170 states to 170 states and 204 transitions.
[2025-05-07 17:27:44,457 INFO  L79                 Accepts]: Start accepts. Automaton has 170 states and 204 transitions. Word has length 86
[2025-05-07 17:27:44,457 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,457 INFO  L485      AbstractCegarLoop]: Abstraction has 170 states and 204 transitions.
[2025-05-07 17:27:44,457 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.6) internal successors, (38), 6 states have internal predecessors, (38), 3 states have call successors, (24), 1 states have call predecessors, (24), 5 states have return successors, (24), 5 states have call predecessors, (24), 3 states have call successors, (24)
[2025-05-07 17:27:44,457 INFO  L278                IsEmpty]: Start isEmpty. Operand 170 states and 204 transitions.
[2025-05-07 17:27:44,458 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:27:44,458 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,458 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]
[2025-05-07 17:27:44,459 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:27:44,459 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,459 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,459 INFO  L85        PathProgramCache]: Analyzing trace with hash -137226261, now seen corresponding path program 1 times
[2025-05-07 17:27:44,459 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,459 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1441348659]
[2025-05-07 17:27:44,459 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,459 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,485 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:27:44,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:27:44,497 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,497 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,576 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:27:44,576 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,576 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1441348659]
[2025-05-07 17:27:44,577 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1441348659] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,577 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,577 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:44,577 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1397026168]
[2025-05-07 17:27:44,577 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,577 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:44,577 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,578 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:44,578 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:44,578 INFO  L87              Difference]: Start difference. First operand 170 states and 204 transitions. Second operand  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:27:44,625 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,625 INFO  L93              Difference]: Finished difference Result 167 states and 197 transitions.
[2025-05-07 17:27:44,626 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:44,626 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 4 states have call successors, (21) Word has length 76
[2025-05-07 17:27:44,626 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,627 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:27:44,627 INFO  L226             Difference]: Without dead ends: 166
[2025-05-07 17:27:44,628 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:27:44,628 INFO  L437           NwaCegarLoop]: 194 mSDtfsCounter, 0 mSDsluCounter, 761 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 955 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:27:44,628 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 955 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:44,629 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 166 states.
[2025-05-07 17:27:44,633 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 166 to 166.
[2025-05-07 17:27:44,634 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 166 states, 64 states have (on average 1.078125) internal successors, (69), 69 states have internal predecessors, (69), 61 states have call successors, (63), 40 states have call predecessors, (63), 40 states have return successors, (63), 56 states have call predecessors, (63), 61 states have call successors, (63)
[2025-05-07 17:27:44,635 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 166 states to 166 states and 195 transitions.
[2025-05-07 17:27:44,635 INFO  L79                 Accepts]: Start accepts. Automaton has 166 states and 195 transitions. Word has length 76
[2025-05-07 17:27:44,635 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,635 INFO  L485      AbstractCegarLoop]: Abstraction has 166 states and 195 transitions.
[2025-05-07 17:27:44,635 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (21), 1 states have call predecessors, (21), 5 states have return successors, (21), 5 states have call predecessors, (21), 4 states have call successors, (21)
[2025-05-07 17:27:44,635 INFO  L278                IsEmpty]: Start isEmpty. Operand 166 states and 195 transitions.
[2025-05-07 17:27:44,636 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-05-07 17:27:44,636 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,636 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]
[2025-05-07 17:27:44,636 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:27:44,636 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,637 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,637 INFO  L85        PathProgramCache]: Analyzing trace with hash 124228719, now seen corresponding path program 1 times
[2025-05-07 17:27:44,637 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,637 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [345325955]
[2025-05-07 17:27:44,637 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,637 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,671 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-05-07 17:27:44,687 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-05-07 17:27:44,687 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,687 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,737 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:27:44,737 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,737 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [345325955]
[2025-05-07 17:27:44,737 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [345325955] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,737 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,737 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:44,737 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [665843786]
[2025-05-07 17:27:44,738 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,738 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:44,738 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,739 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:44,739 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:44,739 INFO  L87              Difference]: Start difference. First operand 166 states and 195 transitions. Second operand  has 4 states, 3 states have (on average 11.333333333333334) internal successors, (34), 4 states have internal predecessors, (34), 3 states have call successors, (21), 1 states have call predecessors, (21), 3 states have return successors, (21), 4 states have call predecessors, (21), 3 states have call successors, (21)
[2025-05-07 17:27:44,774 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,774 INFO  L93              Difference]: Finished difference Result 168 states and 196 transitions.
[2025-05-07 17:27:44,774 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:44,774 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 11.333333333333334) internal successors, (34), 4 states have internal predecessors, (34), 3 states have call successors, (21), 1 states have call predecessors, (21), 3 states have return successors, (21), 4 states have call predecessors, (21), 3 states have call successors, (21) Word has length 76
[2025-05-07 17:27:44,775 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,775 INFO  L225             Difference]: With dead ends: 168
[2025-05-07 17:27:44,775 INFO  L226             Difference]: Without dead ends: 164
[2025-05-07 17:27:44,776 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:27:44,776 INFO  L437           NwaCegarLoop]: 190 mSDtfsCounter, 1 mSDsluCounter, 353 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 543 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:27:44,776 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 543 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:44,777 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 164 states.
[2025-05-07 17:27:44,780 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 164 to 162.
[2025-05-07 17:27:44,780 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 64 states have (on average 1.0625) internal successors, (68), 68 states have internal predecessors, (68), 57 states have call successors, (59), 40 states have call predecessors, (59), 40 states have return successors, (59), 53 states have call predecessors, (59), 57 states have call successors, (59)
[2025-05-07 17:27:44,781 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 186 transitions.
[2025-05-07 17:27:44,781 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 186 transitions. Word has length 76
[2025-05-07 17:27:44,781 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,781 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 186 transitions.
[2025-05-07 17:27:44,782 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 11.333333333333334) internal successors, (34), 4 states have internal predecessors, (34), 3 states have call successors, (21), 1 states have call predecessors, (21), 3 states have return successors, (21), 4 states have call predecessors, (21), 3 states have call successors, (21)
[2025-05-07 17:27:44,782 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 186 transitions.
[2025-05-07 17:27:44,783 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:27:44,783 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,783 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:44,783 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:27:44,783 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,783 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,784 INFO  L85        PathProgramCache]: Analyzing trace with hash 1630827633, now seen corresponding path program 1 times
[2025-05-07 17:27:44,784 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,784 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1768039019]
[2025-05-07 17:27:44,784 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,784 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,823 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:27:44,827 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:27:44,827 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,827 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:44,892 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:27:44,892 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:44,892 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1768039019]
[2025-05-07 17:27:44,892 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1768039019] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:44,893 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:44,893 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:44,893 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1512136702]
[2025-05-07 17:27:44,893 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:44,893 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:44,893 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:44,894 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:44,894 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:44,894 INFO  L87              Difference]: Start difference. First operand 162 states and 186 transitions. Second operand  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 3 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:27:44,925 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:44,925 INFO  L93              Difference]: Finished difference Result 166 states and 191 transitions.
[2025-05-07 17:27:44,925 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:44,926 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 3 states have call predecessors, (31), 4 states have call successors, (31) Word has length 111
[2025-05-07 17:27:44,926 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:44,926 INFO  L225             Difference]: With dead ends: 166
[2025-05-07 17:27:44,926 INFO  L226             Difference]: Without dead ends: 166
[2025-05-07 17:27:44,927 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:27:44,927 INFO  L437           NwaCegarLoop]: 185 mSDtfsCounter, 1 mSDsluCounter, 346 mSDsCounter, 0 mSdLazyCounter, 14 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 531 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 14 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:44,927 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 531 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 14 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:44,928 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 166 states.
[2025-05-07 17:27:44,931 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 166 to 164.
[2025-05-07 17:27:44,931 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 164 states, 65 states have (on average 1.0615384615384615) internal successors, (69), 69 states have internal predecessors, (69), 57 states have call successors, (59), 40 states have call predecessors, (59), 41 states have return successors, (61), 54 states have call predecessors, (61), 57 states have call successors, (61)
[2025-05-07 17:27:44,932 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 164 states to 164 states and 189 transitions.
[2025-05-07 17:27:44,932 INFO  L79                 Accepts]: Start accepts. Automaton has 164 states and 189 transitions. Word has length 111
[2025-05-07 17:27:44,932 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:44,932 INFO  L485      AbstractCegarLoop]: Abstraction has 164 states and 189 transitions.
[2025-05-07 17:27:44,933 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 16.333333333333332) internal successors, (49), 4 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 3 states have return successors, (31), 3 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:27:44,933 INFO  L278                IsEmpty]: Start isEmpty. Operand 164 states and 189 transitions.
[2025-05-07 17:27:44,934 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-05-07 17:27:44,934 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:44,934 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:44,934 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:27:44,934 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:44,934 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:44,934 INFO  L85        PathProgramCache]: Analyzing trace with hash 277372397, now seen corresponding path program 1 times
[2025-05-07 17:27:44,934 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:44,935 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [822689224]
[2025-05-07 17:27:44,935 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:44,935 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:44,961 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-05-07 17:27:44,979 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-05-07 17:27:44,979 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:44,979 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,083 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:27:45,084 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:45,084 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [822689224]
[2025-05-07 17:27:45,084 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [822689224] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:45,084 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:45,084 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:27:45,084 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2056016479]
[2025-05-07 17:27:45,084 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:45,084 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:45,085 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:45,085 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:45,085 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:45,085 INFO  L87              Difference]: Start difference. First operand 164 states and 189 transitions. Second operand  has 6 states, 5 states have (on average 9.8) internal successors, (49), 6 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (31), 6 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:27:45,124 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,124 INFO  L93              Difference]: Finished difference Result 157 states and 174 transitions.
[2025-05-07 17:27:45,124 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:45,124 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.8) internal successors, (49), 6 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (31), 6 states have call predecessors, (31), 4 states have call successors, (31) Word has length 111
[2025-05-07 17:27:45,125 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,126 INFO  L225             Difference]: With dead ends: 157
[2025-05-07 17:27:45,126 INFO  L226             Difference]: Without dead ends: 154
[2025-05-07 17:27:45,126 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:27:45,126 INFO  L437           NwaCegarLoop]: 171 mSDtfsCounter, 0 mSDsluCounter, 669 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 840 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:27:45,127 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 840 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:45,127 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 154 states.
[2025-05-07 17:27:45,131 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 154 to 154.
[2025-05-07 17:27:45,132 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 154 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 49 states have call successors, (51), 40 states have call predecessors, (51), 40 states have return successors, (51), 47 states have call predecessors, (51), 49 states have call successors, (51)
[2025-05-07 17:27:45,133 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 168 transitions.
[2025-05-07 17:27:45,133 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 168 transitions. Word has length 111
[2025-05-07 17:27:45,133 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,133 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 168 transitions.
[2025-05-07 17:27:45,133 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.8) internal successors, (49), 6 states have internal predecessors, (49), 4 states have call successors, (31), 1 states have call predecessors, (31), 5 states have return successors, (31), 6 states have call predecessors, (31), 4 states have call successors, (31)
[2025-05-07 17:27:45,133 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 168 transitions.
[2025-05-07 17:27:45,134 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 137
[2025-05-07 17:27:45,135 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,135 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27:45,135 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:27:45,135 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:45,135 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:45,135 INFO  L85        PathProgramCache]: Analyzing trace with hash 1899059109, now seen corresponding path program 1 times
[2025-05-07 17:27:45,135 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:45,136 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1514776338]
[2025-05-07 17:27:45,136 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,136 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:45,178 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 136 statements into 1 equivalence classes.
[2025-05-07 17:27:45,181 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 136 of 136 statements.
[2025-05-07 17:27:45,181 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,181 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,285 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:27:45,285 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:45,285 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1514776338]
[2025-05-07 17:27:45,285 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1514776338] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:45,285 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:45,285 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:45,285 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [946395290]
[2025-05-07 17:27:45,285 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:45,285 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:45,286 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:45,286 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:45,286 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:45,286 INFO  L87              Difference]: Start difference. First operand 154 states and 168 transitions. Second operand  has 4 states, 3 states have (on average 20.0) internal successors, (60), 4 states have internal predecessors, (60), 3 states have call successors, (38), 1 states have call predecessors, (38), 3 states have return successors, (38), 3 states have call predecessors, (38), 3 states have call successors, (38)
[2025-05-07 17:27:45,294 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,294 INFO  L93              Difference]: Finished difference Result 156 states and 169 transitions.
[2025-05-07 17:27:45,294 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:45,295 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 20.0) internal successors, (60), 4 states have internal predecessors, (60), 3 states have call successors, (38), 1 states have call predecessors, (38), 3 states have return successors, (38), 3 states have call predecessors, (38), 3 states have call successors, (38) Word has length 136
[2025-05-07 17:27:45,295 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,295 INFO  L225             Difference]: With dead ends: 156
[2025-05-07 17:27:45,295 INFO  L226             Difference]: Without dead ends: 147
[2025-05-07 17:27:45,296 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:27:45,296 INFO  L437           NwaCegarLoop]: 168 mSDtfsCounter, 1 mSDsluCounter, 323 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 491 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:27:45,296 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 491 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:45,297 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 147 states.
[2025-05-07 17:27:45,299 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 147 to 147.
[2025-05-07 17:27:45,300 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 147 states, 64 states have (on average 1.015625) internal successors, (65), 65 states have internal predecessors, (65), 42 states have call successors, (44), 40 states have call predecessors, (44), 40 states have return successors, (44), 41 states have call predecessors, (44), 42 states have call successors, (44)
[2025-05-07 17:27:45,300 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 147 states to 147 states and 153 transitions.
[2025-05-07 17:27:45,300 INFO  L79                 Accepts]: Start accepts. Automaton has 147 states and 153 transitions. Word has length 136
[2025-05-07 17:27:45,301 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,301 INFO  L485      AbstractCegarLoop]: Abstraction has 147 states and 153 transitions.
[2025-05-07 17:27:45,301 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 20.0) internal successors, (60), 4 states have internal predecessors, (60), 3 states have call successors, (38), 1 states have call predecessors, (38), 3 states have return successors, (38), 3 states have call predecessors, (38), 3 states have call successors, (38)
[2025-05-07 17:27:45,301 INFO  L278                IsEmpty]: Start isEmpty. Operand 147 states and 153 transitions.
[2025-05-07 17:27:45,302 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 137
[2025-05-07 17:27:45,302 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,302 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27:45,302 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:27:45,302 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:45,303 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:45,303 INFO  L85        PathProgramCache]: Analyzing trace with hash -908604245, now seen corresponding path program 1 times
[2025-05-07 17:27:45,303 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:45,303 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1606049302]
[2025-05-07 17:27:45,303 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,303 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:45,339 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 136 statements into 1 equivalence classes.
[2025-05-07 17:27:45,378 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 136 of 136 statements.
[2025-05-07 17:27:45,378 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,378 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,550 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:27:45,550 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:45,550 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1606049302]
[2025-05-07 17:27:45,550 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1606049302] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:45,551 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:45,551 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:45,551 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1504611753]
[2025-05-07 17:27:45,551 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:45,551 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:45,551 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:45,552 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:45,552 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:45,552 INFO  L87              Difference]: Start difference. First operand 147 states and 153 transitions. Second operand  has 7 states, 5 states have (on average 12.0) internal successors, (60), 7 states have internal predecessors, (60), 5 states have call successors, (38), 1 states have call predecessors, (38), 5 states have return successors, (38), 6 states have call predecessors, (38), 5 states have call successors, (38)
[2025-05-07 17:27:45,638 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,638 INFO  L93              Difference]: Finished difference Result 151 states and 157 transitions.
[2025-05-07 17:27:45,638 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:45,639 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 12.0) internal successors, (60), 7 states have internal predecessors, (60), 5 states have call successors, (38), 1 states have call predecessors, (38), 5 states have return successors, (38), 6 states have call predecessors, (38), 5 states have call successors, (38) Word has length 136
[2025-05-07 17:27:45,639 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,640 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:27:45,640 INFO  L226             Difference]: Without dead ends: 151
[2025-05-07 17:27:45,640 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:27:45,640 INFO  L437           NwaCegarLoop]: 151 mSDtfsCounter, 2 mSDsluCounter, 734 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 885 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:45,641 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 885 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:45,641 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 151 states.
[2025-05-07 17:27:45,645 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 151 to 149.
[2025-05-07 17:27:45,645 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 65 states have (on average 1.0153846153846153) internal successors, (66), 66 states have internal predecessors, (66), 42 states have call successors, (44), 40 states have call predecessors, (44), 41 states have return successors, (45), 42 states have call predecessors, (45), 42 states have call successors, (45)
[2025-05-07 17:27:45,646 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 155 transitions.
[2025-05-07 17:27:45,646 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 155 transitions. Word has length 136
[2025-05-07 17:27:45,647 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,647 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 155 transitions.
[2025-05-07 17:27:45,647 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 12.0) internal successors, (60), 7 states have internal predecessors, (60), 5 states have call successors, (38), 1 states have call predecessors, (38), 5 states have return successors, (38), 6 states have call predecessors, (38), 5 states have call successors, (38)
[2025-05-07 17:27:45,647 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 155 transitions.
[2025-05-07 17:27:45,649 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 137
[2025-05-07 17:27:45,649 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,649 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27:45,649 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:27:45,649 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:45,649 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:45,650 INFO  L85        PathProgramCache]: Analyzing trace with hash 905692463, now seen corresponding path program 1 times
[2025-05-07 17:27:45,650 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:45,650 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1421228731]
[2025-05-07 17:27:45,650 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,650 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:45,693 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 136 statements into 1 equivalence classes.
[2025-05-07 17:27:45,701 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 136 of 136 statements.
[2025-05-07 17:27:45,701 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,701 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:45,799 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:27:45,799 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:45,799 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1421228731]
[2025-05-07 17:27:45,799 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1421228731] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:45,799 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:45,799 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:45,799 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1222041489]
[2025-05-07 17:27:45,799 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:45,800 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:45,800 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:45,800 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:45,800 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:45,800 INFO  L87              Difference]: Start difference. First operand 149 states and 155 transitions. Second operand  has 4 states, 3 states have (on average 20.0) internal successors, (60), 4 states have internal predecessors, (60), 4 states have call successors, (38), 1 states have call predecessors, (38), 3 states have return successors, (38), 4 states have call predecessors, (38), 4 states have call successors, (38)
[2025-05-07 17:27:45,815 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:45,815 INFO  L93              Difference]: Finished difference Result 151 states and 156 transitions.
[2025-05-07 17:27:45,816 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:27:45,816 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 20.0) internal successors, (60), 4 states have internal predecessors, (60), 4 states have call successors, (38), 1 states have call predecessors, (38), 3 states have return successors, (38), 4 states have call predecessors, (38), 4 states have call successors, (38) Word has length 136
[2025-05-07 17:27:45,816 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:45,817 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:27:45,817 INFO  L226             Difference]: Without dead ends: 141
[2025-05-07 17:27:45,818 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:27:45,818 INFO  L437           NwaCegarLoop]: 153 mSDtfsCounter, 1 mSDsluCounter, 290 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 443 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:45,818 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 443 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:45,819 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-05-07 17:27:45,824 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 141.
[2025-05-07 17:27:45,825 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 141 states, 62 states have (on average 1.0) internal successors, (62), 62 states have internal predecessors, (62), 39 states have call successors, (40), 39 states have call predecessors, (40), 39 states have return successors, (40), 39 states have call predecessors, (40), 39 states have call successors, (40)
[2025-05-07 17:27:45,826 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 141 states to 141 states and 142 transitions.
[2025-05-07 17:27:45,826 INFO  L79                 Accepts]: Start accepts. Automaton has 141 states and 142 transitions. Word has length 136
[2025-05-07 17:27:45,826 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:45,826 INFO  L485      AbstractCegarLoop]: Abstraction has 141 states and 142 transitions.
[2025-05-07 17:27:45,826 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 20.0) internal successors, (60), 4 states have internal predecessors, (60), 4 states have call successors, (38), 1 states have call predecessors, (38), 3 states have return successors, (38), 4 states have call predecessors, (38), 4 states have call successors, (38)
[2025-05-07 17:27:45,827 INFO  L278                IsEmpty]: Start isEmpty. Operand 141 states and 142 transitions.
[2025-05-07 17:27:45,828 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 137
[2025-05-07 17:27:45,828 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:45,829 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27:45,829 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:27:45,829 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:45,829 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:45,829 INFO  L85        PathProgramCache]: Analyzing trace with hash -210365757, now seen corresponding path program 1 times
[2025-05-07 17:27:45,830 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:45,830 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1922159339]
[2025-05-07 17:27:45,830 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:45,830 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:45,888 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 136 statements into 1 equivalence classes.
[2025-05-07 17:27:45,921 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 136 of 136 statements.
[2025-05-07 17:27:45,921 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:45,921 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:46,054 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:27:46,055 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:46,055 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1922159339]
[2025-05-07 17:27:46,055 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1922159339] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:46,055 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:46,055 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:27:46,055 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2090820488]
[2025-05-07 17:27:46,055 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:46,055 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:27:46,055 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:46,056 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:27:46,056 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:46,056 INFO  L87              Difference]: Start difference. First operand 141 states and 142 transitions. Second operand  has 7 states, 6 states have (on average 10.0) internal successors, (60), 7 states have internal predecessors, (60), 4 states have call successors, (38), 1 states have call predecessors, (38), 6 states have return successors, (38), 6 states have call predecessors, (38), 4 states have call successors, (38)
[2025-05-07 17:27:46,093 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:46,093 INFO  L93              Difference]: Finished difference Result 151 states and 155 transitions.
[2025-05-07 17:27:46,093 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:27:46,093 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 10.0) internal successors, (60), 7 states have internal predecessors, (60), 4 states have call successors, (38), 1 states have call predecessors, (38), 6 states have return successors, (38), 6 states have call predecessors, (38), 4 states have call successors, (38) Word has length 136
[2025-05-07 17:27:46,094 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:46,094 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:27:46,094 INFO  L226             Difference]: Without dead ends: 137
[2025-05-07 17:27:46,094 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:46,095 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 714 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 860 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:27:46,095 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 860 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:27:46,095 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-05-07 17:27:46,097 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 137.
[2025-05-07 17:27:46,098 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 60 states have (on average 1.0) internal successors, (60), 60 states have internal predecessors, (60), 38 states have call successors, (38), 38 states have call predecessors, (38), 38 states have return successors, (38), 38 states have call predecessors, (38), 38 states have call successors, (38)
[2025-05-07 17:27:46,098 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 136 transitions.
[2025-05-07 17:27:46,098 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 136 transitions. Word has length 136
[2025-05-07 17:27:46,098 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:46,099 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 136 transitions.
[2025-05-07 17:27:46,099 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 10.0) internal successors, (60), 7 states have internal predecessors, (60), 4 states have call successors, (38), 1 states have call predecessors, (38), 6 states have return successors, (38), 6 states have call predecessors, (38), 4 states have call successors, (38)
[2025-05-07 17:27:46,099 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 136 transitions.
[2025-05-07 17:27:46,099 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 137
[2025-05-07 17:27:46,100 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:46,100 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:27:46,100 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:27:46,100 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:46,100 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:46,100 INFO  L85        PathProgramCache]: Analyzing trace with hash 1208995263, now seen corresponding path program 1 times
[2025-05-07 17:27:46,100 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:46,100 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1336671951]
[2025-05-07 17:27:46,100 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:46,100 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:46,144 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 136 statements into 1 equivalence classes.
[2025-05-07 17:27:46,169 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 136 of 136 statements.
[2025-05-07 17:27:46,169 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:46,169 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:46,638 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:27:46,638 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:46,638 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1336671951]
[2025-05-07 17:27:46,638 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1336671951] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:46,638 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:46,638 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [14] imperfect sequences [] total 14
[2025-05-07 17:27:46,638 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1398903883]
[2025-05-07 17:27:46,638 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:46,638 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-05-07 17:27:46,638 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:46,639 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-05-07 17:27:46,639 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=157, Unknown=0, NotChecked=0, Total=182
[2025-05-07 17:27:46,639 INFO  L87              Difference]: Start difference. First operand 137 states and 136 transitions. Second operand  has 14 states, 11 states have (on average 5.454545454545454) internal successors, (60), 12 states have internal predecessors, (60), 7 states have call successors, (38), 1 states have call predecessors, (38), 11 states have return successors, (38), 12 states have call predecessors, (38), 7 states have call successors, (38)
[2025-05-07 17:27:46,744 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:46,744 INFO  L93              Difference]: Finished difference Result 94 states and 93 transitions.
[2025-05-07 17:27:46,745 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:27:46,745 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 11 states have (on average 5.454545454545454) internal successors, (60), 12 states have internal predecessors, (60), 7 states have call successors, (38), 1 states have call predecessors, (38), 11 states have return successors, (38), 12 states have call predecessors, (38), 7 states have call successors, (38) Word has length 136
[2025-05-07 17:27:46,745 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:46,745 INFO  L225             Difference]: With dead ends: 94
[2025-05-07 17:27:46,745 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:27:46,746 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 16 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=207, Unknown=0, NotChecked=0, Total=240
[2025-05-07 17:27:46,746 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 2 mSDsluCounter, 991 mSDsCounter, 0 mSdLazyCounter, 105 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1076 SdHoareTripleChecker+Invalid, 105 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 105 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:46,746 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1076 Invalid, 105 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 105 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:27:46,747 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:27:46,747 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:27:46,747 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:27:46,747 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:27:46,747 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 136
[2025-05-07 17:27:46,747 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:46,747 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:27:46,747 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 11 states have (on average 5.454545454545454) internal successors, (60), 12 states have internal predecessors, (60), 7 states have call successors, (38), 1 states have call predecessors, (38), 11 states have return successors, (38), 12 states have call predecessors, (38), 7 states have call successors, (38)
[2025-05-07 17:27:46,747 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:27:46,748 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:27:46,750 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:27:46,750 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:27:46,753 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:46,755 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:27:46,757 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:27:46 BoogieIcfgContainer
[2025-05-07 17:27:46,757 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:27:46,758 INFO  L158              Benchmark]: Toolchain (without parser) took 4410.87ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 138.8MB in the beginning and 231.1MB in the end (delta: -92.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:46,758 INFO  L158              Benchmark]: SmtParser took 0.18ms. 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:27:46,758 INFO  L158              Benchmark]: ChcToBoogie took 48.59ms. Allocated memory is still 234.9MB. Free memory was 138.6MB in the beginning and 135.0MB in the end (delta: 3.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:27:46,759 INFO  L158              Benchmark]: Boogie Preprocessor took 78.25ms. Allocated memory is still 234.9MB. Free memory was 135.0MB in the beginning and 131.0MB in the end (delta: 4.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:46,759 INFO  L158              Benchmark]: RCFGBuilder took 552.33ms. Allocated memory is still 234.9MB. Free memory was 131.0MB in the beginning and 139.5MB in the end (delta: -8.6MB). Peak memory consumption was 26.9MB. Max. memory is 33.6GB.
[2025-05-07 17:27:46,759 INFO  L158              Benchmark]: TraceAbstraction took 3728.04ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 139.0MB in the beginning and 231.1MB in the end (delta: -92.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:27:46,760 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.18ms. Allocated memory is still 234.9MB. Free memory is still 173.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 48.59ms. Allocated memory is still 234.9MB. Free memory was 138.6MB in the beginning and 135.0MB in the end (delta: 3.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 78.25ms. Allocated memory is still 234.9MB. Free memory was 135.0MB in the beginning and 131.0MB in the end (delta: 4.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 552.33ms. Allocated memory is still 234.9MB. Free memory was 131.0MB in the beginning and 139.5MB in the end (delta: -8.6MB). Peak memory consumption was 26.9MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3728.04ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 139.0MB in the beginning and 231.1MB in the end (delta: -92.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 41 procedures, 182 locations, 307 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.7s, OverallIterations: 14, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 142 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 13 mSDsluCounter, 10876 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 8379 mSDsCounter, 20 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 390 IncrementalHoareTripleChecker+Invalid, 410 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 20 mSolverCounterUnsat, 2497 mSDtfsCounter, 390 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 85 GetRequests, 28 SyntacticMatches, 0 SemanticMatches, 57 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=182occurred in iteration=0, InterpolantAutomatonStates: 82, 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, 14 MinimizatonAttempts, 12 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 1.8s InterpolantComputationTime, 1359 NumberOfCodeBlocks, 1359 NumberOfCodeBlocksAsserted, 14 NumberOfCheckSat, 1345 ConstructedInterpolants, 0 QuantifiedInterpolants, 1624 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 14 InterpolantComputations, 14 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:27:46,771 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
