diff --git a/docs/papers/amend.md b/docs/papers/amend.md index 37d532949..55e756c1b 100644 --- a/docs/papers/amend.md +++ b/docs/papers/amend.md @@ -27,8 +27,8 @@ edge being *tainted* by the decision diagram's reduction rule [[ATVA v2.0 ------------------------ -For *Nested Sweeping*, we need to mark an arc's *source* to be originating from -the *outer sweep*. Yet, the *flag* was up to this point used to store the +For *Nested Sweeping*, we need to *taint* an arc's *source* to be originating +from the *outer sweep*. Yet, the *flag* was up to this point used to store the *out-index* of the source. Hence, for *internal nodes* we introduce the out-index (*p*) on the second least-significant bit - essentially adding a second (possibly non-Boolean) *flag*. @@ -54,7 +54,7 @@ To get the maximum width safe from overflows back up to 6 TiB, we have removed the most significant *terminal bit flag*. Instead, now all pointers dedicate the ℓ most significant bits to its *level*. The largest level is dedicated to *null* and the second-largest to *terminals*. This decreases the number of BDD labels -by 2 and also restricts *terminal* values to it into 64-ℓ-1-1 = 62-ℓ bits. Yet, +by 2 and also restricts *terminal* values to fit into 64-ℓ-1-1 = 62-ℓ bits. Yet, this is fine for `bool`, `char`, `int`, and `float`. **Figure 10 (a):**