Anomaly in call

[ahuelsing]

Line 121 of attached file (had to rename it from eca to txt) causes "anomaly: EcLib.EcPV.EqObsInError". The tactic executed is a call.

SEUFCMA_EUFCMA(1).txt

[ahuelsing]

Sorry, did not save before store
SEUFCMA_EUFCMA.txt

[fdupress]

Thanks. (Now) Reproduced on main.

Prognosis here is that this gets fixed with a proper error message (that call with an invariant only works when both sides end with a call to an abstract procedure).

[fdupress]

Raised in mk_inv_spec (src/phl/ecPhlCall.ml, line 508).