diff --git a/_layouts/default.html b/_layouts/default.html
index 8ee9fe0..5eff81a 100644
--- a/_layouts/default.html
+++ b/_layouts/default.html
@@ -20,7 +20,7 @@
     {% include components/header.html %}
     <div class="main-content-wrap">
       {% include components/breadcrumbs.html %}
-      <div id="main-content" class="main-content">
+      <div id="main-content" class="main-content" tabindex="-1">
         <main>
           {% if site.heading_anchors != false %}
             {% include vendor/anchor_headings.html html=content beforeHeading="true" anchorBody="<svg viewBox=\"0 0 16 16\" aria-hidden=\"true\"><use xlink:href=\"#svg-link\"></use></svg>" anchorClass="anchor-heading" anchorAttrs="aria-labelledby=\"%html_id%\"" %}
diff --git a/pages/diagnostics/errors.md b/pages/diagnostics/errors.md
index d3e7e4c..e38300e 100644
--- a/pages/diagnostics/errors.md
+++ b/pages/diagnostics/errors.md
@@ -14,6 +14,7 @@ An error can be caused by a refinement violation, an invalid refinement, or anot
 | --- | --- |
 | `RefinementError` | A refinement was violated or could not be proven |
 | `StateRefinementError` | A state refinement was violated or could not be proven |
+| `SMTUnknownError` | The solver could not determine whether a refinement holds |
 | `NotFoundError` | An element used in a refinement could not be found |
 | `SyntaxError` | The syntax used in a refinement is invalid |
 | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments |
diff --git a/pages/resources.md b/pages/resources.md
index f256691..9d2a206 100644
--- a/pages/resources.md
+++ b/pages/resources.md
@@ -14,7 +14,7 @@ description: Find LiquidJava papers, posters, and source repositories for deeper
 
 ## Posters
 
-- [Usability-Oriented Design of Liquid Types for Java](https://icse2023.paperlessevents.com.au/share/Gamboa-85), ICSE 2023 Digital Poster Session
+- [Usability-Oriented Design of Liquid Types for Java](https://conf.researchr.org/details/icse-2023/icse-2023-technical-track/142/Usability-Oriented-Design-of-Liquid-Types-for-Java), ICSE 2023 Poster Session
 - [LiquidJava: Adding Lightweight Verification to Java](https://catarinagamboa.github.io/assets/docs/poster_LiquidJava.pdf), INForum 2021
 - [Improving the Usability of LiquidJava](https://rcosta358.github.io/improving_the_usability_of_liquidjava.pdf), 11th LASIGE Workshop Poster Session
 - [Barista: Synthesizing Typestate Specifications with LLM Agents](https://rcosta358.github.io/barista.pdf), 11th LASIGE Workshop Poster Session