Skip to content

Commit

Permalink
Fix brittleness test
Browse files Browse the repository at this point in the history
  • Loading branch information
Aleksandr Fedchin committed Mar 21, 2024
1 parent d713eb1 commit fc8b1ec
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions assets/src/brittleness/RationalAdd.dfy.expect
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
RationalAdd.dfy(4,4): Warning: /!\ No terms found to trigger on.
RationalAdd.dfy(4,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
|
4 | exists n: int, m: int :: m > 0 && x == (n as real) / (m as real)
| ^^^^^^
Expand All @@ -16,12 +16,12 @@ RationalAdd.dfy(17,12): Related location: this is the postcondition that could n
RationalAdd.dfy(42,11): Error: assertion might not hold
|
42 | assert (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

RationalAdd.dfy(43,11): Error: assertion might not hold
|
43 | assert r == (((x1 * y2) + (y1 * x2)) as real) / (final_d as real);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 9 verified, 3 errors

0 comments on commit fc8b1ec

Please sign in to comment.