From 8e1a27e4aa15788cb3294503a3cc78397400440c Mon Sep 17 00:00:00 2001
From: Sean Huh <sokwhan@google.com>
Date: Wed, 21 Oct 2026 17:45:37 -0700
Subject: [PATCH] Cover verifier behavior that no test exercised

PiperOrigin-RevId: 1004364292
---
 .../main/java/dev/cel/verifier/BUILD.bazel    |    9 +-
 .../cel/verifier/CelAstToZ3Translator.java    | 1262 +----------------
 .../dev/cel/verifier/CelVerifierZ3Impl.java   |    4 +-
 .../CelZ3ComprehensionTranslator.java         |  535 +++++++
 .../java/dev/cel/verifier/CelZ3Exprs.java     |  162 +++
 .../cel/verifier/CelZ3OperatorTranslator.java |  139 +-
 .../cel/verifier/CelZ3StructTranslator.java   |  560 ++++++++
 .../cel/verifier/CelZ3TranslationContext.java |  142 ++
 .../CelZ3TypeConstraintGenerator.java         |  231 +++
 .../dev/cel/verifier/CelZ3TypeSystem.java     |  137 +-
 .../dev/cel/verifier/TranslatedValue.java     |   26 +-
 .../cel/verifier/axioms/OptionalAxioms.java   |    7 +-
 .../dev/cel/verifier/axioms/TypeAxiom.java    |    3 +-
 .../verifier/CelPolicyVerifierImplTest.java   |   25 +
 .../cel/verifier/CelVerifierZ3ImplTest.java   |   11 +
 15 files changed, 1792 insertions(+), 1461 deletions(-)
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java

diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
index bd455ab50..6b498a162 100644
--- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
+++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
@@ -112,7 +112,10 @@ java_library(
 
 java_library(
     name = "type_system",
-    srcs = ["CelZ3TypeSystem.java"],
+    srcs = [
+        "CelZ3Exprs.java",
+        "CelZ3TypeSystem.java",
+    ],
     compatible_with = [],
     tags = [
     ],
@@ -157,10 +160,14 @@ java_library(
         "CelAstAlphaHasher.java",
         "CelAstToZ3Translator.java",
         "CelVerifierZ3Impl.java",
+        "CelZ3ComprehensionTranslator.java",
         "CelZ3CounterexampleGenerator.java",
         "CelZ3ExtensionalityAxioms.java",
         "CelZ3FunctionRegistry.java",
         "CelZ3OperatorTranslator.java",
+        "CelZ3StructTranslator.java",
+        "CelZ3TranslationContext.java",
+        "CelZ3TypeConstraintGenerator.java",
         "TranslatedValue.java",
     ],
     compatible_with = [],
diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
index 913582ee4..404ed9900 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
@@ -18,15 +18,11 @@
 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;
 import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.BoolExpr;
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
-import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;
-import com.microsoft.z3.IntExpr;
 import com.microsoft.z3.Quantifier;
 import com.microsoft.z3.SeqExpr;
 import com.microsoft.z3.Sort;
@@ -35,20 +31,11 @@
 import dev.cel.common.ast.CelBlock;
 import dev.cel.common.ast.CelConstant;
 import dev.cel.common.ast.CelExpr;
-import dev.cel.common.ast.CelExpr.CelComprehension;
 import dev.cel.common.ast.CelExpr.CelList;
 import dev.cel.common.ast.CelExpr.ExprKind;
 import dev.cel.common.types.CelKind;
 import dev.cel.common.types.CelType;
 import dev.cel.common.types.CelTypeProvider;
-import dev.cel.common.types.CelTypes;
-import dev.cel.common.types.ListType;
-import dev.cel.common.types.MapType;
-import dev.cel.common.types.NullableType;
-import dev.cel.common.types.OptionalType;
-import dev.cel.common.types.SimpleType;
-import dev.cel.common.types.StructType;
-import dev.cel.common.types.StructTypeReference;
 import dev.cel.common.types.TypeType;
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -58,14 +45,13 @@
 import java.util.Map;
 import java.util.Optional;
 import java.util.Set;
-import java.util.function.Supplier;
 
 /**
  * Internal translator from CEL AST to Z3 SMT expressions using a 4-valued logic tagged union.
  *
  * <p><b>Lifetime & Mutability:</b> This translator is stateful and highly mutable. It accumulates
- * type constraints, loop variables (via its symbol table), and uninterpreted functions (via field
- * caches) during AST traversal.
+ * constraints and symbol bindings in a shared {@link CelZ3TranslationContext}, and literal caches
+ * in itself and its delegate translators.
  *
  * <ul>
  *   <li>It is <b>not thread-safe</b>.
@@ -80,39 +66,26 @@
 final class CelAstToZ3Translator {
   private static final String MAP_REF_PREFIX = "!mapRef_";
   private static final String LIST_REF_PREFIX = "!listRef_";
-  private static final String MSG_REF_PREFIX = "!msg_ref";
-  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";
-  private static final long MAX_UINT32 = 0xFFFFFFFFL;
   private final Context ctx;
   private final CelZ3TypeSystem typeSystem;
+  private final CelZ3TranslationContext context;
+  private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
   private final CelZ3OperatorTranslator operatorTranslator;
-  private final Map<String, TranslatedValue> symbolTable;
-  private final Set<BoolExpr> typeConstraints;
-  private final Map<Expr<?>, CelType> inputVariableTypes;
+  private final CelZ3ComprehensionTranslator comprehensionTranslator;
+  private final CelZ3StructTranslator structTranslator;
   private final ImmutableSet<String> unknownIdentifiers;
-  private final int comprehensionUnrollLimit;
-  private final CelTypeProvider typeProvider;
-  private final List<BoolExpr> truncationConditions;
-  private final Map<String, Expr<?>> emptyMessageCache;
   private final Map<Object, Expr<?>> listLiteralCache;
-  private Expr<?> emptyListCache;
-  private Expr<?> emptyMapCache;
 
   /**
    * Returns a set of Z3 boolean expressions representing type constraints for the translated AST.
    */
   Set<BoolExpr> getTypeConstraints() {
-    return typeConstraints;
+    return context.constraints();
   }
 
   BoolExpr hasTruncation() {
-    return CelZ3TypeSystem.mkOrFlattened(ctx, truncationConditions);
+    return context.hasTruncation();
   }
 
   CelZ3TypeSystem getTypeSystem() {
@@ -131,7 +104,7 @@ BoolExpr isTrue(Expr<?> celValue) {
    * reserved policy symbols such as 'rule.result' to the composed policy graph.
    */
   void bindSymbol(String varName, TranslatedValue value) {
-    symbolTable.put(varName, value);
+    context.bindSymbol(varName, value);
   }
 
   TranslatedValue translate(CelAbstractSyntaxTree ast) {
@@ -148,13 +121,13 @@ TranslatedValue translate(CelAbstractSyntaxTree ast) {
     Set<Expr<?>> mapRefs = new LinkedHashSet<>();
     Set<Expr<?>> msgRefs = new LinkedHashSet<>();
 
-    for (Expr<?> constraint : typeConstraints) {
+    for (Expr<?> constraint : context.constraints()) {
       collectReferences(constraint, visited, listRefs, mapRefs, msgRefs);
     }
     collectReferences(result.z3Expr(), visited, listRefs, mapRefs, msgRefs);
 
-    this.typeConstraints.addAll(
-        CelZ3ExtensionalityAxioms.generateAxioms(ctx, typeSystem, listRefs, mapRefs, msgRefs));
+    CelZ3ExtensionalityAxioms.generateAxioms(ctx, typeSystem, listRefs, mapRefs, msgRefs)
+        .forEach(context::addConstraint);
 
     return result;
   }
@@ -195,7 +168,7 @@ private TranslatedValue translateExpr(CelExpr celExpr, CelAbstractSyntaxTree ast
       case IDENT:
         return translateIdent(celExpr, ast);
       case SELECT:
-        return translateSelect(celExpr, ast);
+        return structTranslator.translateSelect(celExpr, ast);
       case CALL:
         return translateCall(celExpr, ast);
       case LIST:
@@ -203,9 +176,9 @@ private TranslatedValue translateExpr(CelExpr celExpr, CelAbstractSyntaxTree ast
       case MAP:
         return translateMap(celExpr, ast);
       case STRUCT:
-        return translateStruct(celExpr, ast);
+        return structTranslator.translateStruct(celExpr, ast);
       case COMPREHENSION:
-        return translateComprehension(celExpr, ast);
+        return comprehensionTranslator.translateComprehension(celExpr, ast);
       default:
         throw new IllegalArgumentException("Unsupported expression kind: " + kind);
     }
@@ -255,22 +228,22 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as
       }
     }
     TranslatedValue tv =
-        symbolTable.computeIfAbsent(
+        context.computeSymbolIfAbsent(
             name,
             n -> {
               Expr<?> v = ctx.mkConst(n, typeSystem.celValueSort());
-              inputVariableTypes.put(v, type);
+              context.addInputVariable(v, type);
 
               // Variables at rest can never be pre-cooked Errors
               // Basically prevents error being a counterexample of var == var
-              typeConstraints.add(ctx.mkNot(typeSystem.isError(v)));
+              context.addConstraint(ctx.mkNot(typeSystem.isError(v)));
 
-              BoolExpr constraint = createTypeConstraint(v, exprId, ast);
+              BoolExpr constraint = typeConstraintGenerator.createTypeConstraint(v, exprId, ast);
               if (unknownIdentifiers.contains(name)) {
-                typeConstraints.add(ctx.mkOr(typeSystem.isUnknown(v), constraint));
+                context.addConstraint(ctx.mkOr(typeSystem.isUnknown(v), constraint));
               } else {
-                typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(v)));
-                typeConstraints.add(constraint);
+                context.addConstraint(ctx.mkNot(typeSystem.isUnknown(v)));
+                context.addConstraint(constraint);
               }
 
               return TranslatedValue.create(
@@ -324,7 +297,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
         elementsTv.add(elem);
       }
       listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX);
-      typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq));
+      context.addConstraint(ctx.mkEq(typeSystem.getSeq(listRef), seq));
       propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values);
       Expr<?> finalListRef = listRef;
       cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef));
@@ -379,9 +352,9 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
               ctx.mkITE(finalPresence, ctx.mkStore(mapPresence, key, ctx.mkTrue()), mapPresence);
     }
 
-    typeConstraints.add(ctx.mkEq(typeSystem.getMapValues(mapRef), mapValues));
-    typeConstraints.add(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence));
-    typeConstraints.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq));
+    context.addConstraint(ctx.mkEq(typeSystem.getMapValues(mapRef), mapValues));
+    context.addConstraint(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence));
+    context.addConstraint(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq));
 
     Expr<?> result = typeSystem.wrapMap(mapRef);
     propagateTruncatedTypeConstraint(result, values);
@@ -398,490 +371,11 @@ private void propagateTruncatedTypeConstraint(Expr<?> container, Iterable<Expr<?
             typeSystem.isErrorOrUnknown(container),
             typeSystem.hasTruncatedTypeConstraint(container));
     for (Expr<?> element : elements) {
-      typeConstraints.add(
+      context.addConstraint(
           ctx.mkImplies(typeSystem.hasTruncatedTypeConstraint(element), hasTruncated));
     }
   }
 
