From a6797198388c1500ff7f1cb777ae2742e21bb15a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 24 Jun 2024 15:32:56 +0200 Subject: [PATCH] expect --- assets/src/brittleness/RationalAdd.dfy.expect | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/assets/src/brittleness/RationalAdd.dfy.expect b/assets/src/brittleness/RationalAdd.dfy.expect index bfc885e..3e45191 100644 --- a/assets/src/brittleness/RationalAdd.dfy.expect +++ b/assets/src/brittleness/RationalAdd.dfy.expect @@ -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) | ^^^^^^ @@ -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