added test for uninterpreted functions

Author: Daniel Kroening

regression/cbmc/uninterpreted_function/uf2.c

@@ -0,0 +1,12 @@
+int __CPROVER_uninterpreted_f(int, int);
+
+main()
+{
+  int a, b;
+
+  int inst1 = __CPROVER_uninterpreted_f(1, a);
+  int inst2 = __CPROVER_uninterpreted_f(1, b);
+
+  if(a == b)
+    __CPROVER_assert(inst1 == inst2, "functional consistency");
+}

regression/cbmc/uninterpreted_function/uf2.desc

@@ -0,0 +1,10 @@
+CORE
+uf2.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Basic test for an uninterpreted function.

scripts/delete_failing_smt2_solver_tests

@@ -75,6 +75,7 @@ rm struct7/test.desc
 rm trace-values/trace-values.desc
 rm trace_show_function_calls/test.desc
 rm uninterpreted_function/uf1.desc
+rm uninterpreted_function/uf2.desc
 rm union12/test.desc
 rm union6/test.desc
 rm union7/test.desc