Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Dec 29, 2025

LAnd, LOr and LNot are constraint regardless of what's in their arguments (they don't need a != 0 added outside if something is non-constraint inside).

This caused us to not validate some witnesses containing trivial invariants in #1897 (comment).
For example x >= 0 && 1 does not need to be turned into (x >= 0 && 1) != 0 because one argument of && contains a non-constraint. Such doubly-constraint expression is not supported by our Apron conversion.
Instead, it can stay as it is, so the x >= 0 part is supported, but just the 1 part will be unsupported (#1610), which is irrelevant.

LAnd, LOr and LNot are constraint regardless of what's in their arguments (they don't need a != 0 added outside if something is non-constraint inside).
@sim642 sim642 added this to the SV-COMP 2027 milestone Dec 29, 2025
@sim642 sim642 added bug sv-comp SV-COMP (analyses, results), witnesses relational Relational analyses (Apron, affeq, lin2var) labels Dec 29, 2025
@sim642
Copy link
Member Author

sim642 commented Dec 31, 2025

I did verify-validate sv-benchmarks runs on level02.

There's an increase in the number of confirmed invariants:
image

There are now 50 more self-validated witnesses: https://goblint.cs.ut.ee/results/307-all-validate-level02-pr-1904-after/table-generator-cmp.table.html#/table?filter=1(0*status*(status(notIn(true)),category(notIn()))),3(0*status*(status(in(true)),category(notIn()))).
These mostly overlap with #1897 (comment), because it's a different way to deal with the same issue: instead of not generating trivial invariants, don't be bothered about triviality during validation. But we should have both PRs regardless because this also helps with validation of other tools' witnesses because there are others who also have generated trivial invariants.

@sim642 sim642 force-pushed the apron-unassume-extra-trivial branch from cc08e03 to 54c2bb9 Compare January 9, 2026 13:18
@sim642 sim642 merged commit 63e20a1 into master Jan 9, 2026
18 of 19 checks passed
@sim642 sim642 deleted the apron-unassume-extra-trivial branch January 9, 2026 14:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug relational Relational analyses (Apron, affeq, lin2var) sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant