diff --git a/website/scripts/check-doc-examples.py b/website/scripts/check-doc-examples.py
index 7bf5622e75..2c48ef57d4 100644
--- a/website/scripts/check-doc-examples.py
+++ b/website/scripts/check-doc-examples.py
@@ -4,7 +4,8 @@
 Every ``.. code-block:: cpp`` block (a ```` ```cpp ```` fence in Markdown) must
 compile with cpp-verify, and when the next code block on the page is a
 ``text`` block that shows verdicts, verifying the example must give those
-verdicts. A comment right before a block changes how it is checked; several
+verdicts. The errors and warnings that block shows must be among those the
+verifier prints, apart from the location before each. A comment right before a block changes how it is checked; several
 may be stacked (in Markdown, ``<!-- cppverify-example: ... -->``):
 
     .. cppverify-example: fragment         part of a larger program: not run
@@ -17,6 +18,8 @@
                                            counterexample
     .. cppverify-example: unresolved NAME ...
                                            these stay unresolved
+    .. cppverify-example: rejects          the example is an error: cpp-verify
+                                           reports one and exits non-zero
 
 An example whose page shows no verdicts is verified too: every function
 must verify, unless a comment says it fails or stays unresolved. Comments
@@ -44,6 +47,8 @@
     r" (.+?)(?=\s+\[|\s+\(|$)")
 FAILED = re.compile(r"error: (verification failed|spec [\w ]+? failed): "
                     r"(.+?)(?=\s+\[|\s+\(|$)")
+LOCATION = re.compile(r"^\S+\.(?:cpp|h):\d+:\d+: ")
+DIAGNOSTIC = re.compile(r"^(?:error|warning): ")
 
 
 class Block:
@@ -119,10 +124,28 @@ def blocks(page):
     return found
 
 
+def diagnostics(text):
+    """The errors and warnings a text block shows, without their locations;
+    failures are compared as verdicts."""
+    shown = []
+    for line in text.splitlines():
+        line = LOCATION.sub("", line.strip())
+        if DIAGNOSTIC.match(line) and not FAILED.match(line):
+            shown.append(" ".join(line.split()))
+    return shown
+
+
+def missing_diagnostics(shown, output):
+    printed = [" ".join(LOCATION.sub("", line.strip()).split())
+               for line in output.splitlines()]
+    return [line for line in shown
+            if not any(line in candidate for candidate in printed)]
+
+
 def verdicts(text):
     shown = set()
     for line in text.splitlines():
-        line = re.sub(r"^\S+\.cpp:\d+:\d+: ", "", line.strip())
+        line = LOCATION.sub("", line.strip())
         match = VERDICT.match(line)
         if match:
             shown.add((match.group(1), match.group(2).strip()))
@@ -169,8 +192,19 @@ def check(cpp_verify, job):
     """Returns None, or a failure message and whether every mismatch is a
     function left unresolved where a proof was expected, which only the
     wall-clock budgets of a loaded machine can cause."""
-    block, source, arguments, expected, fails, unresolved = job
+    block, source, arguments, expected, fails, unresolved, shown, rejects = job
     where = f"{block.page}:{block.line}"
+    if rejects:
+        code, output = run(cpp_verify, source, arguments, 300)
+        if code is None or code == 0 or "error:" not in output:
+            return (f"{where}: the example should be an error, but cpp-verify "
+                    f"accepts it:\n{(output or '').strip()[:1500]}"), False
+        missing = missing_diagnostics(shown, output)
+        if missing:
+            return (f"{where}: the page shows diagnostics cpp-verify does not "
+                    f"print:\n" + "\n".join(f"  {line}" for line in missing) +
+                    f"\nactual output:\n{output.strip()[:2500]}"), False
+        return None
     code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300)
     if code is None or code != 0 or "error:" in output:
         return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False
@@ -180,6 +214,10 @@ def check(cpp_verify, job):
         return f"{where}: verifying the example timed out", False
     given = verdicts(output)
     unproved = {name_of(verdict) for verdict in given if verdict[0] == "Unresolved"}
+    if missing := missing_diagnostics(shown, output):
+        return (f"{where}: the page shows diagnostics cpp-verify does not "
+                f"print:\n" + "\n".join(f"  {line}" for line in missing) +
+                f"\nactual output:\n{output.strip()[:2500]}"), False
     if not expected:
         wrong = []
         for verdict in sorted(given):
@@ -237,17 +275,21 @@ def main():
                     print(f"{page}:{block.line}: unknown example label {name}")
                     return 1
                 context.append(labels[name])
-            text = "".join(context) + block.text
+            # Locations in messages count from the block's first line.
+            text = "".join(context) + "#line 1\n" + block.text
             for name in modes.get("label", []):
                 labels[name] = block.text
             compiled.append(block.text)
             expected = set()
+            shown = []
             following = page_blocks[position + 1:position + 2]
             if following and following[0].language == "text":
                 expected = verdicts(following[0].text)
+                shown = diagnostics(following[0].text)
             jobs.append((block, PRELUDE + text, modes.get("flags", []),
                          expected, set(modes.get("fails", [])),
-                         set(modes.get("unresolved", []))))
+                         set(modes.get("unresolved", [])), shown,
+                         "rejects" in modes))
 
     failures = []
     alone = []
@@ -271,7 +313,7 @@ def main():
             failures.append(result[0])
     for failure in failures:
         print(failure, end="\n\n")
-    shown = sum(1 for job in jobs if job[3])
+    shown = sum(1 for job in jobs if job[3] or job[6])
     print(f"{len(jobs)} examples checked ({shown} against the verdicts their "
           f"pages show), {len(failures)} failed")
     return 1 if failures else 0
diff --git a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst
index 2b26adde96..2b41863930 100644
--- a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst
+++ b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst
@@ -154,7 +154,41 @@ measure whatever the spec's other calls return:
    }
 
 A recursive call inside ``cppverify::forall``, ``cppverify::exists``, or ``cppverify::choose`` must
-decrease the measure for every value of the bound variable. Spec functions may
+decrease the measure for every value of the bound variable. A call in the body
+of a ``cppverify::choose`` is a call of the function the choose is written in, so it
+is checked like any other:
+
+.. cppverify-example: fails stuck
+.. cppverify-example: unresolved forty_two
+
+.. code-block:: cpp
+
+   cv::spec int stuck(int n)
+     cv::decreases(n)
+   {
+     return n <= 0 ? 0 : cv::choose(k, k == stuck(n) + 1);
+   }
+
+   int forty_two(int x)
+     cv::post(cv::result == 42)
+   {
+     cv::check(stuck(x) >= 0 || stuck(x) < 0);
+     if (x == 1)
+       return 0;
+     return 42;
+   }
+
+.. code-block:: text
+
+   stuck.cpp:4:42: error: spec decreases failed: stuck [backend=z3] [reason=counterexample] (n [type=math-i32] = 1)
+   Unresolved: forty_two [backend=z3] [reason=spec.termination] (relies on the definition of stuck, whose termination is not established)
+
+At ``n = 1`` the definition says that ``stuck(1)`` equals ``stuck(1) + 1``, a
+contradiction, and a proof that used it could prove anything. Before 0.2 the
+call inside the choose was not seen as a recursive call: ``stuck`` was
+accepted, and ``forty_two`` verified although it returns ``0`` at ``x = 1``.
+
+Spec functions may
 call each other in a cycle when they share a measure of the same length and
 every call within the cycle lowers it; the termination proof treats all of them
 as opaque:
diff --git a/website/source/book/part-ii/ch16-when-verification-fails.rst b/website/source/book/part-ii/ch16-when-verification-fails.rst
index c2c19fadf6..7db5d0f911 100644
--- a/website/source/book/part-ii/ch16-when-verification-fails.rst
+++ b/website/source/book/part-ii/ch16-when-verification-fails.rst
@@ -311,6 +311,44 @@ problem, and those are exactly the places checked above: a verified callee
 returns, so ordinary calls cannot cut paths (a callee with
 ``cppverify::decreases(*)`` may not, and its callers are reported ``[partial]``).
 
+A finding that no execution reaches a claim rests on the facts its query
+uses, as a proof does. When a result is ``Unresolved`` because one of those
+facts is not established, the finding is dropped where the missing fact may
+be its cause:
+
+.. cppverify-example: fails contradictory
+.. cppverify-example: unresolved relies_on_it
+
+.. code-block:: cpp
+
+   int contradictory(int x)
+     cv::post(cv::result == x && cv::result == x + 1)   // no result satisfies this
+   {
+     return x;
+   }
+
+   int relies_on_it(int x)
+     cv::post(cv::result == 7)
+   {
+     return contradictory(x);
+   }
+
+.. code-block:: text
+
+   vacuity.cpp:2:28: error: verification failed: contradictory [...::postcondition@2:28] (...) [backend=z3] [reason=counterexample]
+   Unresolved: relies_on_it [backend=z3] [reason=callee.contract] (relies on the contract of contradictory, which is not established)
+
+``relies_on_it`` proves its postcondition only because the contract of
+``contradictory`` cannot hold, which is the problem to fix, and the reason
+names it. Whether no execution reaches its end is a question about that
+contract too, so it is not reported. A spec whose termination fails can
+contradict itself the same way, and whether the solver notices is not a fact
+about the program. A finding about the entry state alone is kept when what is
+missing is a callee's contract, since no callee contract enters the entry
+state: an unsatisfiable precondition is still reported, with ``[vacuous]``.
+Before 0.2, ``relies_on_it`` was also reported ``[vacuous]``, with the warning
+that no execution reaches its end.
+
 Quantifiers that run away
 -------------------------
 
diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst
index 56b1a9d692..cb8c49d27b 100644
--- a/website/source/book/part-ii/ch17-backends-modular-calls.rst
+++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst
@@ -215,7 +215,8 @@ uses, ``[partial]``, and the vacuity checks. Where the source run reports
 ``Verified``, replay therefore reports ``Proved obligations: f (dependencies
 not checked in replay)``, with JSON status ``proved-obligations``. A
 counterexample is checked against the definitions alone and is still a
-failure.
+failure. The archive section of :doc:`../../language/tooling` shows a source run
+and its replay side by side.
 
 Source-built and replayed records pass through the same conservative
 canonicalizer before hashing and dispatch. It folds only trivial Boolean
diff --git a/website/source/language/dynamic-storage.rst b/website/source/language/dynamic-storage.rst
index 5cb2ca63ce..83ef033f12 100644
--- a/website/source/language/dynamic-storage.rst
+++ b/website/source/language/dynamic-storage.rst
@@ -282,7 +282,41 @@ type permits, compared for equality, converted to ``bool``, deleted, passed
 through the checked verified scalar interfaces above, or returned by the
 inferred fresh-owned factory boundary. These limits apply to the pointer, not
 to the value read through it: ``*p + 1``, ``*p < 50``, ``*p + *q``, and
-``sq(*p)`` in a spec call are ordinary integer expressions.
+``sq(*p)`` in a spec call are ordinary integer expressions. Both functions
+below verify:
+
+.. code-block:: cpp
+
+   cv::spec int sq(int x) { return x * x; }
+
+   int next_value(int v)
+     cv::pre(v < 100)
+     cv::post(cv::result == v + 1)
+   {
+     int *p = new int(v);
+     int r = *p + 1;
+     delete p;
+     return r;
+   }
+
+   int square_stored(int v)
+     cv::pre(0 <= v && v <= 100)
+     cv::post(cv::result == sq(v))
+   {
+     int *p = new int(v);
+     int *q = new int(v);
+     int r = *p * *q;
+     cv::check(r == sq(*p));
+     delete p;
+     delete q;
+     return r;
+   }
+
+Before 0.2, such expressions were rejected as if they computed with the
+pointer itself, and the file stopped: ``error: next_value: arithmetic on
+dynamic-storage pointers is unsupported``, and for the spec call ``error:
+square_stored: dynamic-storage pointers cannot cross a function-call
+boundary``.
 
 Type-erasing or indirect copies, ownership-taking pointer parameters,
 arithmetic-derived ownership, uninitialized/freed/multiple/escaped results,
diff --git a/website/source/language/expressions.rst b/website/source/language/expressions.rst
index a33b11410a..b02b0a4ea7 100644
--- a/website/source/language/expressions.rst
+++ b/website/source/language/expressions.rst
@@ -12,9 +12,75 @@ Contract expressions
 - collection operations of ``<cppverify.h>`` (``s.len()``, ``s[i]``,
   ``a.contains(x)``, ``m[k]``, ...)
 
-Must be contextually ``bool`` where used as conditions. They exist only for
-verification: a quantifier or a ``cppverify::choose`` in executable code is an
-error, outside an unevaluated operand such as ``sizeof``.
+Must be contextually ``bool`` where used as conditions.
+
+Quantifiers exist only for verification
+---------------------------------------
+
+A quantifier or a ``cppverify::choose`` has no value at run time: the compiler
+cannot evaluate ``cv::forall(k, 0, n, a[k] >= 0)`` without running a loop the
+program never wrote. So these expressions may appear only where the verifier
+reads them and the compiler does not: in a contract clause, a
+``cv::check``, a ghost block or ghost variable, a spec or proof function, and
+an unevaluated operand such as ``sizeof``. Every use below is allowed:
+
+.. code-block:: cpp
+
+   bool first_is_zero(const int *a, int n)
+     cv::pre(valid(a, n) && n > 0)
+     cv::post(cv::result == (a[0] == 0))
+     cv::post(!cv::result || cv::exists(k, 0, n, a[k] == 0))
+   {
+     cv::check(cv::forall(k, 0, 1, k == 0));
+     cv::ghost { bool any_zero = cv::exists(k, 0, n, a[k] == 0); }
+     return a[0] == 0;
+   }
+
+In executable code (a function body outside a ghost block, an initializer, a
+default argument that a call uses, a lambda, or a template's body) the same
+expression is an error, reported once where it is written, for the outermost
+quantifier:
+
+.. cppverify-example: rejects
+
+.. code-block:: cpp
+
+   bool all_nonnegative(const int *a, int n)
+     cv::pre(valid(a, n))
+   {
+     return cv::forall(k, 0, n, a[k] >= 0);
+   }
+
+.. code-block:: text
+
+   quantifiers.cpp:4:10: error: cppverify::forall exists only for verification and cannot be used in executable code; use it in a contract, ghost block, or spec or proof function
+       4 |   return cv::forall(k, 0, n, a[k] >= 0);
+         |          ^
+
+To compute such a value at run time, write the loop, and state what it
+computes in the postcondition with the quantifier:
+
+.. code-block:: cpp
+
+   bool all_nonnegative(const int *a, int n)
+     cv::pre(valid(a, n) && n >= 0)
+     cv::post(cv::result == cv::forall(k, 0, n, a[k] >= 0))
+   {
+     for (int i = 0; i < n; i = i + 1)
+       cv::invariant(0 <= i && i <= n)
+       cv::invariant(cv::forall(k, 0, i, a[k] >= 0))
+       cv::decreases(n - i)
+     {
+       if (a[i] < 0)
+         return false;
+     }
+     return true;
+   }
+
+Before 0.2, ``cv::forall`` and ``cv::exists`` in executable code compiled
+without a diagnostic to an undefined value (LLVM's ``poison``), while the
+verifier read them as quantifiers, so a function could verify and still
+behave arbitrarily when run. ``cv::choose`` was already rejected there.
 
 The range ``[lo, hi)`` may be **symbolic** (e.g. ``cppverify::forall(i, 0, n, ...)``).
 A bounded quantifier reaches the solver as a quantifier, whatever its range:
diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst
index 46ab769d90..d7b610135c 100644
--- a/website/source/language/functions-loops.rst
+++ b/website/source/language/functions-loops.rst
@@ -127,6 +127,55 @@ all denote the argument's entry value, as in ACSL, even when the callee
 reassigns its by-value parameter; a caller can therefore use the
 postcondition directly.
 
+Templates and member functions
+------------------------------
+
+Templates and member functions compile with contracts, but they are not
+verified yet:
+
+- The contracts of a function template, of a class template's members, and a
+  class template's type invariants compile, instantiate with the template,
+  and are ignored, with a ``-Wcontract-unsupported`` warning that names the
+  template. Contracts on a member function are ignored the same way.
+- A template without contracts changes nothing for the rest of the file, as
+  long as verified code does not call it.
+
+.. code-block:: cpp
+
+   template <typename T>
+   T clamp_low(T v, T lo)
+     cv::post(cv::result >= lo)
+   {
+     return v < lo ? lo : v;
+   }
+
+   int clamp_int(int v)
+     cv::post(cv::result >= 0)
+   {
+     return v < 0 ? 0 : v;
+   }
+
+.. code-block:: text
+
+   templates.cpp:2:3: warning: contracts in function template 'clamp_low' are not yet supported and are ignored [-Wcontract-unsupported]
+       2 | T clamp_low(T v, T lo)
+         |   ^
+   Verified: clamp_int [backend=z3]
+
+Two uses still stop the file with an error, and no function in it gets a
+verdict:
+
+- a call to a template from verified code, such as ``return clamp_low(v,
+  0);`` in a function with a contract: ``error: use: call to function
+  without a verification contract: clamp_low``;
+- a template whose body has a contract statement (``cv::check``, a ghost
+  block): ``error: twice: function template verification is unsupported``.
+
+Before 0.2, a template whose contract depends on its parameters did not
+compile (``value of type '<dependent type>' is not contextually convertible to
+'bool'``), and a template without any contract, even one nothing calls,
+stopped the file with ``function template verification is unsupported``.
+
 Behaviors
 ---------
 
@@ -229,6 +278,31 @@ that terminate. Ghost-block and proof-function loops are erased at runtime and
 must have a real measure, unless their condition is the constant false;
 ``cppverify::decreases(*)`` is rejected there.
 
+A loop whose condition is the constant false runs its body at most once (a
+``do`` loop exactly once), so it needs no invariant or measure, and the state
+after it is the one its body leaves. This is the shape of the usual
+statement-like macro:
+
+.. code-block:: cpp
+
+   #define SWAP(a, b) do { int t = a; a = b; b = t; } while (0)
+
+   int swapped_difference(int a, int b)
+     cv::pre(0 <= a && a <= 1000 && 0 <= b && b <= 1000)
+     cv::post(cv::result == b - a)
+   {
+     SWAP(a, b);
+     return a - b;
+   }
+
+.. code-block:: text
+
+   Verified: swapped_difference [backend=z3]
+
+Before 0.2, such a loop was treated like any other: what it might change was
+forgotten after it, so ``a - b`` failed with an ``overflow`` counterexample
+for values the swap never produces.
+
 Nobody knows whether this loop ends for every start, so it has no measure:
 
 .. code-block:: cpp
diff --git a/website/source/language/ghost-proofs.rst b/website/source/language/ghost-proofs.rst
index c0bbd5d336..c3a8be1eae 100644
--- a/website/source/language/ghost-proofs.rst
+++ b/website/source/language/ghost-proofs.rst
@@ -111,6 +111,74 @@ Proof functions may update their own local values and call other proof
 functions, but cannot write executable memory/global state or call executable
 functions. Their loops require ``cppverify::decreases`` just like recursive proof calls.
 
+Spec functions stay out of executable code
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A spec function is never compiled, so a call from code that runs would have
+nothing to call. Clang reports such a use where it is written, also inside a
+lambda, generic or not:
+
+.. cppverify-example: rejects
+
+.. code-block:: cpp
+
+   cv::spec int twice(int x) { return 2 * x; }
+
+   int apply(int v)
+   {
+     auto f = [](auto x) { return twice(x); };
+     return f(v);
+   }
+
+.. code-block:: text
+
+   lambda.cpp:5:32: error: spec function 'twice' exists only for verification and cannot be used in executable code; use it in a contract, ghost block, or spec or proof function
+       5 |   auto f = [](auto x) { return twice(x); };
+         |                                ^
+
+A generic lambda's body is checked for each type it is called with. Before
+0.2, a spec function called from a generic lambda compiled, and the program
+then failed to link (``undefined reference to `twice(int)'``). In a contract,
+a ghost block, or another spec or proof function the same call is fine.
+
+Values a spec reads are exact
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Arithmetic in a spec body is mathematical, and that includes the values the
+spec reads through a pointer: an ``int`` read from memory is its value as an
+integer, and adding to it never wraps.
+
+.. cppverify-example: fails wraps
+
+.. code-block:: cpp
+
+   cv::spec int pair_sum(const int *p) { return p[0] + p[1]; }
+
+   cv::proof void large(const int *p)
+     cv::pre(valid(p, 2))
+     cv::pre(p[0] == 2147483647 && p[1] == 1)
+     cv::post(pair_sum(p) == 2147483648)
+   {
+   }
+
+   cv::proof void wraps(const int *p)
+     cv::pre(valid(p, 2))
+     cv::pre(p[0] == 2147483647 && p[1] == 1)
+     cv::post(pair_sum(p) < 0)
+   {
+   }
+
+.. code-block:: text
+
+   Verified: spec axiom: pair_sum
+   Verified: large [backend=z3]
+   reads.cpp:13:24: error: verification failed: wraps [...::postcondition@13:24] (counterexample: ...) [backend=z3] [reason=counterexample]
+
+Before 0.2, a value read in a spec body kept its machine type, so the sum
+above wrapped to a negative ``int``: ``wraps`` verified, and ``large`` could
+not even be lowered (``equality operands have different logic sorts``).
+Machine values that come from calls were already exact.
+
 .. code-block:: cpp
 
    cv::spec int safe_div(int a, int b)
diff --git a/website/source/language/integers.rst b/website/source/language/integers.rst
index afb583de8a..1dc6b67227 100644
--- a/website/source/language/integers.rst
+++ b/website/source/language/integers.rst
@@ -162,6 +162,41 @@ This permits constructing the sign bit (for example, ``1 << 31`` for a 32-bit
 ``E1 * 2^E2`` modulo ``2^N``, as the standard defines, so ``-1 << 1`` is
 ``-2``; only the shift count must be in range.
 
+The same function shows both rules. As C++17, doubling a negative value by a
+shift is undefined, and the verifier finds the input:
+
+.. cppverify-example: label doubled
+.. cppverify-example: fails doubled
+
+.. code-block:: cpp
+
+   int doubled(int x)
+     cv::pre(-1000 <= x && x <= 1000)
+     cv::post(cv::result == 2 * x)
+   {
+     return x << 1;
+   }
+
+.. code-block:: text
+
+   shift.cpp:5:3: error: verification failed: doubled [...::shift@5:3] (counterexample: x [ssa=x_0] [type=i32] = -1; trace: return.return@5:3 value=-2) [backend=z3] [reason=counterexample]
+
+Compiled as C++20, with ``cpp-verify shift.cpp -- -std=c++20``, the same
+function verifies:
+
+.. cppverify-example: with doubled
+.. cppverify-example: flags --extra-arg=-std=c++20
+
+.. code-block:: cpp
+
+   // doubled, as above
+
+.. code-block:: text
+
+   Verified: doubled [backend=z3]
+
+Before 0.2 the C++17 rule applied in every language mode.
+
 Calls crossing between mathematical ``cppverify::spec`` code and lifted machine
 ``constexpr`` code convert at each parameter and return boundary. A machine
 result converts exactly to an unbounded integer; an unsigned result has already
@@ -205,6 +240,83 @@ conversions. Signedness, widening, and narrowing therefore occur before a
 callee contract is instantiated and before a returned value is used by the
 caller.
 
+Enumerations
+------------
+
+A value of an enumeration type has the values C++ gives that type
+([dcl.enum]/8), which are not just its enumerators:
+
+- With a fixed underlying type (every ``enum class``, which is ``int`` unless
+  it says otherwise, and every ``enum E : T``), the values are those of the
+  underlying type.
+- Without one (``enum E { ... }``), the values are those of the smallest
+  bit-field that holds every enumerator. For ``{ Red, Green, Blue }`` that is
+  ``0`` to ``3``; with a negative enumerator the range is signed.
+
+Every executable or proof value of an enumeration type, wherever it comes
+from (a parameter, a read from memory, a call's result, a variable after a
+loop), is assumed to lie in that range. Converting an integer into an
+enumeration without a fixed type is undefined behavior when the value is out
+of range, so the conversion is an ``overflow`` obligation:
+
+.. cppverify-example: fails unchecked
+
+.. code-block:: cpp
+
+   enum Color { Red, Green, Blue };
+
+   int code(Color c)
+     cv::post(0 <= cv::result && cv::result <= 3)
+   {
+     return c;
+   }
+
+   Color from_code(int v)
+     cv::pre(0 <= v && v <= 3)
+   {
+     return static_cast<Color>(v);
+   }
+
+   Color unchecked(int v)
+     cv::pre(-10 <= v && v <= 10)
+   {
+     return static_cast<Color>(v);
+   }
+
+.. code-block:: text
+
+   Verified: code [backend=z3]
+   Verified: from_code [backend=z3]
+   colors.cpp:18:3: error: verification failed: unchecked [...::overflow@18:3] (counterexample: v [ssa=v_0] [type=i32] = -1; ...) [backend=z3] [reason=counterexample]
+
+``code`` may return ``3``: no enumerator has that value, but ``Color`` does.
+With a fixed underlying type, every value of that type is possible:
+
+.. cppverify-example: fails level
+
+.. code-block:: cpp
+
+   enum class Level : unsigned char { Low, Mid, High };
+
+   int level(Level l)
+     cv::post(0 <= cv::result && cv::result <= 2)
+   {
+     return static_cast<int>(l);
+   }
+
+.. code-block:: text
+
+   levels.cpp:4:28: error: verification failed: level [...::postcondition@4:28] (counterexample: result [ssa=__result_1] [type=i32] = 3, l [ssa=l_0] [type=u8] = 3; ...) [backend=z3] [reason=counterexample]
+
+The range is a fact about machine values. In a ``cv::spec``, a parameter of an
+enumeration type is a mathematical integer like any other, so a spec's claim
+about it is proved without the range: ``cv::spec bool small(Color c)
+cv::post(cv::result) { return c < 4; }`` fails at ``c = 4``.
+
+Before 0.2 the range was not assumed where a value comes in, so a true
+claim such as ``code``'s failed with a value no ``Color`` can hold (for
+example ``c = 4294967295``).
+
 Exact ``int`` boundaries
 ------------------------
 
diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst
index a838ddb485..1228ac4332 100644
--- a/website/source/language/limitations.rst
+++ b/website/source/language/limitations.rst
@@ -149,8 +149,11 @@ C++ feature boundaries
      - ``switch``, range-``for``, ``goto``, labels, conditionless ``for``,
        loop condition declarations, and ``break``/``continue`` in ``do``
        loops. An expression or statement nested more than 256 operations
-       deep (a sum of 300 terms, say) is reported where it is; split it into
-       intermediate variables.
+       deep (a sum of 300 terms, say) is reported where it is, and the file
+       stops: ``error: total: the expression at 4:276 nests more than 256
+       operations deep, which the verifier does not support; split it into
+       intermediate variables``. Before 0.2, such an expression could crash
+       the verifier.
    * - Advanced C++
      - Not in the verified core.
      - Exceptions, lambdas, coroutines, RTTI, virtual dispatch, multiple
diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst
index 90dc60a4c3..7cb5df657f 100644
--- a/website/source/language/pointers.rst
+++ b/website/source/language/pointers.rst
@@ -45,6 +45,79 @@ storage not yet initialized is ``Unresolved`` (``construct.unsupported``). Mutab
 by default (over whole ``valid(p, n)`` extents);
 ``cppverify::aliases(left, right)`` permits same-object aliasing.
 
+Out-parameters
+~~~~~~~~~~~~~~
+
+A function is verified as if it read its reference and pointer parameters'
+storage, so every such parameter must refer to initialized storage at a call.
+C++ requires less: a function that writes its parameter before reading it,
+an out-parameter, may receive storage that is not initialized yet. Until a
+contract can say that a function writes a parameter first, such a call is
+``Unresolved`` with reason ``construct.unsupported``: neither proved nor
+reported as a failure.
+
+.. cppverify-example: unresolved seven
+.. cppverify-example: fails read_too_early
+
+.. code-block:: cpp
+
+   void init(int &out)
+     cv::modifies(out)
+     cv::post(out == 7)
+   {
+     out = 7;
+   }
+
+   int seven()
+     cv::post(cv::result == 7)
+   {
+     int a;
+     init(a);
+     return a;
+   }
+
+   int seven_initialized()
+     cv::post(cv::result == 7)
+   {
+     int a = 0;
+     init(a);
+     return a;
+   }
+
+   int read_too_early()
+     cv::post(cv::result == 3)
+   {
+     int a;
+     int &r = a;
+     int copy = r;
+     r = 3;
+     return copy;
+   }
+
+.. code-block:: text
+
+   Verified: init [backend=z3]
+   out.cpp:12:3: Unresolved: seven [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage)
+   Verified: seven_initialized [backend=z3]
+   out.cpp:29:3: error: verification failed: read_too_early [...::initialization@29:3] (...) [backend=z3] [reason=counterexample]
+
+- Initializing the storage before the call, as ``seven_initialized`` does, is
+  the way to verify such code today.
+- The same holds for an element of a local array (``init(arr[0])``), for
+  storage from ``new int`` passed to a pointer parameter before anything
+  writes it (``int *p = new int; init_ptr(p);``), and for a function that
+  returns a pointer to storage not initialized yet.
+- A local reference may bind storage that is not initialized, as C++ allows,
+  and a write through it initializes the object. A read before the first
+  write is a real error, reported where it happens, as in ``read_too_early``.
+
+Before 0.2 each of these calls was a reported failure (``verification failed:
+... initialization``), and ``int a; init(a);`` stopped the whole file with
+``error: seven: read of uninitialized local value: a``.
+
+Aliasing between parameters
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
 The default is a precondition every caller must establish. A function that
 works when its parameters share storage says so with ``cppverify::aliases``, and its
 body is then verified for both cases:
@@ -355,10 +428,40 @@ between pointers that may come from either) is ``construct.unsupported``:
 neither proved nor reported as an error. Proving ``left == right`` does not
 change that.
 
-Pointers loaded from memory, null or dangling operands, out-of-range
-positions, unrepresentable distances, pointer compound assignment, and
-pointer difference inside explicit ``cppverify::spec`` or lifted ``constexpr`` functions
-fail closed.
+Two null pointers differ by 0, as C++ defines ([expr.add]/5); a difference
+with one null operand is undefined and fails:
+
+.. cppverify-example: fails one_null
+
+.. code-block:: cpp
+
+   long two_nulls(const int *p, const int *q)
+     cv::pre(p == nullptr && q == nullptr)
+     cv::post(cv::result == 0)
+   {
+     return p - q;
+   }
+
+   long one_null(const int *p, const int *q)
+     cv::pre(p == nullptr && q != nullptr)
+   {
+     return p - q;
+   }
+
+.. code-block:: text
+
+   Verified: two_nulls [backend=z3]
+   nulls.cpp:11:3: error: verification failed: one_null [...::pointer-difference@11:3] (counterexample: p [ssa=p_0] [type=pointer] = 0, q [ssa=q_0] [type=pointer] = 1; ...) [backend=z3] [reason=counterexample]
+
+Before 0.2, ``two_nulls`` failed the same way.
+
+A difference with one null operand, a dangling operand, a position outside
+its object, or a distance that does not fit ``ptrdiff_t`` fails with a
+counterexample. A difference of pointers loaded from memory, pointer compound
+assignment (``p += k``), and a pointer difference inside a ``cv::spec`` or
+lifted ``constexpr`` function are rejected: the run stops with an error naming
+the construct, for example ``error: gap: pointer difference in spec or lifted
+constexpr functions is unsupported``.
 
 Local scalar dynamic storage
 ----------------------------
