fast_check_subsumption causes Could not convert ML predicate to sort Bool error

[palinatolmach]

Related: #2287

fast_check_subsumption = True was introduced in #2243, causing failures in erc20 claims in CI tests. As @tothtamas28 found out, it's causing the following issue when running

poetry -C kevm-pyk run -- kevm kompile-spec tests/specs/erc20/verification.k --main-module VERIFICATION --output definition
poetry -C kevm-pyk run -- kevm prove tests/specs/erc20/hkg/transferFrom-failure-2-spec.k --definition definition --spec-module TRANSFERFROM-FAILURE-2-SPEC  --verbose --use-booster

Output (the interesting part):

INFO 2024-02-08 14:47:50,556 pyk.ktool.kprint - Invoking kore_to_kast
ERROR 2024-02-08 14:47:50,607 kevm_pyk.utils - Proof crashed: f0d4602717667cc05239620de33a8499dfb5c725aa4bcfa12a98ff90d1a94187
Could not convert ML predicate to sort Bool: KApply(label=KLabel(name='#Ceil', params=(KSort(name='Map'), KSort(name='GeneratedTopCell'))), args=(KApply(label=KLabel(name='_Map_', params=()), args=(KVariable(name='ORIGSTORAGE_CELL_311d596d', sort=KSort(name='Map')), KVariable(name='ORIGSTORAGE_CELL_a1996eba', sort=KSort(name='Map')))),))
Traceback (most recent call last):
  File "/home/ttoth/git/evm-semantics/kevm-pyk/src/kevm_pyk/utils.py", line 132, in run_prover
    prover.advance_proof(
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 863, in advance_proof
    self.save_failure_info()
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 868, in save_failure_info
    self.proof.failure_info = self.failure_info()
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 871, in failure_info
    return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 940, in from_proof
    _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
  File "/home/ttoth/git/pyk/src/pyk/kcfg/explore.py", line 265, in implication_failure_reason
    negative_cell_constraints = list(filter(_is_negative_cell_subst, antecedent.constraints))
  File "/home/ttoth/git/pyk/src/pyk/kcfg/explore.py", line 216, in _is_negative_cell_subst
    constraint_bool = ml_pred_to_bool(constraint)
  File "/home/ttoth/git/pyk/src/pyk/kast/manip.py", line 161, in ml_pred_to_bool
    return _ml_constraint_to_bool(kast)
  File "/home/ttoth/git/pyk/src/pyk/kast/manip.py", line 159, in _ml_constraint_to_bool
    raise ValueError(f'Could not convert ML predicate to sort Bool: {_kast}')
ValueError: Could not convert ML predicate to sort Bool: KApply(label=KLabel(name='#Ceil', params=(KSort(name='Map'), KSort(name='GeneratedTopCell'))), args=(KApply(label=KLabel(name='_Map_', params=()), args=(KVariable(name='ORIGSTORAGE_CELL_311d596d', sort=KSort(name='Map')), KVariable(name='ORIGSTORAGE_CELL_a1996eba', sort=KSort(name='Map')))),))

fast_check_subsumption has been temporarily set to False in #2287 to unblock pyk upgrade, but we should further investigate the failures associated with this option.