Skip to content

Commit

Permalink
accept
Browse files Browse the repository at this point in the history
the newlines are gone again, due to an older Silicon backend
  • Loading branch information
ggreif committed Nov 18, 2022
1 parent b68376c commit 1a82e29
Show file tree
Hide file tree
Showing 4 changed files with 0 additions and 5 deletions.
2 changes: 0 additions & 2 deletions test/viper/ok/assertions.silicon.ok
Original file line number Diff line number Diff line change
@@ -1,4 +1,2 @@
[0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. ([email protected])

[1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. ([email protected])

1 change: 0 additions & 1 deletion test/viper/ok/async.silicon.ok
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
[0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. ([email protected])

1 change: 0 additions & 1 deletion test/viper/ok/claim-broken.silicon.ok
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
[0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. ([email protected])

1 change: 0 additions & 1 deletion test/viper/ok/invariant.silicon.ok
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
[0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. ([email protected])

0 comments on commit 1a82e29

Please sign in to comment.