X-Git-Url: http://git.lttng.org/?a=blobdiff_plain;f=verif%2Fnico-md-merge%2Fcommit_sum.ltl;fp=verif%2Fnico-md-merge%2Fcommit_sum.ltl;h=0000000000000000000000000000000000000000;hb=a219d12930979a81f43a3a3f5499b2bd00141a84;hp=b43d29225e1134620422884c4b19d452e704b4f1;hpb=31efe1f8304f09a4f4139c387a98d3215cd423c9;p=lttv.git

diff --git a/verif/nico-md-merge/commit_sum.ltl b/verif/nico-md-merge/commit_sum.ltl
deleted file mode 100755
index b43d2922..00000000
--- a/verif/nico-md-merge/commit_sum.ltl
+++ /dev/null
@@ -1,6 +0,0 @@
-// The sum of all subbuffer commit counts must always be lower or equal
-// to the writer head, because space must be reserved before it is
-// written to and then committed.
-// assert(write_off - _commit_sum >= 0 && write_off - _commit_sum < HALF_UCHAR);
-
-[] (wcsum1 && wcsum2)