diff --git a/regression/cbmc/Pointer1/test.desc b/regression/cbmc/Pointer1/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer1/test.desc +++ b/regression/cbmc/Pointer1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer10/test.desc b/regression/cbmc/Pointer10/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer10/test.desc +++ b/regression/cbmc/Pointer10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer11/test.desc b/regression/cbmc/Pointer11/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer11/test.desc +++ b/regression/cbmc/Pointer11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer12/test.desc b/regression/cbmc/Pointer12/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer12/test.desc +++ b/regression/cbmc/Pointer12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer14/test.desc b/regression/cbmc/Pointer14/test.desc index 350a589e4a6..706031b1df9 100644 --- a/regression/cbmc/Pointer14/test.desc +++ b/regression/cbmc/Pointer14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer15/test.desc b/regression/cbmc/Pointer15/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer15/test.desc +++ b/regression/cbmc/Pointer15/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer17/test.desc b/regression/cbmc/Pointer17/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer17/test.desc +++ b/regression/cbmc/Pointer17/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer18/full-slice.desc b/regression/cbmc/Pointer18/full-slice.desc index 37c7526ffee..f3b62857e9e 100644 --- a/regression/cbmc/Pointer18/full-slice.desc +++ b/regression/cbmc/Pointer18/full-slice.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 1 --no-unwinding-assertions --pointer-check --full-slice ^EXIT=0$ diff --git a/regression/cbmc/Pointer18/test.desc b/regression/cbmc/Pointer18/test.desc index 0b21ec028ac..ecf5b01e3d6 100644 --- a/regression/cbmc/Pointer18/test.desc +++ b/regression/cbmc/Pointer18/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 1 --no-unwinding-assertions --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer25/test.desc b/regression/cbmc/Pointer25/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer25/test.desc +++ b/regression/cbmc/Pointer25/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer26/test.desc b/regression/cbmc/Pointer26/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer26/test.desc +++ b/regression/cbmc/Pointer26/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer27/test.desc b/regression/cbmc/Pointer27/test.desc index 17695a197ac..3bb3ae685d6 100644 --- a/regression/cbmc/Pointer27/test.desc +++ b/regression/cbmc/Pointer27/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer29/test.desc b/regression/cbmc/Pointer29/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer29/test.desc +++ b/regression/cbmc/Pointer29/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer30/test.desc b/regression/cbmc/Pointer30/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer30/test.desc +++ b/regression/cbmc/Pointer30/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer6/test.desc b/regression/cbmc/Pointer6/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer6/test.desc +++ b/regression/cbmc/Pointer6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer7/test.desc b/regression/cbmc/Pointer7/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer7/test.desc +++ b/regression/cbmc/Pointer7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer8/test.desc b/regression/cbmc/Pointer8/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer8/test.desc +++ b/regression/cbmc/Pointer8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer9/test.desc b/regression/cbmc/Pointer9/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer9/test.desc +++ b/regression/cbmc/Pointer9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic10/test.desc b/regression/cbmc/Pointer_Arithmetic10/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic10/test.desc +++ b/regression/cbmc/Pointer_Arithmetic10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic12/test.desc b/regression/cbmc/Pointer_Arithmetic12/test.desc index b3a154d150b..59cb00eeef9 100644 --- a/regression/cbmc/Pointer_Arithmetic12/test.desc +++ b/regression/cbmc/Pointer_Arithmetic12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --32 --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic14/test.desc b/regression/cbmc/Pointer_Arithmetic14/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer_Arithmetic14/test.desc +++ b/regression/cbmc/Pointer_Arithmetic14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic15/test.desc b/regression/cbmc/Pointer_Arithmetic15/test.desc index 95f0fe0bf7f..1c32ff1427b 100644 --- a/regression/cbmc/Pointer_Arithmetic15/test.desc +++ b/regression/cbmc/Pointer_Arithmetic15/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Pointer_Arithmetic17/test.desc b/regression/cbmc/Pointer_Arithmetic17/test.desc index c50a02a2204..ed1cdd73006 100644 --- a/regression/cbmc/Pointer_Arithmetic17/test.desc +++ b/regression/cbmc/Pointer_Arithmetic17/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic19/test.desc b/regression/cbmc/Pointer_Arithmetic19/test.desc index 86a2eb68229..0799414e2cd 100644 --- a/regression/cbmc/Pointer_Arithmetic19/test.desc +++ b/regression/cbmc/Pointer_Arithmetic19/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --program-only ASSERT\(\{ 42, 43 \}\[POINTER_OFFSET\(p!0@1#2\) / \d+l*\] == 43\)$ diff --git a/regression/cbmc/Pointer_Arithmetic2/test.desc b/regression/cbmc/Pointer_Arithmetic2/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic2/test.desc +++ b/regression/cbmc/Pointer_Arithmetic2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic3/test.desc b/regression/cbmc/Pointer_Arithmetic3/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic3/test.desc +++ b/regression/cbmc/Pointer_Arithmetic3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic4/test.desc b/regression/cbmc/Pointer_Arithmetic4/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic4/test.desc +++ b/regression/cbmc/Pointer_Arithmetic4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic5/test.desc b/regression/cbmc/Pointer_Arithmetic5/test.desc index f9c919bbdc2..4861061b8e0 100644 --- a/regression/cbmc/Pointer_Arithmetic5/test.desc +++ b/regression/cbmc/Pointer_Arithmetic5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check --function f ^EXIT=10$ diff --git a/regression/cbmc/Pointer_Arithmetic6/test.desc b/regression/cbmc/Pointer_Arithmetic6/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic6/test.desc +++ b/regression/cbmc/Pointer_Arithmetic6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic7/test.desc b/regression/cbmc/Pointer_Arithmetic7/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic7/test.desc +++ b/regression/cbmc/Pointer_Arithmetic7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic9/test.desc b/regression/cbmc/Pointer_Arithmetic9/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic9/test.desc +++ b/regression/cbmc/Pointer_Arithmetic9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Assume1/test.desc b/regression/cbmc/Pointer_Assume1/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Pointer_Assume1/test.desc +++ b/regression/cbmc/Pointer_Assume1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array5/test.desc b/regression/cbmc/Pointer_array5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer_array5/test.desc +++ b/regression/cbmc/Pointer_array5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract1/test.desc b/regression/cbmc/Pointer_byte_extract1/test.desc index 12fc8ce06e1..ad10409bb6f 100644 --- a/regression/cbmc/Pointer_byte_extract1/test.desc +++ b/regression/cbmc/Pointer_byte_extract1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract3/test.desc b/regression/cbmc/Pointer_byte_extract3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer_byte_extract3/test.desc +++ b/regression/cbmc/Pointer_byte_extract3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract6/test.desc b/regression/cbmc/Pointer_byte_extract6/test.desc index 466da18b2b5..00550a6e62f 100644 --- a/regression/cbmc/Pointer_byte_extract6/test.desc +++ b/regression/cbmc/Pointer_byte_extract6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc index 0570ab7aba7..5a2330a5aad 100644 --- a/regression/cbmc/Pointer_byte_extract9/test.desc +++ b/regression/cbmc/Pointer_byte_extract9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index af678d78121..a38989b4d0d 100644 --- a/regression/cbmc/pointer-overflow1/test.desc +++ b/regression/cbmc/pointer-overflow1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-overflow-check --unsigned-overflow-check ^EXIT=10$ diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc index 29f2ee235f8..2f2365bd2fb 100644 --- a/regression/cbmc/pointer-overflow2/test.desc +++ b/regression/cbmc/pointer-overflow2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-overflow-check ^EXIT=0$ diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc index a82964bcaa3..71c50f53cf1 100644 --- a/regression/cbmc/pointer-overflow3/test.desc +++ b/regression/cbmc/pointer-overflow3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-overflow-check ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE diff --git a/regression/cbmc/pointer-overflow4/test.desc b/regression/cbmc/pointer-overflow4/test.desc index 0c24bc9b6df..9db69c89e6c 100644 --- a/regression/cbmc/pointer-overflow4/test.desc +++ b/regression/cbmc/pointer-overflow4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-overflow-check ^\[main.overflow.1\] line 10 arithmetic overflow on signed \* in (0x)?[0-9a-fA-F]+l* \* \(signed (long (long )?)?int\)4ul*: FAILURE$