diff --git a/website/source/language/syntax.rst b/website/source/language/syntax.rst
index cba8f0edb2..f6c128a580 100644
--- a/website/source/language/syntax.rst
+++ b/website/source/language/syntax.rst
@@ -35,6 +35,54 @@ does after ``namespace cv = cppverify;`` and ``using namespace cppverify;``:
   qualifier) belong to the compiler; cpp-verify neither parses nor verifies
   them.
 
+One condition per clause
+------------------------
+
+Each clause takes exactly one expression. To state two conditions, join them
+with ``&&`` or write two clauses, which mean the same: every ``cv::pre`` must
+hold, and so must every ``cv::post``.
+
+.. code-block:: cpp
+
+   int clamp(int x)
+     cv::post(cv::result >= 0 && cv::result <= 10)
+   {
+     return x < 0 ? 0 : x > 10 ? 10 : x;
+   }
+
+   int clamp_again(int x)
+     cv::post(cv::result >= 0)
+     cv::post(cv::result <= 10)
+   {
+     return x < 0 ? 0 : x > 10 ? 10 : x;
+   }
+
+Anything written after the expression, inside the parentheses, is an error.
+A missing ``&&`` is the usual cause:
+
+.. cppverify-example: rejects
+
+.. code-block:: cpp
+
+   int clamp(int x)
+     cv::post(cv::result >= 0 cv::result <= 10)
+   {
+     return x < 0 ? 0 : x > 10 ? 10 : x;
+   }
+
+.. code-block:: text
+
+   clauses.cpp:2:28: error: expected ')' after cppverify::post expression
+       2 |   cv::post(cv::result >= 0 cv::result <= 10)
+         |                            ^
+   clauses.cpp:2:11: note: to match this '('
+       2 |   cv::post(cv::result >= 0 cv::result <= 10)
+         |           ^
+
+Before 0.2, the parser kept the first condition and dropped the rest without
+a word, so a clause with a missing ``&&`` checked less than it said: the
+example above verified ``cv::result >= 0`` alone.
+
 Full table:
 
 .. list-table::
diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index fde467c193..e01e583bb8 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -34,23 +34,148 @@ Other compiler flags come from the ``compile_commands.json`` beside the file or
 above it, or in the directory ``-p DIR`` names; a file the database does not list gets the
 flags of a listed neighbour. Without a database the file is compiled with those two flags
 alone. Flags after ``--`` replace the database, and ``--extra-arg=FLAG`` adds one flag either
-way. A ``.h`` file given as input is a C++ header. A compiler error, in a command line or in
-the file, stops that file without verifying it, and ``cpp-verify`` then exits with status 1.
+way.
 
-Ctrl-C stops the run: the solvers stop at once, each function whose verification had not
-finished is reported as ``Interrupted: f`` (JSON reason ``interrupted``), a proof that rests on
-its contract is not established, the input files not yet read are skipped, and ``cpp-verify``
-exits with status 130. A second Ctrl-C ends it at once.
+Input files and compiler errors
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Every input is compiled as C++, a header too: a ``.h`` file given as input is
+a C++ header, and its functions are verified like those of a ``.cpp`` file.
+
+.. code-block:: cpp
+
+   inline int clamp100(int x)
+     cv::post(cv::result <= 100)
+   {
+     return x > 100 ? 100 : x;
+   }
+
+.. code-block:: text
+
+   $ cpp-verify mathx.h --
+   Verified: clamp100 [backend=z3]
+
+A compiler error stops the file it belongs to, whether it is in the file or
+in its command line: the file is not verified, the next input files are, and
+``cpp-verify`` exits with status 1.
+
+.. code-block:: text
+
+   $ cpp-verify abs.cpp -- -fbogus-flag
+   error: unknown argument: '-fbogus-flag'
+   Error while processing abs.cpp.
+
+Before 0.2, an error in a command line was printed and then ignored: the
+file was verified anyway, under other options than the ones given, and
+``cpp-verify`` exited with status 0. A ``.h`` input was compiled as C, which
+printed ``error: invalid argument '-std=c++17' not allowed with 'C'``.
+
+Stopping a run with Ctrl-C
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Ctrl-C (``SIGINT``) stops the run at once, however long its queries are:
+
+- every solver stops, Z3 and cvc5 alike, and so does a counterexample check
+  in progress;
+- each function whose verification had not finished is reported as
+  ``Interrupted: f`` (JSON ``"status":"unresolved"`` with reason
+  ``interrupted``), and its partial results are not printed;
+- a proof that rests on the contract of an interrupted function is not
+  established, so its caller is ``Unresolved`` with reason
+  ``callee.contract``; a proof that rests only on finished functions keeps
+  its verdict;
+- the input files not yet read are skipped, and ``cpp-verify`` exits with
+  status 130, as a shell expects after Ctrl-C;
+- a second Ctrl-C ends the process at once, without a report.
+
+.. cppverify-example: fragment
+
+.. code-block:: cpp
+
+   int fast(int x)
+     cv::pre(0 <= x && x < 100)
+     cv::post(cv::result == x + 1)
+   {
+     return x + 1;
+   }
+
+   cv::proof void cubes(int x, int y, int z)   // no solver settles this
+     cv::pre(x > 0 && y > 0 && z > 0)
+     cv::post(x * x * x + y * y * y != z * z * z)
+   {
+   }
+
+.. code-block:: text
+
+   $ cpp-verify --timeout=600000 slow.cpp --
+   ^C
+   Verified: fast [backend=z3]
+   slow.cpp:8:16: Interrupted: cubes
+   $ echo $?
+   130
+
+Before 0.2, Ctrl-C printed an LLVM crash report and the run went on, or the
+process crashed, because each Z3 check installed its own signal handler.
+
+Versions
+~~~~~~~~
 
 ``cpp-verify --version`` shows the cpp-verify release and repository revision, the LLVM
 release it is built on, and each backend: the Z3 linked into it, and the cvc5 and Lean
