Skip to content

Commit

Permalink
try fix test
Browse files Browse the repository at this point in the history
  • Loading branch information
fabiomadge committed Oct 17, 2024
1 parent 9bedde6 commit 804aa4c
Showing 1 changed file with 3 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -377,7 +377,7 @@ method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
</span><span class="na" id="360:1">// False antecedent assert statement.
method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
var y := x*x;
assert </span><span class="nc" id="363:10">y < 0 ==> x </span><span class="na" id="363:22"><</span><span class="nc" id="363:23"> 0</span><span class="na" id="363:25">;
assert y < 0 ==> x < 0;
}

// False antecedent ensures clause.
Expand Down Expand Up @@ -459,11 +459,11 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (
function {:testEntry} GetX(c: C): int
reads c
{
</span><span class="nc" id="445:3">c.</span><span class="na" id="445:5">x
</span><span class="nc" id="446:3">c.</span><span class="na" id="446:5">x
}

method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
assume </span><span class="nc" id="449:10">t</span><span class="na" id="449:11">rue;
assume </span><span class="nc" id="450:10">t</span><span class="na" id="450:11">rue;
assert 1 + x == x + 1;
}

Expand Down

0 comments on commit 804aa4c

Please sign in to comment.