Pieter Bos

Thanks for looking into it, I think your take on it is right! I do think it would be nicer / more consistent if there was a global default encoding...

I ran into this while toying with a newer z3. Do you think the proposed workaround (setting a high timeout just for push) is an option for silicon?

We encountered this issue, I think it applies here (but please let me know if not) Here is a reduced example from a case we encountered: ```silver field f: Int...

I think that the failures themselves are already almost the correct measure since they're (all?) case classes, except that the `offendingNode` is compared structurally, so maybe something like: ```scala class...

Yes, I think this is a good way to expose this behaviour to the viper frontends :). I imagine we will need to put a running tally or so into...

@thesamet any chance you could have a look?

Thanks! I can't test it out immediately in our build because we use [mill](https://github.com/com-lihaoyi/mill), which has a different entry point for scalapbc [here](https://github.com/com-lihaoyi/mill/blob/25d975dda4f68c27835f4ee4ec491199a06b3a25/contrib/scalapblib/src/mill/contrib/scalapblib/ScalaPBWorker.scala#L21-L22). I'll try to hack in a solution...

Still posting the stuff below in case I'm wrong, but I just now realized: isn't this stack trace from creating the actual task objects, rather than evaluating any tasks? I...

- [x] The LLVM specification parser sets `specLevel = 1` but there are proper `StartSpec`/`EndSpec` tokens that appear to be parsed, what gives? - [x] Can't derive the localInclude of...

If you have a reproducer for an example needing so much stack memory I'd appreciate it :)