@@ -19,10 +19,10 @@ This is a Maven multi-module build (`pom.xml` is the umbrella):
 Verifier package map (`liquidjava-verifier/src/main/java/liquidjava/`):
 - `api/` — entrypoints; `CommandLineLauncher` is the CLI main.
 - `processor/` — Spoon processors. `RefinementProcessor` orchestrates; `refinement_checker/` contains `RefinementTypeChecker`, `MethodsFirstChecker`, `ExternalRefinementTypeChecker`, plus `general_checkers/` and `object_checkers/` for typestate.
-- `ast/` — AST of the Refinements Language (RJ).
-- `rj_language/` — parser from refinement strings to RJ AST.
+- `rj_language/` — the Refinements Language (RJ): `parsing/` (refinement strings → AST), `ast/`, `opt/` (expression simplification), `visitors/`.
 - `smt/` — Z3 translation (`TranslatorToZ3`, `ExpressionToZ3Visitor`, `SMTEvaluator`, `Counterexample`).
-- `errors/`, `utils/`, `diagnostics/`.
+- `diagnostics/` — error and warning reporting (`errors/`, `warnings/`).
+- `utils/` — shared utilities and constants.
 
 ## Commands
 
@@ -31,7 +31,7 @@ Build / install everything:
 mvn clean install
 ```
 
-Run the test suite (verifier module, runs whole `testSuite/` dir):
+Run the test suite (verifier module, runs whole `testSuite/` dir); `./mvnw` works in place of `mvn`:
 ```bash
 mvn test
 ```
@@ -42,7 +42,7 @@ mvn -pl liquidjava-verifier -Dtest=TestExamples test
 mvn -pl liquidjava-verifier -Dtest=TestExamples#testMultiplePaths test
 ```
 
-Verify a specific file/directory from CLI (uses the `liquidjava` script in repo root, macOS/Linux):
+Verify a specific file/directory from CLI (uses the `liquidjava` script in repo root, macOS/Linux; it recompiles the verifier only when local sources or Maven files changed):
 ```bash
 ./liquidjava liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java
 ```
@@ -52,24 +52,25 @@ mvn exec:java -pl liquidjava-verifier \
   -Dexec.mainClass="liquidjava.api.CommandLineLauncher" \
   -Dexec.args="/path/to/file_or_dir"
 ```
+CLI options: one or more paths, `-h`/`--help`, `-v`/`--version`, `-d`/`--debug` (debug logging, skips expression simplification), `-lsp`/`--language-server`.
 
 Code formatting runs automatically in the `validate` phase via `formatter-maven-plugin` (configured for Java 20 in `liquidjava-verifier/pom.xml`); no separate lint command.
 
 ## Test Suite Conventions
 
 Tests are discovered by `TestExamples#testPath` (parameterized) under `liquidjava-example/src/main/java/testSuite/`:
 
-- Single-file cases: filename starts with `Correct…` or `Error…`.
-- Directory cases: directory name contains the substring `correct` or `error`.
-- Anything else is **ignored** (so helper sources can live alongside).
-- Expected errors for a failing case are declared with inline `// <Error Title>` comments on **the line where each error should be reported** (regex `//\s*(.*?\bError\b)`, case-insensitive — see `TestUtils#getExpectedErrorsFromFile`). Both the title and the line number must match, and the count of comments must equal the count of reported errors. Directory cases work the same way: the scanner walks every file in the directory; there are no `.expected` files.
+- Every `.java` file outside a leaf directory is a single-file test case.
+- Every leaf directory (no subdirectories) is a single test case covering all its files.
+- File and directory names do not matter (the `Correct…`/`Error…`/`…_correct`/`…_error` names are only a convention).
+- Expected diagnostics are declared with inline `// Expect: <Title> Error` or `// Expect: Warning` comments on **the line where each diagnostic should be reported** (regex `//\s*Expect:\s*(.*?\b(Error|Warning)\b)`, case-insensitive — see `TestUtils#getExpectedDiagnosticsFromFile`). For errors both the title and the line must match; for warnings only the line. The number of expectations must equal the number of reported diagnostics, so a test with no expectations must produce none. Directory cases collect expectations from every file in the directory; there are no `.expected` files.
 
-When adding new test cases, place them under `liquidjava-example/src/main/java/testSuite/` following the naming rules above — that is the only way they get picked up.
+When adding new test cases, place them under `liquidjava-example/src/main/java/testSuite/` — that is the only way they get picked up.
 
 ## Architecture Notes That Span Files
 
 - **Two-pass typechecking.** `MethodsFirstChecker` collects method signatures and refinement contracts before `RefinementTypeChecker` walks bodies, so forward references and recursion resolve. Edits to one usually need a matching change in the other.
 - **Refinement string → AST → Z3.** A `@Refinement("a > 0")` string flows: `rj_language` parser → `ast` nodes → `smt/TranslatorToZ3` / `ExpressionToZ3Visitor`. New predicate forms generally require touching all three.
-- **External refinements.** `ExternalRefinementTypeChecker` plus `*Refinements.java` companion files specify contracts for third-party APIs without modifying their sources. The `co-specifying-liquidjava` skill covers this workflow.
+- **External refinements.** `ExternalRefinementTypeChecker` plus `*Refinements.java` companion files specify contracts for third-party APIs without modifying their sources.
 - **Typestate** lives in `processor/refinement_checker/object_checkers/` and uses `@StateRefinement` / `@StateSet` from the API. Ghost-state predicates flow through the same SMT pipeline as value refinements.
-- **Z3 dependency.** The verifier shells out to Z3 via JNI bindings; failures often surface as `SMTResult` errors or counterexamples, not Java exceptions.
+- **Z3 dependency.** The verifier calls Z3 in-process through the Java bindings bundled by `z3-turnkey` (no separate Z3 install); failures often surface as `SMTResult` errors or counterexamples, not Java exceptions.