diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index e4fd61a058f..b7181ece960 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/regression/cbmc/Quantifiers-not-exists/test.desc @@ -3,11 +3,11 @@ main.c ^\*\* Results:$ ^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$ -^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$ -^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$ -^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$ -^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$ -^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$ +^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.3\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.4\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.6\] assertion tmp_if_expr\$\d+: SUCCESS$ ^\*\* 0 of 6 failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 2c1c7dab05f..b588f1621aa 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -6,7 +6,7 @@ main.c ^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$ -^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$ +^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$ ^\*\* 0 of 5 failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index 1451871c4ec..ba904aec101 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -2,8 +2,8 @@ CORE main.c ^\*\* Results:$ -^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$ -^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$ +^\[main.assertion.1\] assertion tmp_if_expr(\$\d+)?: FAILURE$ +^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$ ^\*\* 1 of 2 failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index 9b90858ce5a..5ffe7f3fa78 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-2/test.desc @@ -3,10 +3,10 @@ main.c --function fun --cover branch ^\*\* 7 of 7 covered \(100.0%\)$ ^Test suite:$ -^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$ -^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ -^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$ -^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$ +^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index 2ea09c85011..a816cc3039a 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/regression/cbmc/pointer-function-parameters/test.desc @@ -3,9 +3,9 @@ main.c --function fun --cover branch ^\*\* 5 of 5 covered \(100\.0%\)$ ^Test suite:$ -^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ -^a=&tmp\$\d+!0, tmp\$\d+=4$ -^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$ +^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$ ^EXIT=0$ ^SIGNAL=0$ --