-  private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
-    CelExpr.CelStruct createStruct = celExpr.struct();
-    if (isJsonWkt(createStruct.messageName())) {
-      return translateJsonWktStruct(celExpr, createStruct, ast);
-    }
-    if (CelTypes.isWrapperType(createStruct.messageName())) {
-      return translateWrapperWktStruct(celExpr, createStruct, ast);
-    }
-    if (createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE)) {
-      return translateTimestampWktStruct(celExpr, createStruct, ast);
-    }
-    if (createStruct.messageName().equals(CelTypes.DURATION_MESSAGE)) {
-      return translateDurationWktStruct(celExpr, createStruct, ast);
-    }
-
-    // Bypass SMT when the struct is empty (return the cached SMT default pointer)
-    if (createStruct.entries().isEmpty()) {
-      return TranslatedValue.create(
-          getDefaultValueForType(StructTypeReference.create(createStruct.messageName())),
-          celExpr,
-          typeSystem,
-          ctx.mkFalse());
-    }
-
-    Expr<?> msgRef = typeSystem.mkMessageRefConst(MSG_REF_PREFIX);
-
-    // Initialize the values array with Unknown. Missing fields and explicit primitive defaults
-    // will both bypass the store and fall back to this Unknown base. However, their msgPresence
-    // will evaluate to false, allowing translateSelect to properly return the default value.
-    ArrayExpr msgValues = ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown());
-    ArrayExpr msgPresence = ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse());
-
-    List<TranslatedValue> elementsTv = new ArrayList<>();
-
-    for (CelExpr.CelStruct.Entry entryAst : createStruct.entries()) {
-      Expr<?> key = ctx.mkString(entryAst.fieldKey());
-      TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
-      Expr<?> value = valueTv.z3Expr();
-
-      CelType fieldType =
-          typeProvider
-              .findType(createStruct.messageName())
-              .filter(t -> t instanceof StructType)
-              .map(t -> (StructType) t)
-              .flatMap(t -> t.findField(entryAst.fieldKey()))
-              .map(StructType.Field::type)
-              .orElseGet(() -> extractAstTypeOrDefault(ast, entryAst.value().id()));
-      Expr<?> defaultVal = getDefaultValueForType(fieldType);
-
-      Expr<?> finalValue = value;
-      BoolExpr optionalHasValue = ctx.mkTrue();
-      if (entryAst.optionalEntry()) {
-        Expr<?> checkedValue =
-            typeSystem.withRuntimeError(value, ctx.mkNot(typeSystem.isOptional(value)));
-        valueTv =
-            TranslatedValue.create(
-                checkedValue, entryAst.value(), typeSystem, valueTv.isApproximate());
-        Expr<?> optRef = typeSystem.getOptionalRef(checkedValue);
-        optionalHasValue = typeSystem.optHasValue(optRef);
-        finalValue = typeSystem.getOptionalValue(optRef);
-      }
-      elementsTv.add(valueTv);
-
-      // Canonicalization Trick:
-      //
-      // We avoid storing explicit default values (e.g. `single_int32: 0`)
-      // in `msgValues`, leaving them as `Unknown` (identical to missing fields).
-      // This structurally aligns defaults with missing fields, allowing Z3's native array equality
-      // (`msg1 == msg2`) to work without using quantifiers (which avoids MBQI loops).
-      // Because proto3 singular primitives do not have field presence, we also skip setting
-      // `msgPresence`.
-      BoolExpr isDefaultPrimitive =
-          fieldType.kind().isPrimitive() ? ctx.mkEq(finalValue, defaultVal) : ctx.mkFalse();
-
-      BoolExpr shouldBypass = ctx.mkOr(ctx.mkNot(optionalHasValue), isDefaultPrimitive);
-
-      msgValues =
-          (ArrayExpr) ctx.mkITE(shouldBypass, msgValues, ctx.mkStore(msgValues, key, finalValue));
-
-      msgPresence =
-          (ArrayExpr)
-              ctx.mkITE(shouldBypass, msgPresence, ctx.mkStore(msgPresence, key, ctx.mkTrue()));
-    }
-
-    typeConstraints.add(
-        ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString(createStruct.messageName())));
-    typeConstraints.add(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues));
-    typeConstraints.add(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence));
-
-    Expr<?> result = typeSystem.wrapMessage(msgRef);
-    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
-  }
-
-  private static boolean isJsonWkt(String messageName) {
-    return messageName.equals(CelTypes.VALUE_MESSAGE)
-        || messageName.equals(CelTypes.LIST_VALUE_MESSAGE)
-        || messageName.equals(CelTypes.STRUCT_MESSAGE);
-  }
-
-  // Concretize JSON WKT unwrapping directly into native Z3 primitives to avoid
-  // sort incompatibilities (Message == String) and solver performance penalties (quantifiers).
-  private TranslatedValue translateJsonWktStruct(
-      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
-    Expr<?> fallback;
-    if (createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)) {
-      fallback = typeSystem.mkNull();
-    } else if (createStruct.messageName().equals(CelTypes.LIST_VALUE_MESSAGE)) {
-      fallback = getDefaultValueForType(ListType.create(SimpleType.DYN));
-    } else {
-      fallback = getDefaultValueForType(MapType.create(SimpleType.STRING, SimpleType.DYN));
-    }
-
-    if (createStruct.entries().isEmpty()) {
-      return TranslatedValue.create(fallback, celExpr, typeSystem, ctx.mkFalse());
-    }
-
-    // JSON WKT messages (gp.Struct, gp.Value, gp.ListValue) can only have a single top-level
-    // field entry in non-empty creation literals (e.g., 'fields' for Struct, 'values' for
-    // ListValue, or a single 'oneof' field for Value).
-    CelExpr.CelStruct.Entry entry = Iterables.getOnlyElement(createStruct.entries());
-
-    // Translate the value to properly capture approximations and Optionals
-    TranslatedValue entryTv = translateExpr(entry.value(), ast);
-    Expr<?> finalVal = entryTv.z3Expr();
-
-    boolean isNullValueField =
-        createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)
-            && entry.fieldKey().equals(NULL_VALUE_FIELD);
-
-    if (entry.optionalEntry()) {
-      Expr<?> checkedVal =
-          typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal)));
-      entryTv =
-          TranslatedValue.create(
-              checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
-      Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
-      BoolExpr hasValue = typeSystem.optHasValue(optRef);
-
-      Expr<?> unpackedVal = typeSystem.getOptionalValue(optRef);
-      if (isNullValueField) {
-        unpackedVal = typeSystem.mkNull();
-      }
-      finalVal = ctx.mkITE(hasValue, unpackedVal, fallback);
-    } else if (isNullValueField) {
-      finalVal = typeSystem.mkNull();
-    }
-
-    return TranslatedValue.propagateStrict(
-        ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
-  }
-
-  private TranslatedValue translateWrapperWktStruct(
-      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
-    String typeName = createStruct.messageName();
-    CelType wrapperType =
-        CelTypes.getWellKnownCelType(typeName)
-            .orElseThrow(
-                () -> new IllegalArgumentException("Unexpected wrapper type: " + typeName));
-    CelType targetType = ((NullableType) wrapperType).targetType();
-    Expr<?> currentVal = getDefaultValueForType(targetType);
-
-    List<TranslatedValue> entryTvs = new ArrayList<>();
-    for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
-      TranslatedValue entryTv = translateExpr(entry.value(), ast);
-      Expr<?> val = entryTv.z3Expr();
-      if (entry.optionalEntry()) {
-        Expr<?> checkedVal =
-            typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
-        entryTv =
-            TranslatedValue.create(
-                checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
-        Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
-        BoolExpr hasValue = typeSystem.optHasValue(optRef);
-        currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal);
-      } else {
-        currentVal = val;
-      }
-      entryTvs.add(entryTv);
-    }
-    BoolExpr validValue = createTypeConstraintForType(currentVal, targetType);
-    if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) {
-      IntExpr intVal = typeSystem.getInt(currentVal);
-      validValue =
-          ctx.mkAnd(
-              validValue,
-              ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)),
-              ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE)));
-    } else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) {
-      IntExpr uintVal = typeSystem.getUint(currentVal);
-      validValue =
-          ctx.mkAnd(
-              validValue,
-              ctx.mkGe(uintVal, ctx.mkInt(0)),
-              ctx.mkLe(uintVal, ctx.mkInt(MAX_UINT32)));
-    } else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) {
-      FPExpr doubleVal = typeSystem.getDouble(currentVal);
-      FPExpr narrowedFloat =
-          ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), doubleVal, ctx.mkFPSortSingle());
-      FPExpr widenedDouble =
-          ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), narrowedFloat, ctx.mkFPSortDouble());
-      currentVal = typeSystem.wrapDouble(widenedDouble);
-    }
-    currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue));
-    return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
-  }
-
-  @FunctionalInterface
-  private interface TimeWktValueFactory {
-    Expr<?> create(IntExpr seconds, IntExpr nanos, IntExpr totalNanos);
-  }
-
-  private TranslatedValue translateTimestampWktStruct(
-      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
-    return translateTimeWktStruct(
-        celExpr,
-        createStruct,
-        ast,
-        /* minNanos= */ 0,
-        (seconds, nanos, totalNanos) ->
-            typeSystem.withRuntimeError(
-                typeSystem.wrapTimestamp(totalNanos),
-                typeSystem.checkTimestampOverflow(totalNanos)));
-  }
-
-  private TranslatedValue translateDurationWktStruct(
-      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
-    return translateTimeWktStruct(
-        celExpr,
-        createStruct,
-        ast,
-        CelZ3TypeSystem.MIN_DURATION_NANOS,
-        (seconds, nanos, totalNanos) -> {
-          BoolExpr signMismatch =
-              ctx.mkOr(
-                  ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
-                  ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
-          return typeSystem.withRuntimeError(
-              typeSystem.wrapDuration(totalNanos),
-              signMismatch,
-              typeSystem.checkDurationOverflow(totalNanos));
-        });
-  }
-
-  private TranslatedValue translateTimeWktStruct(
-      CelExpr celExpr,
-      CelExpr.CelStruct createStruct,
-      CelAbstractSyntaxTree ast,
-      int minNanos,
-      TimeWktValueFactory valueFactory) {
-    List<TranslatedValue> entryTvs = new ArrayList<>();
-    Expr<?> secondsVal =
-        resolveStructFieldValue(createStruct, SECONDS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
-    Expr<?> nanosVal =
-        resolveStructFieldValue(createStruct, NANOS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
-
-    IntExpr seconds = typeSystem.getInt(secondsVal);
-    IntExpr nanos = typeSystem.getInt(nanosVal);
-    IntExpr totalNanos =
-        (IntExpr)
-            ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos);
-
-    BoolExpr typeError =
-        ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal)));
-    BoolExpr nanosOutOfRange =
-        ctx.mkOr(
-            ctx.mkLt(nanos, ctx.mkInt(minNanos)),
-            ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
-
-    Expr<?> result =
-        typeSystem.withRuntimeError(
-            valueFactory.create(seconds, nanos, totalNanos), typeError, nanosOutOfRange);
-    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
-  }
-
-  private Expr<?> resolveStructFieldValue(
-      CelExpr.CelStruct createStruct,
-      String fieldName,
-      Expr<?> defaultValue,
-      CelAbstractSyntaxTree ast,
-      List<TranslatedValue> entryTvs) {
-    return Streams.findLast(
-            createStruct.entries().stream().filter(entry -> entry.fieldKey().equals(fieldName)))
-        .<Expr<?>>map(
-            entry -> {
-              TranslatedValue entryTv = translateExpr(entry.value(), ast);
-              Expr<?> val = entryTv.z3Expr();
-              if (entry.optionalEntry()) {
-                Expr<?> checkedVal =
-                    typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
-                entryTv =
-                    TranslatedValue.create(
-                        checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
-                Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
-                val =
-                    ctx.mkITE(
-                        typeSystem.optHasValue(optRef),
-                        typeSystem.getOptionalValue(optRef),
-                        defaultValue);
-              }
-              entryTvs.add(entryTv);
-              return val;
-            })
-        .orElse(defaultValue);
-  }
-
-  private Expr<?> getDefaultValueForType(CelType type) {
-    if (type instanceof NullableType) {
-      return typeSystem.mkNull();
-    }
-    if (type instanceof OptionalType) {
-      return typeSystem.mkOptionalNone();
-    }
-    if (type.equals(SimpleType.INT)) {
-      return typeSystem.mkInt(0);
-    }
-    if (type.equals(SimpleType.BOOL)) {
-      return typeSystem.wrapBool(ctx.mkFalse());
-    }
-    if (type.equals(SimpleType.STRING)) {
-      return typeSystem.mkString("");
-    }
-    if (type.equals(SimpleType.BYTES)) {
-      return typeSystem.mkBytes("");
-    }
-    if (type.equals(SimpleType.DOUBLE)) {
-      return typeSystem.mkDouble(0.0);
-    }
-    if (type.equals(SimpleType.UINT)) {
-      return typeSystem.mkUint(0);
-    }
-    if (type.equals(SimpleType.TIMESTAMP)) {
-      return typeSystem.wrapTimestamp(ctx.mkInt(0));
-    }
-    if (type.equals(SimpleType.DURATION)) {
-      return typeSystem.wrapDuration(ctx.mkInt(0));
-    }
-    if (type instanceof ListType) {
-      if (emptyListCache == null) {
-        emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX);
-        typeConstraints.add(
-            ctx.mkEq(
-                typeSystem.getSeq(emptyListCache),
-                ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()))));
-      }
-      return typeSystem.wrapList(emptyListCache);
-    }
-    if (type instanceof MapType) {
-      if (emptyMapCache == null) {
-        emptyMapCache = typeSystem.mkMapRefConst(EMPTY_MAP_PREFIX);
-        typeConstraints.add(
-            ctx.mkEq(
-                typeSystem.getMapPresence(emptyMapCache),
-                ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse())));
-        typeConstraints.add(
-            ctx.mkEq(
-                typeSystem.getMapValues(emptyMapCache),
-                ctx.mkConstArray(typeSystem.celValueSort(), typeSystem.mkUnknown())));
-        typeConstraints.add(
-            ctx.mkEq(
-                typeSystem.getMapKeys(emptyMapCache),
-                ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()))));
-      }
-      return typeSystem.wrapMap(emptyMapCache);
-    }
-    if (type.kind() == CelKind.STRUCT) {
-      String messageName = type.name();
-      Expr<?> msgRef =
-          emptyMessageCache.computeIfAbsent(
-              messageName,
-              name -> {
-                Expr<?> ref = typeSystem.mkMessageRefConst(EMPTY_MSG_REF_PREFIX + name);
-                typeConstraints.add(
-                    ctx.mkEq(
-                        typeSystem.getMsgPresence(ref),
-                        ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse())));
-                typeConstraints.add(
-                    ctx.mkEq(
-                        typeSystem.getMsgValues(ref),
-                        ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown())));
-                typeConstraints.add(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name)));
-                return ref;
-              });
-      return typeSystem.wrapMessage(msgRef);
-    }
-    return typeSystem.mkUnknown();
-  }
-
-  private static final class FieldAccess {
-    private final BoolExpr presence;
-    private final Expr<?> value;
-
-    private FieldAccess(BoolExpr presence, Expr<?> value) {
-      this.presence = presence;
-      this.value = value;
-    }
-  }
-
-  private FieldAccess getMapAccess(Expr<?> operand, String field, BoolExpr typeGuard) {
-    Expr<?> mapRef = typeSystem.getMapRef(operand);
-    Expr<?> mapFieldZ3Str = typeSystem.mkString(field);
-    BoolExpr presence =
-        (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str);
-    Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str);
-    constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value);
-    return new FieldAccess(presence, value);
-  }
-
-  private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGuard) {
-    Expr<?> msgRef = typeSystem.getMessageRef(operand);
-    Expr<?> msgFieldZ3Str = ctx.mkString(field);
-    BoolExpr presence =
-        (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str);
-    Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str);
-    constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value);
-    return new FieldAccess(presence, value);
-  }
-
-  private void constrainPresentValue(BoolExpr guard, Expr<?> value) {
-    typeConstraints.add(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value))));
-  }
-
-  private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
-    CelExpr.CelSelect select = celExpr.select();
-    long exprId = celExpr.id();
-    TranslatedValue operandTv = translateExpr(select.operand(), ast);
-    Expr<?> operand = operandTv.z3Expr();
-    String field = select.field();
-    CelType operandType = extractAstTypeOrDefault(ast, select.operand().id());
-
-    Expr<?> presenceResult;
-    Expr<?> valueResult;
-
-    if (operandType instanceof MapType) {
-      FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue());
-      presenceResult = mapAcc.presence;
-      valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
-    } else if (operandType.kind() == CelKind.STRUCT) {
-      FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue());
-      presenceResult = msgAcc.presence;
-      Expr<?> defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
-      valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
-    } else {
-      // Dynamic type: generate the full SMT decision tree
-      BoolExpr isMap = typeSystem.isMap(operand);
-      BoolExpr isMessage = typeSystem.isMessage(operand);
-
-      FieldAccess mapAcc = getMapAccess(operand, field, isMap);
-      FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
-
-      presenceResult =
-          CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
-              .addCase(isMessage, msgAcc.presence)
-              .addCase(isMap, mapAcc.presence)
-              .build(ctx.mkFalse());
-
-      Expr<?> defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
-      Expr<?> msgRead = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
-      Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
-
-      valueResult =
-          CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
-              .addCase(isMessage, msgRead)
-              .addCase(isMap, mapRead)
-              .build(typeSystem.mkError());
-    }
-
-    Expr<?> fieldAccess = select.testOnly() ? typeSystem.wrapBool(presenceResult) : valueResult;
-
-    typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast));
-
-    TranslatedValue result =
-        TranslatedValue.propagateStrict(
-            ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv));
-    // Map presence is only linked to the keys up to the unroll limit.
-    return operandType.kind() == CelKind.STRUCT
-        ? result
-        : result.withApproximation(operatorTranslator.isTruncatedMap(operand));
-  }
-
   private TranslatedValue translateBlock(
       List<CelExpr> boundExprs, int currentIndex, CelExpr resultExpr, CelAbstractSyntaxTree ast) {
     if (currentIndex >= boundExprs.size()) {
@@ -892,7 +386,7 @@ private TranslatedValue translateBlock(
     TranslatedValue subExprVal = translateExpr(subExprAst, ast);
     String varName = CelBlock.INDEX_PREFIX + currentIndex;
 
-    return withScope(
+    return context.withScope(
         varName, subExprVal, () -> translateBlock(boundExprs, currentIndex + 1, resultExpr, ast));
   }
 
@@ -936,9 +430,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
 
               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)));
