@@ -370,14 +370,12 @@ public class InvariantsExample {
 
 ### Limitations
 
-*   **Unsupported Standard Functions (Uninterpreted Functions):** Not all
-    CEL standard library functions have SMT axioms defined yet. Unsupported
-    functions are treated as *uninterpreted functions* by Z3 (the solver
-    only guarantees that identical inputs yield identical outputs, but does
-    not understand the function's internal logic or return types).
-    Consequently, verifications that rely on the specific semantics of
-    these functions may return `VerificationStatus.INCONCLUSIVE`. Support for
-    more standard library functions will be added incrementally.
+*   **Uninterpreted Functions:** Custom functions, and standard library
+    functions that don't have SMT axioms yet, are treated as uninterpreted:
+    the solver only knows that identical inputs yield identical outputs.
+    Results that depend on their return values are `INCONCLUSIVE`, and a
+    `VERIFIED` result assumes they return a value of their declared type
+    rather than an error.
 
 ### Best Practices & Performance
 
 
@@ -16,6 +16,7 @@
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.ImmutableSortedSet;
 import com.google.common.collect.Iterables;
 import com.google.common.collect.Streams;
 import com.microsoft.z3.ArithExpr;
@@ -83,6 +84,7 @@ final class CelAstToZ3Translator {
   private static final String EMPTY_MSG_REF_PREFIX = "!empty_msg_ref_";
   private static final String EMPTY_LIST_PREFIX = "!empty_list";
   private static final String EMPTY_MAP_PREFIX = "!empty_map";
+  private static final String FUNCTION_PREFIX = "!fn_";
   private static final String NULL_VALUE_FIELD = "null_value";
   private static final String SECONDS_FIELD = "seconds";
   private static final String NANOS_FIELD = "nanos";
@@ -927,21 +929,40 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
               Sort[] argSorts = new Sort[args.size()];
               Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
               FuncDecl<?> funcDecl =
-                  typeSystem.internFuncDecl(functionName, argSorts, typeSystem.celValueSort());
+                  typeSystem.internFuncDecl(
+                      uninterpretedFunctionSymbol(exprId, ast),
+                      argSorts,
+                      typeSystem.celValueSort());
 
               Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
               Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
               typeConstraints.add(createTypeConstraint(callRes, exprId, ast));
               typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
               typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
 
-              boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
-              BoolExpr isApprox = ctx.mkBool(!isDynamic);
+              // The solver picks the result freely, so a model depending on it is never exact.
               return TranslatedValue.propagateStrict(
-                  ctx, typeSystem, functionName, callRes, Optional.of(expr), isApprox, args);
+                  ctx,
+                  typeSystem,
+                  functionName,
+                  callRes,
+                  Optional.of(expr),
+                  /* baseTaint= */ ctx.mkTrue(),
+                  args);
             });
   }
 
