summaryrefslogtreecommitdiff
path: root/Test/floats/float11.bpl.expect
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 21:11:23 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 21:11:23 -0600
commit754f7d3ef36e11740a40a2d687f3b15195f63d9a (patch)
tree25b2ca0d03416aa6873680424fc481aeed004d67 /Test/floats/float11.bpl.expect
parent5cff8cd77c629ec8e48a2498b1e704173306586a (diff)
Polished up the floats test folder. Preparing to rebase
Diffstat (limited to 'Test/floats/float11.bpl.expect')
-rw-r--r--Test/floats/float11.bpl.expect8
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect
index 19e55fef..9365da58 100644
--- a/Test/floats/float11.bpl.expect
+++ b/Test/floats/float11.bpl.expect
@@ -1,7 +1,7 @@
-..\Test\floats\float11.bpl(21,2): Error BP5001: This assertion might not hold.
+float11.bpl(21,2): Error BP5001: This assertion might not hold.
Execution trace:
- ..\Test\floats\float11.bpl(12,7): anon0
- ..\Test\floats\float11.bpl(16,2): anon3_LoopHead
- ..\Test\floats\float11.bpl(16,2): anon3_LoopDone
+ float11.bpl(12,7): anon0
+ float11.bpl(16,2): anon3_LoopHead
+ float11.bpl(16,2): anon3_LoopDone
Boogie program verifier finished with 0 verified, 1 error