From d4becf263871e69f51da6425d4fd1777dd3e1d39 Mon Sep 17 00:00:00 2001
From: Sean Huh <sokwhan@google.com>
Date: Wed, 21 Oct 2026 10:04:31 -0700
Subject: [PATCH] Expose the verifier's counterexamples as structured
 CelWitness values

PiperOrigin-RevId: 1004026905
---
 verifier/README.md                            |    5 +-
 .../main/java/dev/cel/verifier/BUILD.bazel    |    8 +
 .../cel/verifier/CelAstToZ3Translator.java    | 1084 +----------------
 .../cel/verifier/CelVerificationResult.java   |   65 +-
 .../dev/cel/verifier/CelVerifierZ3Impl.java   |   71 +-
 .../java/dev/cel/verifier/CelWitness.java     |   52 +
 .../CelZ3ComprehensionTranslator.java         |  535 ++++++++
 .../CelZ3CounterexampleGenerator.java         |  462 +++----
 .../java/dev/cel/verifier/CelZ3Exprs.java     |    2 +
 .../cel/verifier/CelZ3OperatorTranslator.java |   89 +-
 .../cel/verifier/CelZ3StructTranslator.java   |  560 +++++++++
 .../cel/verifier/CelZ3TranslationContext.java |  148 +++
 .../verifier/CelPolicyVerifierImplTest.java   |   29 +-
 .../cel/verifier/CelVerifierZ3ImplTest.java   |  232 +++-
 .../verifier/tools/CelVerifierReplTest.java   |    2 +-
 15 files changed, 1951 insertions(+), 1393 deletions(-)
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelWitness.java
 create mode 100644 verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.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

