Make cbmc-incr-smt2 test patterns platform-agnostic

Not all platforms have 32-bit int, and the size of long int may be the
same as int.

Author: tautschnig

regression/cbmc-incr-smt2/arrays_traces/array_write.desc

@@ -3,7 +3,7 @@ array_write.c
 --trace
 Passing problem to incremental SMT2 solving
 ^Trace for main\.assertion\.2
-example_array\[\d{1,4}ll?\]=42
+example_array\[\d{1,4}l?l?\]=42
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/enums/enum_in_array.desc

@@ -4,9 +4,9 @@ enum_in_array.c
 Passing problem to incremental SMT2 solving
 line 18 Array at index 0 is V0, so this should fail: FAILURE
 i=0u \(00000000 00000000 00000000 00000000\)
-e\[0l+\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
-e\[1l+\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
-e\[2l+\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
+e\[0l*\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
+e\[1l*\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+e\[2l*\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc

@@ -4,13 +4,13 @@ test.c
 Starting Bounded Model Checking
 ^\(set-option :produce-models true\)$
 ^\(set-logic ALL\)$
-^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec 64\)\)$
+^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec \d+\)\)$
 ^Passing problem to incremental SMT2 solving via SMT2 incremental dry-run$
 ^\(define-fun B0 \(\) Bool true\)$
 ^\(define-fun B2 \(\) Bool \(not false\)\)$
 ^\(assert B2\)$
-^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 64\)\)\)$
-^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 64\)\)\)$
+^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 \d+\)\)\)$
+^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 \d+\)\)\)$
 ^\(check-sat\)$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/pointers/object_size.desc

@@ -5,9 +5,9 @@ line 12 Expected int sizes\.: SUCCESS
 line 13 Size is always 2\. \(Can be disproved\.\): FAILURE
 line 14 Size is always 4\. \(Can be disproved\.\): FAILURE
 line 16 Size of NULL\.: FAILURE
-size=2ul
-size=4ul
-null_size=0ul
+size=2ul*
+size=4ul*
+null_size=0ul*
 ^EXIT=10$
 ^SIGNAL=0$
 --