We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents f81c8c0 + e968dee commit 011a1c3Copy full SHA for 011a1c3
regression/cbmc/ACSL/operators.c
@@ -1,7 +1,7 @@
1
void boolean()
2
{
3
__CPROVER_bool a, b;
4
- __CPROVER_assert((a ≡ b) == (a == b), "≥");
+ __CPROVER_assert((a ≡ b) == (a == b), "≡");
5
__CPROVER_assert((a ≢ b) == (a != b), "≢");
6
__CPROVER_assert((a ⇒ b) == (!a || b), "⇒");
7
__CPROVER_assert((a ⇔ b) == (a == b), "⇔");
@@ -16,7 +16,7 @@ void relations()
16
int a, b;
17
__CPROVER_assert((a ≥ b) == (a >= b), "≥");
18
__CPROVER_assert((a ≤ b) == (a <= b), "≤");
19
20
21
__CPROVER_assert((− a) == (-a), "−");
22
}
0 commit comments