diff --git a/verifier/README.md b/verifier/README.md
index d0c054485..7d9d7f899 100644
--- a/verifier/README.md
+++ b/verifier/README.md
@@ -224,8 +224,8 @@ public class PolicyVerifierExample {
         System.out.println(result.message());
         // Output:
         // Equivalence violation detected. Counterexample input:
-        //   country = "a"
         //   role = "editor"
+        //   country = "a"
         //   port = 443
         break;
       case INCONCLUSIVE:
@@ -241,7 +241,8 @@ public class PolicyVerifierExample {
 When checking whether an expression is satisfiable using `isSatisfiable`, the
 verifier returns `VERIFIED` if there exists at least one input combination
 where the expression evaluates to `true`. Furthermore, `result.message()`
-provides concrete satisfying model assignments (witness/test case generation).
+provides concrete satisfying model assignments (witness/test case generation),
+and `result.witness()` exposes them as CEL runtime values.
 
 ```java
 import dev.cel.common.CelAbstractSyntaxTree;
diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
index d48faf98f..2d2549456 100644
--- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
+++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
@@ -15,6 +15,7 @@ java_library(
         "CelVerificationResult.java",
         "CelVerifier.java",
         "CelVerifierBuilder.java",
+        "CelWitness.java",
     ],
     tags = [
     ],
@@ -23,6 +24,7 @@ java_library(
         "//common:cel_ast",
         "//common/types:type_providers",
         "@maven//:com_google_errorprone_error_prone_annotations",
+        "@maven//:com_google_guava_guava",
     ],
 )
 
@@ -160,10 +162,13 @@ 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",
     ],
@@ -183,10 +188,13 @@ java_library(
         "//common/ast",
         "//common/ast:cel_block",
         "//common/internal:cel_descriptor_pools",
+        "//common/internal:proto_time_utils",
         "//common/internal:well_known_proto",
         "//common/types",
         "//common/types:cel_types",
         "//common/types:type_providers",
+        "//common/values",
+        "//common/values:cel_byte_string",
         "//optimizer",
         "//optimizer:optimization_exception",
         "//optimizer:optimizer_builder",
diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
index 20050cd82..db344960b 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,46 +66,37 @@
 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 CelZ3OperatorTranslator operatorTranslator;
+  private final CelZ3TranslationContext context;
   private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
-  private final Map<String, TranslatedValue> symbolTable;
-  private final Set<BoolExpr> typeConstraints;
-  private final Map<Expr<?>, CelType> inputVariableTypes;
+  private final CelZ3OperatorTranslator operatorTranslator;
+  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 CelZ3Exprs.mkOrFlattened(ctx, truncationConditions);
+    return context.hasTruncation();
   }
 
   CelZ3TypeSystem getTypeSystem() {
     return typeSystem;
   }
 
+  /** Returns the input variables, in order of first appearance. */
+  Set<Expr<?>> getInputVariables() {
+    return context.inputVariables();
+  }
+
   /**
    * Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true.
    */
@@ -132,7 +109,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) {
@@ -149,13 +126,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;
   }
@@ -196,7 +173,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:
@@ -204,9 +181,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);
     }
@@ -256,22 +233,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 = 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(
@@ -325,7 +302,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));
@@ -380,9 +357,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);
@@ -399,491 +376,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 =
-        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);
-        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(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);
-    constrainPresentValue(CelZ3Exprs.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 =
-          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;
-
-    typeConstraints.add(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(operatorTranslator.isTruncatedMap(operand));
-  }
-
   private TranslatedValue translateBlock(
       List<CelExpr> boundExprs, int currentIndex, CelExpr resultExpr, CelAbstractSyntaxTree ast) {
     if (currentIndex >= boundExprs.size()) {
@@ -894,7 +391,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));
   }
 
@@ -938,10 +435,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(
+              context.addConstraint(
                   typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast));
-              typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
-              typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
+              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(
@@ -979,482 +476,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, 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 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 <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, 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);
-    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(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 Optional<Object> toCacheKey(CelExpr expr) {
     switch (expr.exprKind().getKind()) {
       case CONSTANT:
@@ -1480,18 +501,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,
@@ -1500,26 +509,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.typeConstraintGenerator =
-        new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit);
-    this.operatorTranslator =
-        new CelZ3OperatorTranslator(
-            ctx,
-            typeSystem,
-            this.typeConstraints::add,
-            typeConstraintGenerator::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/CelVerificationResult.java b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java
index 5a4c7ada6..f4c4a8123 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java
@@ -15,6 +15,8 @@
 package dev.cel.verifier;
 
 import com.google.auto.value.AutoValue;
+import java.util.Map;
+import java.util.Optional;
 
 /** Result object containing the outcome of a CEL AST verification check. */
 @AutoValue
@@ -43,6 +45,12 @@ public enum VerificationStatus {
    */
   public abstract String counterexample();
 
+  /**
+   * Returns the counterexample or satisfying input found by the solver, if any. Its variables are
+   * empty when the outcome doesn't depend on any input.
+   */
+  public abstract Optional<CelWitness> witness();
+
   /**
    * Returns a message detailing the outcome of the verification check, such as a counterexample
    * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
@@ -53,28 +61,65 @@ public String message() {
   }
 
   static CelVerificationResult verified() {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
+    return create(VerificationStatus.VERIFIED, "");
   }
 
-  static CelVerificationResult verified(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
+  static CelVerificationResult verified(String reason, CelWitness satisfyingInput) {
+    return create(
+        VerificationStatus.VERIFIED, reason, satisfyingInput, /* isCounterexample= */ false);
   }
 
   static CelVerificationResult failed(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
+    return create(VerificationStatus.VIOLATED, reason);
   }
 
-  static CelVerificationResult failed(String reason, String counterexample) {
-    return new AutoValue_CelVerificationResult(
-        VerificationStatus.VIOLATED, reason, counterexample);
+  static CelVerificationResult failed(String reason, CelWitness counterexample) {
+    return create(
+        VerificationStatus.VIOLATED, reason, counterexample, /* isCounterexample= */ true);
   }
 
   static CelVerificationResult inconclusive(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
+    return create(VerificationStatus.INCONCLUSIVE, reason);
+  }
+
+  static CelVerificationResult inconclusive(
+      String reason, CelWitness witness, boolean isCounterexample) {
+    return create(VerificationStatus.INCONCLUSIVE, reason, witness, isCounterexample);
   }
 
-  static CelVerificationResult inconclusive(String reason, String counterexample) {
+  private static CelVerificationResult create(VerificationStatus status, String reason) {
+    return new AutoValue_CelVerificationResult(status, reason, "", Optional.empty());
+  }
+
+  private static CelVerificationResult create(
+      VerificationStatus status, String reason, CelWitness witness, boolean isCounterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.INCONCLUSIVE, reason, counterexample);
+        status,
+        reason,
+        describe(witness, status == VerificationStatus.INCONCLUSIVE, isCounterexample),
+        Optional.of(witness));
+  }
+
+  private static String describe(
+      CelWitness witness, boolean isApproximate, boolean isCounterexample) {
+    if (witness.variables().isEmpty()) {
+      return isCounterexample
+          ? " (The expression fails unconditionally, regardless of input state)"
+          : " (The expression is satisfiable unconditionally, regardless of input state)";
+    }
+
+    StringBuilder sb = new StringBuilder();
+    if (isCounterexample) {
+      sb.append(isApproximate ? " Potential counterexample input:" : " Counterexample input:");
+    } else {
+      sb.append(isApproximate ? " Potential satisfying input:" : " Satisfying input:");
+    }
+    for (Map.Entry<String, CelWitness.Variable> variable : witness.variables().entrySet()) {
+      sb.append("\n  ")
+          .append(variable.getKey())
+          .append(" = ")
+          .append(variable.getValue().displayValue());
+    }
+    return sb.toString();
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
index ceb5ae3d8..131b3c24c 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
@@ -256,23 +256,13 @@ public CelVerificationResult verifyEquivalence(
       switch (result.outcome) {
         case EXACT_MATCH:
           return CelVerificationResult.failed(
-              "Equivalence violation detected.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ false,
-                  /* isCounterexample= */ true));
+              "Equivalence violation detected.", extractWitness(ctx, translator, result.model));
         case APPROXIMATE_MATCH:
           return CelVerificationResult.inconclusive(
               "Inconclusive: a divergence may exist, but it depends on approximations, missing"
                   + " theories, or loop bounds.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ true);
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               "Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -343,22 +333,13 @@ CelVerificationResult verifyImplication(
         case EXACT_MATCH:
           return CelVerificationResult.failed(
               String.format("%s violation detected.", subjectName),
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ false,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model));
         case APPROXIMATE_MATCH:
           return CelVerificationResult.inconclusive(
               "Inconclusive: a counterexample may exist, but it depends on approximations, missing"
                   + " theories, or loop bounds.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ true);
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               String.format(
@@ -403,23 +384,10 @@ private CelVerificationResult checkSatisfiability(
 
       switch (result.outcome) {
         case EXACT_MATCH:
+          CelWitness witness = extractWitness(ctx, translator, result.model);
           return searchForCounterexample
-              ? CelVerificationResult.failed(
-                  "Condition is not always true.",
-                  getCounterexampleString(
-                      ctx,
-                      translator.getTypeSystem(),
-                      result.model,
-                      /* isApproximate= */ false,
-                      /* isCounterexample= */ true))
-              : CelVerificationResult.verified(
-                  "Condition is satisfiable."
-                      + getCounterexampleString(
-                          ctx,
-                          translator.getTypeSystem(),
-                          result.model,
-                          /* isApproximate= */ false,
-                          /* isCounterexample= */ false));
+              ? CelVerificationResult.failed("Condition is not always true.", witness)
+              : CelVerificationResult.verified("Condition is satisfiable.", witness);
 
         case APPROXIMATE_MATCH:
           String prefix =
@@ -430,12 +398,8 @@ private CelVerificationResult checkSatisfiability(
                       + " approximations, missing theories, or loop bounds.";
           return CelVerificationResult.inconclusive(
               prefix,
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ searchForCounterexample));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ searchForCounterexample);
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
@@ -538,14 +502,13 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn
         parameterizeUnknowns);
   }
 
-  private static String getCounterexampleString(
-      Context ctx,
-      CelZ3TypeSystem typeSystem,
-      Model model,
-      boolean isApproximate,
-      boolean isCounterexample) {
+  private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) {
     return CelZ3CounterexampleGenerator.generate(
-        ctx, typeSystem, model, isApproximate, isCounterexample);
+        ctx,
+        translator.getTypeSystem(),
+        model,
+        comprehensionUnrollLimit,
+        translator.getInputVariables());
   }
 
   private enum SolverOutcome {
diff --git a/verifier/src/main/java/dev/cel/verifier/CelWitness.java b/verifier/src/main/java/dev/cel/verifier/CelWitness.java
new file mode 100644
index 000000000..6dcc2eef6
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelWitness.java
@@ -0,0 +1,52 @@
+// 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.auto.value.AutoValue;
+import com.google.common.collect.ImmutableMap;
+import java.util.Optional;
+
+/** An input assignment found by the solver: a counterexample or a satisfying input. */
+@AutoValue
+public abstract class CelWitness {
+
+  /** The value the solver assigned to one input variable. */
+  @AutoValue
+  public abstract static class Variable {
+
+    /**
+     * Returns the value in its CEL runtime representation ({@code Long}, {@code UnsignedLong},
+     * {@code Double}, {@code Boolean}, {@code String}, {@code CelByteString}, {@code Instant},
+     * {@code Duration}, {@code NullValue}, {@code ImmutableList}, {@code ImmutableMap} or {@code
+     * Optional}, nested accordingly), or empty if it has no exact runtime equivalent (e.g. an
+     * unknown).
+     */
+    public abstract Optional<Object> value();
+
+    // The value as a CEL literal where one exists, for display.
+    abstract String displayValue();
+
+    static Variable create(Optional<Object> value, String displayValue) {
+      return new AutoValue_CelWitness_Variable(value, displayValue);
+    }
+  }
+
+  /** Returns the variables keyed by name, in order of first appearance. */
+  public abstract ImmutableMap<String, Variable> variables();
+
+  static CelWitness create(ImmutableMap<String, Variable> variables) {
+    return new AutoValue_CelWitness(variables);
+  }
+}
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/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
index 22d7b8a42..6be869333 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
@@ -14,7 +14,11 @@
 
 package dev.cel.verifier;
 
-import com.google.common.base.Preconditions;
+import static java.nio.charset.StandardCharsets.UTF_8;
+
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
+import com.google.common.primitives.UnsignedLong;
 import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
@@ -23,281 +27,306 @@
 import com.microsoft.z3.IntNum;
 import com.microsoft.z3.Model;
 import com.microsoft.z3.RatNum;
+import dev.cel.common.internal.ProtoTimeUtils;
+import dev.cel.common.values.CelByteString;
+import dev.cel.common.values.NullValue;
+import java.math.BigDecimal;
 import java.math.BigInteger;
+import java.time.Duration;
+import java.time.Instant;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.HashSet;
 import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Optional;
 import java.util.Set;
-import org.jspecify.annotations.Nullable;
+import java.util.stream.IntStream;
 
-/** Generates human-readable counterexample strings from Z3 models. */
+/** Extracts {@link CelWitness}es from Z3 models. */
 @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
 final class CelZ3CounterexampleGenerator {
 
   private static final int MAX_ELEMENTS_TO_PRINT = 15;
+  private static final BigInteger NANOS_PER_SECOND =
+      BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
 
-  private CelZ3CounterexampleGenerator() {}
+  private final Context ctx;
+  private final CelZ3TypeSystem typeSystem;
+  private final Model model;
+  private final int comprehensionUnrollLimit;
 
-  static String generate(
+  static CelWitness generate(
       Context ctx,
       CelZ3TypeSystem typeSystem,
       Model model,
-      boolean isApproximate,
-      boolean isCounterexample) {
-    FuncDecl[] constDecls = model.getConstDecls();
-
-    List<String> bindings = new ArrayList<>();
-    for (FuncDecl decl : constDecls) {
-      String name = decl.getName().toString();
-      // Filter out internal solver-generated Skolem constants (e.g., k!1, seq.empty!0).
-      // `!` is not a valid CEL identifier.
-      if (name.contains("!")) {
-        continue;
-      }
-      Expr<?> constInterp = model.getConstInterp(decl);
-      if (constInterp != null) {
-        bindings.add(
-            String.format("\n  %s = %s", name, formatExpr(ctx, typeSystem, model, constInterp)));
-      }
+      int comprehensionUnrollLimit,
+      Set<Expr<?>> inputs) {
+    CelZ3CounterexampleGenerator generator =
+        new CelZ3CounterexampleGenerator(ctx, typeSystem, model, comprehensionUnrollLimit);
+    ImmutableMap.Builder<String, CelWitness.Variable> variables = ImmutableMap.builder();
+    for (Expr<?> input : inputs) {
+      Value value = generator.extract(generator.evaluate(input));
+      variables.put(
+          input.getFuncDecl().getName().toString(),
+          CelWitness.Variable.create(value.runtimeValue, value.display));
+    }
+    return CelWitness.create(variables.buildOrThrow());
+  }
+
+  // A model value's CEL runtime representation, if it has an exact one, and its display.
+  private static final class Value {
+    private final Optional<Object> runtimeValue;
+    private final String display;
+
+    private static Value exact(Object runtimeValue, String display) {
+      return new Value(Optional.of(runtimeValue), display);
     }
 
-    if (bindings.isEmpty()) {
-      return isCounterexample
-          ? " (The expression fails unconditionally, regardless of input state)"
-          : " (The expression is satisfiable unconditionally, regardless of input state)";
+    private static Value inexact(String display) {
+      return new Value(Optional.empty(), display);
     }
 
-    String prefix;
-    if (isCounterexample) {
-      prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:";
-    } else {
-      prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:";
+    private Value(Optional<Object> runtimeValue, String display) {
+      this.runtimeValue = runtimeValue;
+      this.display = display;
     }
-    return prefix + String.join("", bindings);
   }
 
-  private static String formatExpr(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, @Nullable Expr<?> expr) {
-    Preconditions.checkState(expr != null, "Z3 failed to evaluate the expression natively.");
-
+  private Value extract(Expr<?> expr) {
     FuncDecl decl = expr.getFuncDecl();
+    Expr<?>[] args = expr.getArgs();
 
-    // Handle CelType constructors wrapper unwrapping
     if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
-      return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
-    } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
-      return formatTimestamp(expr.getArgs()[0]);
-    } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
-      return formatDuration(expr.getArgs()[0]);
+      BigInteger val = ((IntNum) args[0]).getBigInteger();
+      return isInRange(val, Long.MIN_VALUE, Long.MAX_VALUE)
+          ? Value.exact(val.longValue(), val.toString())
+          : Value.inexact(val.toString());
     } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
-      return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
+      BigInteger val = ((IntNum) args[0]).getBigInteger();
+      String display = val + "u";
+      return val.signum() >= 0 && val.bitLength() <= 64
+          ? Value.exact(UnsignedLong.valueOf(val), display)
+          : Value.inexact(display);
     } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {
-      return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
+      return Value.exact(args[0].isTrue(), args[0].toString());
+    } else if (decl.equals(typeSystem.doubleCons().ConstructorDecl())) {
+      return extractDouble((FPNum) args[0]);
     } else if (decl.equals(typeSystem.stringCons().ConstructorDecl())) {
-      return expr.getArgs()[0].toString();
+      return extractString(args[0], /* isBytes= */ false);
     } else if (decl.equals(typeSystem.bytesCons().ConstructorDecl())) {
-      return "b" + expr.getArgs()[0];
-    } else if (decl.equals(typeSystem.doubleCons().ConstructorDecl())) {
-      Expr<?> doubleArg = expr.getArgs()[0];
-      if (doubleArg instanceof FPNum) {
-        FPNum fpNum = (FPNum) doubleArg;
-        if (fpNum.isNaN()) {
-          return "NaN";
-        }
-        if (fpNum.isInf()) {
-          return fpNum.isNegative() ? "-Infinity" : "Infinity";
-        }
-        if (fpNum.isZero()) {
-          return fpNum.isNegative() ? "-0.0" : "0.0";
-        }
-        Expr<?> realExpr = ctx.mkFPToReal(fpNum).simplify();
-        if (realExpr instanceof RatNum) {
-          RatNum ratNum = (RatNum) realExpr;
-          double val =
-              ratNum.getBigIntNumerator().doubleValue()
-                  / ratNum.getBigIntDenominator().doubleValue();
-          return Double.toString(val);
-        }
+      return extractString(args[0], /* isBytes= */ true);
+    } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
+      BigInteger nanos = ((IntNum) args[0]).getBigInteger();
+      BigInteger nanoAdjustment = nanos.mod(NANOS_PER_SECOND);
+      BigInteger seconds = nanos.subtract(nanoAdjustment).divide(NANOS_PER_SECOND);
+      if (!isInRange(
+          seconds, ProtoTimeUtils.TIMESTAMP_SECONDS_MIN, ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)) {
+        return Value.inexact("timestamp(" + seconds + ")");
       }
-      return doubleArg.toString();
+      Instant instant = Instant.ofEpochSecond(seconds.longValue(), nanoAdjustment.longValue());
+      return Value.exact(instant, "timestamp(\"" + instant + "\")");
+    } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
+      BigInteger nanos = ((IntNum) args[0]).getBigInteger();
+      String display =
+          nanos.remainder(NANOS_PER_SECOND).signum() == 0
+              ? "duration(\"" + nanos.divide(NANOS_PER_SECOND) + "s\")"
+              : "duration(\"" + nanos + "ns\")";
+      return isInRange(nanos, Long.MIN_VALUE, Long.MAX_VALUE)
+          ? Value.exact(Duration.ofNanos(nanos.longValue()), display)
+          : Value.inexact(display);
     } else if (decl.equals(typeSystem.listCons().ConstructorDecl())) {
-      return reconstructList(ctx, typeSystem, model, expr.getArgs()[0]);
+      return extractList(args[0]);
     } else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) {
-      return reconstructMap(ctx, typeSystem, model, expr.getArgs()[0]);
+      return extractMap(args[0]);
     } else if (decl.equals(typeSystem.messageCons().ConstructorDecl())) {
-      return reconstructMessage(ctx, typeSystem, model, expr.getArgs()[0]);
+      return extractMessage(args[0]);
     } else if (decl.equals(typeSystem.errorCons().ConstructorDecl())) {
-      return "Error";
+      return Value.inexact("Error");
     } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) {
-      return "Unknown";
+      return Value.inexact("Unknown");
     } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) {
-      return "null";
-    } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) {
-      Expr<?> optRef = expr.getArgs()[0];
-      Expr<?> hasValueExpr =
-          evaluateStrict(
-              model,
-              typeSystem.optHasValue(optRef),
-              String.format("Z3 failed to evaluate optHasValue natively for %s", optRef));
-      if (hasValueExpr.isTrue()) {
-        Expr<?> valueExpr =
-            evaluateStrict(
-                model,
-                typeSystem.getOptionalValue(optRef),
-                String.format("Z3 failed to evaluate optValue natively for %s", optRef));
-        return "optional(" + formatExpr(ctx, typeSystem, model, valueExpr) + ")";
-      } else if (hasValueExpr.isFalse()) {
-        return "optional.none()";
-      }
+      return Value.exact(NullValue.NULL_VALUE, "null");
     }
 
-    return expr.toString();
+    // Optional is the only remaining constructor.
+    if (!evaluate(typeSystem.optHasValue(args[0])).isTrue()) {
+      return Value.exact(Optional.empty(), "optional.none()");
+    }
+    Value value = extract(evaluate(typeSystem.getOptionalValue(args[0])));
+    return new Value(
+        value.runtimeValue.<Object>map(Optional::of), "optional.of(" + value.display + ")");
   }
 
-  private static String formatTimestamp(Expr<?> nanosExpr) {
-    BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
-    BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
-    BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
-    BigInteger seconds = divRem[0];
-    BigInteger nanos = divRem[1];
-    if (nanos.signum() < 0) {
-      seconds = seconds.subtract(BigInteger.ONE);
-      nanos = nanos.add(nanosPerSecond);
+  private static boolean isInRange(BigInteger val, long min, long max) {
+    return val.compareTo(BigInteger.valueOf(min)) >= 0
+        && val.compareTo(BigInteger.valueOf(max)) <= 0;
+  }
+
+  private Value extractDouble(FPNum fpNum) {
+    if (fpNum.isNaN()) {
+      return Value.exact(Double.NaN, "double(\"NaN\")");
+    }
+    if (fpNum.isInf()) {
+      return fpNum.isNegative()
+          ? Value.exact(Double.NEGATIVE_INFINITY, "double(\"-Infinity\")")
+          : Value.exact(Double.POSITIVE_INFINITY, "double(\"Infinity\")");
     }
-    if (nanos.equals(BigInteger.ZERO)) {
-      return "timestamp(" + seconds + ")";
+    double val;
+    if (fpNum.isZero()) {
+      // The real conversion below would lose the sign of -0.0.
+      val = fpNum.isNegative() ? -0.0 : 0.0;
+    } else {
+      RatNum ratNum = (RatNum) ctx.mkFPToReal(fpNum).simplify();
+      // Finite doubles are dyadic rationals, so the decimal expansion is finite and exact.
+      val =
+          new BigDecimal(ratNum.getBigIntNumerator())
+              .divide(new BigDecimal(ratNum.getBigIntDenominator()))
+              .doubleValue();
     }
-    return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}";
+    return Value.exact(val, Double.toString(val));
   }
 
-  private static String formatDuration(Expr<?> nanosExpr) {
-    BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
-    BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
-    BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
-    if (divRem[1].equals(BigInteger.ZERO)) {
-      return "duration('" + divRem[0] + "s')";
+  private static Value extractString(Expr<?> arg, boolean isBytes) {
+    int[] codePoints = decodeZ3String(arg.getString());
+    // Bytes are modeled as their UTF-8 decoding, which is lossy for non-ASCII bytes. Java merges
+    // adjacent surrogates into one code point, which would change the string's size.
+    boolean isExact =
+        Arrays.stream(codePoints)
+            .allMatch(
+                isBytes
+                    ? c -> c < 0x80
+                    : c -> c < Character.MIN_SURROGATE || c > Character.MAX_SURROGATE);
+    String str = new String(codePoints, 0, codePoints.length);
+    String display = quote(str, isBytes);
+    if (!isExact) {
+      return Value.inexact(display);
     }
-    return "duration('" + totalNanos + "ns')";
+    return Value.exact(isBytes ? CelByteString.copyFromUtf8(str) : str, display);
   }
 
-  private static String reconstructList(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef) {
-    Expr<?> lenExpr =
-        evaluateStrict(
-            model,
-            ctx.mkLength(typeSystem.getSeq(listRef)),
-            String.format("Z3 failed to evaluate length for list %s", listRef));
-    Preconditions.checkState(
-        lenExpr instanceof IntNum, "Expected IntNum length for list %s, got %s", listRef, lenExpr);
-    long length = ((IntNum) lenExpr).getInt64();
-    int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT);
-    List<String> elements = new ArrayList<>();
-    for (int i = 0; i < printLimit; i++) {
-      Expr<?> elem =
-          evaluateStrict(
-              model,
-              ctx.mkNth(typeSystem.getSeq(listRef), ctx.mkInt(i)),
-              String.format(
-                  "Z3 failed to evaluate list element at index %d for list %s", i, listRef));
-      elements.add(formatExpr(ctx, typeSystem, model, elem));
+  // Z3 escapes characters outside printable ASCII, and a backslash before 'u', as \\u{hex}.
+  private static int[] decodeZ3String(String encoded) {
+    IntStream.Builder codePoints = IntStream.builder();
+    for (int i = 0; i < encoded.length(); ) {
+      if (encoded.startsWith("\\u{", i)) {
+        int end = encoded.indexOf('}', i);
+        codePoints.add(Integer.parseInt(encoded.substring(i + 3, end), 16));
+        i = end + 1;
+      } else {
+        codePoints.add(encoded.charAt(i++));
+      }
     }
-    if (length > printLimit) {
-      elements.add("... (" + (length - printLimit) + " more elements)");
+    return codePoints.build().toArray();
+  }
+
+  private static String quote(String str, boolean isBytes) {
+    StringBuilder sb = new StringBuilder(isBytes ? "b\"" : "\"");
+    for (int i = 0; i < str.length(); ) {
+      int codePoint = str.codePointAt(i);
+      i += Character.charCount(codePoint);
+      if (codePoint == '"' || codePoint == '\\') {
+        sb.append('\\').appendCodePoint(codePoint);
+      } else if (isBytes && (codePoint < 0x20 || codePoint >= 0x7f)) {
+        // Bytes literals don't accept \\u escapes, so write the character's UTF-8 bytes as \\xHH.
+        for (byte b : new String(Character.toChars(codePoint)).getBytes(UTF_8)) {
+          sb.append(String.format("\\x%02x", b & 0xff));
+        }
+      } else if (Character.isISOControl(codePoint)
+          || Character.getType(codePoint) == Character.SURROGATE) {
+        // Control characters and lone surrogates can't appear raw in a literal: \\uHHHH.
+        sb.append(String.format("\\u%04x", codePoint));
+      } else {
+        sb.appendCodePoint(codePoint);
+      }
     }
+    return sb.append('"').toString();
+  }
 
-    return "[" + String.join(", ", elements) + "]";
+  private Value extractList(Expr<?> listRef) {
+    long length = evaluateLength(ctx.mkLength(typeSystem.getSeq(listRef)));
+    // Elements past the unroll limit are unconstrained, so they may violate the declared type.
+    boolean isExact = length <= comprehensionUnrollLimit;
+    long limit = isExact ? length : Math.min(length, MAX_ELEMENTS_TO_PRINT);
+    ImmutableList.Builder<Object> values = ImmutableList.builder();
+    List<String> elements = new ArrayList<>();
+    for (long i = 0; i < limit; i++) {
+      Value elem = extract(evaluate(ctx.mkNth(typeSystem.getSeq(listRef), ctx.mkInt(i))));
+      if (elem.runtimeValue.isPresent()) {
+        values.add(elem.runtimeValue.get());
+      } else {
+        isExact = false;
+      }
+      elements.add(elem.display);
+    }
+    String display = join("[", elements, length, "elements", "]");
+    return isExact ? Value.exact(values.build(), display) : Value.inexact(display);
   }
 
-  private static String reconstructMap(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
-    Expr<?> lenExpr =
-        evaluateStrict(
-            model,
-            ctx.mkLength(typeSystem.getMapKeys(mapRef)),
-            String.format("Z3 failed to evaluate length for map %s", mapRef));
-    Preconditions.checkState(
-        lenExpr instanceof IntNum, "Expected IntNum length for map %s, got %s", mapRef, lenExpr);
-
-    long length = ((IntNum) lenExpr).getInt64();
-    int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT);
+  private Value extractMap(Expr<?> mapRef) {
+    long length = evaluateLength(ctx.mkLength(typeSystem.getMapKeys(mapRef)));
+    // Entries past the unroll limit are unconstrained, so they may violate the declared type.
+    boolean isExact = length <= comprehensionUnrollLimit;
+    long limit = isExact ? length : Math.min(length, MAX_ELEMENTS_TO_PRINT);
+    ImmutableMap.Builder<Object, Object> values = ImmutableMap.builder();
     List<String> entries = new ArrayList<>();
     Set<Expr<?>> seenKeys = new HashSet<>();
-    for (int i = 0; i < printLimit; i++) {
-      Expr<?> key =
-          evaluateStrict(
-              model,
-              ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)),
-              String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef));
-      if (!seenKeys.add(key)) {
+    ArrayExpr keySet = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse());
+    for (long i = 0; i < limit; i++) {
+      Expr<?> key = evaluate(ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)));
+      keySet = ctx.mkStore(keySet, key, ctx.mkTrue());
+      if (!seenKeys.add(key)
+          || !evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key)).isTrue()) {
         continue;
       }
-      Expr<?> presence =
-          evaluateStrict(
-              model,
-              ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key),
-              String.format(
-                  "Z3 failed to evaluate map presence for key %s in map %s", key, mapRef));
-      if (presence.isTrue()) {
-        Expr<?> value =
-            evaluateStrict(
-                model,
-                ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), key),
-                String.format("Z3 failed to evaluate map value for key %s in map %s", key, mapRef));
-        entries.add(
-            formatExpr(ctx, typeSystem, model, key)
-                + ": "
-                + formatExpr(ctx, typeSystem, model, value));
+      Value keyValue = extract(key);
+      Value value =
+          extract(evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), key)));
+      if (keyValue.runtimeValue.isPresent() && value.runtimeValue.isPresent()) {
+        values.put(keyValue.runtimeValue.get(), value.runtimeValue.get());
+      } else {
+        isExact = false;
       }
+      entries.add(keyValue.display + ": " + value.display);
     }
-    if (length > printLimit) {
-      entries.add("... (" + (length - printLimit) + " more entries)");
-    }
+    // Maps nested in dyn values aren't constrained to be well formed: the size comes from the key
+    // sequence and membership from the presence array, so they must agree.
+    isExact =
+        isExact
+            && seenKeys.size() == length
+            && evaluate(ctx.mkEq(typeSystem.getMapPresence(mapRef), keySet)).isTrue();
 
-    return "{" + String.join(", ", entries) + "}";
+    String display = join("{", entries, length, "entries", "}");
+    return isExact ? Value.exact(values.buildOrThrow(), display) : Value.inexact(display);
   }
 
-  private static String reconstructMessage(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> msgRef) {
-    Expr<?> presenceArray =
-        evaluateStrict(
-            model,
-            typeSystem.getMsgPresence(msgRef),
-            String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef));
-
-    Expr<?> typeNameExpr =
-        evaluateStrict(
-            model,
-            typeSystem.getMsgTypeName(msgRef),
-            String.format("Z3 failed to evaluate type name natively for msg %s", msgRef));
+  private static String join(
+      String prefix, List<String> displayed, long length, String noun, String suffix) {
+    List<String> shown =
+        new ArrayList<>(displayed.subList(0, Math.min(displayed.size(), MAX_ELEMENTS_TO_PRINT)));
+    if (length > MAX_ELEMENTS_TO_PRINT) {
+      shown.add("... (" + (length - MAX_ELEMENTS_TO_PRINT) + " more " + noun + ")");
+    }
+    return prefix + String.join(", ", shown) + suffix;
+  }
 
-    String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");
+  // TODO: Build message values.
+  private Value extractMessage(Expr<?> msgRef) {
+    Expr<?> presenceArray = evaluate(typeSystem.getMsgPresence(msgRef));
+    String typeName = evaluate(typeSystem.getMsgTypeName(msgRef)).getString();
 
     Set<Expr<?>> keys = new LinkedHashSet<>();
     extractKeys(presenceArray, keys);
 
     List<String> entries = new ArrayList<>();
     for (Expr<?> key : keys) {
-      Expr<?> presence =
-          evaluateStrict(
-              model,
-              ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), key),
-              String.format(
-                  "Z3 failed to evaluate msg presence for key %s in msg %s", key, msgRef));
-
-      if (presence.isTrue()) {
-        Expr<?> value =
-            evaluateStrict(
-                model,
-                ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), key),
-                String.format("Z3 failed to evaluate msg value for key %s in msg %s", key, msgRef));
-
-        String fieldName = formatExpr(ctx, typeSystem, model, key).replace("\"", "");
-        entries.add(fieldName + ": " + formatExpr(ctx, typeSystem, model, value));
+      if (evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), key)).isTrue()) {
+        Expr<?> value = evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), key));
+        entries.add(key.getString() + ": " + extract(value).display);
       }
     }
 
-    return typeName + "{" + String.join(", ", entries) + "}";
+    return Value.inexact(typeName + "{" + String.join(", ", entries) + "}");
   }
 
   private static void extractKeys(Expr<?> arrayExpr, Set<Expr<?>> keys) {
@@ -314,8 +343,6 @@ private static void extractKeys(Expr<?> arrayExpr, Set<Expr<?>> keys) {
 
       if (declName.equals("store")) {
         Expr<?>[] args = arrayExpr.getArgs();
-        Preconditions.checkState(
-            args.length == 3, "Z3 store array operation must have exactly 3 arguments");
         keys.add(args[1]);
         arrayExpr = args[0];
         continue;
@@ -324,13 +351,20 @@ private static void extractKeys(Expr<?> arrayExpr, Set<Expr<?>> keys) {
     }
   }
 
-  private static Expr<?> evaluateStrict(Model model, Expr<?> expr, String errorMessage) {
-    // There are no free variables remaining after the solver is ran, so the completion flag has
-    // no effect.
-    Expr<?> evaluated = model.evaluate(expr, /* completion= */ true);
-    if (evaluated == null) {
-      throw new IllegalStateException(errorMessage);
-    }
-    return evaluated;
+  private long evaluateLength(Expr<?> lengthExpr) {
+    return ((IntNum) evaluate(lengthExpr)).getInt64();
+  }
+
+  private Expr<?> evaluate(Expr<?> expr) {
+    // Model completion assigns a value to any input the model leaves unconstrained.
+    return model.evaluate(expr, /* completion= */ true);
+  }
+
+  private CelZ3CounterexampleGenerator(
+      Context ctx, CelZ3TypeSystem typeSystem, Model model, int comprehensionUnrollLimit) {
+    this.ctx = ctx;
+    this.typeSystem = typeSystem;
+    this.model = model;
+    this.comprehensionUnrollLimit = comprehensionUnrollLimit;
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
index b2b4d86dd..de0460e3a 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
@@ -52,6 +52,7 @@ public static BoolExpr mkOrFlattened(Context ctx, List<BoolExpr> args) {
         filteredArgs.add(arg);
       }
     }
+    // Performance only: both shortcuts are equivalent to the mkOr below.
     if (filteredArgs.isEmpty()) {
       return ctx.mkFalse();
     }
@@ -82,6 +83,7 @@ public static BoolExpr mkAndFlattened(Context ctx, List<BoolExpr> args) {
         filteredArgs.add(arg);
       }
     }
+    // Performance only: both shortcuts are equivalent to the mkAnd below.
     if (filteredArgs.isEmpty()) {
       return ctx.mkTrue();
     }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
index eb4b7636e..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;
@@ -154,7 +150,7 @@ Optional<TranslatedValue> translateFunctionCall(
               typeSystem.isOptional(operand),
               typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)),
               operand);
-      currentApprox = CelZ3Exprs.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 CelZ3Exprs.mkOrFlattened(
-        ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
+        ctx, context.isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
   }
 
   private BoolExpr mkTypeGuard(Expr<?> arg, CelType expectedType) {
@@ -677,10 +675,12 @@ private BoolExpr unrollListEquality(
 
   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())));
     }
   }
 
@@ -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();
 
@@ -925,12 +921,12 @@ private Expr<?> buildMapIndex(
             .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,7 +985,7 @@ 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(
             CelZ3Exprs.mkOrFlattened(
@@ -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
@@ -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
@@ -1170,20 +1155,12 @@ private BoolExpr mayObserveTruncatedTypeConstraint(
             .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..c98877185
--- /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);
+    }
+
+    // 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()));
+    }
+
+    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..da93e0358
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
@@ -0,0 +1,148 @@
+// 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.LinkedHashMap;
+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 input variables, in order of first appearance. */
+  Set<Expr<?>> inputVariables() {
+    return inputVariableTypes.keySet();
+  }
+
+  /** 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 LinkedHashMap<>();
+    this.truncationConditions = new ArrayList<>();
+    this.symbolTable = new HashMap<>();
+  }
+}
diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
index 5a9eaea02..87db12f78 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 =
@@ -528,11 +553,11 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws
         .isEqualTo(
             "Invariant 'universal_no_unapproved_privileged_prod' violation detected."
                 + " Counterexample input:\n"
+                + "  is_admin = true\n"
                 + "  is_owner = false\n"
                 + "  is_privileged = true\n"
                 + "  is_prod = true\n"
-                + "  has_approval = false\n"
-                + "  is_admin = true");
+                + "  has_approval = false");
   }
 
   @Test
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
index 217b2168e..14599372e 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -25,10 +25,14 @@
 import com.google.testing.junit.testparameterinjector.TestParameter;
 import com.google.testing.junit.testparameterinjector.TestParameterInjector;
 // import com.google.testing.testsize.MediumTest;
+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 com.microsoft.z3.Solver;
+import com.microsoft.z3.Status;
 import dev.cel.bundle.Cel;
 import dev.cel.bundle.CelFactory;
 import dev.cel.common.CelAbstractSyntaxTree;
@@ -81,6 +85,7 @@ public final class CelVerifierZ3ImplTest {
           .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))
           .addCompilerLibraries(
               CelExtensions.bindings(), CelOptionalLibrary.INSTANCE, CelExtensions.comprehensions())
+          .addRuntimeLibraries(CelOptionalLibrary.INSTANCE)
           .addMessageTypes(TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor())
           .addVar("x", SimpleType.INT)
           .addVar("u", SimpleType.UINT)
@@ -196,13 +201,22 @@ private enum IsSatisfiableTestCase {
         "size(int_list) == 6 && dyn(b ? [1] : int_list) == [1]", "b = true"),
     TIMESTAMP_SUBSECOND_SATISFIABLE(
         "ts == google.protobuf.Timestamp{seconds: 10, nanos: 500}",
-        "ts = google\\.protobuf\\.Timestamp\\{seconds: 10, nanos: 500\\}"),
+        "ts = timestamp\\(\"1970-01-01T00:00:10\\.000000500Z\"\\)"),
     TIMESTAMP_NEGATIVE_SUBSECOND_SATISFIABLE(
         "ts == google.protobuf.Timestamp{seconds: -1, nanos: 500}",
-        "ts = google\\.protobuf\\.Timestamp\\{seconds: -1, nanos: 500\\}"),
+        "ts = timestamp\\(\"1969-12-31T23:59:59\\.000000500Z\"\\)"),
     DURATION_SUBSECOND_SATISFIABLE(
         "dur == google.protobuf.Duration{seconds: 1, nanos: 500}",
-        "dur = duration\\('1000000500ns'\\)"),
+        "dur = duration\\(\"1000000500ns\"\\)"),
+    // Timestamps nested in dyn aren't range constrained, and RFC 3339 can't express these.
+    TIMESTAMP_ABOVE_RANGE_SATISFIABLE(
+        "type(dyn_var) == google.protobuf.Timestamp"
+            + " && dyn_var > google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}",
+        "dyn_var = timestamp\\(\\d+\\)"),
+    TIMESTAMP_BELOW_RANGE_SATISFIABLE(
+        "type(dyn_var) == google.protobuf.Timestamp"
+            + " && dyn_var < google.protobuf.Timestamp{seconds: -62135596800}",
+        "dyn_var = timestamp\\(-\\d+\\)"),
     ;
 
     private final String expr;
@@ -239,6 +253,192 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception
     assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)");
   }
 
+  private enum WitnessTestCase {
+    INT_MIN("x == -9223372036854775808", "x", "-9223372036854775808"),
+    INT_MAX("x == 9223372036854775807", "x", "9223372036854775807"),
+    UINT_MAX("u == 18446744073709551615u", "u", "18446744073709551615u"),
+    SUBNORMAL_DOUBLE("d == 4.9e-324", "d", "4.9E-324"),
+    POSITIVE_INFINITY("d > 1.7976931348623157e308", "d", "double(\"Infinity\")"),
+    NEGATIVE_INFINITY("d < -1.7976931348623157e308", "d", "double(\"-Infinity\")"),
+    BOOL("a", "a", "true"),
+    UNICODE_STRING("string_var == 'é'", "string_var", "\"é\""),
+    ESCAPED_STRING("string_var == '\"\\\\\\n\\x01'", "string_var", "\"\\\"\\\\\\u000a\\u0001\""),
+    ESCAPED_BYTES("by == b'a\\x01\"'", "by", "b\"a\\x01\\\"\""),
+    MIN_TIMESTAMP("ts == timestamp(-62135596800)", "ts", "timestamp(\"0001-01-01T00:00:00Z\")"),
+    SUBSECOND_TIMESTAMP(
+        "ts == google.protobuf.Timestamp{seconds: -1, nanos: 500}",
+        "ts",
+        "timestamp(\"1969-12-31T23:59:59.000000500Z\")"),
+    DURATION("timestamp(100) - timestamp(50) == dur", "dur", "duration(\"50s\")"),
+    SUBSECOND_DURATION(
+        "dur == google.protobuf.Duration{seconds: -1, nanos: -500}",
+        "dur",
+        "duration(\"-1000000500ns\")"),
+    NULL("dyn_var == null", "dyn_var", "null"),
+    EMPTY_LIST("int_list == []", "int_list", "[]"),
+    LIST_WITH_NULL("dyn_list == [true, null]", "dyn_list", "[true, null]"),
+    MAP("string_int_map == {'a': 1}", "string_int_map", "{\"a\": 1}"),
+    OPTIONAL("opt_var == optional.of(1)", "opt_var", "optional.of(1)"),
+    OPTIONAL_NONE("opt_var == optional.none()", "opt_var", "optional.none()");
+
+    private final String expr;
+    private final String variableName;
+    private final String expectedDisplayValue;
+
+    WitnessTestCase(String expr, String variableName, String expectedDisplayValue) {
+      this.expr = expr;
+      this.variableName = variableName;
+      this.expectedDisplayValue = expectedDisplayValue;
+    }
+  }
+
+  @Test
+  public void isSatisfiable_witnessValueSatisfiesExpressionAndDisplayRoundTrips(
+      @TestParameter WitnessTestCase testCase) throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    CelWitness.Variable variable = result.witness().get().variables().get(testCase.variableName);
+    assertThat(variable.displayValue()).isEqualTo(testCase.expectedDisplayValue);
+    ImmutableMap<String, Object> input =
+        ImmutableMap.of(testCase.variableName, variable.value().get());
+    assertThat(CEL.createProgram(ast).eval(input)).isEqualTo(true);
+    CelAbstractSyntaxTree displayRoundTrip =
+        CEL.compile(testCase.variableName + " == " + variable.displayValue()).getAst();
+    assertThat(CEL.createProgram(displayRoundTrip).eval(input)).isEqualTo(true);
+  }
+
+  private enum InexactWitnessTestCase {
+    INT_OUT_OF_RANGE("type(dyn_var) == int && dyn_var > 9223372036854775807", "dyn_var"),
+    UINT_OUT_OF_RANGE("type(dyn_var) == uint && dyn_var > 18446744073709551615u", "dyn_var"),
+    NEGATIVE_UINT("type(dyn_var) == uint && dyn_var < 0u", "dyn_var"),
+    TIMESTAMP_OUT_OF_RANGE(
+        "type(dyn_var) == google.protobuf.Timestamp"
+            + " && dyn_var > google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}",
+        "dyn_var"),
+    SURROGATE_STRING(
+        "size(string_var) == 1 && string_var > '\\ud7ff' && string_var < '\\ue000'", "string_var"),
+    NON_ASCII_BYTES("by == b'\\xc3\\xa9'", "by"),
+    LIST_PAST_UNROLL_LIMIT("size(int_list) == 6", "int_list"),
+    MAP_PAST_UNROLL_LIMIT("size(string_int_map) == 6", "string_int_map"),
+    LIST_WITH_INEXACT_ELEMENT(
+        "size(dyn_list) == 1 && type(dyn_list[0]) == int && dyn_list[0] > 9223372036854775807",
+        "dyn_list"),
+    MAP_WITH_INEXACT_KEY(
+        "size(dyn_int_map) == 1"
+            + " && dyn_int_map.exists(k, type(k) == int && k > 9223372036854775807)",
+        "dyn_int_map"),
+    MAP_WITH_INEXACT_VALUE(
+        "size(string_dyn_map) == 1 && type(string_dyn_map['a']) == int"
+            + " && string_dyn_map['a'] > 9223372036854775807",
+        "string_dyn_map"),
+    OPTIONAL_WITH_INEXACT_VALUE(
+        "opt_dyn_var.hasValue() && type(opt_dyn_var.value()) == int"
+            + " && opt_dyn_var.value() > 9223372036854775807",
+        "opt_dyn_var");
+
+    private final String expr;
+    private final String variableName;
+
+    InexactWitnessTestCase(String expr, String variableName) {
+      this.expr = expr;
+      this.variableName = variableName;
+    }
+  }
+
+  @Test
+  public void isSatisfiable_noExactRuntimeValue_witnessValueEmpty(
+      @TestParameter InexactWitnessTestCase testCase) throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.witness().get().variables().get(testCase.variableName).value()).isEmpty();
+  }
+
+  // A map value in the model, as its key sequence and its present keys.
+  private enum InexactMapTestCase {
+    DUPLICATE_KEY(ImmutableList.of("a", "a"), ImmutableList.of("a")),
+    ABSENT_KEY(ImmutableList.of("a", "b"), ImmutableList.of("a")),
+    PRESENT_KEY_NOT_IN_SEQUENCE(ImmutableList.of(), ImmutableList.of("a")),
+    // Entries past the unroll limit (5) may violate the declared type.
+    PAST_UNROLL_LIMIT(
+        ImmutableList.of("a", "b", "c", "d", "e", "f"),
+        ImmutableList.of("a", "b", "c", "d", "e", "f"));
+
+    private final ImmutableList<String> keySequence;
+    private final ImmutableList<String> presentKeys;
+
+    InexactMapTestCase(ImmutableList<String> keySequence, ImmutableList<String> presentKeys) {
+      this.keySequence = keySequence;
+      this.presentKeys = presentKeys;
+    }
+  }
+
+  @Test
+  @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
+  public void generateWitness_mapWithoutExactValue_valueEmpty(
+      @TestParameter InexactMapTestCase testCase) {
+    try (Context ctx = new Context()) {
+      CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx, /* parameterizeUnknowns= */ false);
+      Expr<?> map = ctx.mkConst("map", typeSystem.celValueSort());
+      Expr<?> mapRef = typeSystem.getMapRef(map);
+      SeqExpr keys = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));
+      for (String key : testCase.keySequence) {
+        keys = ctx.mkConcat(keys, ctx.mkUnit(typeSystem.mkString(key)));
+      }
+      ArrayExpr presence = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse());
+      for (String key : testCase.presentKeys) {
+        presence = ctx.mkStore(presence, (Expr) typeSystem.mkString(key), ctx.mkTrue());
+      }
+      Solver solver = ctx.mkSolver();
+      solver.add(typeSystem.isMap(map));
+      solver.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keys));
+      solver.add(ctx.mkEq(typeSystem.getMapPresence(mapRef), presence));
+      assertThat(solver.check()).isEqualTo(Status.SATISFIABLE);
+
+      CelWitness witness =
+          CelZ3CounterexampleGenerator.generate(
+              ctx,
+              typeSystem,
+              solver.getModel(),
+              /* comprehensionUnrollLimit= */ 5,
+              ImmutableSet.of(map));
+
+      assertThat(witness.variables().get("map").value()).isEmpty();
+    }
+  }
+
+  @Test
+  public void isSatisfiable_listAtDisplayLimit_displaysAllElements() throws Exception {
+    String list =
+        IntStream.rangeClosed(1, 15).mapToObj(Integer::toString).collect(joining(", ", "[", "]"));
+    CelAbstractSyntaxTree ast = CEL.compile("int_list == " + list).getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.message()).endsWith("int_list = " + list);
+  }
+
+  @Test
+  public void isSatisfiable_listPastDisplayLimit_elidesRemainingElements() throws Exception {
+    CelVerifier verifier =
+        CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(16).build();
+    String list =
+        IntStream.rangeClosed(1, 16).mapToObj(Integer::toString).collect(joining(", ", "[", "]"));
+    CelAbstractSyntaxTree ast = CEL.compile("int_list == " + list).getAst();
+
+    CelVerificationResult result = verifier.isSatisfiable(ast);
+
+    assertThat(result.message())
+        .endsWith(
+            "int_list = "
+                + IntStream.rangeClosed(1, 15)
+                    .mapToObj(Integer::toString)
+                    .collect(joining(", ", "[", ", ... (1 more elements)]")));
+  }
+
   @Test
   public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception {
     CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst();
@@ -742,6 +942,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 +1181,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 +1249,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 {
@@ -1059,6 +1264,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown(
 
     assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED);
     assertThat(result.message()).contains("x = Unknown");
+    assertThat(result.witness().get().variables().get("x").value()).isEmpty();
   }
 
   @Test
@@ -1456,12 +1662,12 @@ private enum IsAlwaysTrueViolationTestCase {
         "dur != dur",
         "Condition is not always true\\.",
         "Counterexample input:",
-        "dur = duration\\('-?\\d+s'\\)"),
+        "dur = duration\\(\"-?\\d+s\"\\)"),
     TIMESTAMP_VARIABLE_COUNTEREXAMPLE(
         "ts != ts",
         "Condition is not always true\\.",
         "Counterexample input:",
-        "ts = timestamp\\(-?\\d+\\)"),
+        "ts = timestamp\\(\"[^\"]+\"\\)"),
     UNINTERPRETED_CONVERSION_NULL_FAILS_WITH_ERRORS(
         "string(null) == string(null)", "Condition is not always true\\."),
     LAW_OF_EXCLUDED_MIDDLE_FAILS_WITH_ERRORS(
@@ -1501,7 +1707,7 @@ private enum IsAlwaysTrueViolationTestCase {
         "opt_dyn_var.hasValue() ? type(opt_dyn_var.value()) == int : true",
         "Condition is not always true\\.",
         "Counterexample input:",
-        "opt_dyn_var = optional\\(Unknown\\)"),
+        "opt_dyn_var = optional\\.of\\(Unknown\\)"),
     OPTIONAL_ENTRY_DYN_VAR_TYPE_MISMATCH(
         "[?dyn_var] == [?dyn_var] ? true : true",
         "Condition is not always true\\.",
@@ -1569,6 +1775,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",
@@ -1619,7 +1831,7 @@ private enum IsAlwaysTrueViolationTestCase {
         "request == request",
         "Condition is not always true\\.",
         "Counterexample input:",
-        "request = NaN"),
+        "request = double\\(\"NaN\"\\)"),
     CROSS_TYPE_NUMERIC_EQUALITY_APPROXIMATION_VIOLATION(
         "dyn_var == 1.0",
         "Condition is not always true\\.",
@@ -2594,9 +2806,9 @@ private enum CounterexampleFormatTestCase {
         "role == \"user\"",
         ImmutableList.of("role = \"admin\"", "role = \"user\"")),
     DOUBLE("d == 1.5", "d == 2.5", ImmutableList.of("d = 1\\.5", "d = 2\\.5")),
-    DOUBLE_NAN("d != d", "false", ImmutableList.of("d = NaN")),
-    DOUBLE_INF("d == (1.0 / 0.0)", "false", ImmutableList.of("d = Infinity")),
-    DOUBLE_NEG_INF("d == (-1.0 / 0.0)", "false", ImmutableList.of("d = -Infinity")),
+    DOUBLE_NAN("d != d", "false", ImmutableList.of("d = double\\(\"NaN\"\\)")),
+    DOUBLE_INF("d == (1.0 / 0.0)", "false", ImmutableList.of("d = double\\(\"Infinity\"\\)")),
+    DOUBLE_NEG_INF("d == (-1.0 / 0.0)", "false", ImmutableList.of("d = double\\(\"-Infinity\"\\)")),
     DOUBLE_NEG_ZERO("d == 0.0 && 1.0 / d == (-1.0 / 0.0)", "false", ImmutableList.of("d = -0\\.0")),
     DOUBLE_POS_ZERO("d == 0.0 && 1.0 / d == (1.0 / 0.0)", "false", ImmutableList.of("d = 0\\.0")),
     UINT("u == 443u", "u == 80u", ImmutableList.of("u = 443u", "u = 80u")),
diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java
index 31e7ec5b8..31432ba3f 100644
--- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java
@@ -231,7 +231,7 @@ public void repl_durationSatisfyingInputFormat() throws Exception {
         runReplWithCommands(":var dur duration", "timestamp(100) - timestamp(50) == dur", ":quit");
 
     assertThat(output[0]).contains("[VERIFIED]");
-    assertThat(output[0]).contains("dur = duration('50s')");
+    assertThat(output[0]).contains("dur = duration(\"50s\")");
     assertThat(output[1]).isEmpty();
   }