+  /**
+   * Returns the Z3 symbol for an uninterpreted call. Each set of candidate overloads gets its own
+   * symbol, since distinct overloads may have different implementations even on equal values (e.g.
+   * empty lists of different element types). The prefix keeps it apart from variables and internal
+   * symbols.
+   */
+  private static String uninterpretedFunctionSymbol(long exprId, CelAbstractSyntaxTree ast) {
+    ImmutableList<String> overloadIds = ast.getReferenceOrThrow(exprId).overloadIds();
+    return FUNCTION_PREFIX + String.join("|", ImmutableSortedSet.copyOf(overloadIds));
+  }
+
   /**
    * Whether a call may construct a container that embeds its args (e.g. list concatenation, map
    * insertion or optional.of). Indexing and conditionals return existing values instead, so
 
@@ -2750,9 +2750,9 @@ public void isAlwaysTrue_operationError_counterexampleFormat() throws Exception
   }
 
   @Test
-  public void isAlwaysTrue_dynamicFunction_nan_violated() throws Exception {
-    // request() == request() is a tautology only if request() does not evaluate to NaN.
-    // Since request() returns DYN, Z3 can assign NaN to its return value, and NaN == NaN is false.
+  public void isAlwaysTrue_dynamicFunction_inconclusive() throws Exception {
+    // request() == request() fails only if request() returns NaN. The solver may pick NaN for an
+    // uninterpreted function, but the actual function may never return it.
     CelCompiler celCompiler =
         CEL.toCompilerBuilder()
             .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))
@@ -2764,8 +2764,26 @@ public void isAlwaysTrue_dynamicFunction_nan_violated() throws Exception {
     CelAbstractSyntaxTree ast = celCompiler.compile("request() == request()").getAst();
     CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
 
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+    assertThat(result.message()).contains("depends on approximations");
+  }
+
+  @Test
+  public void isAlwaysTrue_dynamicFunctionShortCircuited_violated() throws Exception {
+    // x == 0 falsifies the condition regardless of request()'s value.
+    CelCompiler celCompiler =
+        CEL.toCompilerBuilder()
+            .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))
+            .addFunctionDeclarations(
+                CelFunctionDecl.newFunctionDeclaration(
+                    "request",
+                    CelOverloadDecl.newGlobalOverload("request_overload", SimpleType.DYN)))
+            .build();
+    CelAbstractSyntaxTree ast = celCompiler.compile("x != 0 && request() == 1").getAst();
+    CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
+
     assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED);
-    assertThat(result.message()).contains("request = NaN");
+    assertThat(result.message()).contains("x = 0");
   }
 
   @Test
@@ -2785,9 +2803,46 @@ public void isAlwaysTrue_boolFunction_verified() throws Exception {
   }
 
   @Test
-  public void verifyEquivalence_functionError_equivalent() throws Exception {
-    // request() and request() are equivalent, even if request() throws an Error,
-    // because Error == Error structurally in Z3 equivalence.
+  public void isAlwaysTrue_distinctFunctionSymbols_inconclusive(
+      @TestParameter({
+            // Member and global overloads of the same name.
+            "fx(role, country) == role.fx(country)",
+            // Overloads whose argument values coincide (empty lists of different element types).
+            "size(int_list) == 0 && size(string_list) == 0 ? f(int_list) == f(string_list) : true",
+            // A zero-arity function and a variable of the same name.
+            "g() == g"
+          })
+          String expression)
+      throws Exception {
+    CelCompiler celCompiler =
+        CEL.toCompilerBuilder()
+            .addVar("string_list", ListType.create(SimpleType.STRING))
+            .addVar("g", SimpleType.INT)
+            .addFunctionDeclarations(
+                CelFunctionDecl.newFunctionDeclaration(
+                    "fx",
+                    CelOverloadDecl.newGlobalOverload(
+                        "fx_global", SimpleType.BOOL, SimpleType.STRING, SimpleType.STRING),
+                    CelOverloadDecl.newMemberOverload(
+                        "fx_member", SimpleType.BOOL, SimpleType.STRING, SimpleType.STRING)),
+                CelFunctionDecl.newFunctionDeclaration(
+                    "f",
+                    CelOverloadDecl.newGlobalOverload(
+                        "f_list_int", SimpleType.INT, ListType.create(SimpleType.INT)),
+                    CelOverloadDecl.newGlobalOverload(
+                        "f_list_string", SimpleType.INT, ListType.create(SimpleType.STRING))),
+                CelFunctionDecl.newFunctionDeclaration(
+                    "g", CelOverloadDecl.newGlobalOverload("g_zero", SimpleType.INT)))
+            .build();
+    CelAbstractSyntaxTree ast = celCompiler.compile(expression).getAst();
+    CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+  }
+
+  @Test
+  public void verifyEquivalence_identicalFunctionCalls_equivalent() throws Exception {
+    // Identical calls to an uninterpreted function always produce identical results.
     CelCompiler celCompiler =
         CEL.toCompilerBuilder()
             .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))