pysat: Clausification of nested Implication fails

I am not sure if I have some big misunderstanding, but I can’t get clausification of conjunctions of implications to work. Conjunctions of other conjunctions or disjunctions I got to work fine.

Here is my minimal test case:

import pysat
print(pysat.VERSION)
from pysat.formula import Atom, Implies, And
And(Implies(Atom(1), Atom(2))).clausify()

And the result is

(1, 8, 'dev', 1)
Traceback (most recent call last):
  File "/home/maweki/s/python/orange-boxes/case.py", line 4, in <module>
    And(Implies(Atom(1), Atom(2))).clausify()
  File "/home/maweki/.local/lib/python3.12/site-packages/pysat/formula.py", line 1167, in clausify
    self._clausify(name_required=False)
  File "/home/maweki/.local/lib/python3.12/site-packages/pysat/formula.py", line 1594, in _clausify
    sub._clausify(name_required=True)
  File "/home/maweki/.local/lib/python3.12/site-packages/pysat/formula.py", line 2134, in _clausify
    self.clauses.append([self.name, -self.clauses[0][i]])
                                     ~~~~~~~~~~~~~~~^^^
IndexError: list index out of range

Clausify of the implication itself works fine.

But using And, Or, Neg to nest the implication leads to this error.

Or(Implies(Atom(1), Atom(2))).clausify()
And(Implies(Atom(1), Atom(2))).clausify()
Neg(Implies(Atom(1), Atom(2))).clausify()

All of these fail

Edit: it seems to me, that this codepath must raise an exception as it always goes out of bounds

https://github.com/pysathq/pysat/blob/a3266647552e72abdab838944817e2f92a06fc00/pysat/formula.py#L2132C1-L2134C70

            # clauses representing converse implication
            for i in range(1, len(self.clauses[0]) + 1):
                self.clauses.append([self.name, -self.clauses[0][i]])