diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java
new file mode 100644
index 00000000..d51af9a0
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java
@@ -0,0 +1,123 @@
+package de.uzl.its.swat.common;
+
+import java.lang.ref.ReferenceQueue;
+import java.lang.ref.WeakReference;
+import java.util.HashSet;
+
+/**
+ * Bookkeeping that lets {@link UtilInstrumented#refEquals} reproduce Java's reference identity
+ * although the NoCache transformer de-interns string literals and the boxing caches.
+ *
+ * <p>Every object that SWAT creates in place of a shared instance (a string literal, a {@code
+ * valueOf} result, an {@code intern()} result) is registered here. Two such objects are one
+ * instance in the original program exactly when their values are equal (and, for boxes, the value
+ * is in the cache range). Objects that are not registered keep their own identity.
+ *
+ * <p>This class is not instrumented and its methods are ignored invocations: their results only
+ * depend on where an object was created, which the control flow already determines, so the
+ * symbolic state receives them as concrete values.
+ */
+@SuppressWarnings("unused")
+public final class RefIdentity {
+
+    private static final ReferenceQueue<Object> queue = new ReferenceQueue<>();
+    private static final HashSet<Key> deInterned = new HashSet<>();
+
+    private RefIdentity() {}
+
+    /** Registers {@code copy} as standing for the shared instance of its value. */
+    public static void markDeInterned(Object copy) {
+        if (copy == null) return;
+        synchronized (deInterned) {
+            expunge();
+            deInterned.add(new Key(copy, queue));
+        }
+    }
+
+    public static boolean isDeInterned(Object o) {
+        if (o == null) return false;
+        synchronized (deInterned) {
+            return deInterned.contains(new Key(o, null));
+        }
+    }
+
+    /**
+     * Whether {@code s} is, in the original program, the canonical (interned) instance of its value:
+     * a de-interned copy, or a pooled string that reached the program without passing the NoCache
+     * transformer (e.g. a literal returned by the JDK). The pool lookup interns a fresh copy rather
+     * than {@code s}, so it never turns {@code s} itself into the pooled instance.
+     */
+    public static boolean isCanonicalString(String s) {
+        return isDeInterned(s) || isPooledOnly(s);
+    }
+
+    /** Whether {@code s} is an unregistered string that is the pooled instance of its value. */
+    public static boolean isPooledOnly(String s) {
+        return !isDeInterned(s) && new String(s).intern() == s;
+    }
+
+    /**
+     * Whether {@code o} is, in the original program, a cached box: a de-interned {@code valueOf}
+     * copy (cached if its value is in the cache range, which the caller checks), or the cached
+     * instance itself.
+     */
+    public static boolean isCanonicalBox(Object o) {
+        if (isDeInterned(o)) return true;
+        if (o instanceof Integer i) return i == Integer.valueOf(i.intValue());
+        if (o instanceof Long l) return l == Long.valueOf(l.longValue());
+        if (o instanceof Short s) return s == Short.valueOf(s.shortValue());
+        if (o instanceof Byte b) return b == Byte.valueOf(b.byteValue());
+        if (o instanceof Character c) return c == Character.valueOf(c.charValue());
+        if (o instanceof Boolean b) return b == Boolean.valueOf(b.booleanValue());
+        return false;
+    }
+
+    /**
+     * {@code s.intern() == s} with the JVM's own side effect: an unregistered string whose value is
+     * not pooled yet becomes the pooled instance. A registered copy never does, its value is pooled.
+     */
+    public static boolean internsToItself(String s) {
+        return !isDeInterned(s) && s.intern() == s;
+    }
+
+    /** Plain reference identity, kept out of the symbolic state's view of {@code IF_ACMP}. */
+    public static boolean same(Object a, Object b) {
+        return a == b;
+    }
+
+    /**
+     * Marks a reference comparison whose outcome depends on the values of {@code a} and {@code b}
+     * in a way SWAT does not encode. The symbolic state records a reference semantic change when an
+     * argument is symbolic.
+     */
+    public static void valueDependentIdentity(Object a, Object b) {}
+
+    private static void expunge() {
+        Object k;
+        while ((k = queue.poll()) != null) {
+            deInterned.remove(k);
+        }
+    }
+
+    private static final class Key extends WeakReference<Object> {
+        private final int hash;
+
+        Key(Object referent, ReferenceQueue<Object> q) {
+            super(referent, q);
+            this.hash = System.identityHashCode(referent);
+        }
+
+        @Override
+        public int hashCode() {
+            return hash;
+        }
+
+        @Override
+        public boolean equals(Object other) {
+            if (this == other) return true;
+            if (!(other instanceof Key k)) return false;
+            Object referent = get();
+            return referent != null && referent == k.get();
+        }
+    }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java
index 2247fb86..98cf9a46 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java
@@ -42,10 +42,6 @@ public class Util {
 
     private static final HashMap<String, Boolean> shouldInstrumentCache = new HashMap<>();
 
-    // Maintain a set of class names that have been de-interned
-    private static final Set<String> deInternedClasses = new HashSet<>(Arrays.asList(
-            String.class.getName(), Boolean.class.getName(), Byte.class.getName(), Short.class.getName(),
-            Character.class.getName(), Integer.class.getName(), Long.class.getName()));
 
     /**
      * Just a method for validating the engine!
@@ -419,19 +415,4 @@ public static boolean isSymbolicMethod(String cname, String name) {
         return Pattern.matches(symbolicMethodPattern, name);
     }
 
-    static boolean shouldUseValueEquality(Object a, Object b) {
-        // If either is null, Objects.equals handles it correctly anyway
-        if (a == null || b == null) {
-            return true;
-        }
-
-        // Check if either object's class has been de-interned
-        return isDeInternedClass(a.getClass()) || isDeInternedClass(b.getClass());
-    }
-
-    private static boolean isDeInternedClass(Class<?> clazz) {
-        // Check the exact class and optionally superclasses if inheritance matters
-        return deInternedClasses.contains(clazz.getName());
-    }
-
 }
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java
index e288bec7..8282618f 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java
@@ -5,7 +5,6 @@
 
 import java.lang.reflect.InvocationTargetException;
 import java.lang.reflect.Method;
-import java.util.Objects;
 
 @SuppressWarnings("unused")
 public class UtilInstrumented {
@@ -24,14 +23,69 @@ public static void liftClass(Object param, String paramCnameDot, String methodNa
         }
     }
     /**
-     * Conditionally uses Objects.equals() for de-interned classes,
-     * otherwise uses reference equality.
+     * Replaces {@code IF_ACMPEQ}/{@code IF_ACMPNE}: Java reference identity, computed on objects of
+     * which SWAT de-interned the literals and boxing caches (see {@link RefIdentity}).
+     *
+     * <p>Two canonical instances (literals, interned strings, cached boxes) are identical exactly
+     * when their values are equal, and that comparison goes through the modelled {@code equals}
+     * and unboxing calls so the symbolic state sees its dependence on the values. Every other
+     * comparison is plain identity and concrete. The comparisons themselves must not be
+     * {@code IF_ACMP}s here: the symbolic state encodes those on strings as value equality.
      */
     @SuppressWarnings("unused")
     public static boolean refEquals(Object a, Object b) {
-        if (Util.shouldUseValueEquality(a, b)) {
-            return Objects.equals(a, b);
+        if (a instanceof String sa && b instanceof String sb) {
+            if (RefIdentity.isCanonicalString(sa) && RefIdentity.isCanonicalString(sb)) {
+                if (RefIdentity.isPooledOnly(sa) || RefIdentity.isPooledOnly(sb)) {
+                    // Whether a string from uninstrumented code is pooled may depend on its value.
+                    RefIdentity.valueDependentIdentity(sa, sb);
+                }
+                return sa.equals(sb);
+            }
+            return RefIdentity.same(a, b);
         }
-        return a == b;
+        if (RefIdentity.same(a, b)) {
+            return true;
+        }
+        if (RefIdentity.isCanonicalBox(a) && RefIdentity.isCanonicalBox(b)) {
+            // Distinct cached boxes: the same instance iff the values are equal and in the cache range.
+            if (a instanceof Integer x && b instanceof Integer y) {
+                int v = x.intValue();
+                return v == y.intValue() && v >= -128 && v <= 127;
+            }
+            if (a instanceof Long x && b instanceof Long y) {
+                long v = x.longValue();
+                return v == y.longValue() && v >= -128 && v <= 127;
+            }
+            if (a instanceof Short x && b instanceof Short y) {
+                short v = x.shortValue();
+                return v == y.shortValue() && v >= -128 && v <= 127;
+            }
+            if (a instanceof Character x && b instanceof Character y) {
+                char v = x.charValue();
+                return v == y.charValue() && v <= 127;
+            }
+            if (a instanceof Byte x && b instanceof Byte y) {
+                return x.byteValue() == y.byteValue();
+            }
+            if (a instanceof Boolean x && b instanceof Boolean y) {
+                return x.booleanValue() == y.booleanValue();
+            }
+        }
+        return RefIdentity.same(a, b);
+    }
+
+    /**
+     * Replaces {@code String.intern()}: a de-interned copy standing for the pooled instance, or
+     * {@code s} itself when {@code s} is (or, by this call, becomes) the pooled instance.
+     */
+    @SuppressWarnings("unused")
+    public static String intern(String s) {
+        if (RefIdentity.internsToItself(s)) {
+            return s;
+        }
+        String copy = new String(s);
+        RefIdentity.markDeInterned(copy);
+        return copy;
     }
 }
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java
index aba06b80..b301652e 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java
@@ -23,6 +23,7 @@ public void visitLdcInsn(Object value) {
             mv.visitLdcInsn(value);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/String", "<init>",
                     "(Ljava/lang/String;)V", false);
+            markDeInterned();
             //NoCacheTransformer.getPrintBox()
             //        .addMsg("Replacing LDC with new String");
         } else {
@@ -33,14 +34,16 @@ public void visitLdcInsn(Object value) {
     // Intercept method calls to disable interning and caching.
     @Override
     public void visitMethodInsn(int opcode, String owner, String name, String descriptor, boolean isInterface) {
-        // Skip String.intern() calls.
+        // Replace String.intern() with a de-interned copy that stands for the pooled instance.
         if (opcode == Opcodes.INVOKEVIRTUAL &&
                 owner.equals("java/lang/String") &&
                 name.equals("intern") &&
                 descriptor.equals("()Ljava/lang/String;") &&
                 Config.instance().isUseStringInterning()) {
+            mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/UtilInstrumented", "intern",
+                    "(Ljava/lang/String;)Ljava/lang/String;", false);
             NoCacheTransformer.getPrintBox()
-                    .addMsg("Removing String.intern() call");
+                    .addMsg("Replacing String.intern() with UtilInstrumented.intern");
             return;
         }
         // Replace Integer.valueOf(int) with new Integer(int)
@@ -54,6 +57,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Integer", "<init>", "(I)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Integer.valueOf with new Integer");
             return;
@@ -69,6 +73,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.LLOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Long", "<init>", "(J)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Long.valueOf with new Long");
             return;
@@ -84,6 +89,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Short", "<init>", "(S)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Short.valueOf with new Short");
             return;
@@ -99,6 +105,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Byte", "<init>", "(B)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Byte.valueOf with new Byte");
             return;
@@ -114,6 +121,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Character", "<init>", "(C)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Character.valueOf with new Character");
             return;
@@ -129,6 +137,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Boolean", "<init>", "(Z)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Boolean.valueOf with new Boolean");
             return;
@@ -137,6 +146,16 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
         mv.visitMethodInsn(opcode, owner, name, descriptor, isInterface);
     }
 
+    /**
+     * Registers the copy on top of the stack as standing for a shared instance, so that
+     * {@code UtilInstrumented.refEquals} can reproduce the identity of the original program.
+     */
+    private void markDeInterned() {
+        mv.visitInsn(Opcodes.DUP);
+        mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/RefIdentity", "markDeInterned",
+                "(Ljava/lang/Object;)V", false);
+    }
+
     /*
     // Instrument object reference comparisons (IF_ACMPEQ and IF_ACMPNE) to print a warning.
     @Override
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java
index d89f7cc2..e7d8208e 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java
@@ -28,6 +28,7 @@ public class InvocationHandler {
                             "java/io/PrintStream/println",
                             "de/uzl/its/swat/instrument/Intrinsics",
                             "de/uzl/its/swat/common/UtilInstrumented",
+                            "de/uzl/its/swat/common/RefIdentity",
                             "de/uzl/its/swat/witness/Witness",
                             "de/uzl/its/swat/instrument/svcomp/Verifier",
                             "java/io/PrintStream",
@@ -67,8 +68,12 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         Type[] types = Type.getArgumentTypes(desc);
         logger.trace("Invoking method {} in class {} with arguments {}", name, owner, arguments);
 
-        // We do that first to include the pointer in instance invocation cases
-        boolean containsSymbolicArgument = arguments.stream().anyMatch(v -> {
+        boolean ignored = IGNORED_INVOCATIONS.contains(owner + "/" + name)
+                || IGNORED_INVOCATIONS.contains(owner);
+
+        // We do that first to include the pointer in instance invocation cases. Ignored
+        // invocations are never recorded, so their arguments need no (possibly deep) scan.
+        boolean containsSymbolicArgument = !ignored && arguments.stream().anyMatch(v -> {
             try {
                 return v.isSymbolic() || hasSymbolicElement(v);
             } catch (NotImplementedException e) {
@@ -78,7 +83,7 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         });
 
         if (isInstance) {
-            containsSymbolicArgument = containsSymbolicArgument || instance.isSymbolic();
+            containsSymbolicArgument = containsSymbolicArgument || (!ignored && instance.isSymbolic());
             retValue = instance.invokeMethod(name, types, arguments.toArray(new Value[0]));
         } else {
             retValue =
@@ -91,9 +96,7 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         }
 
         // When the method is not implemented and its not on the ignore list, we record it
-        if (retValue instanceof PlaceHolder &&
-                !(IGNORED_INVOCATIONS.contains(owner + "/" + name)
-                || IGNORED_INVOCATIONS.contains(owner))) {
+        if (retValue instanceof PlaceHolder && !ignored) {
 
             if(isInstance) arguments.add(0, instance);
 
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java
new file mode 100644
index 00000000..750ea751
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java
@@ -0,0 +1,27 @@
+package de.uzl.its.swat.symbolic.invoke;
+
+import de.uzl.its.swat.common.exceptions.NotImplementedException;
+import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
+import de.uzl.its.swat.symbolic.value.PlaceHolder;
+import de.uzl.its.swat.symbolic.value.Value;
+
+/**
+ * Symbolic side of {@link de.uzl.its.swat.common.RefIdentity}. Its results are concrete facts about
+ * where objects were created; only {@code valueDependentIdentity} affects the symbolic state.
+ */
+public final class RefIdentityInvocation {
+
+    public static Value<?, ?> invokeStaticMethod(
+            String name, Value<?, ?>[] args, SymbolicTraceHandler symbolicTraceHandler) throws NotImplementedException {
+        if (name.equals("valueDependentIdentity")) {
+            for (Value<?, ?> arg : args) {
+                if (arg.isSymbolic()) {
+                    // A reference comparison decided by symbolic values that SWAT does not encode.
+                    symbolicTraceHandler.recordReferenceSemanticChange();
+                    break;
+                }
+            }
+        }
+        return PlaceHolder.instance;
+    }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java
index 21b2849f..d1a9878d 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java
@@ -53,6 +53,8 @@ public final class StaticInvocation {
                             name, args, desc, symbolicStateHandler);
                     case "java/lang/Double" -> DoubleInvocation.invokeStaticMethod(
                             name, args, desc, symbolicStateHandler);
+                    case "de/uzl/its/swat/common/RefIdentity" -> RefIdentityInvocation.invokeStaticMethod(
+                            name, args, symbolicStateHandler);
                     case "java/util/Objects" -> ObjectsInvocation.invokeStaticMethod(
                             name, args, desc, symbolicStateHandler);
                     default -> PlaceHolder.instance;
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java
index 2f6cf86a..68d77efa 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java
@@ -7,15 +7,10 @@
 import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
 import de.uzl.its.swat.symbolic.value.PlaceHolder;
 import de.uzl.its.swat.symbolic.value.Value;
-import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.BooleanValue;
 import de.uzl.its.swat.symbolic.value.reference.ObjectValue;
-import de.uzl.its.swat.symbolic.value.reference.lang.CharacterObjectValue;
-import de.uzl.its.swat.symbolic.value.reference.lang.StringValue;
-import de.uzl.its.swat.thread.ThreadHandler;
 import org.objectweb.asm.Type;
 
-import static java.lang.Thread.currentThread;
-
 public class ObjectsInvocation {
 
     public static Value<?, ?> invokeStaticMethod(
@@ -35,21 +30,9 @@ public class ObjectsInvocation {
         ObjectValue<?,?> a = args[0].asObjectValue();
         ObjectValue<?,?> b = args[1].asObjectValue();
 
-        // Check for user-de-interned strings with different addresses.
-        // This detects when refEquals (which calls Objects.equals) compares strings
-        // that were explicitly created with new String() in user code.
-        // In such cases, reference equality semantics may differ from what the user intended.
-        if (a instanceof StringValue s1 && b instanceof StringValue s2) {
-            if ((s1.isUserDeInterned() || s2.isUserDeInterned())
-                    && s1.getAddress() != s2.getAddress()) {
-                // Record that reference equality semantics may have changed
-                ThreadHandler.getSymbolicTraceHandler(currentThread().getId())
-                        .recordReferenceSemanticChange();
-            }
-        }
-
         if(a.getAddress() == ObjectValue.ADDRESS_NULL || b.getAddress() == ObjectValue.ADDRESS_NULL) {
-            return PlaceHolder.instance;
+            // A null operand: equal iff both are null, independent of any symbolic content.
+            return new BooleanValue(a.context, a.getAddress() == b.getAddress());
         }
         return a.invokeMethod("equals", null, new Value[]{b} );
     }
diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy
new file mode 100644
index 00000000..331432a4
--- /dev/null
+++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy
@@ -0,0 +1,110 @@
+package de.uzl.its.swat.common
+
+import spock.lang.Specification
+
+/**
+ * Concrete semantics of the IF_ACMP replacement: on objects de-interned the way the NoCache
+ * transformer does it, refEquals must give the answer the original program's {@code ==} gives.
+ */
+class RefEqualsSpec extends Specification {
+
+    /** What the NoCache transformer emits for a string literal. */
+    private static String literal(String s) {
+        String copy = new String(s)
+        RefIdentity.markDeInterned(copy)
+        return copy
+    }
+
+    /** What the NoCache transformer emits for Integer.valueOf. */
+    private static Integer boxed(int v) {
+        Integer copy = new Integer(v)
+        RefIdentity.markDeInterned(copy)
+        return copy
+    }
+
+    def "two de-interned copies of one literal are the same instance"() {
+        expect:
+        UtilInstrumented.refEquals(literal("test"), literal("test"))
+        !UtilInstrumented.refEquals(literal("test"), literal("other"))
+    }
+
+    def "a string built with new String is never a literal"() {
+        given:
+        String s1 = new String(literal("test"))
+
+        expect:
+        !UtilInstrumented.refEquals(s1, literal("test"))
+        UtilInstrumented.refEquals(s1, s1)
+    }
+
+    def "new String of an input differs from the input"() {
+        given:
+        String input = new String("fixed".toCharArray())
+        String s1 = new String(input)
+
+        expect:
+        !UtilInstrumented.refEquals(s1, input)
+        UtilInstrumented.refEquals(input, input)
+    }
+
+    def "a pooled string from uninstrumented code equals a literal of its value"() {
+        expect:
+        UtilInstrumented.refEquals(Boolean.toString(true), literal("true"))
+        !UtilInstrumented.refEquals(Boolean.toString(false), literal("true"))
+    }
+
+    def "intern returns the instance a literal of the same value stands for"() {
+        given:
+        String built = new StringBuilder("te").append("st").toString()
+
+        expect:
+        UtilInstrumented.refEquals(UtilInstrumented.intern(built), literal("test"))
+        !UtilInstrumented.refEquals(built, literal("test"))
+    }
+
+    def "boxes share an instance only inside the cache range"() {
+        expect:
+        UtilInstrumented.refEquals(boxed(v), boxed(v)) == shared
+
+        where:
+        v     || shared
+        0     || true
+        127   || true
+        -128  || true
+        128   || false
+        -129  || false
+        1000  || false
+    }
+
+    def "a box is identical to itself outside the cache range"() {
+        given:
+        Integer b = boxed(1000)
+
+        expect:
+        UtilInstrumented.refEquals(b, b)
+    }
+
+    def "boxes created with new are distinct"() {
+        expect:
+        !UtilInstrumented.refEquals(new Integer(5), new Integer(5))
+        !UtilInstrumented.refEquals(new Integer(5), boxed(5))
+        UtilInstrumented.refEquals(Integer.valueOf(5), boxed(5))
+    }
+
+    def "boxes of different types or with null"() {
+        expect:
+        !UtilInstrumented.refEquals(boxed(5), Long.valueOf(5))
+        !UtilInstrumented.refEquals(boxed(5), null)
+        UtilInstrumented.refEquals(null, null)
+        !UtilInstrumented.refEquals(literal("a"), null)
+    }
+
+    def "other objects compare by identity"() {
+        given:
+        Object o = new Object()
+
+        expect:
+        UtilInstrumented.refEquals(o, o)
+        !UtilInstrumented.refEquals(o, new Object())
+    }
+}
diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py
index a6c70f11..ccc4cd07 100644
--- a/symbolic-explorer/driver/SVCompDriver.py
+++ b/symbolic-explorer/driver/SVCompDriver.py
@@ -464,8 +464,8 @@ def run(self):
             logger.warning(f'[SVCOMP] Found uncaught exceptions during symbolic execution')
             verdict = Verdict.UNKNOWN
 
-        if (verdict == Verdict.VIOLATION) and Database.instance().get_tree(ENDPOINT_ID).reference_semantic_change:
-            logger.warning(f'[SVCOMP] Found reference semantic change (user-de-interned strings compared via Objects.equals) - downgrading VIOLATION to UNKNOWN')
+        if (verdict in (Verdict.SAFE, Verdict.VIOLATION)) and Database.instance().get_tree(ENDPOINT_ID).reference_semantic_change:
+            logger.warning(f'[SVCOMP] Found reference semantic change (reference comparison decided by symbolic values SWAT does not encode) - downgrading {verdict.name} to UNKNOWN')
             verdict = Verdict.UNKNOWN
 
         if verdict == Verdict.NO_SYMBOLIC_VARS: