Implement proper naïve unassume in var_eq

[sim642]

Closes #1710.

This also improves the precision of branch in var_eq by making it learn equalities from branching expressions. Previously it only learned from assignments.

TODO

• Get this to fully validate the case from Reduce var_eq witness invariants from quadratic to linear #1826. Can do all equalities generated by var_eq, but there are a few disjunctions we generate but cannot validate.
• Merge PR Deduplicate stack ARG InlineReturn edges based on InlineEntry lval and args #1828 before.
• Add tests (branch and unassume).
• sv-benchmarks verify-validation run.

[sim642]

The precision improvement of branch didn't give new correct verdicts with 60s on sv-benchmarks.
However, the unassume part makes us self-validate 41 more witnesses than before: https://goblint.cs.ut.ee/results/283-all-validate-pr-1827-after/table-generator-cmp.table.html#/table?hidden=0,1,2,3&filter=4(0*status*(status(in(true)),category(notIn()))),5(0*status*(status(notIn(true)),category(notIn()))),6(0*status*(status(in(true)),category(notIn()))),7(0*status*(status(in(true)),category(notIn()))).