Fix notStrictlyFalse semantics in verifier

PiperOrigin-RevId: 950241075

Author: l46kok

verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

@@ -848,8 +848,8 @@ private TranslatedValue translateConditional(
   private TranslatedValue translateNotStrictlyFalse(List<TranslatedValue> args) {
     TranslatedValue arg = args.get(0);
     BoolExpr isFalse = ctx.mkAnd(arg.isZ3Bool(), ctx.mkNot((BoolExpr) arg.unwrapZ3Bool()));
-    return TranslatedValue.propagateStrict(
-        ctx, typeSystem, typeSystem.wrapBool(ctx.mkNot(isFalse)), arg);
+    return TranslatedValue.create(
+        typeSystem.wrapBool(ctx.mkNot(isFalse)), typeSystem, arg.isApproximate());
   }
 
   private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractSyntaxTree ast) {

verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java

@@ -303,6 +303,7 @@ private enum IsAlwaysTrueTestCase {
     UINT_ARITHMETIC_ZERO("0u + 0u == 0u"),
     MAP_COMPREHENSION("{1: 2, 3: 4}.all(k, k > 0)"),
     NESTED_COMPREHENSIONS("[1, 2].all(x, [3, 4].all(y, x < y || y <= x))"),
+    COMPREHENSION_EXISTS_UNKNOWN_INITIAL_STEP("[1, 2].exists(x, x == 1 ? unknown_var > 0 : true)"),
     CYCLIC_BIND_DOES_NOT_HANG("cel.bind(x, x, x) == x"),
     CEL_BIND_SHADOWING("cel.bind(x, 1, cel.bind(x, 2, x) + x) == 3"),
     CEL_BIND_TO_TRUE("cel.bind(x, true, !x) == false"),