-(``lake``) it finds on ``PATH`` with their versions. cvc5 is tested with 1.1.2, and every
-Lean project pins ``leanprover/lean4:v4.32.2``.
+(``lake``) it finds on ``PATH`` with their versions. cvc5 is tested with 1.1.2 and also
+works with 1.4: a query that needs a constant array, as every one over sets, multisets,
+and maps does, sets cvc5's ``arrays-exp`` option itself, which 1.4 requires. Every Lean
+project pins ``leanprover/lean4:v4.32.2``.
+
+Options that select a backend, and options a run would not use
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An option that only one backend uses selects that backend when ``--backend``
+is not given:
 
-Every option must take effect in the run it is given to. An option that one backend alone
-uses selects that backend when ``--backend`` is not given (``--lean-out`` and
-``--lean-project`` select ``lean``, ``--unroll`` selects ``bmc``), and an option the run
-would ignore is an error.
+.. list-table::
+   :header-rows: 1
+   :widths: 40 60
+
+   * - Option
+     - Selects
+   * - ``--unroll=N``
+     - ``--backend=bmc``
+   * - ``--lean-out=FILE``, ``--lean-project=DIR``
+     - ``--backend=lean``
+
+So ``cpp-verify --unroll=4 file.cpp`` runs bounded model checking and prints
+results such as ``Verified: swapped_difference [backend=bmc, bound=0]``.
+
+An option that the run would not use is an error naming what it needs, and
+nothing is verified:
+
+.. list-table::
+   :header-rows: 1
+   :widths: 45 55
+
+   * - Command
+     - Error
+   * - ``--backend=z3 --unroll=3``
+     - ``error: --unroll requires --backend=bmc``
+   * - ``--backend=z3 --cvc5-path=PATH``
+     - ``error: --cvc5-path requires --backend=cvc5, --backend=portfolio, or --backend=race``
+   * - ``--backend=cvc5 --profile-quantifiers``
+     - ``error: --profile-quantifiers requires a backend that runs Z3: z3, portfolio, race, or bmc``
+   * - ``--lean-out=FILE --int-encoding=bitvector``
+     - ``error: --int-encoding requires a backend that runs an SMT solver``
+   * - ``--proof-cache-max-mb=N`` without ``--proof-cache``
+     - ``error: --proof-cache-max-mb and --proof-cache-max-entries require --proof-cache``
+   * - ``--lean-fallback-scope=all`` without ``--lean-fallback``
+     - ``error: --lean-fallback-scope requires --lean-fallback``
+
+The same rules hold when replaying an archive: ``--check-ub`` and
+``--profile-quantifiers`` are errors there, since an archive keeps the checks
+it was written with, and ``--unroll`` must match the bound a BMC archive
+records. Before 0.2, ``--lean-out`` and ``--lean-project`` needed an explicit
+``--backend=lean``, ``--unroll`` without ``--backend=bmc`` ran Z3 and reported
+an unbounded ``Verified``, and the other options above were ignored without a
+word.
 
 Backends
 --------
