The problem disappears if the >>> is replaced with a +, -, /; the problem remains for all other shift operators, comparison operators, as well as *.

You really do not want to run clean in this context! If you look at what it actually is doing you will see the problem:

[after running all but the last 4 commands of your script]
yosys> debug clean -purge
Finding unused cells or wires in module \equiv..
  removing unused `$equiv' cell `$auto$equiv_make.cc:280:find_same_wires$15'.
  removing unused `$equiv' cell `$auto$equiv_make.cc:280:find_same_wires$16'.
  removing unused non-port wire \tmp4_gold.
  removing unused non-port wire \clock_gold.
  removing unused non-port wire \arst_gold.
  removing unused non-port wire \tmp4_gate.
  removing unused non-port wire \clock_gate.
  removing unused non-port wire \arst_gate.
  removing unused non-port wire \next_11.
  removing unused non-port wire \state_11.
Removed 2 unused cells and 8 unused wires.

If you leave out the clean command it successfully proves equivalent.

Thank you @nakengelhardt I will test proposed solution over more cases.

well some tests that where failing with clean now passing, but some other tests that where passing with clean now failing without it. Would be great having some more universal solution.

It does look like there is a bug in equiv_make that was introduced with #641; we are investigating further. This circuit used to be provable with equiv_simple before that PR.

As it turns out, #641 did not in fact fix anything, but instead disabled a necessary step in equiv_make where the users of the gold and gate versions of a signal get connected to the output of the corresponding $equiv cell. This was only masking a less common bug by introducing a worse bug that would affect nearly all designs. What equiv_make was doing in the example in #639 was unintuitive but not incorrect; the problem causing equiv_simple to pass erroneously is a fundamental design flaw in equiv_simple where it works with wrong assumptions (just picking one input to an $equiv cell as value when proving a different one). We'll revert #641 which will fix this test, but unfortunately the original bug from #639 will remain. Fixing that would require a rewrite of equiv_simple, but we have already started working on a different new tool for equivalence checking with yosys which will hopefully be an improvement over this and the other problems with the equiv_* passes.