Simmo Saan

> * is there an ideal amount of tests I should write or can I write as many as I feel to be necessary? As many as necessary to cover...

This PR has 115 commits which looks like a lot of intermediate changes that got reverted/removed by the end? In that case it would make sense to **squash merge** this...

By the way, are there any programs in sv-benchmarks or our bench where such situation occurs at all?

> I can go for the interactive rebase. Would it be enough if I remove all commits concerning the alternative version, which is completely removed now or should I also...

Since this history contains some merges from `master`, the rebase also starts rebasing some merged things to linearize the history. Using `--rebase-merges` should help, one just needs to not touch...

We've added `executing_speculative_computations` in many places, but not to `memOutOfBounds`, which unfortunately duplicates a lot of the logic on pointer arithmetic, etc. However, I think this shouldn't be a problem...

With `--trace sol --trace sol2 --trace solchange` you can see the last iteration (immediately after the `narrow` by `meet`) of that unknown: ``` %%% sol: Var: L:node 27 "xtmp >...

The upper bound `4294967293` overflows `int`, which is probably why it goes to top. Maybe with `sem.int.signed_overflow` being `assume_none` it'd behave differently? Either way, there's something strange because there should...

Looks like this causes all of our tests to fail because we're probably matching the old format in some scripts. Also, all of the cram tests will get touched by...

I'm still wondering where this notation comes from. I managed to find some kind of default regexes in VSCode here: https://github.com/microsoft/vscode/blob/fad39b690188aa2a5e9ebe87c3d51ee1afdf9dfd/src/vs/workbench/contrib/tasks/common/problemMatcher.ts#L1491-L1603. But none of them matches the format with the...