Skip to content

Commit

Permalink
expect
Browse files Browse the repository at this point in the history
  • Loading branch information
fabiomadge committed Jun 24, 2024
1 parent a679719 commit f0d49eb
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions assets/src/brittleness/RationalAdd.dfy.expect
Original file line number Diff line number Diff line change
Expand Up @@ -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 f0d49eb

Please sign in to comment.