+              context.addConstraint(
+                  typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast));
+              context.addConstraint(ctx.mkNot(typeSystem.isUnknown(callRes)));
+              context.addConstraint(ctx.mkNot(typeSystem.isError(callRes)));
 
               // The solver picks the result freely, so a model depending on it is never exact.
               return TranslatedValue.propagateStrict(
@@ -976,666 +471,6 @@ private static boolean mayEmbedArgs(String functionName, CelType resultType) {
         && !functionName.equals(Operator.CONDITIONAL.getFunction());
   }
 
-  private <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
-    TranslatedValue prev = symbolTable.put(varName, value);
-    try {
-      return action.get();
-    } finally {
-      if (prev != null) {
-        symbolTable.put(varName, prev);
-      } else {
-        symbolTable.remove(varName);
-      }
-    }
-  }
-
-  private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSyntaxTree ast) {
-    CelComprehension comp = celExpr.comprehension();
-    CelExpr iterRangeExpr = comp.iterRange();
-    if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.IDENT) {
-      TranslatedValue boundTv = symbolTable.get(iterRangeExpr.ident().name());
-      if (boundTv != null) {
-        iterRangeExpr = boundTv.celExpr().orElse(iterRangeExpr);
-      }
-    }
-    List<IterationElement> iterationElements = new ArrayList<>();
-    List<BoolExpr> taints = new ArrayList<>();
-    List<Expr<?>> allRangeElems = new ArrayList<>();
-
-    // For statically known list/map literals, unroll them exactly.
-    if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.LIST
-        && iterRangeExpr.list().optionalIndices().isEmpty()) {
-      ImmutableList<CelExpr> elements = iterRangeExpr.list().elements();
-      for (int i = 0; i < elements.size(); i++) {
-        TranslatedValue valueTv = translateExpr(elements.get(i), ast);
-        Expr<?> value = valueTv.z3Expr();
-        taints.add(valueTv.isApproximate());
-        iterationElements.add(new IterationElement(typeSystem.mkInt(i), value));
-        allRangeElems.add(value);
-      }
-    } else if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP
-        && iterRangeExpr.map().entries().stream().noneMatch(CelExpr.CelMap.Entry::optionalEntry)) {
-      for (CelExpr.CelMap.Entry entry : iterRangeExpr.map().entries()) {
-        TranslatedValue keyTv = translateExpr(entry.key(), ast);
-        Expr<?> key = keyTv.z3Expr();
-        taints.add(keyTv.isApproximate());
-        TranslatedValue valueTv = translateExpr(entry.value(), ast);
-        Expr<?> value = valueTv.z3Expr();
-        taints.add(valueTv.isApproximate());
-        iterationElements.add(new IterationElement(key, value));
-        allRangeElems.add(key);
-        allRangeElems.add(value);
-      }
-    } else {
-      return translateDynamicComprehension(celExpr, ast);
-    }
-
-    TranslatedValue accuTv = translateExpr(comp.accuInit(), ast);
-    Expr<?> accu = accuTv.z3Expr();
-    taints.add(accuTv.isApproximate());
-    boolean isMap = iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP;
-    boolean isTwoVar = !comp.iterVar2().isEmpty();
-
-    for (IterationElement iterElem : iterationElements) {
-      Expr<?> currentAccu = accu;
-      accu =
-          withIterationScope(
-              comp,
-              iterElem.keyOrIndex,
-              iterElem.value,
-              currentAccu,
-              isMap,
-              isTwoVar,
-              () -> {
-                TranslatedValue condTv = translateExpr(comp.loopCondition(), ast);
-                TranslatedValue stepTv = translateExpr(comp.loopStep(), ast);
-                taints.add(stepTv.isApproximate());
-                return ctx.mkITE(
-                    (BoolExpr) typeSystem.unwrapBool(condTv.z3Expr()),
-                    stepTv.z3Expr(),
-                    currentAccu);
-              });
-    }
-
-    TranslatedValue resultTv =
-        withScope(
-            comp.accuVar(),
-            TranslatedValue.create(accu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)),
-            () -> translateExpr(comp.result(), ast));
-    Expr<?> result = resultTv.z3Expr();
-    return TranslatedValue.create(
-        typeSystem.propagateErrorAndUnknown(
-            "comprehension",
-            result,
-            allRangeElems,
-            ImmutableList.<Expr<?>>builder().add(result).addAll(allRangeElems).build()),
-        celExpr,
-        typeSystem,
-        resultTv.isApproximate());
-  }
-
-  private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) {
-    return ast.getType(id).orElse(SimpleType.DYN);
-  }
-
-  private static final class BoundedIteration {
-    private final BoolExpr inBounds;
-    private final TranslatedValue stepResult;
-
-    private BoundedIteration(BoolExpr inBounds, TranslatedValue stepResult) {
-      this.inBounds = inBounds;
-      this.stepResult = stepResult;
-    }
-  }
-
-  private TranslatedValue translateDynamicComprehension(
-      CelExpr celExpr, CelAbstractSyntaxTree ast) {
-    CelComprehension comp = celExpr.comprehension();
-    TranslatedValue iterRangeTv = translateExpr(comp.iterRange(), ast);
-    Expr<?> iterRange = iterRangeTv.z3Expr();
-    CelType rangeType = extractAstTypeOrDefault(ast, comp.iterRange().id());
-
-    boolean isList = rangeType instanceof ListType;
-    boolean isMap = rangeType instanceof MapType;
-    if (!isList && !isMap) {
-      BoolExpr isRuntimeListOrMap =
-          ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange));
-      Expr<?> result =
-          ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError());
-      return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap);
-    }
-
-    SeqExpr<?> seq =
-        isMap
-            ? typeSystem.getMapKeys(typeSystem.getMapRef(iterRange))
-            : typeSystem.getSeq(typeSystem.getListRef(iterRange));
-
-    ArithExpr lengthExpr = ctx.mkLength(seq);
-    ArrayExpr mapPresence =
-        isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null;
-
-    BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange);
-    BoolExpr isTruncated =
-        ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)));
-    truncationConditions.add(isTruncated);
-
-    if (isAllMacro(comp) || isExistsMacro(comp)) {
-      return unrollAllAndExists(
-          celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
-    } else {
-      return unrollMapAndFilter(
-          celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
-    }
-  }
-
-  private BoolExpr getBoundedMapBijection(
-      ArrayExpr mapPresence, SeqExpr<?> seq, ArithExpr lengthExpr) {
-    List<BoolExpr> constraints = new ArrayList<>();
-    for (int i = 0; i < comprehensionUnrollLimit; i++) {
-      for (int j = i + 1; j < comprehensionUnrollLimit; j++) {
-        BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr);
-        BoolExpr notEqual =
-            ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j))));
-        constraints.add(ctx.mkImplies(validPair, notEqual));
-      }
-    }
-
-    BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
-
-    ArrayExpr seqMap = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse());
-    for (int i = 0; i < comprehensionUnrollLimit; i++) {
-      seqMap =
-          (ArrayExpr)
-              ctx.mkITE(
-                  ctx.mkLt(ctx.mkInt(i), lengthExpr),
-                  ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
-                  seqMap);
-    }
-    constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
-    return CelZ3TypeSystem.mkAndFlattened(ctx, constraints);
-  }
-
-  private <T> T withIterationScope(
-      CelComprehension comp,
-      Expr<?> keyOrIndex,
-      Expr<?> value,
-      Expr<?> currentAccu,
-      boolean isMap,
-      boolean isTwoVar,
-      Supplier<T> action) {
-    Supplier<T> bindAccu =
-        () ->
-            withScope(
-                comp.accuVar(),
-                TranslatedValue.create(currentAccu, typeSystem, ctx.mkFalse()),
-                action);
-
-    if (isTwoVar) {
-      return withScope(
-          comp.iterVar(),
-          TranslatedValue.create(keyOrIndex, typeSystem, ctx.mkFalse()),
-          () ->
-              withScope(
-                  comp.iterVar2(),
-                  TranslatedValue.create(value, typeSystem, ctx.mkFalse()),
-                  bindAccu));
-    } else {
-      Expr<?> iterVal = isMap ? keyOrIndex : value;
-      return withScope(
-          comp.iterVar(), TranslatedValue.create(iterVal, typeSystem, ctx.mkFalse()), bindAccu);
-    }
-  }
-
-  private IterationElement getIterationElement(
-      Expr<?> xVal, IntExpr idx, Expr<?> iterRange, boolean isMap, boolean isTwoVar) {
-    Expr<?> keyOrIndex;
-    Expr<?> value;
-
-    if (isMap) {
-      keyOrIndex = xVal;
-      if (isTwoVar) {
-        Expr<?> mapRef = typeSystem.getMapRef(iterRange);
-        ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
-        value = ctx.mkSelect(mapValues, keyOrIndex);
-      } else {
-        value = null;
-      }
-    } else {
-      if (isTwoVar) {
-        keyOrIndex = typeSystem.wrapInt(idx);
-        value = xVal;
-      } else {
-        keyOrIndex = null;
-        value = xVal;
-      }
-    }
-    return new IterationElement(keyOrIndex, value);
-  }
-
-  private TranslatedValue unrollAllAndExists(
-      CelExpr celExpr,
-      CelAbstractSyntaxTree ast,
-      SeqExpr<?> seq,
-      ArithExpr lengthExpr,
-      ArrayExpr mapPresence,
-      BoolExpr isTruncated,
-      TranslatedValue iterRangeTv) {
-    CelComprehension comp = celExpr.comprehension();
-    List<BoundedIteration> iterations = new ArrayList<>();
-    TranslatedValue accuInitTv = translateExpr(comp.accuInit(), ast);
-    Expr<?> accuInitExpr = accuInitTv.z3Expr();
-
-    boolean isMap = mapPresence != null;
-    boolean isTwoVar = !comp.iterVar2().isEmpty();
-
-    for (int i = 0; i < comprehensionUnrollLimit; i++) {
-      IntExpr idx = ctx.mkInt(i);
-      BoolExpr inBounds = ctx.mkLt(idx, lengthExpr);
-      Expr<?> xVal = ctx.mkNth(seq, idx);
-
-      constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence);
-
-      IterationElement iterElem =
-          getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar);
-
-      TranslatedValue stepTv =
-          withIterationScope(
-              comp,
-              iterElem.keyOrIndex,
-              iterElem.value,
-              accuInitExpr,
-              isMap,
-              isTwoVar,
-              () -> translateExpr(comp.loopStep(), ast));
-      iterations.add(new BoundedIteration(inBounds, stepTv));
-    }
-
-    return reduceAllOrExists(iterations, isTruncated, iterRangeTv, isAllMacro(comp), celExpr, ast);
-  }
-
-  private TranslatedValue unrollMapAndFilter(
-      CelExpr celExpr,
-      CelAbstractSyntaxTree ast,
-      SeqExpr<?> seq,
-      ArithExpr lengthExpr,
-      ArrayExpr mapPresence,
-      BoolExpr isTruncated,
-      TranslatedValue iterRangeTv) {
-    CelComprehension comp = celExpr.comprehension();
-    // For macros like map and filter, we must sequentially thread the accumulator through the loop
-    TranslatedValue chainedAccuTv = translateExpr(comp.accuInit(), ast);
-    Expr<?> chainedAccu = chainedAccuTv.z3Expr();
-
-    boolean isMap = mapPresence != null;
-    boolean isTwoVar = !comp.iterVar2().isEmpty();
-
-    List<BoolExpr> taints = new ArrayList<>();
-    taints.add(chainedAccuTv.isApproximate());
-    taints.add(iterRangeTv.isApproximate());
-
-    for (int i = 0; i < comprehensionUnrollLimit; i++) {
-      IntExpr idx = ctx.mkInt(i);
-      BoolExpr inBounds = ctx.mkLt(idx, lengthExpr);
-      Expr<?> xVal = ctx.mkNth(seq, idx);
-
-      constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence);
-
-      Expr<?> currentAccu = chainedAccu;
-      IterationElement iterElem =
-          getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar);
-
-      TranslatedValue stepTv =
-          withIterationScope(
-              comp,
-              iterElem.keyOrIndex,
-              iterElem.value,
-              currentAccu,
-              isMap,
-              isTwoVar,
-              () -> translateExpr(comp.loopStep(), ast));
-
-      taints.add(ctx.mkAnd(inBounds, stepTv.isApproximate()));
-      chainedAccu = ctx.mkITE(inBounds, stepTv.z3Expr(), currentAccu);
-    }
-
-    TranslatedValue resultTv =
-        withScope(
-            comp.accuVar(),
-            TranslatedValue.create(
-                chainedAccu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)),
-            () -> translateExpr(comp.result(), ast));
-
-    Expr<?> iterRangeExpr = iterRangeTv.z3Expr();
-    BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr);
-    BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr);
-
-    // TODO: Model the loop condition for custom macros; until then, abstract the
-    // result of any non-true condition, since the unrolled value ignores early exits.
-    BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition()));
-    BoolExpr isAbstracted =
-        CelZ3TypeSystem.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
-    // An error is not final when truncated: an unknown from a later iteration overrides it.
-    Expr<?> finalResult =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
-            .addCase(rangeIsError, typeSystem.mkError())
-            .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast))
-            .build(resultTv.z3Expr());
-
-    BoolExpr finalTaint =
-        (BoolExpr)
-            ctx.mkITE(
-                ctx.mkOr(rangeIsError, rangeIsUnknown),
-                iterRangeTv.isApproximate(),
-                CelZ3TypeSystem.mkOrFlattened(
-                    ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled));
-
-    return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint);
-  }
-
-  private void constrainIterationElement(
-      IntExpr idx, ArithExpr lengthExpr, Expr<?> xVal, BoolExpr inBounds, ArrayExpr mapPresence) {
-    // Constrain out-of-bounds elements to prevent MBQI from infinitely instantiating list/map
-    // axioms
-    BoolExpr outOfBounds = ctx.mkGe(idx, lengthExpr);
-    typeConstraints.add(ctx.mkImplies(outOfBounds, ctx.mkEq(xVal, typeSystem.mkUnknown())));
-
-    // If we are iterating over a map, we can optionally bind the sequence elements
-    // to the map presence array to ensure the solver knows they correspond.
-    if (mapPresence != null) {
-      Expr<?> selectExpr = ctx.mkSelect(mapPresence, xVal);
-      typeConstraints.add(ctx.mkImplies(inBounds, (BoolExpr) selectExpr));
-    }
-  }
-
-  private TranslatedValue reduceAllOrExists(
-      List<BoundedIteration> iterations,
-      BoolExpr isTruncated,
-      TranslatedValue iterRangeTv,
-      boolean isAll,
-      CelExpr compExpr,
-      CelAbstractSyntaxTree ast) {
-    List<BoolExpr> hasMatchList = new ArrayList<>();
-    List<BoolExpr> hasErrorList = new ArrayList<>();
-    List<BoolExpr> hasUnknownList = new ArrayList<>();
-
-    List<BoolExpr> hasSafeMatchList = new ArrayList<>();
-    List<BoolExpr> hasSafeErrorList = new ArrayList<>();
-    List<BoolExpr> hasSafeUnknownList = new ArrayList<>();
-    List<BoolExpr> activeTaints = new ArrayList<>();
-
-    for (BoundedIteration iter : iterations) {
-      TranslatedValue stepTv = iter.stepResult;
-      Expr<?> step = stepTv.z3Expr();
-      BoolExpr isBool = typeSystem.isBool(step);
-      BoolExpr unwrapStep = (BoolExpr) typeSystem.unwrapBool(step);
-
-      // 'all' short-circuits on False, 'exists' short-circuits on True
-      BoolExpr matchCond = isAll ? ctx.mkNot(unwrapStep) : unwrapStep;
-      BoolExpr isMatch = ctx.mkAnd(isBool, matchCond);
-
-      BoolExpr isU = typeSystem.isUnknown(step);
-      BoolExpr isE =
-          ctx.mkOr(typeSystem.isError(step), ctx.mkAnd(ctx.mkNot(isBool), ctx.mkNot(isU)));
-
-      BoolExpr isActive = iter.inBounds;
-
-      hasMatchList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isMatch));
-      hasErrorList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isE));
-      hasUnknownList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isU));
-
-      hasSafeMatchList.add(
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isActive, isMatch, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
-      hasSafeErrorList.add(
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isActive, isE, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
-      hasSafeUnknownList.add(
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isActive, isU, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
-      activeTaints.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, stepTv.isApproximate()));
-    }
-
-    BoolExpr hasMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasMatchList);
-    BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, hasErrorList);
-    BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasUnknownList);
-    BoolExpr rangeIsError = typeSystem.isError(iterRangeTv.z3Expr());
-    BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeTv.z3Expr());
-
-    BoolExpr hasSafeMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeMatchList);
-    BoolExpr hasSafeError = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeErrorList);
-    BoolExpr hasSafeUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeUnknownList);
-    BoolExpr anyActiveTaint = CelZ3TypeSystem.mkOrFlattened(ctx, activeTaints);
-
-    Expr<?> comprehensionUnknown = mkParameterizedUnknown(compExpr, ast);
-    Expr<?> result =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
-            .addCase(rangeIsError, typeSystem.mkError())
-            .addCase(rangeIsUnknown, comprehensionUnknown)
-            .addCase(hasMatch, typeSystem.mkBool(!isAll))
-            .addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown)
-            .addCase(hasError, typeSystem.mkError())
-            .build(typeSystem.mkBool(isAll));
-
-    BoolExpr baseTaint =
-        CelZ3TypeSystem.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate());
-
-    // Taint identically shadows the value flow's short-circuit control structure
-    BoolExpr resultTaint =
-        (BoolExpr)
-            CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
-                .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate())
-                .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch)))
-                .addCase(
-                    ctx.mkOr(hasUnknown, isTruncated),
-                    ctx.mkOr(iterRangeTv.isApproximate(), isTruncated, ctx.mkNot(hasSafeUnknown)))
-                .addCase(hasError, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeError)))
-                .build(baseTaint);
-
-    return TranslatedValue.create(result, compExpr, typeSystem, resultTaint);
-  }
-
-  private static boolean isAllMacro(CelComprehension comp) {
-    return isBooleanAccuInit(comp, true)
-        && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ false);
-  }
-
-  private static boolean isExistsMacro(CelComprehension comp) {
-    return isBooleanAccuInit(comp, false)
-        && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ true);
-  }
-
-  private static boolean isBooleanAccuInit(CelComprehension comp, boolean expectedValue) {
-    return comp.accuInit().constantOrDefault().getKind() == CelConstant.Kind.BOOLEAN_VALUE
-        && comp.accuInit().constant().booleanValue() == expectedValue;
-  }
-
-  private static boolean isLiteralTrue(CelExpr expr) {
-    CelConstant constant = expr.constantOrDefault();
-    return constant.getKind() == CelConstant.Kind.BOOLEAN_VALUE && constant.booleanValue();
-  }
-
-  private static boolean isNotStrictlyFalseLoopCondition(CelComprehension comp, boolean expectNot) {
-    CelExpr.CelCall call = comp.loopCondition().callOrDefault();
-    if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction())
-        && !call.function().equals(Operator.OLD_NOT_STRICTLY_FALSE.getFunction())) {
-      return false;
-    }
-    CelExpr arg = call.args().get(0);
-    if (expectNot) {
-      CelExpr.CelCall notCall = arg.callOrDefault();
-      if (!notCall.function().equals(Operator.LOGICAL_NOT.getFunction())) {
-        return false;
-      }
-      arg = notCall.args().get(0);
-    }
-    return arg.identOrDefault().name().equals(comp.accuVar());
-  }
-
-  private BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSyntaxTree ast) {
-    CelType type =
-        ast.getType(exprId)
-            .orElseThrow(
-                () -> new IllegalArgumentException("Type not found for expr ID: " + exprId));
-    BoolExpr typeConstraint = createTypeConstraintForType(val, type);
-    return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint);
-  }
-
-  private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
-    if (type instanceof NullableType) {
-      NullableType nullableType = (NullableType) type;
-      return ctx.mkOr(
-          typeSystem.isNull(val), createTypeConstraintForType(val, nullableType.targetType()));
-    }
-    if (type instanceof OptionalType) {
-      BoolExpr isOpt = typeSystem.isOptional(val);
-      CelType paramType = type.parameters().get(0);
-      if (paramType.kind().isDyn() || paramType.kind().isTypeParam()) {
-        return isOpt;
-      }
-      Expr<?> optRef = typeSystem.getOptionalRef(val);
-      BoolExpr hasValue = typeSystem.optHasValue(optRef);
-      Expr<?> optVal = typeSystem.getOptionalValue(optRef);
-      BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal));
-      BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType);
-      return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint)));
-    }
-    if (type.equals(SimpleType.BOOL)) {
-      return typeSystem.isBool(val);
-    }
-    if (type.equals(SimpleType.INT)) {
-      IntExpr unwrapped = typeSystem.getInt(val);
-      return ctx.mkAnd(typeSystem.isInt(val), ctx.mkNot(typeSystem.checkIntOverflow(unwrapped)));
-    }
-    if (type.equals(SimpleType.UINT)) {
-      IntExpr unwrapped = typeSystem.getUint(val);
-      return ctx.mkAnd(typeSystem.isUint(val), ctx.mkNot(typeSystem.checkUintOverflow(unwrapped)));
-    }
-    if (type.equals(SimpleType.DOUBLE)) {
-      return typeSystem.isDouble(val);
-    }
-    if (type.equals(SimpleType.STRING)) {
-      return typeSystem.isString(val);
-    }
-    if (type.equals(SimpleType.BYTES)) {
-      return typeSystem.isBytes(val);
-    }
-    if (type.equals(SimpleType.TIMESTAMP)) {
-      IntExpr nanos = typeSystem.getTimestamp(val);
-      return ctx.mkAnd(
-          typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
-    }
-    if (type.equals(SimpleType.DURATION)) {
-      IntExpr nanos = typeSystem.getDuration(val);
-      return ctx.mkAnd(
-          typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
-    }
-
-    if (type instanceof ListType) {
-      // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather
-      // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops.
-      // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧
-      // typeConstraint(seq[i]).
-      BoolExpr isList = typeSystem.isList(val);
-      CelType elemType = ((ListType) type).elemType();
-
-      Expr<?> listRef = typeSystem.getListRef(val);
-      SeqExpr seq = typeSystem.getSeq(listRef);
-      Expr length = ctx.mkLength(seq);
-
-      List<BoolExpr> boundsAndTypes = new ArrayList<>();
-      boundsAndTypes.add(isList);
-      // Elements beyond the limit are unconstrained, which only matters if elemType is known.
-      if (CelZ3OperatorTranslator.isStaticallyKnown(elemType)) {
-        boundsAndTypes.add(
-            ctx.mkImplies(
-                ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
-                typeSystem.hasTruncatedTypeConstraint(val)));
-      }
-      for (int i = 0; i < comprehensionUnrollLimit; i++) {
-        IntExpr idx = ctx.mkInt(i);
-        Expr elem = ctx.mkNth(seq, idx);
-        BoolExpr validIndex = ctx.mkLt(idx, length);
-        // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in
-        // list(dyn). For concrete types, this is already implied by createTypeConstraintForType.
-        boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem))));
-        BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
-        boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
-      }
-
-      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
-    }
-    if (type instanceof MapType) {
-      // Do NOT emit a for-all quantifier over map keys or values here.
-      // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using
-      // bounded unrolling over the key sequence up to comprehensionUnrollLimit.
-      // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key)
-      //         ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val))
-      BoolExpr isMap = typeSystem.isMap(val);
-      MapType mapType = (MapType) type;
-      CelType keyType = mapType.keyType();
-      CelType valType = mapType.valueType();
-
-      Expr<?> mapRef = typeSystem.getMapRef(val);
-      SeqExpr seq = typeSystem.getMapKeys(mapRef);
-      Expr length = ctx.mkLength(seq);
-      ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
-      ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
-
-      List<BoolExpr> boundsAndTypes = new ArrayList<>();
-      boundsAndTypes.add(isMap);
-      boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
-      // Entries beyond the limit are unconstrained, which matters if keyType or valType is known.
-      if (CelZ3OperatorTranslator.isStaticallyKnown(keyType)
-          || CelZ3OperatorTranslator.isStaticallyKnown(valType)) {
-        boundsAndTypes.add(
-            ctx.mkImplies(
-                ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
-                typeSystem.hasTruncatedTypeConstraint(val)));
-      }
-
-      for (int i = 0; i < comprehensionUnrollLimit; i++) {
-        IntExpr idx = ctx.mkInt(i);
-        Expr key = ctx.mkNth(seq, idx);
-        BoolExpr validIndex = ctx.mkLt(idx, length);
-
-        BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key);
-        BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key));
-        // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in
-        // map(dyn, ...). For concrete map types, this is already implied by keyType constraints.
-        boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError)));
-        boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType)));
-
-        BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key);
-        BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
-
-        Expr mapVal = ctx.mkSelect(mapValues, key);
-        BoolExpr valNotError = ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal));
-        boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
-        boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
-      }
-
-      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
-    }
-    if (type.kind() == CelKind.STRUCT) {
-      return ctx.mkAnd(
-          typeSystem.isMessage(val),
-          ctx.mkEq(
-              typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)), ctx.mkString(type.name())));
-    }
-    // Fallback: no type constraint
-    return ctx.mkTrue();
-  }
-
-  private static final class IterationElement {
-    private final Expr<?> keyOrIndex;
-    private final Expr<?> value;
-
-    private IterationElement(Expr<?> keyOrIndex, Expr<?> value) {
-      this.keyOrIndex = keyOrIndex;
-      this.value = value;
-    }
-  }
-
   private Optional<Object> toCacheKey(CelExpr expr) {
     switch (expr.exprKind().getKind()) {
       case CONSTANT:
@@ -1661,18 +496,6 @@ private Optional<Object> toCacheKey(CelExpr expr) {
     }
   }
 
-  private Expr<?> mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) {
-    CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr);
-
-    ImmutableList.Builder<Expr<?>> smtArgs = ImmutableList.builder();
-    for (CelExpr freeVar : sig.freeVariables()) {
-      smtArgs.add(translateExpr(freeVar, ast).z3Expr());
-    }
-
-    return typeSystem.mkParameterizedUnknown(
-        "!trunc_" + Long.toHexString(sig.staticHash()), smtArgs.build());
-  }
-
   CelAstToZ3Translator(
       Context ctx,
       int comprehensionUnrollLimit,
@@ -1681,24 +504,13 @@ private Expr<?> mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast)
       CelTypeProvider typeProvider,
       boolean parameterizeUnknowns) {
     this.ctx = ctx;
-    this.comprehensionUnrollLimit = comprehensionUnrollLimit;
     this.typeSystem = new CelZ3TypeSystem(ctx, parameterizeUnknowns);
-    this.typeConstraints = new LinkedHashSet<>();
-    this.inputVariableTypes = new HashMap<>();
-    this.operatorTranslator =
-        new CelZ3OperatorTranslator(
-            ctx,
-            typeSystem,
-            this.typeConstraints::add,
-            this::createTypeConstraintForType,
-            val -> inputVariableTypes.getOrDefault(val, SimpleType.DYN),
-            functionRegistry,
-            comprehensionUnrollLimit);
-    this.symbolTable = new HashMap<>();
+    this.context = new CelZ3TranslationContext(ctx, typeSystem, comprehensionUnrollLimit);
+    this.typeConstraintGenerator = context.typeConstraintGenerator();
+    this.operatorTranslator = new CelZ3OperatorTranslator(context, functionRegistry);
+    this.comprehensionTranslator = new CelZ3ComprehensionTranslator(context, this::translateExpr);
+    this.structTranslator = new CelZ3StructTranslator(context, typeProvider, this::translateExpr);
     this.unknownIdentifiers = unknownIdentifiers;
-    this.emptyMessageCache = new HashMap<>();
     this.listLiteralCache = new HashMap<>();
-    this.typeProvider = typeProvider;
-    this.truncationConditions = new ArrayList<>();
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
index c2a505216..ceb5ae3d8 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
@@ -227,7 +227,7 @@ public CelVerificationResult verifyEquivalence(
       // an unknown only by its attributes (e.g. `a && true` and `a` both yield unknown {a}). Two
       // distinct unknowns may thus still be equivalent.
       BoolExpr combinedTaint =
-          CelZ3TypeSystem.mkOrFlattened(
+          CelZ3Exprs.mkOrFlattened(
               ctx,
               tvA.isApproximate(),
               tvB.isApproximate(),
@@ -318,7 +318,7 @@ CelVerificationResult verifyImplication(
       BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition));
 
       BoolExpr combinedTaint =
-          CelZ3TypeSystem.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate());
+          CelZ3Exprs.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate());
       BoolExpr unknownCondition =
           ctx.mkOr(
               translator.getTypeSystem().isUnknown(assumeTv.z3Expr()),
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
new file mode 100644
index 000000000..df34f00aa
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
@@ -0,0 +1,535 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.common.collect.ImmutableList;
+import com.microsoft.z3.ArithExpr;
+import com.microsoft.z3.ArrayExpr;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.IntExpr;
+import com.microsoft.z3.SeqExpr;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.Operator;
+import dev.cel.common.ast.CelConstant;
+import dev.cel.common.ast.CelExpr;
+import dev.cel.common.ast.CelExpr.CelComprehension;
+import dev.cel.common.ast.CelExpr.ExprKind;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.ListType;
+import dev.cel.common.types.MapType;
+import dev.cel.common.types.SimpleType;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.function.BiFunction;
+import java.util.function.Supplier;
+
+/** Translates CEL comprehensions to Z3, unrolling them up to the comprehension unroll limit. */
+@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
+final class CelZ3ComprehensionTranslator {
+
+  private final CelZ3TranslationContext context;
+  private final Context ctx;
+  private final CelZ3TypeSystem typeSystem;
+  private final int comprehensionUnrollLimit;
+  private final BiFunction<CelExpr, CelAbstractSyntaxTree, TranslatedValue> exprTranslator;
+
+  TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSyntaxTree ast) {
+    CelComprehension comp = celExpr.comprehension();
+    CelExpr iterRangeExpr = comp.iterRange();
+    if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.IDENT) {
+      iterRangeExpr =
+          context
+              .lookupSymbol(iterRangeExpr.ident().name())
+              .flatMap(TranslatedValue::celExpr)
+              .orElse(iterRangeExpr);
+    }
+    List<IterationElement> iterationElements = new ArrayList<>();
+    List<BoolExpr> taints = new ArrayList<>();
+    List<Expr<?>> allRangeElems = new ArrayList<>();
+
+    // For statically known list/map literals, unroll them exactly.
+    if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.LIST
+        && iterRangeExpr.list().optionalIndices().isEmpty()) {
+      ImmutableList<CelExpr> elements = iterRangeExpr.list().elements();
+      for (int i = 0; i < elements.size(); i++) {
+        TranslatedValue valueTv = translateExpr(elements.get(i), ast);
+        Expr<?> value = valueTv.z3Expr();
+        taints.add(valueTv.isApproximate());
+        iterationElements.add(new IterationElement(typeSystem.mkInt(i), value));
+        allRangeElems.add(value);
+      }
+    } else if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP
+        && iterRangeExpr.map().entries().stream().noneMatch(CelExpr.CelMap.Entry::optionalEntry)) {
+      for (CelExpr.CelMap.Entry entry : iterRangeExpr.map().entries()) {
+        TranslatedValue keyTv = translateExpr(entry.key(), ast);
+        Expr<?> key = keyTv.z3Expr();
+        taints.add(keyTv.isApproximate());
+        TranslatedValue valueTv = translateExpr(entry.value(), ast);
+        Expr<?> value = valueTv.z3Expr();
+        taints.add(valueTv.isApproximate());
+        iterationElements.add(new IterationElement(key, value));
+        allRangeElems.add(key);
+        allRangeElems.add(value);
+      }
+    } else {
+      return translateDynamicComprehension(celExpr, ast);
+    }
+
+    TranslatedValue accuTv = translateExpr(comp.accuInit(), ast);
+    Expr<?> accu = accuTv.z3Expr();
+    taints.add(accuTv.isApproximate());
+    boolean isMap = iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP;
+    boolean isTwoVar = !comp.iterVar2().isEmpty();
+
+    for (IterationElement iterElem : iterationElements) {
+      Expr<?> currentAccu = accu;
+      accu =
+          withIterationScope(
+              comp,
+              iterElem.keyOrIndex,
+              iterElem.value,
+              currentAccu,
+              isMap,
+              isTwoVar,
+              () -> {
+                TranslatedValue condTv = translateExpr(comp.loopCondition(), ast);
+                TranslatedValue stepTv = translateExpr(comp.loopStep(), ast);
+                taints.add(stepTv.isApproximate());
+                return ctx.mkITE(
+                    (BoolExpr) typeSystem.unwrapBool(condTv.z3Expr()),
+                    stepTv.z3Expr(),
+                    currentAccu);
+              });
+    }
+
+    TranslatedValue resultTv =
+        context.withScope(
+            comp.accuVar(),
+            TranslatedValue.create(accu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)),
+            () -> translateExpr(comp.result(), ast));
+    Expr<?> result = resultTv.z3Expr();
+    return TranslatedValue.create(
+        typeSystem.propagateErrorAndUnknown(
+            "comprehension",
+            result,
+            allRangeElems,
+            ImmutableList.<Expr<?>>builder().add(result).addAll(allRangeElems).build()),
+        celExpr,
+        typeSystem,
+        resultTv.isApproximate());
+  }
+
+  private static final class BoundedIteration {
+    private final BoolExpr inBounds;
+    private final TranslatedValue stepResult;
+
+    private BoundedIteration(BoolExpr inBounds, TranslatedValue stepResult) {
+      this.inBounds = inBounds;
+      this.stepResult = stepResult;
+    }
+  }
+
+  private TranslatedValue translateDynamicComprehension(
+      CelExpr celExpr, CelAbstractSyntaxTree ast) {
+    CelComprehension comp = celExpr.comprehension();
+    TranslatedValue iterRangeTv = translateExpr(comp.iterRange(), ast);
+    Expr<?> iterRange = iterRangeTv.z3Expr();
+    CelType rangeType = ast.getType(comp.iterRange().id()).orElse(SimpleType.DYN);
+
+    boolean isList = rangeType instanceof ListType;
+    boolean isMap = rangeType instanceof MapType;
+    if (!isList && !isMap) {
+      BoolExpr isRuntimeListOrMap =
+          ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange));
+      Expr<?> result =
+          ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError());
+      return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap);
+    }
+
+    SeqExpr<?> seq =
+        isMap
+            ? typeSystem.getMapKeys(typeSystem.getMapRef(iterRange))
+            : typeSystem.getSeq(typeSystem.getListRef(iterRange));
+
+    ArithExpr lengthExpr = ctx.mkLength(seq);
+    ArrayExpr mapPresence =
+        isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null;
+
+    BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange);
+    BoolExpr isTruncated =
+        ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)));
+    context.addTruncationCondition(isTruncated);
+
+    if (isAllMacro(comp) || isExistsMacro(comp)) {
+      return unrollAllAndExists(
+          celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
+    } else {
+      return unrollMapAndFilter(
+          celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
+    }
+  }
+
+  private <T> T withIterationScope(
+      CelComprehension comp,
+      Expr<?> keyOrIndex,
+      Expr<?> value,
+      Expr<?> currentAccu,
+      boolean isMap,
+      boolean isTwoVar,
+      Supplier<T> action) {
+    Supplier<T> bindAccu =
+        () ->
+            context.withScope(
+                comp.accuVar(),
+                TranslatedValue.create(currentAccu, typeSystem, ctx.mkFalse()),
+                action);
+
+    if (isTwoVar) {
+      return context.withScope(
+          comp.iterVar(),
+          TranslatedValue.create(keyOrIndex, typeSystem, ctx.mkFalse()),
+          () ->
+              context.withScope(
+                  comp.iterVar2(),
+                  TranslatedValue.create(value, typeSystem, ctx.mkFalse()),
+                  bindAccu));
+    } else {
+      Expr<?> iterVal = isMap ? keyOrIndex : value;
+      return context.withScope(
+          comp.iterVar(), TranslatedValue.create(iterVal, typeSystem, ctx.mkFalse()), bindAccu);
+    }
+  }
+
+  private IterationElement getIterationElement(
+      Expr<?> xVal, IntExpr idx, Expr<?> iterRange, boolean isMap, boolean isTwoVar) {
+    Expr<?> keyOrIndex;
+    Expr<?> value;
+
+    if (isMap) {
+      keyOrIndex = xVal;
+      if (isTwoVar) {
+        Expr<?> mapRef = typeSystem.getMapRef(iterRange);
+        ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
+        value = ctx.mkSelect(mapValues, keyOrIndex);
+      } else {
+        value = null;
+      }
+    } else {
+      if (isTwoVar) {
+        keyOrIndex = typeSystem.wrapInt(idx);
+        value = xVal;
+      } else {
+        keyOrIndex = null;
+        value = xVal;
+      }
+    }
+    return new IterationElement(keyOrIndex, value);
+  }
+
+  private TranslatedValue unrollAllAndExists(
+      CelExpr celExpr,
+      CelAbstractSyntaxTree ast,
+      SeqExpr<?> seq,
+      ArithExpr lengthExpr,
+      ArrayExpr mapPresence,
+      BoolExpr isTruncated,
+      TranslatedValue iterRangeTv) {
+    CelComprehension comp = celExpr.comprehension();
+    List<BoundedIteration> iterations = new ArrayList<>();
+    TranslatedValue accuInitTv = translateExpr(comp.accuInit(), ast);
+    Expr<?> accuInitExpr = accuInitTv.z3Expr();
+
+    boolean isMap = mapPresence != null;
+    boolean isTwoVar = !comp.iterVar2().isEmpty();
+
+    for (int i = 0; i < comprehensionUnrollLimit; i++) {
+      IntExpr idx = ctx.mkInt(i);
+      BoolExpr inBounds = ctx.mkLt(idx, lengthExpr);
+      Expr<?> xVal = ctx.mkNth(seq, idx);
+
+      constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence);
+
+      IterationElement iterElem =
+          getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar);
+
+      TranslatedValue stepTv =
+          withIterationScope(
+              comp,
+              iterElem.keyOrIndex,
+              iterElem.value,
+              accuInitExpr,
+              isMap,
+              isTwoVar,
+              () -> translateExpr(comp.loopStep(), ast));
+      iterations.add(new BoundedIteration(inBounds, stepTv));
+    }
+
+    return reduceAllOrExists(iterations, isTruncated, iterRangeTv, isAllMacro(comp), celExpr, ast);
+  }
+
+  private TranslatedValue unrollMapAndFilter(
+      CelExpr celExpr,
+      CelAbstractSyntaxTree ast,
+      SeqExpr<?> seq,
+      ArithExpr lengthExpr,
+      ArrayExpr mapPresence,
+      BoolExpr isTruncated,
+      TranslatedValue iterRangeTv) {
+    CelComprehension comp = celExpr.comprehension();
+    // For macros like map and filter, we must sequentially thread the accumulator through the loop
+    TranslatedValue chainedAccuTv = translateExpr(comp.accuInit(), ast);
+    Expr<?> chainedAccu = chainedAccuTv.z3Expr();
+
+    boolean isMap = mapPresence != null;
+    boolean isTwoVar = !comp.iterVar2().isEmpty();
+
+    List<BoolExpr> taints = new ArrayList<>();
+    taints.add(chainedAccuTv.isApproximate());
+    taints.add(iterRangeTv.isApproximate());
+
+    for (int i = 0; i < comprehensionUnrollLimit; i++) {
+      IntExpr idx = ctx.mkInt(i);
+      BoolExpr inBounds = ctx.mkLt(idx, lengthExpr);
+      Expr<?> xVal = ctx.mkNth(seq, idx);
+
+      constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence);
+
+      Expr<?> currentAccu = chainedAccu;
+      IterationElement iterElem =
+          getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar);
+
+      TranslatedValue stepTv =
+          withIterationScope(
+              comp,
+              iterElem.keyOrIndex,
+              iterElem.value,
+              currentAccu,
+              isMap,
+              isTwoVar,
+              () -> translateExpr(comp.loopStep(), ast));
+
+      taints.add(ctx.mkAnd(inBounds, stepTv.isApproximate()));
+      chainedAccu = ctx.mkITE(inBounds, stepTv.z3Expr(), currentAccu);
+    }
+
+    TranslatedValue resultTv =
+        context.withScope(
+            comp.accuVar(),
+            TranslatedValue.create(chainedAccu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)),
+            () -> translateExpr(comp.result(), ast));
+
+    Expr<?> iterRangeExpr = iterRangeTv.z3Expr();
+    BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr);
+    BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr);
+
+    // TODO: Model the loop condition for custom macros; until then, abstract the
+    // result of any non-true condition, since the unrolled value ignores early exits.
+    BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition()));
+    BoolExpr isAbstracted =
+        CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
+    // An error is not final when truncated: an unknown from a later iteration overrides it.
+    Expr<?> finalResult =
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+            .addCase(rangeIsError, typeSystem.mkError())
+            .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast))
+            .build(resultTv.z3Expr());
+
+    BoolExpr finalTaint =
+        (BoolExpr)
+            ctx.mkITE(
+                ctx.mkOr(rangeIsError, rangeIsUnknown),
+                iterRangeTv.isApproximate(),
+                CelZ3Exprs.mkOrFlattened(
+                    ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled));
+
+    return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint);
+  }
+
+  private void constrainIterationElement(
+      IntExpr idx, ArithExpr lengthExpr, Expr<?> xVal, BoolExpr inBounds, ArrayExpr mapPresence) {
+    // Constrain out-of-bounds elements to prevent MBQI from infinitely instantiating list/map
+    // axioms
+    BoolExpr outOfBounds = ctx.mkGe(idx, lengthExpr);
+    context.addConstraint(ctx.mkImplies(outOfBounds, ctx.mkEq(xVal, typeSystem.mkUnknown())));
+
+    // If we are iterating over a map, we can optionally bind the sequence elements
+    // to the map presence array to ensure the solver knows they correspond.
+    if (mapPresence != null) {
+      Expr<?> selectExpr = ctx.mkSelect(mapPresence, xVal);
+      context.addConstraint(ctx.mkImplies(inBounds, (BoolExpr) selectExpr));
+    }
+  }
+
+  private TranslatedValue reduceAllOrExists(
+      List<BoundedIteration> iterations,
+      BoolExpr isTruncated,
+      TranslatedValue iterRangeTv,
+      boolean isAll,
+      CelExpr compExpr,
+      CelAbstractSyntaxTree ast) {
+    List<BoolExpr> hasMatchList = new ArrayList<>();
+    List<BoolExpr> hasErrorList = new ArrayList<>();
+    List<BoolExpr> hasUnknownList = new ArrayList<>();
+
+    List<BoolExpr> hasSafeMatchList = new ArrayList<>();
+    List<BoolExpr> hasSafeErrorList = new ArrayList<>();
+    List<BoolExpr> hasSafeUnknownList = new ArrayList<>();
+    List<BoolExpr> activeTaints = new ArrayList<>();
+
+    for (BoundedIteration iter : iterations) {
+      TranslatedValue stepTv = iter.stepResult;
+      Expr<?> step = stepTv.z3Expr();
+      BoolExpr isBool = typeSystem.isBool(step);
+      BoolExpr unwrapStep = (BoolExpr) typeSystem.unwrapBool(step);
+
+      // 'all' short-circuits on False, 'exists' short-circuits on True
+      BoolExpr matchCond = isAll ? ctx.mkNot(unwrapStep) : unwrapStep;
+      BoolExpr isMatch = ctx.mkAnd(isBool, matchCond);
+
+      BoolExpr isU = typeSystem.isUnknown(step);
+      BoolExpr isE =
+          ctx.mkOr(typeSystem.isError(step), ctx.mkAnd(ctx.mkNot(isBool), ctx.mkNot(isU)));
+
+      BoolExpr isActive = iter.inBounds;
+
+      hasMatchList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isMatch));
+      hasErrorList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isE));
+      hasUnknownList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isU));
+
+      hasSafeMatchList.add(
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isActive, isMatch, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
+      hasSafeErrorList.add(
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isActive, isE, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
+      hasSafeUnknownList.add(
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isActive, isU, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
+      activeTaints.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, stepTv.isApproximate()));
+    }
+
+    BoolExpr hasMatch = CelZ3Exprs.mkOrFlattened(ctx, hasMatchList);
+    BoolExpr hasError = CelZ3Exprs.mkOrFlattened(ctx, hasErrorList);
+    BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasUnknownList);
+    BoolExpr rangeIsError = typeSystem.isError(iterRangeTv.z3Expr());
+    BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeTv.z3Expr());
+
+    BoolExpr hasSafeMatch = CelZ3Exprs.mkOrFlattened(ctx, hasSafeMatchList);
+    BoolExpr hasSafeError = CelZ3Exprs.mkOrFlattened(ctx, hasSafeErrorList);
+    BoolExpr hasSafeUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasSafeUnknownList);
+    BoolExpr anyActiveTaint = CelZ3Exprs.mkOrFlattened(ctx, activeTaints);
+
+    Expr<?> comprehensionUnknown = mkParameterizedUnknown(compExpr, ast);
+    Expr<?> result =
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+            .addCase(rangeIsError, typeSystem.mkError())
+            .addCase(rangeIsUnknown, comprehensionUnknown)
+            .addCase(hasMatch, typeSystem.mkBool(!isAll))
+            .addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown)
+            .addCase(hasError, typeSystem.mkError())
+            .build(typeSystem.mkBool(isAll));
+
+    BoolExpr baseTaint = CelZ3Exprs.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate());
+
+    // Taint identically shadows the value flow's short-circuit control structure
+    BoolExpr resultTaint =
+        (BoolExpr)
+            CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+                .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate())
+                .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch)))
+                .addCase(
+                    ctx.mkOr(hasUnknown, isTruncated),
+                    ctx.mkOr(iterRangeTv.isApproximate(), isTruncated, ctx.mkNot(hasSafeUnknown)))
+                .addCase(hasError, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeError)))
+                .build(baseTaint);
+
+    return TranslatedValue.create(result, compExpr, typeSystem, resultTaint);
+  }
+
+  private static boolean isAllMacro(CelComprehension comp) {
+    return isBooleanAccuInit(comp, true)
+        && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ false);
+  }
+
+  private static boolean isExistsMacro(CelComprehension comp) {
+    return isBooleanAccuInit(comp, false)
+        && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ true);
+  }
+
+  private static boolean isBooleanAccuInit(CelComprehension comp, boolean expectedValue) {
+    return comp.accuInit().constantOrDefault().getKind() == CelConstant.Kind.BOOLEAN_VALUE
+        && comp.accuInit().constant().booleanValue() == expectedValue;
+  }
+
+  private static boolean isLiteralTrue(CelExpr expr) {
+    CelConstant constant = expr.constantOrDefault();
+    return constant.getKind() == CelConstant.Kind.BOOLEAN_VALUE && constant.booleanValue();
+  }
+
+  private static boolean isNotStrictlyFalseLoopCondition(CelComprehension comp, boolean expectNot) {
+    CelExpr.CelCall call = comp.loopCondition().callOrDefault();
+    if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction())
+        && !call.function().equals(Operator.OLD_NOT_STRICTLY_FALSE.getFunction())) {
+      return false;
+    }
+    CelExpr arg = call.args().get(0);
+    if (expectNot) {
+      CelExpr.CelCall notCall = arg.callOrDefault();
+      if (!notCall.function().equals(Operator.LOGICAL_NOT.getFunction())) {
+        return false;
+      }
+      arg = notCall.args().get(0);
+    }
+    return arg.identOrDefault().name().equals(comp.accuVar());
+  }
+
+  private static final class IterationElement {
+    private final Expr<?> keyOrIndex;
+    private final Expr<?> value;
+
+    private IterationElement(Expr<?> keyOrIndex, Expr<?> value) {
+      this.keyOrIndex = keyOrIndex;
+      this.value = value;
+    }
+  }
+
+  private Expr<?> mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) {
+    CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr);
+
+    ImmutableList.Builder<Expr<?>> smtArgs = ImmutableList.builder();
+    for (CelExpr freeVar : sig.freeVariables()) {
+      smtArgs.add(translateExpr(freeVar, ast).z3Expr());
+    }
+
+    return typeSystem.mkParameterizedUnknown(
+        "!trunc_" + Long.toHexString(sig.staticHash()), smtArgs.build());
+  }
+
+  private TranslatedValue translateExpr(CelExpr expr, CelAbstractSyntaxTree ast) {
+    return exprTranslator.apply(expr, ast);
+  }
+
+  CelZ3ComprehensionTranslator(
+      CelZ3TranslationContext context,
+      BiFunction<CelExpr, CelAbstractSyntaxTree, TranslatedValue> exprTranslator) {
+    this.context = context;
+    this.ctx = context.ctx();
+    this.typeSystem = context.typeSystem();
+    this.comprehensionUnrollLimit = context.comprehensionUnrollLimit();
+    this.exprTranslator = exprTranslator;
+  }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
new file mode 100644
index 000000000..de0460e3a
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
@@ -0,0 +1,162 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.common.collect.Lists;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+
+/** Helpers for building Z3 expressions that are independent of the CEL encoding. */
+public final class CelZ3Exprs {
+
+  /**
+   * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
+   *
+   * <p>Returns {@code false} if the list is empty.
+   */
+  public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) {
+    return mkOrFlattened(ctx, Arrays.asList(args));
+  }
+
+  /**
+   * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
+   *
+   * <p>Returns {@code false} if the list is empty.
+   */
+  public static BoolExpr mkOrFlattened(Context ctx, List<BoolExpr> args) {
+    // Pruning true/false constants in Java is significantly faster than building
+    // larger ASTs and letting Z3 process them natively.
+    List<BoolExpr> filteredArgs = new ArrayList<>();
+    for (BoolExpr arg : args) {
+      if (arg.isTrue()) {
+        return ctx.mkTrue();
+      }
+      if (!arg.isFalse()) {
+        filteredArgs.add(arg);
+      }
+    }
+    // Performance only: both shortcuts are equivalent to the mkOr below.
+    if (filteredArgs.isEmpty()) {
+      return ctx.mkFalse();
+    }
+    if (filteredArgs.size() == 1) {
+      return filteredArgs.get(0);
+    }
+    return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0]));
+  }
+
+  /**
+   * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs.
+   *
+   * <p>Returns {@code true} if the list is empty.
+   */
+  public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) {
+    return mkAndFlattened(ctx, Arrays.asList(args));
+  }
+
+  public static BoolExpr mkAndFlattened(Context ctx, List<BoolExpr> args) {
+    // Pruning true/false constants in Java is significantly faster than building
+    // larger ASTs and letting Z3 process them natively.
+    List<BoolExpr> filteredArgs = new ArrayList<>();
+    for (BoolExpr arg : args) {
+      if (arg.isFalse()) {
+        return ctx.mkFalse();
+      }
+      if (!arg.isTrue()) {
+        filteredArgs.add(arg);
+      }
+    }
+    // Performance only: both shortcuts are equivalent to the mkAnd below.
+    if (filteredArgs.isEmpty()) {
+      return ctx.mkTrue();
+    }
+    if (filteredArgs.size() == 1) {
+      return filteredArgs.get(0);
+    }
+    return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0]));
+  }
+
+  /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */
+  public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
+    if (arg.isTrue()) {
+      return ctx.mkFalse();
+    }
+    if (arg.isFalse()) {
+      return ctx.mkTrue();
+    }
+    return ctx.mkNot(arg);
+  }
+
+  /**
+   * Helper to build a chain of nested ITE (If-Then-Else) conditions.
+   *
+   * <p>Conditions are evaluated in the order they are added. Branches with {@code isFalse()}
+   * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to
+   * avoid allocating dead AST paths in Z3.
+   */
+  public static final class SwitchBuilder {
+
+    private static final class SwitchCase {
+      private final BoolExpr condition;
+      private final Expr<?> value;
+
+      private SwitchCase(BoolExpr condition, Expr<?> value) {
+        this.condition = condition;
+        this.value = value;
+      }
+    }
+
+    private final Context ctx;
+    private final List<SwitchCase> cases;
+
+    public static SwitchBuilder newBuilder(Context ctx) {
+      return new SwitchBuilder(ctx);
+    }
+
+    @CanIgnoreReturnValue
+    public SwitchBuilder addCase(BoolExpr condition, Expr<?> value) {
+      // Skip branches that can never be hit (e.g. `isFalse()` probes).
+      if (condition.isFalse()) {
+        return this;
+      }
+      cases.add(new SwitchCase(condition, value));
+      return this;
+    }
+
+    public Expr<?> build(Expr<?> defaultFallback) {
+      Expr<?> result = defaultFallback;
+      for (SwitchCase c : Lists.reverse(cases)) {
+        // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite.
+        if (c.value.equals(result)) {
+          continue;
+        }
+        result = ctx.mkITE(c.condition, c.value, result);
+      }
+      return result;
+    }
+
+    private SwitchBuilder(Context ctx) {
+      this.ctx = ctx;
+      this.cases = new ArrayList<>();
+    }
+  }
+
+  private CelZ3Exprs() {}
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
index d4fd31962..55aa62882 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
@@ -47,18 +47,14 @@
 import java.util.Arrays;
 import java.util.List;
 import java.util.Optional;
