actually on that previous example, if you do want to get it to prove with smtbmc with multiclock on, you can use the kind of things you wrote before, something like
```
(* gclk *) wire gclk;
always_ff @(posedge clk) assume($changed({rst_n, clk}));
```