Broadcasting new theorems causing existing exec proofs to fail

[LoganSchmalz]

I am messing with broadcasting and experiencing an issue where broadcasting a new theorem causes existing previously-successful executable functions to have assertions fail. Is this expected behavior?

[ahuoguo]

I have also experienced this. If you broadcast too aggressively, the search space for SMT solvers increases by a lot, which might result in verification failure.

[LoganSchmalz]

Interesting. I would expect it to happen if you broadcast truly excessively, but I seem to be running into this even with only two or three theorems broadcast. Are you suggesting this is a timeout? I am getting an explicit assertion failed message and it doesn't seem to be taking substantially longer.

Is there a different error message for timeouts, or is it possible to increase the limit for Verus (I tried increasing the rlimit but that doesn't seem to have done anything)?

[ahuoguo]

Broadcasting two or three functions might cause triggers to behave very differently, and the solver will give you a fast unknown answer.

I’m not sure if there are other ways to “increase timeouts”. The thing to do is probably limit the shaky assertions. Can you try spinoff prover for that exact function failing.

[LoganSchmalz]

It doesn't look like spinoff has changed anything either. It must be something funny with the way the SMT solver is handling the context, as you said, "a fast unknown answer".

[tjhance]

This kind of "flaky" proof behavior often happens because of heuristics in the SMT solver that cause unintuitive behaviors. There have been some attempts to quantify this behavior by some of the Verus team, see for example Mariposa or Cazamariposas