Test for concretized string literal in trace

Checks that the string literal is present in the trace even if it is not
part of the decision. As a side-effect, this checks that the length is
properly assigned to the string, even if it cannot be retrieved from the
solver.

Author: Joel Allred

jbmc/regression/jbmc-strings/literal_length/test.class

@@ -0,0 +1,12 @@
+CORE
+test.class
+--function test.main --trace
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 6.* FAILURE$
+abc_constarray=\{ 'a', 'b', 'c' \}
+--
+--
+Check that the string literal used in the constructor is properly concretized
+in the trace even if it is not part of the equation.
+This is necessary for test generation.

jbmc/regression/jbmc-strings/literal_length/test.desc

@@ -0,0 +1,8 @@
+public class test
+{
+  public static void main()
+  {
+    String x = new String("abc");
+    assert false;
+  }
+}