Julian Erhard

Helmut and I were discussing just now. He thought that there might be a problem with destabilize leading to calls to `solve` for the same unknown, if the unknown depends...

@sim642 @vesalvojdani Did you benchmark this?

> His idea was to add x to the called set again before calling destabilize x, and removing it after that again. We tried this, and it fixes the termination...

> > His idea was to add x to the called set again before calling destabilize x, and removing it after that again. > > We tried this, and it...

Yes, that looks like a good starting point.

>For the first example at least, var_eq contains an additional equality between {0, main__i2} in what the solver computed, that is not there for the RHS, but he value domain...

Reverting 8bc2c89 does indeed make both test case failures disapper. Still have to investigate on how to properly fix this.

Even when not using the `pval` passed to the `tf` in line 697 by uncommenting the line here: https://github.com/goblint/analyzer/blob/1cf9b408a5846678103cc96a150767a29db3ab7e/src/framework/constraints.ml#L697-L700 the early evaluation of the `stricts` here: https://github.com/goblint/analyzer/blob/1cf9b408a5846678103cc96a150767a29db3ab7e/src/framework/constraints.ml#L729-L730 is somehow enough...

>This dependence is just very roundabout: instead of directly passing something from ctx to join, it's put into a global OCaml variable and then read on the other side. If...

What precision should the queries and e.g. the apron analysis use? In both, some IntDomTuple values are constructed. If one adapts the IntDomTuple to take a precision for all operations...