@@ -289,7 +414,9 @@ Parallel solving and proof caching
 
 ``--jobs`` sets one pool of exactly that many workers. Each function is a
 task on it, with its own backends; its obligations are tasks on the same
-pool (a task waiting for them runs them itself, so the pool never grows), and
+pool (a task waiting for them runs its own unstarted ones itself, never
+another function's, so the pool never grows and a function whose queries
+are done reports at once), and
 with workers to spare its whole query races the obligations solved one by
 one: both are exact, so a proof by either decides the function and
 interrupts the other. A query over sequences is also solved without the
@@ -371,7 +498,9 @@ Each non-success verification result also carries a stable reason code. Current
 codes include ``counterexample``, ``solver.timeout``, ``solver.unknown``,
 ``solver.resource-limit``, ``solver.unavailable``,
 ``solver.invocation-failed``, ``solver.malformed-output``,
-``query.size-limit``, ``encoding.failed``,
+``query.size-limit``, ``encoding.failed`` (the obligations could not be
+encoded for the solver; when Z3 rejected a call, the message quotes it:
+``Z3 reported an error: ...``),
 ``obligation.invalid``, ``logic.unsupported``, ``query.missing``,
 ``backend.invalid-result``,
 ``backend.inconsistent-results``, ``bmc.incomplete-bound``,
