MOPSA flagging a tautological assertion
Hi, I'm working with MOPSA 1.0~pre2 (git branch:master commit:1be4dcb3 commit-date:2024-01-26 17:17:06 +0100) and just noticed that MOPSA warns me about the second assertion in the following code:
extern int __VERIFIER_nondet_int(void);
int main() {
int var0 = __VERIFIER_nondet_int();
_mopsa_assert(var0 > 0 || var0 < 1U);
_mopsa_assume(var0 < 0);
int var1 = __VERIFIER_nondet_int();
_mopsa_assume(var0 < var1);
_mopsa_assert(var0 < var1);
}
I invoked ~/mopsa-analyzer/bin/mopsa -config ~/mopsa-analyzer/share/mopsa/configs/c/default.json test.c.
MOPSA should be able to see that the assertion holds by the previous assumption. Interestingly the second assertion is found safe once I replace ">" by ">=" in the first assertion.