diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsChecker.java b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsChecker.java
index d0ea37cd4830..b09b5a06a3db 100644
--- a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsChecker.java
+++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsChecker.java
@@ -19,7 +19,7 @@
  * CalledMethodsChecker} used as a subchecker in the ResourceLeakChecker, and never independently.
  * Runs the MustCallChecker as a subchecker in order to share the CFG.
  */
-@StubFiles("IOUtils.astub")
+@StubFiles({"IOUtils.astub", "log4j.astub"})
 public class RLCCalledMethodsChecker extends CalledMethodsChecker {
 
   /** Creates a RLCCalledMethodsChecker. */
diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/jdk.astub b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/jdk.astub
new file mode 100644
index 000000000000..e9bf472a03c0
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/jdk.astub
@@ -0,0 +1,32 @@
+package java.lang;
+
+import java.io.PrintStream;
+import java.io.PrintWriter;
+import org.checkerframework.checker.lock.qual.GuardSatisfied;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+
+public interface AutoCloseable {
+  @SideEffectFree
+  void close(@GuardSatisfied AutoCloseable this) throws Exception;
+}
+
+public class Throwable {
+  @SideEffectFree
+  public void printStackTrace();
+
+  @SideEffectFree
+  public void printStackTrace(PrintStream s);
+
+  @SideEffectFree
+  public void printStackTrace(PrintWriter s);
+}
+
+package java.io;
+
+import org.checkerframework.checker.lock.qual.GuardSatisfied;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+
+public interface Closeable extends AutoCloseable {
+  @SideEffectFree
+  public void close(@GuardSatisfied Closeable this) throws IOException;
+}
diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/log4j.astub b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/log4j.astub
new file mode 100644
index 000000000000..c0393daadd93
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/log4j.astub
@@ -0,0 +1,212 @@
+import org.checkerframework.dataflow.qual.SideEffectFree;
+
+// Log4j 1.x API stubs (package org.apache.log4j).
+package org.apache.log4j;
+
+class Category {
+  @SideEffectFree public void debug(Object message);
+  @SideEffectFree public void debug(Object message, Throwable t);
+  @SideEffectFree public void info(Object message);
+  @SideEffectFree public void info(Object message, Throwable t);
+  @SideEffectFree public void warn(Object message);
+  @SideEffectFree public void warn(Object message, Throwable t);
+  @SideEffectFree public void error(Object message);
+  @SideEffectFree public void error(Object message, Throwable t);
+  @SideEffectFree public void fatal(Object message);
+  @SideEffectFree public void fatal(Object message, Throwable t);
+  @SideEffectFree public void log(Priority priority, Object message);
+  @SideEffectFree public void log(Priority priority, Object message, Throwable t);
+  @SideEffectFree public void log(String callerFQCN, Priority level, Object message, Throwable t);
+}
+
+class Logger extends Category {
+    @SideEffectFree public void trace(Object message);
+    @SideEffectFree public void trace(Object message, Throwable t);
+}
+
+// Log4j 2.x API stubs (package org.apache.logging.log4j).
+package org.apache.logging.log4j;
+
+import org.apache.logging.log4j.message.Message;
+
+interface Logger {
+  @SideEffectFree void trace(CharSequence message);
+  @SideEffectFree void trace(CharSequence message, Throwable throwable);
+  @SideEffectFree void trace(Object message);
+  @SideEffectFree void trace(Object message, Throwable throwable);
+  @SideEffectFree void trace(String message);
+  @SideEffectFree void trace(String message, Throwable throwable);
+  @SideEffectFree void trace(String message, Object p0);
+  @SideEffectFree void trace(String message, Object p0, Object p1);
+  @SideEffectFree void trace(String message, Object p0, Object p1, Object p2);
+  @SideEffectFree void trace(String message, Object p0, Object p1, Object p2, Object p3);
+  @SideEffectFree void trace(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4);
+  @SideEffectFree void trace(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
+  @SideEffectFree void trace(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6);
+  @SideEffectFree void trace(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7);
+  @SideEffectFree void trace(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8);
+  @SideEffectFree void trace(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8, Object p9);
+  @SideEffectFree void trace(String message, Object... params);
+  @SideEffectFree void trace(Message message);
+  @SideEffectFree void trace(Message message, Throwable throwable);
+
+  @SideEffectFree void debug(CharSequence message);
+  @SideEffectFree void debug(CharSequence message, Throwable throwable);
+  @SideEffectFree void debug(Object message);
+  @SideEffectFree void debug(Object message, Throwable throwable);
+  @SideEffectFree void debug(String message);
+  @SideEffectFree void debug(String message, Throwable throwable);
+  @SideEffectFree void debug(String message, Object p0);
+  @SideEffectFree void debug(String message, Object p0, Object p1);
+  @SideEffectFree void debug(String message, Object p0, Object p1, Object p2);
+  @SideEffectFree void debug(String message, Object p0, Object p1, Object p2, Object p3);
+  @SideEffectFree void debug(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4);
+  @SideEffectFree void debug(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
+  @SideEffectFree void debug(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6);
+  @SideEffectFree void debug(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7);
+  @SideEffectFree void debug(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8);
+  @SideEffectFree void debug(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8, Object p9);
+  @SideEffectFree void debug(String message, Object... params);
+  @SideEffectFree void debug(Message message);
+  @SideEffectFree void debug(Message message, Throwable throwable);
+
+  @SideEffectFree void info(CharSequence message);
+  @SideEffectFree void info(CharSequence message, Throwable throwable);
+  @SideEffectFree void info(Object message);
+  @SideEffectFree void info(Object message, Throwable throwable);
+  @SideEffectFree void info(String message);
+  @SideEffectFree void info(String message, Throwable throwable);
+  @SideEffectFree void info(String message, Object p0);
+  @SideEffectFree void info(String message, Object p0, Object p1);
+  @SideEffectFree void info(String message, Object p0, Object p1, Object p2);
+  @SideEffectFree void info(String message, Object p0, Object p1, Object p2, Object p3);
+  @SideEffectFree void info(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4);
+  @SideEffectFree void info(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
+  @SideEffectFree void info(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6);
+  @SideEffectFree void info(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7);
+  @SideEffectFree void info(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8);
+  @SideEffectFree void info(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8, Object p9);
+  @SideEffectFree void info(String message, Object... params);
+  @SideEffectFree void info(Message message);
+  @SideEffectFree void info(Message message, Throwable throwable);
+
+  @SideEffectFree void warn(CharSequence message);
+  @SideEffectFree void warn(CharSequence message, Throwable throwable);
+  @SideEffectFree void warn(Object message);
+  @SideEffectFree void warn(Object message, Throwable throwable);
+  @SideEffectFree void warn(String message);
+  @SideEffectFree void warn(String message, Throwable throwable);
+  @SideEffectFree void warn(String message, Object p0);
+  @SideEffectFree void warn(String message, Object p0, Object p1);
+  @SideEffectFree void warn(String message, Object p0, Object p1, Object p2);
+  @SideEffectFree void warn(String message, Object p0, Object p1, Object p2, Object p3);
+  @SideEffectFree void warn(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4);
+  @SideEffectFree void warn(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
+  @SideEffectFree void warn(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6);
+  @SideEffectFree void warn(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7);
+  @SideEffectFree void warn(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8);
+  @SideEffectFree void warn(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8, Object p9);
+  @SideEffectFree void warn(String message, Object... params);
+  @SideEffectFree void warn(Message message);
+  @SideEffectFree void warn(Message message, Throwable throwable);
+
+  @SideEffectFree void error(CharSequence message);
+  @SideEffectFree void error(CharSequence message, Throwable throwable);
+  @SideEffectFree void error(Object message);
+  @SideEffectFree void error(Object message, Throwable throwable);
+  @SideEffectFree void error(String message);
+  @SideEffectFree void error(String message, Throwable throwable);
+  @SideEffectFree void error(String message, Object p0);
+  @SideEffectFree void error(String message, Object p0, Object p1);
+  @SideEffectFree void error(String message, Object p0, Object p1, Object p2);
+  @SideEffectFree void error(String message, Object p0, Object p1, Object p2, Object p3);
+  @SideEffectFree void error(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4);
+  @SideEffectFree void error(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
+  @SideEffectFree void error(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6);
+  @SideEffectFree void error(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7);
+  @SideEffectFree void error(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8);
+  @SideEffectFree void error(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8, Object p9);
+  @SideEffectFree void error(String message, Object... params);
+  @SideEffectFree void error(Message message);
+  @SideEffectFree void error(Message message, Throwable throwable);
+
+  @SideEffectFree void fatal(CharSequence message);
+  @SideEffectFree void fatal(CharSequence message, Throwable throwable);
+  @SideEffectFree void fatal(Object message);
+  @SideEffectFree void fatal(Object message, Throwable throwable);
+  @SideEffectFree void fatal(String message);
+  @SideEffectFree void fatal(String message, Throwable throwable);
+  @SideEffectFree void fatal(String message, Object p0);
+  @SideEffectFree void fatal(String message, Object p0, Object p1);
+  @SideEffectFree void fatal(String message, Object p0, Object p1, Object p2);
+  @SideEffectFree void fatal(String message, Object p0, Object p1, Object p2, Object p3);
+  @SideEffectFree void fatal(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4);
+  @SideEffectFree void fatal(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
+  @SideEffectFree void fatal(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6);
+  @SideEffectFree void fatal(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7);
+  @SideEffectFree void fatal(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8);
+  @SideEffectFree void fatal(
+      String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
+      Object p6, Object p7, Object p8, Object p9);
+  @SideEffectFree void fatal(String message, Object... params);
+  @SideEffectFree void fatal(Message message);
+  @SideEffectFree void fatal(Message message, Throwable throwable);
+}
diff --git a/checker/tests/resourceleak/TwoResourcesECM.java b/checker/tests/resourceleak/TwoResourcesECM.java
index dfa42c4ab9a1..484a0377aa8f 100644
--- a/checker/tests/resourceleak/TwoResourcesECM.java
+++ b/checker/tests/resourceleak/TwoResourcesECM.java
@@ -12,19 +12,12 @@
 class TwoResourcesECM {
   @Owning Socket s1, s2;
 
-  // The contracts.postcondition error below is thrown because s1 is not final,
-  // and therefore might theoretically be side-effected by the call to s2.close()
-  // even on the non-exceptional path. See ReplicaInputStreams.java for a variant
-  // of this test where such an error is not issued. Because this method can leak
-  // along both regular and exceptional exits, both errors are issued.
-  //
   // The contracts.exceptional.postcondition error is thrown because destructors
   // have to close their resources even on exception.  If s1.close() throws an
   // exception, then s2.close() will not be called.
   @EnsuresCalledMethods(
       value = {"this.s1", "this.s2"},
       methods = {"close"})
-  // :: error: [contracts.postcondition]
   // :: error: [contracts.exceptional.postcondition]
   public void dispose() throws IOException {
     s1.close();
diff --git a/checker/tests/resourceleak/sideeffect-free-stubs/AutoCloseableClose.java b/checker/tests/resourceleak/sideeffect-free-stubs/AutoCloseableClose.java
new file mode 100644
index 000000000000..1bf028fb5a6f
--- /dev/null
+++ b/checker/tests/resourceleak/sideeffect-free-stubs/AutoCloseableClose.java
@@ -0,0 +1,30 @@
+// RLC uses Called Methods facts to remember that a resource has already been closed.
+// This test checks that the RLC-specific SideEffectFree stub for AutoCloseable.close()
+// preserves those facts across another close call in the same destructor, rather than
+// conservatively forgetting them after the first invocation.
+
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.mustcall.qual.Owning;
+
+final class TestAutoCloseable implements AutoCloseable {
+  @Override
+  public void close() {}
+}
+
+class AutoCloseableClose implements AutoCloseable {
+  private @Owning AutoCloseable first = new TestAutoCloseable();
+  private @Owning AutoCloseable second = new TestAutoCloseable();
+
+  @Override
+  @EnsuresCalledMethods(
+      value = {"this.first", "this.second"},
+      methods = "close")
+  public void close() {
+    try {
+      first.close();
+      second.close();
+    } catch (Exception e) {
+      throw new AssertionError(e);
+    }
+  }
+}
diff --git a/checker/tests/resourceleak/sideeffect-free-stubs/CloseableClose.java b/checker/tests/resourceleak/sideeffect-free-stubs/CloseableClose.java
new file mode 100644
index 000000000000..d268c5614eb1
--- /dev/null
+++ b/checker/tests/resourceleak/sideeffect-free-stubs/CloseableClose.java
@@ -0,0 +1,34 @@
+// RLC uses Called Methods facts to remember that a resource has already been closed.
+// This test checks that the RLC-specific SideEffectFree stub for Closeable.close()
+// preserves those facts across another close call in the same destructor, rather than
+// conservatively forgetting them after the first invocation.
+
+import java.io.Closeable;
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.mustcall.qual.Owning;
+
+final class TestCloseable implements Closeable {
+  @Override
+  public void close() {}
+}
+
+class CloseableClose implements Closeable {
+  private @Owning Closeable first = new TestCloseable();
+  private @Owning Closeable second = new TestCloseable();
+
+  @Override
+  @EnsuresCalledMethods(
+      value = {"this.first", "this.second"},
+      methods = "close")
+  public void close() {
+    try {
+      try {
+        first.close();
+      } catch (Exception ignored) {
+      }
+      second.close();
+    } catch (Exception e) {
+      throw new AssertionError(e);
+    }
+  }
+}
diff --git a/checker/tests/resourceleak/sideeffect-free-stubs/Log4j1ObjectCalls.java b/checker/tests/resourceleak/sideeffect-free-stubs/Log4j1ObjectCalls.java
new file mode 100644
index 000000000000..be2a5f821710
--- /dev/null
+++ b/checker/tests/resourceleak/sideeffect-free-stubs/Log4j1ObjectCalls.java
@@ -0,0 +1,68 @@
+// This test covers the Log4j 1.x API in package org.apache.log4j.
+// The RLC-specific stub marks logging methods as @SideEffectFree, so logging after a resource is
+// closed should not wipe out the close fact.
+
+import java.io.Closeable;
+import org.apache.log4j.Logger;
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.mustcall.qual.Owning;
+
+class Log4j1DebugObject implements Closeable {
+  private final Logger logger = Logger.getLogger("Log4j1DebugObject");
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.debug("after close");
+  }
+}
+
+class Log4j1DebugWithThrowable implements Closeable {
+  private final Logger logger = Logger.getLogger("Log4j1DebugWithThrowable");
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.debug("after close", new RuntimeException());
+  }
+}
+
+class Log4j1InfoObject implements Closeable {
+  private final Logger logger = Logger.getLogger("Log4j1InfoObject");
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.info("after close");
+  }
+}
+
+class Log4j1WarnObject implements Closeable {
+  private final Logger logger = Logger.getLogger("Log4j1WarnObject");
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.warn("after close");
+  }
+}
+
+class Log4j1ErrorObject implements Closeable {
+  private final Logger logger = Logger.getLogger("Log4j1ErrorObject");
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.error("after close");
+  }
+}
diff --git a/checker/tests/resourceleak/sideeffect-free-stubs/Log4j2ObjectCalls.java b/checker/tests/resourceleak/sideeffect-free-stubs/Log4j2ObjectCalls.java
new file mode 100644
index 000000000000..a1780612487c
--- /dev/null
+++ b/checker/tests/resourceleak/sideeffect-free-stubs/Log4j2ObjectCalls.java
@@ -0,0 +1,86 @@
+// This test covers the Log4j 2.x API in package org.apache.logging.log4j.
+// real library API. The RLC-specific stub marks logging methods as @SideEffectFree, so logging
+// after a resource is closed should not wipe out the close fact.
+
+import java.io.Closeable;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.mustcall.qual.Owning;
+
+final class CloseableResource implements Closeable {
+  @Override
+  public void close() {}
+}
+
+class Log4j2DebugObject implements Closeable {
+  private static final Logger logger = LogManager.getLogger();
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.debug("after close");
+  }
+}
+
+class Log4j2DebugVarargs implements Closeable {
+  private static final Logger logger = LogManager.getLogger();
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.debug("closed resource {}", "name");
+  }
+}
+
+class Log4j2InfoObject implements Closeable {
+  private static final Logger logger = LogManager.getLogger();
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.info("after close");
+  }
+}
+
+class Log4j2WarnObject implements Closeable {
+  private static final Logger logger = LogManager.getLogger();
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.warn("after close");
+  }
+}
+
+class Log4j2ErrorObject implements Closeable {
+  private static final Logger logger = LogManager.getLogger();
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.error("after close");
+  }
+}
+
+class Log4j2ErrorWithThrowable implements Closeable {
+  private static final Logger logger = LogManager.getLogger();
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    logger.error("after close", new RuntimeException());
+  }
+}
diff --git a/checker/tests/resourceleak/sideeffect-free-stubs/ThrowablePrintStackTrace.java b/checker/tests/resourceleak/sideeffect-free-stubs/ThrowablePrintStackTrace.java
new file mode 100644
index 000000000000..84aaebb00508
--- /dev/null
+++ b/checker/tests/resourceleak/sideeffect-free-stubs/ThrowablePrintStackTrace.java
@@ -0,0 +1,47 @@
+// RLC-specific stubs mark Throwable.printStackTrace overloads as SideEffectFree so
+// that debugging/logging after a resource is closed does not wipe out the close fact.
+// This file checks the no-arg, PrintStream, and PrintWriter variants.
+
+import java.io.Closeable;
+import java.io.PrintStream;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.mustcall.qual.Owning;
+
+class ThrowablePrintStackTrace implements Closeable {
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    new RuntimeException("debug").printStackTrace();
+  }
+}
+
+class ThrowablePrintStackTracePrintStream implements Closeable {
+  private static final PrintStream STREAM = System.err;
+
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    new RuntimeException("debug").printStackTrace(STREAM);
+  }
+}
+
+class ThrowablePrintStackTracePrintWriter implements Closeable {
+  private static final PrintWriter WRITER = new PrintWriter(new StringWriter());
+
+  private @Owning CloseableResource resource = new CloseableResource();
+
+  @Override
+  @EnsuresCalledMethods(value = "this.resource", methods = "close")
+  public void close() {
+    resource.close();
+    new RuntimeException("debug").printStackTrace(WRITER);
+  }
+}