mirror of
https://github.com/YosysHQ/yosys.git
synced 2026-09-05 19:36:55 +02:00
Both backends only looked for $assert/$assume/$cover, so a $check cell was never visited and the resulting formal output carried no proof obligations at all. write_smv already errors via its catch-all; this follows its message.