Regression tests for Character.getNumericValue

This used to make CBMC crash but is now evaluated correctly.

Author: romainbrenguier

regression/strings/CharacterGetNumericValue/test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test.java line 8 .* SUCCESS$
+assertion at file test.java line 10 .* FAILURE$
+--
+^warning: ignoring

regression/strings/CharacterGetNumericValue/test.desc

@@ -0,0 +1,12 @@
+public class test
+{
+
+    public static void main(String[] args)
+    {
+        char c = 'a';
+        if(args.length>1)
+            assert Character.getNumericValue(c) == 10;
+        else
+            assert Character.getNumericValue(c) != 10;
+    }
+}