-import java.util.function.BiFunction;
-import java.util.function.Consumer;
-import java.util.function.Function;
 
 /** Handles mapping CEL Operators to Z3 SMT logic. */
 @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
 final class CelZ3OperatorTranslator {
   private final Context ctx;
   private final CelZ3TypeSystem typeSystem;
-  private final Consumer<BoolExpr> constraintSink;
-  private final BiFunction<Expr<?>, CelType, BoolExpr> typeConstraintGenerator;
-  private final Function<Expr<?>, CelType> guaranteedTypes;
+  private final CelZ3TranslationContext context;
+  private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
   private final CelZ3FunctionRegistry functionRegistry;
   private final int comprehensionUnrollLimit;
 
@@ -117,7 +113,7 @@ Optional<TranslatedValue> translateFunctionCall(
       }
 
       Optional<CelZ3OverloadResult> evaluatedResultOpt =
-          translator.translate(ctx, typeSystem, constraintSink, z3Args, argApproximations);
+          translator.translate(ctx, typeSystem, context::addConstraint, z3Args, argApproximations);
 
       if (!evaluatedResultOpt.isPresent()) {
         continue;
@@ -131,7 +127,7 @@ Optional<TranslatedValue> translateFunctionCall(
         typeGuards.add(mkTypeGuard(z3Args.get(i), overload.parameterTypes().get(i)));
       }
 
-      BoolExpr typeGuard = CelZ3TypeSystem.mkAndFlattened(ctx, typeGuards);
+      BoolExpr typeGuard = CelZ3Exprs.mkAndFlattened(ctx, typeGuards);
       currentZ3Result = ctx.mkITE(typeGuard, evaluatedResult.z3Expr(), currentZ3Result);
       currentApprox =
           (BoolExpr) ctx.mkITE(typeGuard, evaluatedResult.isApproximate(), currentApprox);
@@ -144,7 +140,7 @@ Optional<TranslatedValue> translateFunctionCall(
     Operator op = opOpt.orElse(null);
     if (op == Operator.IN) {
       currentApprox =
-          CelZ3TypeSystem.mkOrFlattened(
+          CelZ3Exprs.mkOrFlattened(
               ctx, currentApprox, constrainInWitnessTypes(args.get(0), args.get(1), ast));
     } else if (op == Operator.OPTIONAL_SELECT) {
       // A chained optional select (e.g. `a.?b.?c`) selects from the value of an optional operand.
@@ -154,7 +150,7 @@ Optional<TranslatedValue> translateFunctionCall(
               typeSystem.isOptional(operand),
               typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)),
               operand);
-      currentApprox = CelZ3TypeSystem.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target));
+      currentApprox = CelZ3Exprs.mkOrFlattened(ctx, currentApprox, context.isTruncatedMap(target));
     }
 
     return Optional.of(
@@ -197,10 +193,10 @@ private BoolExpr constrainInWitnessTypes(
       SeqExpr<?> seq = typeSystem.getSeq(typeSystem.getListRef(rhs));
       for (Expr<?> cand : candidates) {
         BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(cand));
-        constraintSink.accept(
+        context.addConstraint(
             ctx.mkImplies(
                 ctx.mkAnd(typeSystem.isList(rhs), structContains),
-                typeConstraintGenerator.apply(cand, elemType)));
+                typeConstraintGenerator.createTypeConstraintForType(cand, elemType)));
       }
       // With a concrete element type, the constraints above cover any match in rhs.
       return isConcrete(elemType)