@@ -458,6 +587,48 @@ replacement character, so every emitted JSON record remains valid UTF-8.
 Portable obligation archives
 ----------------------------
 
+An archive holds the verification conditions of a file's functions, so they
+can be checked again, by another solver or on another machine, without the
+C++ source:
+
+.. code-block:: cpp
+
+   int abs_value(int x)
+     cv::pre(x > -2147483647 - 1)
+     cv::post(cv::result == (x < 0 ? -x : x))
+   {
+     return x < 0 ? -x : x;
+   }
+
+   int twice_abs(int x)
+     cv::pre(-1000 < x && x < 1000)
+     cv::post(cv::result >= 0)
+   {
+     int a = abs_value(x);
+     return 2 * a;
+   }
+
+.. code-block:: text
+
+   $ cpp-verify --obligation-out=abs.cpv abs.cpp --
+   Verified: abs_value [backend=z3]
+   Verified: twice_abs [backend=z3]
+   $ cpp-verify --obligation-in=abs.cpv
+   Proved obligations: abs_value (dependencies not checked in replay) [backend=z3] [semantic-hash=sha256:...]
+   Proved obligations: twice_abs (dependencies not checked in replay) [backend=z3] [semantic-hash=sha256:...]
+
+Replay proves each function's obligations, but a verdict also rests on
+facts outside them: ``twice_abs`` is ``Verified`` only because
+``abs_value``'s contract is, and an archive does not record that. Replay
+therefore reports ``Proved obligations``, JSON status
+``proved-obligations``, never ``Verified``. The same holds for what spec
+facts, trusted contracts, ``[partial]``, and the vacuity checks add to a
+source verdict. A counterexample in replay is still a failure: it is checked
+against the definitions the archive carries. Before 0.2, replay printed
+``Verified`` for each module whose obligations held, even when the source
+run did not verify the function, for example when a callee's verification
+failed.
+
 ``--obligation-out`` writes ``cppverify.obligation/2`` records only after exact
 serialize/deserialize/validate/reserialize checks. Stable wire tags make the
 format independent of C++ enum ordinals. The reader rejects malformed magic,
@@ -600,7 +771,24 @@ sees contracts exactly as the compiler does. With them:
 - completion after ``cv::`` lists the constructs with their documentation, and the
   ``<cppverify.h>`` collections;
 - ``clang-format`` puts each clause on its own line and the body's brace below them, as it
-  does for a trailing ``requires`` clause, and writes a range footprint as ``p[lo : n]``.
+  does for a trailing ``requires`` clause, and writes a range footprint as ``p[lo : n]``
+  (before 0.2 it wrote ``p [0:n]``, as if the brackets began an Objective-C message):
+
+  .. code-block:: text
+
+     void fill(int *p, int n, int v)
+       cv::pre(valid(p, n) && n >= 0)
+       cv::modifies(p[0 : n])
+       cv::post(cv::forall(k, 0, n, p[k] == v))
+     {
+       for (int i = 0; i < n; i = i + 1)
+         cv::invariant(0 <= i && i <= n)
+         cv::modifies(p[0 : n])
+         cv::decreases(n - i)
+       {
+         p[i] = v;
+       }
+     }
 
 clangd needs ``-fverify-contracts`` in each file's compile command. A
 ``compile_commands.json`` from a build that uses the flag provides it; otherwise add it in a
@@ -625,6 +813,41 @@ A tool that does not use this build's parser (a stock clangd, Visual Studio's In
 reports the constructs as errors; a stock ``clang-format`` keeps every clause on the
 declarator's line. Tools built on this build's libclang see the contracts as well.
 
+Contracts in Clang's other tools
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The contract constructs have a meaning for Clang's own analyses too: a
+contract expression is never evaluated, and ghost code emits no code.
+
+- A contract expression cannot throw, so ``noexcept`` of one is ``true``. It
+  is not a constant expression either: a ``static_assert`` or an enumerator
+  cannot use its value (``error: expression is not an integral constant
+  expression``).
+
+  .. code-block:: cpp
+
+     static_assert(noexcept(cv::exists(k, 0, 3, k == 1)), "contracts do not throw");
+
+- The static analyzer (``clang++ --analyze -fverify-contracts``) and the
+  warnings computed from the control-flow graph skip ghost code and contract
+  statements, so they analyze the code after them: a null dereference after a
+  ``cv::ghost`` block or a ``cv::check`` is reported as it would be without them.
+- libclang, and the tools built on it (``c-index-test``, the Python bindings,
+  IDE indexers), shows each construct as an unexposed expression or statement
+  (``CXCursor_UnexposedExpr``, ``CXCursor_UnexposedStmt``), with its operands
+  as child cursors.
+- A contract expression cannot appear in a mangled name yet: a template whose
+  signature contains one, such as
+  ``int (&)[sizeof(cv::exists(k, 0, 3, k == T()), T())]``, is reported when it is
+  instantiated, with ``error: cannot yet mangle ExistsExpr expression``, as
+  Clang reports other expressions without a mangling.
+
+Before 0.2, ``noexcept`` of a contract expression crashed the compiler or
+made it hang, as did a contract expression in a C++98 constant; the analyzer
+ended every path at a ghost block, so it reported nothing after one; libclang
+hid the constructs and, in a precondition, their operands; and a contract
+expression in a template's signature was mangled to a malformed symbol.
+
 Migrating from the keyword syntax
 ---------------------------------
 
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index ae06cee333..b8abf5d90b 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -13,6 +13,155 @@ next release with ``-dev``.
 
 The data formats keep versions of their own, listed with each release.
 
