Enable previously-failing test Linking7/member-name-mismatch

Now that value-set soundly simplifies member-of-cast-of-struct, this test works as expected.
This also improves the specificity of the two tests in this directory.

This is disabled under SMT2 for the same reason as the existing test.desc -- it involves a
struct-to-struct cast, which SMT2's `convert_typecast` doesn't handle yet.

Author: smowton

regression/cbmc/Linking7/member-name-mismatch.desc

@@ -1,11 +1,11 @@
-KNOWNBUG
+CORE
 main.c
 module2.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.c == 41: FAILURE
 ^\*\* 1 of 2 failed
 --
 ^warning: ignoring
---
-This is either a bug in goto-symex or value_sett (where the invariant fails).

regression/cbmc/Linking7/test.desc

@@ -5,5 +5,7 @@ module.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 ^\*\* 1 of 2 failed
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.b == 41: FAILURE
 --
 ^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -36,6 +36,7 @@ rm Float6/test.desc
 rm Float8/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
+rm Linking7/member-name-mismatch.desc
 rm Malloc19/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc