Simmo Saan

Although this doesn't really explain the case from #1577: ```console ./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/termination.prp ../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c --html --enable dbg.termination-bounds ``` outputs (among other things) ``` [Success][Termination] Loop terminates: bounded...

> Iirc, there is some problem to be considered for when things become negative... But I would have to check that again. That might explain some of this because subtraction...

Why does this need to be inside the solver? This sounds like _widening delay_, which can be completely solver-independent and can be implemented simply as a lifting of a domain...

> @sim642 One could implement a similar feature as a domain lifter, yes. However, the effect would be subtly different: Here the delay (gas) is applied per unknown, whereas tracking...

> However, as @michael-schwarz said, the widening gas will probably mainly be meaningful for globals, so it's good to control the gas of globals and locals independently. This would be...

We discussed this during GobCon and here's the summary. Currently, `module type WPointSelect` and all of its various implementations are somewhat deep in the `Td3.Base` module itself, but the logic...

> I have extracted the modules out of td3.Base. For now, I have placed them in their own module in `src/solver`. Since this directory so far only contains solver implementations,...

**11-restart/13-changed_start_state2.c** confuses me a lot: 1. d09998584d1a38f7a8baab033af4331b692e05e7 put the TODOs there, but I don't really understand why. /cc @michael-schwarz 2. I cannot find anywhere were global variable initializers are even...

Soundness checks would've had to use `UNKNOWN!` though (or at least `UNKNOWN` if it's just our own intended imprecision from joins). I'm not sure if they're supposed to be passing...

When I looked into different logs (out vs inside of dune, full suite vs one test) I saw different results: sometimes the incremental run was success, sometimes unknown. Apparently there's...