@@ -210,14 +206,16 @@ private BoolExpr constrainInWitnessTypes(
       // IN_MAP only probes the presence of lhs itself.
       ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs));
       BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, lhs);
-      constraintSink.accept(
+      context.addConstraint(
           ctx.mkImplies(
               ctx.mkAnd(typeSystem.isMap(rhs), inMap),
-              typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType())));
-      return isTruncatedMap(rhs);
+              context
+                  .typeConstraintGenerator()
+                  .createTypeConstraintForType(lhs, ((MapType) rhsType).keyType())));
+      return context.isTruncatedMap(rhs);
     }
-    return CelZ3TypeSystem.mkOrFlattened(
-        ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
+    return CelZ3Exprs.mkOrFlattened(
+        ctx, context.isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
   }
 
   private BoolExpr mkTypeGuard(Expr<?> arg, CelType expectedType) {
@@ -385,7 +383,7 @@ private TranslatedValue translateBinaryLogicalAndOr(
             : ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr());
 
     Expr<?> resultZ3 =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(hasMatch, typeSystem.mkBool(!isAnd))
             .addCase(hasUnknown, unknownResult)
             .addCase(hasError, typeSystem.mkError())
@@ -394,10 +392,10 @@ private TranslatedValue translateBinaryLogicalAndOr(
     // An exact short-circuiting operand alone decides the result. Otherwise, an approximate operand
     // may really be the absorbing value (e.g. `unknown && false` is false).
     BoolExpr resultTaint =
-        CelZ3TypeSystem.mkAndFlattened(
+        CelZ3Exprs.mkAndFlattened(
             ctx,
-            CelZ3TypeSystem.mkNotFlattened(ctx, hasSafeMatch),
-            CelZ3TypeSystem.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate()));
+            CelZ3Exprs.mkNotFlattened(ctx, hasSafeMatch),
+            CelZ3Exprs.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate()));
 
     return TranslatedValue.create(resultZ3, typeSystem, resultTaint);
   }
@@ -435,7 +433,7 @@ private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTr
               typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg));
       Expr<?> doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr)));
       result =
-          CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+          CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
               .addCase(typeSystem.isInt(z3Expr), intResult)
               .addCase(typeSystem.isDouble(z3Expr), doubleResult)
               .build(typeSystem.mkError());
@@ -498,7 +496,7 @@ private BoolExpr getNumericEqualityWithConstant(
     BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
 
     return (BoolExpr)
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(typeSystem.isInt(symVal), intEq)
             .addCase(typeSystem.isUint(symVal), uintEq)
             .addCase(typeSystem.isDouble(symVal), doubleEq)
@@ -610,7 +608,7 @@ private BoolExpr getDynamicNumericEquality(Expr<?> z3Expr0, Expr<?> z3Expr1) {
             ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1));
 
     return (BoolExpr)
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(bothIntOrUint, ctx.mkEq(val0, val1))
             .addCase(
                 bothDouble,
@@ -672,15 +670,17 @@ private BoolExpr unrollListEquality(
       taints.add(elemEquality.isApproximate());
     }
 
-    return CelZ3TypeSystem.mkAndFlattened(ctx, equalities);
+    return CelZ3Exprs.mkAndFlattened(ctx, equalities);
   }
 
   private void constrainListElement(SeqExpr<?> seq, IntExpr idx, Expr<?> elem, CelType listType) {
     if (listType instanceof ListType) {
-      constraintSink.accept(
+      context.addConstraint(
           ctx.mkImplies(
               ctx.mkLt(idx, ctx.mkLength(seq)),
-              typeConstraintGenerator.apply(elem, ((ListType) listType).elemType())));
+              context
+                  .typeConstraintGenerator()
+                  .createTypeConstraintForType(elem, ((ListType) listType).elemType())));
     }
   }
 
@@ -740,7 +740,7 @@ private TranslatedValue translateEquality(
     String opName = isEquals ? Operator.EQUALS.getFunction() : Operator.NOT_EQUALS.getFunction();
 
     return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1)
