Error in Spacer

[blishko]

For this example I am getting an error when running Z3 (both Z3 4.8.9 and current master 620204bbb) with the option fp.xform.inline_eager=false. The error reported is (error "line 289 column 47: spacer: could not validate a proof step")

When I use options fp.xform.slice=false fp.xform.inline_eager=false Z3 actually seg-faults.

When the default options are used, the production of the certificate succeeds.

I am running Z3 on macOS 10.13.6.