Property index 0 is greater than the number of properties in file (.btor2)

[CrazybinaryLi]

When I refactored the property：
always @(posedge clk) begin
if (qed_ready) begin
sqed: assert ((mem1 == mem17) && (mem2 == mem18) &&
(mem3 == mem19) && (mem4 == mem20) &&
(mem5 == mem21) && (mem6 == mem22) &&
(mem7 == mem23) && (mem8 == mem24) &&
(mem9 == mem25) && (mem10 == mem26) &&
(mem11 == mem27) && (mem12 == mem28) &&
(mem13 == mem29) && (mem14 == mem30) &&
(mem15 == mem31)
);
end
end
into the following form:
property self_consistency;
@(posedge clk) qed_ready |-> ((mem1 == mem17) && (mem2 == mem18) &&
(mem3 == mem19) && (mem4 == mem20) &&
(mem5 == mem21) && (mem6 == mem22) &&
(mem7 == mem23) && (mem8 == mem24) &&
(mem9 == mem25) && (mem10 == mem26) &&
(mem11 == mem27) && (mem12 == mem28) &&
(mem13 == mem29) && (mem14 == mem30) &&
(mem15 == mem31)
);
endproperty
sqed: assert property (self_consistency);

and attempted to generate a btor2 file, an error occurred during the solving process using Pono.

[alain-rs]

Anything about the Formal subset of SV is not currently supported in Synlig.
We are still working on the synthezisable SV subset support.

If you can sponsor such development we can find resources to work on it and expedite it, else it's probably years away.

An other alternative is you find resources to work on it and we can guide them (for free) on how to add the support.