Arie Gurfinkel

@hgvk94 I think you looked at this already. What was the conclusion?

Check whether you can get the reason for unknown using `get_reason_unknown`. These things are not easy to debug, and you are using quantifiers, which makes things less deterministic. However, I...

The trace seems cut off. It ends with expand-pob not inside propagate with add-lemma.

This was to help reproduce the error. If the problem is due to randomness of heavy load, it might be possible to reproduce it reliably with a different random seed....

if you can repro this reliably then we can figure out how I can run it. My understanding that now it only happens under certain load on your machine. If...

Can you please provide branch and options used.

This PR is current work in progress. Your input does not crash on my version of this branch. The PR will be updated soon. Unfortunately, my current local state is...

Spacer does not deal properly with uninterpreted functions. Non-linear `mod` is treated as UF. This used to "work". But recent fuzzing required being more aggressive at excluding benchmarks that include...

@NikolajBjorner this, and maybe other protections, for supported features seems too harsh for current users. In SeaHorn case, for example, it is assumed that for every `mod(x, y)`, `y` is...

Hey @leonardoalt , this is on my plate as per discussion above. Are you using spacer through the horn tactic? If you use it directly, I believe this check is...