Allow double(string) to return NaN

PiperOrigin-RevId: 1004358780

Author: l46kok

verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java

@@ -234,9 +234,12 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions
           break;
         case DOUBLE:
           sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res)));
-          sink.accept(
-              ctx.mkImplies(
-                  typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))));
+          // Numeric conversions never yield NaN, but parsing does (double('NaN')).
+          if (conversion != Conversions.STRING_TO_DOUBLE) {
+            sink.accept(
+                ctx.mkImplies(
+                    typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))));
+          }
           break;
         case STRING:
           sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res)));

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

@@ -365,6 +365,7 @@ private enum IsSatisfiableInconclusiveTestCase {
     APPROXIMATED_RANGE("int('123') > 100 && int('123') < 200"),
     APPROXIMATED_BRANCHING("int('123') == 123 ? x > 5 : false"),
     APPROXIMATED_STRING_TO_INT_CONSTRAINED("string_var == 'abc' && int(string_var) == 5"),
+    APPROXIMATED_STRING_TO_DOUBLE_NAN("double('NaN') != double('NaN')"),
     // int('x') errors at runtime, so type() of an approximate argument is approximate too.
     APPROXIMATED_TYPE_OF_CONVERSION("type(int('1')) == int"),
     APPROXIMATED_TYPE_OF_CONSTRAINED_CONVERSION(
@@ -473,6 +474,7 @@ private enum IsUnsatisfiableTestCase {
     CONTRADICTORY_TYPES_FOR_DYNAMIC_VARIABLE("unknown_var + 1 == 2 && unknown_var[0] == 1"),
     TYPE_CONVERSION_UNSATISFIABLE_STRING_TO_INT("type(int('1')) == string"),
     TYPE_CONVERSION_UNSATISFIABLE_DOUBLE_TO_STRING("type(string(1.5)) == int"),
+    TYPE_CONVERSION_UNSATISFIABLE_INT_TO_DOUBLE_NAN("double(x) != double(x)"),
     EMPTY_MAP_SIZE_NOT_ZERO("size({}) != 0"),
     TIMESTAMP_INEQUALITY_CONTRADICTION(
         "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"),