Skip to content

Commit

Permalink
Update RationalAdd.dfy.expect
Browse files Browse the repository at this point in the history
  • Loading branch information
Dargones authored Dec 7, 2023
1 parent e1cf47a commit 36626af
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion assets/src/brittleness/RationalAdd.dfy.expect
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
RationalAdd.dfy(4,4): Warning: /!\ No terms found to trigger on.
|
4 | exists n: int, m: int :: m > 0 && x == (n as real) / (m as real)
| ^^^^^^

RationalAdd.dfy(4,4): Warning: /!\ No terms found to trigger on.
RationalAdd.dfy(13,17): Error: a postcondition could not be proved on this return path
|
13 | ghost function add(x: rat, y: rat): rat
Expand Down

0 comments on commit 36626af

Please sign in to comment.