-        .withApproximation(CelZ3TypeSystem.mkOrFlattened(ctx, taints));
+        .withApproximation(CelZ3Exprs.mkOrFlattened(ctx, taints));
   }
 
   private Expr<?> buildListIndex(
@@ -754,12 +754,12 @@ private Expr<?> buildListIndex(
             ctx.mkLt((ArithExpr) index, ctx.mkLength(seq)));
 
     Expr<?> val = ctx.mkNth(seq, (ArithExpr) index);
-    constrainValidElement(ctx.mkAnd(typeGuard, inBounds), val);
+    context.constrainValidValue(ctx.mkAnd(typeGuard, inBounds), val);
 
     if (isOptional) {
       Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val);
-      constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
-      constraintSink.accept(typeSystem.optHasValue(resultOptRef));
+      context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
+      context.addConstraint(typeSystem.optHasValue(resultOptRef));
       return ctx.mkITE(
           inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
     }
@@ -767,10 +767,6 @@ private Expr<?> buildListIndex(
     return ctx.mkITE(inBounds, val, typeSystem.mkError());
   }
 
-  private void constrainValidElement(BoolExpr guard, Expr<?> val) {
-    constraintSink.accept(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(val))));
-  }
-
   private Optional<Long> extractIntNumSafe(Expr<?> expr) {
     Expr<?> simplified = expr.simplify();
 
@@ -814,12 +810,12 @@ private ProbeResult createProbeResult(
     BoolExpr inMap2 = (BoolExpr) ctx.mkSelect(mapPresence, key2);
     Expr<?> val2 = ctx.mkSelect(mapValues, key2);
 
-    BoolExpr condMap1 = CelZ3TypeSystem.mkAndFlattened(ctx, cond1, inMap1);
-    BoolExpr condMap2 = CelZ3TypeSystem.mkAndFlattened(ctx, cond2, inMap2);
+    BoolExpr condMap1 = CelZ3Exprs.mkAndFlattened(ctx, cond1, inMap1);
+    BoolExpr condMap2 = CelZ3Exprs.mkAndFlattened(ctx, cond2, inMap2);
 
-    BoolExpr altInMap = CelZ3TypeSystem.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2);
+    BoolExpr altInMap = CelZ3Exprs.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2);
     Expr<?> altVal =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(inMapOrig, valOrig)
             .addCase(condMap1, val1)
             .addCase(condMap2, val2)
@@ -912,25 +908,25 @@ private Expr<?> buildMapIndex(
 
     BoolExpr finalInMap =
         (BoolExpr)
-            CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+            CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
                 .addCase(isInt, intProbe.altInMap)
                 .addCase(isUint, uintProbe.altInMap)
                 .addCase(isDouble, doubleProbe.altInMap)
                 .build(inMapOrig);
 
     Expr<?> finalVal =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(isInt, intProbe.altVal)
             .addCase(isUint, uintProbe.altVal)
             .addCase(isDouble, doubleProbe.altVal)
             .build(valOrig);
 
-    constrainValidElement(ctx.mkAnd(typeGuard, finalInMap), finalVal);
+    context.constrainValidValue(ctx.mkAnd(typeGuard, finalInMap), finalVal);
 
     if (isOptional) {
       Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal);
-      constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
-      constraintSink.accept(typeSystem.optHasValue(resultOptRef));
+      context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
+      context.addConstraint(typeSystem.optHasValue(resultOptRef));
       return ctx.mkITE(
           finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
     }
@@ -989,10 +985,10 @@ private TranslatedValue translateIndex(
             ctx.mkLt(
                 typeSystem.getInt(rhsTrans),
                 ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(lhsTrans)))));
-    BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, isTruncatedMap(lhsTrans));
+    BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, context.isTruncatedMap(lhsTrans));
     return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args)
         .withApproximation(
-            CelZ3TypeSystem.mkOrFlattened(
+            CelZ3Exprs.mkOrFlattened(
                 ctx, isListIndexTruncated, isMapIndexTruncated, element.isApproximate()));
   }
 
@@ -1030,9 +1026,10 @@ private TranslatedValue buildAndConstrainIndex(
 
       CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType;
       BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue)));
-      BoolExpr typeConstraint = typeConstraintGenerator.apply(actualValue, finalType);
+      BoolExpr typeConstraint =
+          typeConstraintGenerator.createTypeConstraintForType(actualValue, finalType);
       if (isLhsTypeGuaranteed) {
-        constraintSink.accept(ctx.mkImplies(isDefined, typeConstraint));
+        context.addConstraint(ctx.mkImplies(isDefined, typeConstraint));
         return TranslatedValue.create(actualValue, typeSystem, ctx.mkFalse());
       }
       // The type checker may narrow other static types (e.g. `(['a'] + dyn_var)[1]` is typed
@@ -1040,8 +1037,8 @@ private TranslatedValue buildAndConstrainIndex(
       return TranslatedValue.create(
           actualValue,
           typeSystem,
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isDefined, CelZ3TypeSystem.mkNotFlattened(ctx, typeConstraint)));
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isDefined, CelZ3Exprs.mkNotFlattened(ctx, typeConstraint)));
     }
 
     BoolExpr isListGuard =