+0.2.0 (in development)
+----------------------
+
+The changes on ``main`` since 0.1.1, which 0.2.0 will ship. Each entry says
+what 0.1.1 did and what happens now; the page it links shows an example with
+the verifier's output.
+
+Wrong results fixed
+~~~~~~~~~~~~~~~~~~~
+
+These made 0.1.1 report ``Verified`` for a claim that is false, or compile a
+program that cannot work.
+
+**A clause takes one expression.** ``cv::post(cv::result >= 0 cv::result <= 10)``,
+with its ``&&`` missing, kept the first condition and dropped the rest without
+a word, so the clause checked less than it said. Anything after a clause's
+expression is now an error (:doc:`language/syntax`).
+
+**Recursion through** ``cppverify::choose``. A call inside a choose's body was not
+seen as a call of the function the choose is in, so a spec that applied
+itself there skipped its termination check, and its contradictory definition
+let a false claim verify. The call is now checked like any other recursive
+call (:doc:`book/part-ii/ch13-spec-and-proof-functions`).
+
+**Archive replay reports proved obligations, not** ``Verified``. Replay printed
+``Verified`` for every module whose obligations held, although a source
+verdict also rests on facts an archive does not carry, such as a callee's
+contract. It now prints ``Proved obligations: f (dependencies not checked in
+replay)``, JSON status ``proved-obligations`` (:doc:`language/tooling`).
+
+**A spec reads exact values.** A value a spec body read through a pointer kept
+its machine type, so ``p[0] + p[1]`` wrapped: a proof that the sum of
+``2147483647`` and ``1`` is negative verified. Such reads are now mathematical
+integers, as the rest of a spec is (:doc:`language/ghost-proofs`).
+
+**Quantifiers in executable code are errors.** ``cv::forall`` and ``cv::exists``
+outside contracts and ghost code compiled to an undefined value while the
+verifier read them as quantifiers. They are now an error, as ``cv::choose``
+already was (:doc:`language/expressions`).
+
+**Spec functions in generic lambdas are errors.** A spec function called in a
+generic lambda compiled, and the program failed to link. It is now reported
+where it is written (:doc:`language/ghost-proofs`).
+
+**Clang's own analyses.** ``noexcept`` of a contract expression crashed or hung
+the compiler, as did a contract expression in a C++98 constant; the static
+analyzer reported nothing after a ghost block; libclang hid the constructs;
+and a contract expression in a template's signature produced a malformed
+symbol. Each now behaves by the construct's meaning (:doc:`language/tooling`).
+
+Failures that were not real
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+These made 0.1.1 report a failure, or reject a function, for C++ that is
+correct.
+
+**Loops that never repeat.** A loop whose condition is the constant false, as in
+``do { ... } while (0)`` macros, forgot the state it changed, and the code
+after it could fail for values it never produces. Its state now carries over
+(:doc:`language/functions-loops`).
+
+**Null minus null.** The difference of two null pointers failed its
+``pointer-difference`` check; it is 0, as C++ defines (:doc:`language/pointers`).
+
+**C++20 shifts.** A signed left shift followed the C++17 rule in every mode, so
+``-1 << 1`` failed under ``-std=c++20``. From C++20 it is the value C++20
+defines (:doc:`language/integers`).
+
+**Enumeration ranges.** A value of an enumeration without a fixed underlying
+type could take values outside its range, so true claims failed with values
+such as ``c = 4294967295``. Every such value is now assumed to be in the
+range C++ gives it (:doc:`language/integers`).
+
+**Values read through** ``new`` **pointers.** ``*p + 1`` on a pointer from ``new``
+was rejected as arithmetic on the pointer; values read through such a
+pointer are now ordinary integers (:doc:`language/dynamic-storage`).
+
+**Out-parameters.** Passing storage that is not initialized yet to a function
+that writes it (``int a; init(a);``) was a failure, or stopped the file; it is
+now ``Unresolved`` with reason ``construct.unsupported``, until a contract can
+say that a function writes its parameter first (:doc:`language/pointers`).
+
+**Choices in counterexamples.** A counterexample could use a value of
+``cv::choose`` that its body excludes, so true claims about a choice failed.
+Every choice a counterexample uses is now checked against its body
+(:doc:`book/part-ii/ch13-spec-and-proof-functions`).
+
+**Vacuity findings of downgraded results.** A result that is ``Unresolved``
+because a fact it relies on is not established could still be marked
+``[vacuous]``, from that very fact, and whether it was depended on the
+solver's search. Such findings are now dropped
+(:doc:`book/part-ii/ch16-when-verification-fails`).
+
+C++ that compiles now
+~~~~~~~~~~~~~~~~~~~~~
+
+**Contracts in templates.** A template whose contract depends on its
+parameters did not compile. Its contracts now compile and instantiate, and
+are ignored with a ``-Wcontract-unsupported`` warning; a template without
+contracts no longer stops the file (:doc:`language/functions-loops`).
+
+Running cpp-verify
+~~~~~~~~~~~~~~~~~~
+
+**Ctrl-C stops the run.** Ctrl-C printed an LLVM crash report and the run went
+on, or crashed. It now stops every solver at once, reports each unfinished
+function as ``Interrupted``, and exits with status 130
+(:doc:`language/tooling`).
+
+**Options select their backend, and unused options are errors.**
+``--lean-out`` and ``--lean-project`` select Lean and ``--unroll`` selects BMC;
+an option the run would not use, such as ``--unroll`` with ``--backend=z3``, is
+an error that names what it needs, where it was ignored (:doc:`language/tooling`).
+
+**Compiler errors stop their file, and headers are C++.** An error in a command
+line was printed and then ignored, and a ``.h`` input was compiled as C. Now
+the file with the error is not verified and ``cpp-verify`` exits with status 1,
+and a header is C++ (:doc:`language/tooling`).
+
+**Long expressions.** An expression with hundreds of operations used memory
+with the cube of its depth, and one with thousands crashed. The cost is now
+quadratic (a 250-term sum lowers in about 5 s instead of 120 s), and an
+expression nested more than 256 operations deep is reported where it is
+(:doc:`language/limitations`).
+
+**Z3 errors.** A Z3 call that failed went unnoticed, and a later step could
+report something unrelated. The query now ends ``Unresolved`` with reason
+``encoding.failed`` and Z3's message (:doc:`language/tooling`).
+
+**Parallel runs.** With more than one job, a function waiting for its own
+queries could run another function's long query, delaying its result and
+spending its ``--function-timeout``. A waiting function now runs only its own
+queries (:doc:`language/tooling`).
+
+**cvc5 1.4.** Every query over sets, multisets, and maps failed with cvc5 1.4,
+which requires extended arrays for constant arrays; such a query now enables
+them itself (:doc:`language/tooling`).
+
+**clang-format.** A range footprint is written ``p[lo : n]``, not ``p [lo:n]``
+(:doc:`language/tooling`).
+
+Data formats
+~~~~~~~~~~~~
+
+Archives stay ``cppverify.obligation/2`` and JSON diagnostics
+``cppverify.diagnostic/1``. JSON records may carry the status
+``proved-obligations`` (archive replay) and the reason ``interrupted``
+(Ctrl-C).
+
 0.1.1
 -----