Run working cbmc-primitive regressions with SMT2

Adding all cbmc-primitive regression tests that are now passing as the
necessary support has been added. Namely the regression tests using
dynamic memory, byte_extract_exprt and byte_update_exprt are now
supported and have been added.

Author: Enrico Steffinlongo

regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$

regression/cbmc-primitives/dynamic-object-02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 negated_exists.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/same-object-03/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$