@@ -1049,7 +1046,7 @@ private TranslatedValue buildAndConstrainIndex(
     BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans));
 
     return TranslatedValue.create(
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
             .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
             .build(typeSystem.mkError()),
@@ -1080,7 +1077,7 @@ private TranslatedValue translateConditional(
             : cond.z3Expr();
 
     Expr<?> resultZ3 =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(hasUnknown, unknownResult)
             .addCase(hasError, typeSystem.mkError())
             .addCase(condTrue, trueBranch.z3Expr())
@@ -1091,7 +1088,7 @@ private TranslatedValue translateConditional(
 
     BoolExpr resultTaint =
         (BoolExpr)
-            CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+            CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
                 .addCase(hasUnknown, ctx.mkNot(hasSafeUnknown))
                 .addCase(hasError, ctx.mkNot(hasSafeError))
                 .addCase(condTrue, ctx.mkOr(cond.isApproximate(), trueBranch.isApproximate()))
@@ -1118,7 +1115,7 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS
    * so constraints derived from those could exclude valid inputs.
    */
   private CelType guaranteedType(TranslatedValue val) {
-    return guaranteedTypes.apply(val.z3Expr());
+    return context.guaranteedType(val.z3Expr());
   }
 
   /**
@@ -1141,18 +1138,6 @@ private static boolean isNumericType(CelType type) {
     return kind == CelKind.INT || kind == CelKind.UINT || kind == CelKind.DOUBLE;
   }
 
-  /**
-   * Whether {@code val} is a map with more keys than the unroll limit, beyond which its presence is
-   * not linked to its keys.
-   */
-  BoolExpr isTruncatedMap(Expr<?> val) {
-    return ctx.mkAnd(
-        typeSystem.isMap(val),
-        ctx.mkGt(
-            ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))),
-            ctx.mkInt(comprehensionUnrollLimit)));
-  }
-
   /**
    * Whether observing {@code args} together may expose a value beyond a truncated type constraint
    * in any of them. Type constraints at the point of observation rule this out only if every arg
@@ -1163,27 +1148,19 @@ private BoolExpr mayObserveTruncatedTypeConstraint(
     if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) {
       return ctx.mkFalse();
     }
-    return CelZ3TypeSystem.mkOrFlattened(
+    return CelZ3Exprs.mkOrFlattened(
         ctx,
         Arrays.stream(args)
             .map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr()))
             .collect(toImmutableList()));
   }
 
-  CelZ3OperatorTranslator(
-      Context ctx,
-      CelZ3TypeSystem typeSystem,
-      Consumer<BoolExpr> constraintSink,
-      BiFunction<Expr<?>, CelType, BoolExpr> typeConstraintGenerator,
-      Function<Expr<?>, CelType> guaranteedTypes,
-      CelZ3FunctionRegistry functionRegistry,
-      int comprehensionUnrollLimit) {
-    this.ctx = ctx;
-    this.typeSystem = typeSystem;
-    this.constraintSink = constraintSink;
-    this.typeConstraintGenerator = typeConstraintGenerator;
-    this.guaranteedTypes = guaranteedTypes;
+  CelZ3OperatorTranslator(CelZ3TranslationContext context, CelZ3FunctionRegistry functionRegistry) {
+    this.ctx = context.ctx();
+    this.typeSystem = context.typeSystem();
+    this.context = context;
+    this.typeConstraintGenerator = context.typeConstraintGenerator();
     this.functionRegistry = functionRegistry;
-    this.comprehensionUnrollLimit = comprehensionUnrollLimit;
+    this.comprehensionUnrollLimit = context.comprehensionUnrollLimit();
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
new file mode 100644
index 000000000..2f32d52b1
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
@@ -0,0 +1,560 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.Iterables;
+import com.google.common.collect.Streams;
+import com.microsoft.z3.ArrayExpr;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.FPExpr;
+import com.microsoft.z3.IntExpr;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.ast.CelExpr;
+import dev.cel.common.types.CelKind;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.CelTypeProvider;
+import dev.cel.common.types.CelTypes;
+import dev.cel.common.types.ListType;
+import dev.cel.common.types.MapType;
+import dev.cel.common.types.NullableType;
+import dev.cel.common.types.OptionalType;
+import dev.cel.common.types.SimpleType;
+import dev.cel.common.types.StructType;
+import dev.cel.common.types.StructTypeReference;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.function.BiFunction;
+
+/** Translates CEL message construction and field selection to Z3. */
+@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
+final class CelZ3StructTranslator {
+  private static final String MSG_REF_PREFIX = "!msg_ref";
+  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 NULL_VALUE_FIELD = "null_value";
+  private static final String SECONDS_FIELD = "seconds";
+  private static final String NANOS_FIELD = "nanos";
+  private static final long MAX_UINT32 = 0xFFFFFFFFL;
+
+  private final CelZ3TranslationContext context;
+  private final Context ctx;
+  private final CelZ3TypeSystem typeSystem;
+  private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
+  private final CelTypeProvider typeProvider;
+  private final BiFunction<CelExpr, CelAbstractSyntaxTree, TranslatedValue> exprTranslator;
+  private final Map<String, Expr<?>> emptyMessageCache;
+  private Expr<?> emptyListCache;
+  private Expr<?> emptyMapCache;
+
+  TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
+    CelExpr.CelStruct createStruct = celExpr.struct();
+    if (isJsonWkt(createStruct.messageName())) {
+      return translateJsonWktStruct(celExpr, createStruct, ast);
+    }
+    if (CelTypes.isWrapperType(createStruct.messageName())) {
+      return translateWrapperWktStruct(celExpr, createStruct, ast);
+    }
+    if (createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE)) {
+      return translateTimestampWktStruct(celExpr, createStruct, ast);
+    }
+    if (createStruct.messageName().equals(CelTypes.DURATION_MESSAGE)) {
+      return translateDurationWktStruct(celExpr, createStruct, ast);
+    }
+
+    // Performance only: reuses the cached default instead of building an equivalent message.
+    if (createStruct.entries().isEmpty()) {
+      return TranslatedValue.create(
+          getDefaultValueForType(StructTypeReference.create(createStruct.messageName())),
+          celExpr,
+          typeSystem,
+          ctx.mkFalse());
+    }
+
+    Expr<?> msgRef = typeSystem.mkMessageRefConst(MSG_REF_PREFIX);
+
+    // Initialize the values array with Unknown. Missing fields and explicit primitive defaults
+    // will both bypass the store and fall back to this Unknown base. However, their msgPresence
+    // will evaluate to false, allowing translateSelect to properly return the default value.
+    ArrayExpr msgValues = ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown());
+    ArrayExpr msgPresence = ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse());
+
+    List<TranslatedValue> elementsTv = new ArrayList<>();
+
+    for (CelExpr.CelStruct.Entry entryAst : createStruct.entries()) {
+      Expr<?> key = ctx.mkString(entryAst.fieldKey());
+      TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
+      Expr<?> value = valueTv.z3Expr();
+
+      CelType fieldType =
+          typeProvider
+              .findType(createStruct.messageName())
+              .filter(t -> t instanceof StructType)
+              .map(t -> (StructType) t)
+              .flatMap(t -> t.findField(entryAst.fieldKey()))
+              .map(StructType.Field::type)
+              .orElseGet(() -> extractAstTypeOrDefault(ast, entryAst.value().id()));
+      Expr<?> defaultVal = getDefaultValueForType(fieldType);
+
+      Expr<?> finalValue = value;
+      BoolExpr optionalHasValue = ctx.mkTrue();
+      if (entryAst.optionalEntry()) {
+        Expr<?> checkedValue =
+            typeSystem.withRuntimeError(value, ctx.mkNot(typeSystem.isOptional(value)));
+        valueTv =
+            TranslatedValue.create(
+                checkedValue, entryAst.value(), typeSystem, valueTv.isApproximate());
+        Expr<?> optRef = typeSystem.getOptionalRef(checkedValue);
+        optionalHasValue = typeSystem.optHasValue(optRef);
+        finalValue = typeSystem.getOptionalValue(optRef);
+      }
+      elementsTv.add(valueTv);
+
+      // Canonicalization Trick:
+      //
+      // We avoid storing explicit default values (e.g. `single_int32: 0`)
+      // in `msgValues`, leaving them as `Unknown` (identical to missing fields).
+      // This structurally aligns defaults with missing fields, allowing Z3's native array equality
+      // (`msg1 == msg2`) to work without using quantifiers (which avoids MBQI loops).
+      // Because proto3 singular primitives do not have field presence, we also skip setting
+      // `msgPresence`.
+      BoolExpr isDefaultPrimitive =
+          fieldType.kind().isPrimitive() ? ctx.mkEq(finalValue, defaultVal) : ctx.mkFalse();
+
+      BoolExpr shouldBypass = ctx.mkOr(ctx.mkNot(optionalHasValue), isDefaultPrimitive);
+
+      msgValues =
+          (ArrayExpr) ctx.mkITE(shouldBypass, msgValues, ctx.mkStore(msgValues, key, finalValue));
+
+      msgPresence =
+          (ArrayExpr)
+              ctx.mkITE(shouldBypass, msgPresence, ctx.mkStore(msgPresence, key, ctx.mkTrue()));
+    }
+
+    context.addConstraint(
+        ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString(createStruct.messageName())));
+    context.addConstraint(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues));
+    context.addConstraint(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence));
+
+    Expr<?> result = typeSystem.wrapMessage(msgRef);
+    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
+  }
+
+  private static boolean isJsonWkt(String messageName) {
+    return messageName.equals(CelTypes.VALUE_MESSAGE)
+        || messageName.equals(CelTypes.LIST_VALUE_MESSAGE)
+        || messageName.equals(CelTypes.STRUCT_MESSAGE);
+  }
+
+  // Concretize JSON WKT unwrapping directly into native Z3 primitives to avoid
+  // sort incompatibilities (Message == String) and solver performance penalties (quantifiers).
+  private TranslatedValue translateJsonWktStruct(
+      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+    Expr<?> fallback;
+    if (createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)) {
+      fallback = typeSystem.mkNull();
+    } else if (createStruct.messageName().equals(CelTypes.LIST_VALUE_MESSAGE)) {
+      fallback = getDefaultValueForType(ListType.create(SimpleType.DYN));
+    } else {
+      fallback = getDefaultValueForType(MapType.create(SimpleType.STRING, SimpleType.DYN));
+    }
+
+    if (createStruct.entries().isEmpty()) {
+      return TranslatedValue.create(fallback, celExpr, typeSystem, ctx.mkFalse());
+    }
+
+    // JSON WKT messages (gp.Struct, gp.Value, gp.ListValue) can only have a single top-level
+    // field entry in non-empty creation literals (e.g., 'fields' for Struct, 'values' for
+    // ListValue, or a single 'oneof' field for Value).
+    CelExpr.CelStruct.Entry entry = Iterables.getOnlyElement(createStruct.entries());
+
+    // Translate the value to properly capture approximations and Optionals
+    TranslatedValue entryTv = translateExpr(entry.value(), ast);
+    Expr<?> finalVal = entryTv.z3Expr();
+
+    boolean isNullValueField =
+        createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)
+            && entry.fieldKey().equals(NULL_VALUE_FIELD);
+
+    if (entry.optionalEntry()) {
+      Expr<?> checkedVal =
+          typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal)));
+      entryTv =
+          TranslatedValue.create(checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
+      Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
+      BoolExpr hasValue = typeSystem.optHasValue(optRef);
+
+      Expr<?> unpackedVal = typeSystem.getOptionalValue(optRef);
+      if (isNullValueField) {
+        unpackedVal = typeSystem.mkNull();
+      }
+      finalVal = ctx.mkITE(hasValue, unpackedVal, fallback);
+    } else if (isNullValueField) {
+      finalVal = typeSystem.mkNull();
+    }
+
+    return TranslatedValue.propagateStrict(
+        ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
+  }
+
+  private TranslatedValue translateWrapperWktStruct(
+      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+    String typeName = createStruct.messageName();
+    CelType wrapperType =
+        CelTypes.getWellKnownCelType(typeName)
+            .orElseThrow(
+                () -> new IllegalArgumentException("Unexpected wrapper type: " + typeName));
+    CelType targetType = ((NullableType) wrapperType).targetType();
+    Expr<?> currentVal = getDefaultValueForType(targetType);
+
+    List<TranslatedValue> entryTvs = new ArrayList<>();
+    for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
+      TranslatedValue entryTv = translateExpr(entry.value(), ast);
+      Expr<?> val = entryTv.z3Expr();
+      if (entry.optionalEntry()) {
+        Expr<?> checkedVal =
+            typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
+        entryTv =
+            TranslatedValue.create(checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
+        Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
+        BoolExpr hasValue = typeSystem.optHasValue(optRef);
+        currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal);
+      } else {
+        currentVal = val;
+      }
+      entryTvs.add(entryTv);
+    }
+    BoolExpr validValue =
+        typeConstraintGenerator.createTypeConstraintForType(currentVal, targetType);
+    if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) {
+      IntExpr intVal = typeSystem.getInt(currentVal);
+      validValue =
+          ctx.mkAnd(
+              validValue,
+              ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)),
+              ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE)));
+    } else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) {
+      IntExpr uintVal = typeSystem.getUint(currentVal);
+      validValue =
+          ctx.mkAnd(
+              validValue,
+              ctx.mkGe(uintVal, ctx.mkInt(0)),
+              ctx.mkLe(uintVal, ctx.mkInt(MAX_UINT32)));
+    } else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) {
+      FPExpr doubleVal = typeSystem.getDouble(currentVal);
+      FPExpr narrowedFloat =
+          ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), doubleVal, ctx.mkFPSortSingle());
+      FPExpr widenedDouble =
+          ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), narrowedFloat, ctx.mkFPSortDouble());
+      currentVal = typeSystem.wrapDouble(widenedDouble);
+    }
+    currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue));
+    return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
+  }
+
+  @FunctionalInterface
+  private interface TimeWktValueFactory {
+    Expr<?> create(IntExpr seconds, IntExpr nanos, IntExpr totalNanos);
+  }
+
+  private TranslatedValue translateTimestampWktStruct(
+      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+    return translateTimeWktStruct(
+        celExpr,
+        createStruct,
+        ast,
+        /* minNanos= */ 0,
+        (seconds, nanos, totalNanos) ->
+            typeSystem.withRuntimeError(
+                typeSystem.wrapTimestamp(totalNanos),
+                typeSystem.checkTimestampOverflow(totalNanos)));
+  }
+
+  private TranslatedValue translateDurationWktStruct(
+      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+    return translateTimeWktStruct(
+        celExpr,
+        createStruct,
+        ast,
+        CelZ3TypeSystem.MIN_DURATION_NANOS,
+        (seconds, nanos, totalNanos) -> {
+          BoolExpr signMismatch =
+              ctx.mkOr(
+                  ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
+                  ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
+          return typeSystem.withRuntimeError(
+              typeSystem.wrapDuration(totalNanos),
+              signMismatch,
+              typeSystem.checkDurationOverflow(totalNanos));
+        });
+  }
+
+  private TranslatedValue translateTimeWktStruct(
+      CelExpr celExpr,
+      CelExpr.CelStruct createStruct,
+      CelAbstractSyntaxTree ast,
+      int minNanos,
+      TimeWktValueFactory valueFactory) {
+    List<TranslatedValue> entryTvs = new ArrayList<>();
+    Expr<?> secondsVal =
+        resolveStructFieldValue(createStruct, SECONDS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
+    Expr<?> nanosVal =
+        resolveStructFieldValue(createStruct, NANOS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
+
+    IntExpr seconds = typeSystem.getInt(secondsVal);
+    IntExpr nanos = typeSystem.getInt(nanosVal);
+    IntExpr totalNanos =
+        (IntExpr) ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos);
+
+    BoolExpr typeError =
+        ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal)));
+    BoolExpr nanosOutOfRange =
+        ctx.mkOr(
+            ctx.mkLt(nanos, ctx.mkInt(minNanos)),
+            ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
+
+    Expr<?> result =
+        typeSystem.withRuntimeError(
+            valueFactory.create(seconds, nanos, totalNanos), typeError, nanosOutOfRange);
+    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
+  }
+
+  private Expr<?> resolveStructFieldValue(
+      CelExpr.CelStruct createStruct,
+      String fieldName,
+      Expr<?> defaultValue,
+      CelAbstractSyntaxTree ast,
+      List<TranslatedValue> entryTvs) {
+    return Streams.findLast(
+            createStruct.entries().stream().filter(entry -> entry.fieldKey().equals(fieldName)))
+        .<Expr<?>>map(
+            entry -> {
+              TranslatedValue entryTv = translateExpr(entry.value(), ast);
+              Expr<?> val = entryTv.z3Expr();
+              if (entry.optionalEntry()) {
+                Expr<?> checkedVal =
+                    typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
+                entryTv =
+                    TranslatedValue.create(
+                        checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
+                Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
+                val =
+                    ctx.mkITE(
+                        typeSystem.optHasValue(optRef),
+                        typeSystem.getOptionalValue(optRef),
+                        defaultValue);
+              }
+              entryTvs.add(entryTv);
+              return val;
+            })
+        .orElse(defaultValue);
+  }
+
+  private Expr<?> getDefaultValueForType(CelType type) {
+    if (type instanceof NullableType) {
+      return typeSystem.mkNull();
+    }
+    if (type instanceof OptionalType) {
+      return typeSystem.mkOptionalNone();
+    }
+    if (type.equals(SimpleType.INT)) {
+      return typeSystem.mkInt(0);
+    }
+    if (type.equals(SimpleType.BOOL)) {
+      return typeSystem.wrapBool(ctx.mkFalse());
+    }
+    if (type.equals(SimpleType.STRING)) {
+      return typeSystem.mkString("");
+    }
+    if (type.equals(SimpleType.BYTES)) {
+      return typeSystem.mkBytes("");
+    }
+    if (type.equals(SimpleType.DOUBLE)) {
+      return typeSystem.mkDouble(0.0);
+    }
+    if (type.equals(SimpleType.UINT)) {
+      return typeSystem.mkUint(0);
+    }
+    if (type.equals(SimpleType.TIMESTAMP)) {
+      return typeSystem.wrapTimestamp(ctx.mkInt(0));
+    }
+    if (type.equals(SimpleType.DURATION)) {
+      return typeSystem.wrapDuration(ctx.mkInt(0));
+    }
+    if (type instanceof ListType) {
+      if (emptyListCache == null) {
+        emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX);
+        context.addConstraint(
+            ctx.mkEq(
+                typeSystem.getSeq(emptyListCache),
+                ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()))));
+      }
+      return typeSystem.wrapList(emptyListCache);
+    }
+    if (type instanceof MapType) {
+      if (emptyMapCache == null) {
+        emptyMapCache = typeSystem.mkMapRefConst(EMPTY_MAP_PREFIX);
+        context.addConstraint(
+            ctx.mkEq(
+                typeSystem.getMapPresence(emptyMapCache),
+                ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse())));
+        context.addConstraint(
+            ctx.mkEq(
+                typeSystem.getMapValues(emptyMapCache),
+                ctx.mkConstArray(typeSystem.celValueSort(), typeSystem.mkUnknown())));
+        context.addConstraint(
+            ctx.mkEq(
+                typeSystem.getMapKeys(emptyMapCache),
+                ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()))));
+      }
+      return typeSystem.wrapMap(emptyMapCache);
+    }
+    if (type.kind() == CelKind.STRUCT) {
+      String messageName = type.name();
+      Expr<?> msgRef =
+          emptyMessageCache.computeIfAbsent(
+              messageName,
+              name -> {
+                Expr<?> ref = typeSystem.mkMessageRefConst(EMPTY_MSG_REF_PREFIX + name);
+                context.addConstraint(
+                    ctx.mkEq(
+                        typeSystem.getMsgPresence(ref),
+                        ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse())));
+                context.addConstraint(
+                    ctx.mkEq(
+                        typeSystem.getMsgValues(ref),
+                        ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown())));
+                context.addConstraint(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name)));
+                return ref;
+              });
+      return typeSystem.wrapMessage(msgRef);
+    }
+    return typeSystem.mkUnknown();
+  }
+
+  private static final class FieldAccess {
+    private final BoolExpr presence;
+    private final Expr<?> value;
+
+    private FieldAccess(BoolExpr presence, Expr<?> value) {
+      this.presence = presence;
+      this.value = value;
+    }
+  }
+
+  private FieldAccess getMapAccess(Expr<?> operand, String field, BoolExpr typeGuard) {
+    Expr<?> mapRef = typeSystem.getMapRef(operand);
+    Expr<?> mapFieldZ3Str = typeSystem.mkString(field);
+    BoolExpr presence =
+        (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str);
+    Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str);
+    context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
+    return new FieldAccess(presence, value);
+  }
+
+  private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGuard) {
+    Expr<?> msgRef = typeSystem.getMessageRef(operand);
+    Expr<?> msgFieldZ3Str = ctx.mkString(field);
+    BoolExpr presence =
+        (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str);
+    Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str);
+    context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
+    return new FieldAccess(presence, value);
+  }
+
+  TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
+    CelExpr.CelSelect select = celExpr.select();
+    long exprId = celExpr.id();
+    TranslatedValue operandTv = translateExpr(select.operand(), ast);
+    Expr<?> operand = operandTv.z3Expr();
+    String field = select.field();
+    CelType operandType = extractAstTypeOrDefault(ast, select.operand().id());
+
+    Expr<?> presenceResult;
+    Expr<?> valueResult;
+
+    if (operandType instanceof MapType) {
+      FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue());
+      presenceResult = mapAcc.presence;
+      valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
+    } else if (operandType.kind() == CelKind.STRUCT) {
+      FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue());
+      presenceResult = msgAcc.presence;
+      Expr<?> defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
+      valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
+    } else {
+      // Dynamic type: generate the full SMT decision tree
+      BoolExpr isMap = typeSystem.isMap(operand);
+      BoolExpr isMessage = typeSystem.isMessage(operand);
+
+      FieldAccess mapAcc = getMapAccess(operand, field, isMap);
+      FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
+
+      presenceResult =
+          CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+              .addCase(isMessage, msgAcc.presence)
+              .addCase(isMap, mapAcc.presence)
+              .build(ctx.mkFalse());
+
+      Expr<?> defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
+      Expr<?> msgRead = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
+      Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
+
+      valueResult =
+          CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+              .addCase(isMessage, msgRead)
+              .addCase(isMap, mapRead)
+              .build(typeSystem.mkError());
+    }
+
+    Expr<?> fieldAccess = select.testOnly() ? typeSystem.wrapBool(presenceResult) : valueResult;
+
+    context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast));
+
+    TranslatedValue result =
+        TranslatedValue.propagateStrict(
+            ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv));
+    // Map presence is only linked to the keys up to the unroll limit.
+    return operandType.kind() == CelKind.STRUCT
+        ? result
+        : result.withApproximation(context.isTruncatedMap(operand));
+  }
+
+  private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) {
+    return ast.getType(id).orElse(SimpleType.DYN);
+  }
+
+  private TranslatedValue translateExpr(CelExpr expr, CelAbstractSyntaxTree ast) {
+    return exprTranslator.apply(expr, ast);
+  }
+
+  CelZ3StructTranslator(
+      CelZ3TranslationContext context,
+      CelTypeProvider typeProvider,
+      BiFunction<CelExpr, CelAbstractSyntaxTree, TranslatedValue> exprTranslator) {
+    this.context = context;
+    this.ctx = context.ctx();
+    this.typeSystem = context.typeSystem();
+    this.typeConstraintGenerator = context.typeConstraintGenerator();
+    this.typeProvider = typeProvider;
+    this.exprTranslator = exprTranslator;
+    this.emptyMessageCache = new HashMap<>();
+  }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
new file mode 100644
index 000000000..4024e1ff5
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
@@ -0,0 +1,142 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.SimpleType;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Optional;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.function.Supplier;
+
+/** State shared by the translators of a single verification query. */
+final class CelZ3TranslationContext {
+
+  private final Context ctx;
+  private final CelZ3TypeSystem typeSystem;
+  private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
+  private final int comprehensionUnrollLimit;
+  private final Set<BoolExpr> constraints;
+  private final Map<Expr<?>, CelType> inputVariableTypes;
+  private final List<BoolExpr> truncationConditions;
+  private final Map<String, TranslatedValue> symbolTable;
+
+  Context ctx() {
+    return ctx;
+  }
+
+  CelZ3TypeSystem typeSystem() {
+    return typeSystem;
+  }
+
+  CelZ3TypeConstraintGenerator typeConstraintGenerator() {
+    return typeConstraintGenerator;
+  }
+
+  int comprehensionUnrollLimit() {
+    return comprehensionUnrollLimit;
+  }
+
+  /** Returns the constraints asserted so far, in insertion order. */
+  Set<BoolExpr> constraints() {
+    return Collections.unmodifiableSet(constraints);
+  }
+
+  void addConstraint(BoolExpr constraint) {
+    constraints.add(constraint);
+  }
+
+  /** Constrains {@code value} to be neither an error nor unknown whenever {@code guard} holds. */
+  void constrainValidValue(BoolExpr guard, Expr<?> value) {
+    addConstraint(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value))));
+  }
+
+  void addInputVariable(Expr<?> variable, CelType declaredType) {
+    inputVariableTypes.put(variable, declaredType);
+  }
+
+  /** Returns the declared type of an input variable, or dyn for any other value. */
+  CelType guaranteedType(Expr<?> value) {
+    return inputVariableTypes.getOrDefault(value, SimpleType.DYN);
+  }
+
+  /**
+   * Whether {@code val} is a map with more keys than the unroll limit, beyond which its presence is
+   * not linked to its keys.
+   */
+  BoolExpr isTruncatedMap(Expr<?> val) {
+    return ctx.mkAnd(
+        typeSystem.isMap(val),
+        ctx.mkGt(
+            ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))),
+            ctx.mkInt(comprehensionUnrollLimit)));
+  }
+
+  void addTruncationCondition(BoolExpr condition) {
+    truncationConditions.add(condition);
+  }
+
+  BoolExpr hasTruncation() {
+    return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions);
+  }
+
+  void bindSymbol(String name, TranslatedValue value) {
+    symbolTable.put(name, value);
+  }
+
+  Optional<TranslatedValue> lookupSymbol(String name) {
+    return Optional.ofNullable(symbolTable.get(name));
+  }
+
+  TranslatedValue computeSymbolIfAbsent(
+      String name, Function<String, TranslatedValue> mappingFunction) {
+    return symbolTable.computeIfAbsent(name, mappingFunction);
+  }
+
+  /** Binds {@code varName} to {@code value} while running {@code action}, then restores it. */
+  <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
+    TranslatedValue prev = symbolTable.put(varName, value);
+    try {
+      return action.get();
+    } finally {
+      if (prev != null) {
+        symbolTable.put(varName, prev);
+      } else {
+        symbolTable.remove(varName);
+      }
+    }
+  }
+
+  CelZ3TranslationContext(Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) {
+    this.ctx = ctx;
+    this.typeSystem = typeSystem;
+    this.typeConstraintGenerator =
+        new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit);
+    this.comprehensionUnrollLimit = comprehensionUnrollLimit;
+    this.constraints = new LinkedHashSet<>();
+    this.inputVariableTypes = new HashMap<>();
+    this.truncationConditions = new ArrayList<>();
+    this.symbolTable = new HashMap<>();
+  }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java
new file mode 100644
index 000000000..1f6e86475
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java
@@ -0,0 +1,231 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.microsoft.z3.ArithExpr;
+import com.microsoft.z3.ArrayExpr;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.IntExpr;
+import com.microsoft.z3.SeqExpr;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.types.CelKind;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.ListType;
+import dev.cel.common.types.MapType;
+import dev.cel.common.types.NullableType;
+import dev.cel.common.types.OptionalType;
+import dev.cel.common.types.SimpleType;
+import java.util.ArrayList;
+import java.util.List;
+
+/** Generates Z3 constraints restricting a value to the values of a CEL type. */
+@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
+final class CelZ3TypeConstraintGenerator {
+
+  private final Context ctx;
+  private final CelZ3TypeSystem typeSystem;
+  private final int comprehensionUnrollLimit;
+
+  BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSyntaxTree ast) {
+    CelType type =
+        ast.getType(exprId)
+            .orElseThrow(
+                () -> new IllegalArgumentException("Type not found for expr ID: " + exprId));
+    BoolExpr typeConstraint = createTypeConstraintForType(val, type);
+    return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint);
+  }
+
+  BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
+    if (type instanceof NullableType) {
+      NullableType nullableType = (NullableType) type;
+      return ctx.mkOr(
+          typeSystem.isNull(val), createTypeConstraintForType(val, nullableType.targetType()));
+    }
+    if (type instanceof OptionalType) {
+      BoolExpr isOpt = typeSystem.isOptional(val);
+      CelType paramType = type.parameters().get(0);
+      if (!CelZ3OperatorTranslator.isStaticallyKnown(paramType)) {
+        return isOpt;
+      }
+      Expr<?> optRef = typeSystem.getOptionalRef(val);
+      BoolExpr hasValue = typeSystem.optHasValue(optRef);
+      Expr<?> optVal = typeSystem.getOptionalValue(optRef);
+      BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal));
+      BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType);
+      return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint)));
+    }
+    if (type.equals(SimpleType.BOOL)) {
+      return typeSystem.isBool(val);
+    }
+    if (type.equals(SimpleType.INT)) {
+      IntExpr unwrapped = typeSystem.getInt(val);
+      return ctx.mkAnd(typeSystem.isInt(val), ctx.mkNot(typeSystem.checkIntOverflow(unwrapped)));
+    }
+    if (type.equals(SimpleType.UINT)) {
+      IntExpr unwrapped = typeSystem.getUint(val);
+      return ctx.mkAnd(typeSystem.isUint(val), ctx.mkNot(typeSystem.checkUintOverflow(unwrapped)));
+    }
+    if (type.equals(SimpleType.DOUBLE)) {
+      return typeSystem.isDouble(val);
+    }
+    if (type.equals(SimpleType.STRING)) {
+      return typeSystem.isString(val);
+    }
+    if (type.equals(SimpleType.BYTES)) {
+      return typeSystem.isBytes(val);
+    }
+    if (type.equals(SimpleType.TIMESTAMP)) {
+      IntExpr nanos = typeSystem.getTimestamp(val);
+      return ctx.mkAnd(
+          typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
+    }
+    if (type.equals(SimpleType.DURATION)) {
+      IntExpr nanos = typeSystem.getDuration(val);
+      return ctx.mkAnd(
+          typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
+    }
+
+    if (type instanceof ListType) {
+      // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather
+      // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops.
+      // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧
+      // typeConstraint(seq[i]).
+      BoolExpr isList = typeSystem.isList(val);
+      CelType elemType = ((ListType) type).elemType();
+
+      Expr<?> listRef = typeSystem.getListRef(val);
+      SeqExpr seq = typeSystem.getSeq(listRef);
+      Expr length = ctx.mkLength(seq);
+
+      List<BoolExpr> boundsAndTypes = new ArrayList<>();
+      boundsAndTypes.add(isList);
+      // Elements beyond the limit are unconstrained, which only matters if elemType is known.
+      if (CelZ3OperatorTranslator.isStaticallyKnown(elemType)) {
+        boundsAndTypes.add(
+            ctx.mkImplies(
+                ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
+                typeSystem.hasTruncatedTypeConstraint(val)));
+      }
+      for (int i = 0; i < comprehensionUnrollLimit; i++) {
+        IntExpr idx = ctx.mkInt(i);
+        Expr elem = ctx.mkNth(seq, idx);
+        BoolExpr validIndex = ctx.mkLt(idx, length);
+        // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in
+        // list(dyn). For concrete types, this is already implied by createTypeConstraintForType.
+        boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem))));
+        BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
+        boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
+      }
+
+      return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
+    }
+    if (type instanceof MapType) {
+      // Do NOT emit a for-all quantifier over map keys or values here.
+      // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using
+      // bounded unrolling over the key sequence up to comprehensionUnrollLimit.
+      // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key)
+      //         ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val))
+      BoolExpr isMap = typeSystem.isMap(val);
+      MapType mapType = (MapType) type;
+      CelType keyType = mapType.keyType();
+      CelType valType = mapType.valueType();
+
+      Expr<?> mapRef = typeSystem.getMapRef(val);
+      SeqExpr seq = typeSystem.getMapKeys(mapRef);
+      Expr length = ctx.mkLength(seq);
+      ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
+      ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
+
+      List<BoolExpr> boundsAndTypes = new ArrayList<>();
+      boundsAndTypes.add(isMap);
+      boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
+      // Entries beyond the limit are unconstrained, which matters if keyType or valType is known.
+      if (CelZ3OperatorTranslator.isStaticallyKnown(keyType)
+          || CelZ3OperatorTranslator.isStaticallyKnown(valType)) {
+        boundsAndTypes.add(
+            ctx.mkImplies(
+                ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
+                typeSystem.hasTruncatedTypeConstraint(val)));
+      }
+
+      for (int i = 0; i < comprehensionUnrollLimit; i++) {
+        IntExpr idx = ctx.mkInt(i);
+        Expr key = ctx.mkNth(seq, idx);
+        BoolExpr validIndex = ctx.mkLt(idx, length);
+
+        BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key);
+        BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key));
+        // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in
+        // map(dyn, ...). For concrete map types, this is already implied by keyType constraints.
+        boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError)));
+        boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType)));
+
+        BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key);
+        BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
+
+        Expr mapVal = ctx.mkSelect(mapValues, key);
+        BoolExpr valNotError = ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
+      }
+
+      return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
+    }
+    if (type.kind() == CelKind.STRUCT) {
+      return ctx.mkAnd(
+          typeSystem.isMessage(val),
+          ctx.mkEq(
+              typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)), ctx.mkString(type.name())));
+    }
+    // Fallback: no type constraint
+    return ctx.mkTrue();
+  }
+
+  private BoolExpr getBoundedMapBijection(
+      ArrayExpr mapPresence, SeqExpr<?> seq, ArithExpr lengthExpr) {
+    List<BoolExpr> constraints = new ArrayList<>();
+    for (int i = 0; i < comprehensionUnrollLimit; i++) {
+      for (int j = i + 1; j < comprehensionUnrollLimit; j++) {
+        BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr);
+        BoolExpr notEqual =
+            ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j))));
+        constraints.add(ctx.mkImplies(validPair, notEqual));
+      }
+    }
+
+    BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
+
+    ArrayExpr seqMap = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse());
+    for (int i = 0; i < comprehensionUnrollLimit; i++) {
+      seqMap =
+          (ArrayExpr)
+              ctx.mkITE(
+                  ctx.mkLt(ctx.mkInt(i), lengthExpr),
+                  ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
+                  seqMap);
+    }
+    constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
+    return CelZ3Exprs.mkAndFlattened(ctx, constraints);
+  }
+
+  CelZ3TypeConstraintGenerator(
+      Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) {
+    this.ctx = ctx;
+    this.typeSystem = typeSystem;
+    this.comprehensionUnrollLimit = comprehensionUnrollLimit;
+  }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
index 7defbc706..d164505c4 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
@@ -16,10 +16,8 @@
 
 import com.google.auto.value.AutoValue;
 import com.google.common.collect.ImmutableList;
-import com.google.common.collect.Lists;
 import com.google.common.collect.ObjectArrays;
 import com.google.common.primitives.UnsignedLongs;
-import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import com.microsoft.z3.ArithExpr;
 import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.BoolExpr;
@@ -35,7 +33,6 @@
 import com.microsoft.z3.Sort;
 import dev.cel.common.internal.ProtoTimeUtils;
 import java.math.BigInteger;
-import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashMap;
 import java.util.List;
@@ -404,7 +401,7 @@ public BoolExpr getStructuralEquality(Expr<?> arg0, Expr<?> arg1) {
     // For primitives, generic equality matches the direct Z3 datatype wrapper.
     BoolExpr genericEq = ctx.mkEq(arg0, arg1);
     return (BoolExpr)
-        SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(isListEq, seqEq)
             .addCase(isMapEq, mapEq)
             .addCase(isMsgEq, msgEq)
@@ -489,7 +486,7 @@ Expr<?> propagateErrorAndUnknown(
     BoolExpr hasError = ctx.mkOr(errors);
     BoolExpr hasUnknown = ctx.mkOr(unknowns);
     // Unknowns have higher precedence than error
-    return SwitchBuilder.newBuilder(ctx)
+    return CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
         .addCase(hasUnknown, unknownResult)
         .addCase(hasError, mkError())
         .build(result);
@@ -797,60 +794,6 @@ public <R extends Sort> SeqExpr<R> mkConcatSafe(Expr<?> arg1, Expr<?> arg2) {
     return ctx.mkConcat((Expr<SeqSort<R>>) arg1, (Expr<SeqSort<R>>) arg2);
   }
 
-  /**
-   * Helper to build a chain of nested ITE (If-Then-Else) conditions.
-   *
-   * <p>Conditions are evaluated in the order they are added. Branches with {@code isFalse()}
-   * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to
-   * avoid allocating dead AST paths in Z3.
-   */
-  public static final class SwitchBuilder {
-
-    private static final class SwitchCase {
-      private final BoolExpr condition;
-      private final Expr<?> value;
-
-      private SwitchCase(BoolExpr condition, Expr<?> value) {
-        this.condition = condition;
-        this.value = value;
-      }
-    }
-
-    private final Context ctx;
-    private final List<SwitchCase> cases;
-
-    public static SwitchBuilder newBuilder(Context ctx) {
-      return new SwitchBuilder(ctx);
-    }
-
-    @CanIgnoreReturnValue
-    public SwitchBuilder addCase(BoolExpr condition, Expr<?> value) {
-      // Skip branches that can never be hit (e.g. `isFalse()` probes).
-      if (condition.isFalse()) {
-        return this;
-      }
-      cases.add(new SwitchCase(condition, value));
-      return this;
-    }
-
-    public Expr<?> build(Expr<?> defaultFallback) {
-      Expr<?> result = defaultFallback;
-      for (SwitchCase c : Lists.reverse(cases)) {
-        // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite.
-        if (c.value.equals(result)) {
-          continue;
-        }
-        result = ctx.mkITE(c.condition, c.value, result);
-      }
-      return result;
-    }
-
-    private SwitchBuilder(Context ctx) {
-      this.ctx = ctx;
-      this.cases = new ArrayList<>();
-    }
-  }
-
   @AutoValue
   abstract static class FuncDeclKey {
     abstract String name();
@@ -864,82 +807,6 @@ private static FuncDeclKey create(String name, Sort[] domain, Sort range) {
     }
   }
 
-  /**
-   * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
-   *
-   * <p>Returns {@code false} if the list is empty.
-   */
-  public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) {
-    return mkOrFlattened(ctx, Arrays.asList(args));
-  }
-
-  /**
-   * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
-   *
-   * <p>Returns {@code false} if the list is empty.
-   */
-  public static BoolExpr mkOrFlattened(Context ctx, List<BoolExpr> args) {
-    // Pruning true/false constants in Java is significantly faster than building
-    // larger ASTs and letting Z3 process them natively.
-    List<BoolExpr> filteredArgs = new ArrayList<>();
-    for (BoolExpr arg : args) {
-      if (arg.isTrue()) {
-        return ctx.mkTrue();
-      }
-      if (!arg.isFalse()) {
-        filteredArgs.add(arg);
-      }
-    }
-    if (filteredArgs.isEmpty()) {
-      return ctx.mkFalse();
-    }
-    if (filteredArgs.size() == 1) {
-      return filteredArgs.get(0);
-    }
-    return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0]));
-  }
-
-  /**
-   * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs.
-   *
-   * <p>Returns {@code true} if the list is empty.
-   */
-  public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) {
-    return mkAndFlattened(ctx, Arrays.asList(args));
-  }
-
-  public static BoolExpr mkAndFlattened(Context ctx, List<BoolExpr> args) {
-    // Pruning true/false constants in Java is significantly faster than building
-    // larger ASTs and letting Z3 process them natively.
-    List<BoolExpr> filteredArgs = new ArrayList<>();
-    for (BoolExpr arg : args) {
-      if (arg.isFalse()) {
-        return ctx.mkFalse();
-      }
-      if (!arg.isTrue()) {
-        filteredArgs.add(arg);
-      }
-    }
-    if (filteredArgs.isEmpty()) {
-      return ctx.mkTrue();
-    }
-    if (filteredArgs.size() == 1) {
-      return filteredArgs.get(0);
-    }
-    return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0]));
-  }
-
-  /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */
-  public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
-    if (arg.isTrue()) {
-      return ctx.mkFalse();
-    }
-    if (arg.isFalse()) {
-      return ctx.mkTrue();
-    }
-    return ctx.mkNot(arg);
-  }
-
   CelZ3TypeSystem(Context ctx, boolean parameterizeUnknowns) {
     this.ctx = ctx;
     this.funcDeclCache = new HashMap<>();
diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
index 7172a6a4f..7ea52abc8 100644
--- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
+++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
@@ -160,14 +160,14 @@ static TranslatedValue propagateStrict(
 
       BoolExpr isError = ts.isError(z3Expr);
       BoolExpr isUnknown = ts.isUnknown(z3Expr);
-      BoolExpr isExact = CelZ3TypeSystem.mkNotFlattened(ctx, isApprox);
+      BoolExpr isExact = CelZ3Exprs.mkNotFlattened(ctx, isApprox);
 
       unknowns.add(isUnknown);
-      exactErrors.add(CelZ3TypeSystem.mkAndFlattened(ctx, isError, isExact));
-      exactUnknowns.add(CelZ3TypeSystem.mkAndFlattened(ctx, isUnknown, isExact));
+      exactErrors.add(CelZ3Exprs.mkAndFlattened(ctx, isError, isExact));
+      exactUnknowns.add(CelZ3Exprs.mkAndFlattened(ctx, isUnknown, isExact));
     }
 
-    BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints);
+    BoolExpr anyTaint = CelZ3Exprs.mkOrFlattened(ctx, taints);
     if (nonConstZ3Args.isEmpty()) {
       return create(baseResult, celExpr, ts, anyTaint);
     }
@@ -175,19 +175,19 @@ static TranslatedValue propagateStrict(
     Expr<?> finalResult =
         ts.propagateErrorAndUnknown(opName, baseResult, nonConstZ3Args, allZ3Args);
 
-    BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors);
-    BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns);
-    BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns);
+    BoolExpr hasExactError = CelZ3Exprs.mkOrFlattened(ctx, exactErrors);
+    BoolExpr hasExactUnknown = CelZ3Exprs.mkOrFlattened(ctx, exactUnknowns);
+    BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, unknowns);
 
     BoolExpr isSafe =
-        CelZ3TypeSystem.mkOrFlattened(
+        CelZ3Exprs.mkOrFlattened(
             ctx,
             hasExactUnknown,
-            CelZ3TypeSystem.mkAndFlattened(
-                ctx, hasExactError, CelZ3TypeSystem.mkNotFlattened(ctx, hasUnknown)),
-            CelZ3TypeSystem.mkNotFlattened(ctx, anyTaint));
+            CelZ3Exprs.mkAndFlattened(
+                ctx, hasExactError, CelZ3Exprs.mkNotFlattened(ctx, hasUnknown)),
+            CelZ3Exprs.mkNotFlattened(ctx, anyTaint));
 
-    return create(finalResult, celExpr, ts, CelZ3TypeSystem.mkNotFlattened(ctx, isSafe));
+    return create(finalResult, celExpr, ts, CelZ3Exprs.mkNotFlattened(ctx, isSafe));
   }
 
   /**
@@ -228,7 +228,7 @@ TranslatedValue withApproximation(BoolExpr approxCondition) {
         z3Expr(),
         celExpr(),
         typeSystem(),
-        CelZ3TypeSystem.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition));
+        CelZ3Exprs.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition));
   }
 }
 
diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
index 35f96b7ef..dd983d36b 100644
--- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
+++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
@@ -33,6 +33,7 @@
 import com.microsoft.z3.SeqExpr;
 import dev.cel.common.CelFunctionDecl;
 import dev.cel.common.CelOverloadDecl;
+import dev.cel.verifier.CelZ3Exprs;
 import dev.cel.verifier.CelZ3TypeSystem;
 import java.util.Optional;
 
@@ -107,7 +108,7 @@ final class OptionalAxioms {
                 Expr<?> mapRef = ts.getMapRef(actualOperand);
 
                 Expr<?> presence =
-                    CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+                    CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
                         .addCase(
                             isMsg,
                             ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str))
@@ -117,7 +118,7 @@ final class OptionalAxioms {
                         .build(ctx.mkFalse());
 
                 Expr<?> value =
-                    CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+                    CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
                         .addCase(
                             isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str))
                         .addCase(
@@ -129,7 +130,7 @@ final class OptionalAxioms {
                 BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue());
                 sink.accept(
                     ctx.mkImplies(
-                        CelZ3TypeSystem.mkAndFlattened(
+                        CelZ3Exprs.mkAndFlattened(
                             ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence),
                         valNotError));
 
diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java
index 0d8698518..baebfff60 100644
--- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java
+++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java
@@ -22,6 +22,7 @@
 import dev.cel.common.types.MapType;
 import dev.cel.common.types.OptionalType;
 import dev.cel.common.types.SimpleType;
+import dev.cel.verifier.CelZ3Exprs;
 import dev.cel.verifier.CelZ3TypeSystem;
 import java.util.Optional;
 
@@ -48,7 +49,7 @@ final class TypeAxiom {
           .build();
 
   private static Expr<?> getTypeExpression(Context ctx, CelZ3TypeSystem typeSystem, Expr<?> val) {
-    return CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+    return CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
         .addCase(
             typeSystem.isStruct(val),
             typeSystem.wrapString(typeSystem.getMsgTypeName(typeSystem.getMessageRef(val))))
diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
index 5a9eaea02..41af9ae8c 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
@@ -499,6 +499,31 @@ public void verifyInvariants_verificationVariablesAndMultiClauseLists_verified()
     assertThat(results).containsExactly("ergonomic_inv", CelVerificationResult.verified());
   }
 
+  @Test
+  public void verifyInvariants_literalListVariableBeyondUnrollLimit_verified() throws Exception {
+    String policySource =
+        "name: literal_list_policy\n" //
+            + "rule:\n" //
+            + "  variables:\n" //
+            + "    - xs: '[1, 2, 3, 4, 5, 6]'\n" //
+            + "  match:\n" //
+            + "    - output: 'true'\n" //
+            + "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: all_positive\n" //
+            + "      assert: variables.xs.all(x, x > 0)";
+    CelPolicy policy = PARSER.parse(policySource);
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                POLICY_COMPILER,
+                CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(5).build())
+            .build();
+
+    ImmutableMap<String, CelVerificationResult> results = verifier.verifyInvariants(policy);
+
+    assertThat(results).containsExactly("all_positive", CelVerificationResult.verified());
+  }
+
   @Test
   public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws Exception {
     Cel extendedCel =
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
index 217b2168e..f8c747452 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -742,6 +742,9 @@ private enum IsAlwaysTrueTestCase {
     OPTIONAL_VALUE_VAR("optional.of(x).value() == x"),
     OPTIONAL_HAS_VALUE_VAR("optional.of(x).hasValue()"),
     OPTIONAL_VAR_HAS_VALUE_IMPLIES_INT("opt_var.hasValue() ? type(opt_var.value()) == int : true"),
+    OPTIONAL_LIST_INDEX("size(int_list) > 0 ? int_list[?0].value() == int_list[0] : true"),
+    OPTIONAL_MAP_INDEX(
+        "'a' in string_int_map ? string_int_map[?'a'].value() == string_int_map['a'] : true"),
 
     IEEE_754_PROTO_NEG_ZERO_NEQ(
         "TestAllTypes{single_double: -0.0} != TestAllTypes{single_double: 0.0}"),
@@ -978,6 +981,7 @@ private enum IsAlwaysTrueTestCase {
         "size(int_list) > 15 ? type(int_list[dyn(15)]) == int : true"),
     MAP_INDEX_TYPE_CONSTRAINT(
         "'key' in string_int_map ? type(string_int_map['key']) == int : true"),
+    FIELD_SELECTION_TYPE_CONSTRAINT("type(test_all_types.single_int64) == int"),
     LITERAL_LIST_INDEX("[1, 2][0] == 1"),
     NESTED_LIST_VARIABLES_EQUALITY(
         "nested_list == [[1]] && nested_list_2 == [[1]] ? nested_list == nested_list_2 : true"),
@@ -1045,6 +1049,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown(
             "x == x",
             "[x] == [x]",
             "{1: x} == {1: x}",
+            "size(int_list) == 1 ? int_list.all(i, x == x) : true",
           })
           String expression)
       throws Exception {
@@ -1569,6 +1574,12 @@ private enum IsAlwaysTrueViolationTestCase {
         "[true, 1/0].exists(x, x) == true",
         "Condition is not always true\\.",
         "\\(The expression fails unconditionally, regardless of input state\\)"),
+    // The non-negative element can't make the step false, so only an error at 0 violates it.
+    DYNAMIC_LIST_ALL_STEP_ERROR_PROPAGATES(
+        "size(int_list) == 1 && int_list[0] >= 0 ? int_list.all(x, 10 / x >= 0) : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "int_list = \\[0\\]"),
     DYNAMIC_STRING_MACRO_TYPE_MISMATCH(
         "unknown_var == 1 ? !(unknown_var.contains('a') == true || unknown_var.contains('a') =="
             + " false) : true",