diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc index c32716286d6..9332fb07c38 100644 --- a/regression/cbmc/Array_operations1/test.desc +++ b/regression/cbmc/Array_operations1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=10$ diff --git a/regression/cbmc/Float-equality1/test_no_equality.desc b/regression/cbmc/Float-equality1/test_no_equality.desc index fef87fd5cb3..67cb3bf2767 100644 --- a/regression/cbmc/Float-equality1/test_no_equality.desc +++ b/regression/cbmc/Float-equality1/test_no_equality.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/array-cell-sensitivity7/test_execution.desc b/regression/cbmc/array-cell-sensitivity7/test_execution.desc index 62502389e48..4e577438df9 100644 --- a/regression/cbmc/array-cell-sensitivity7/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity7/test_execution.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/array-cell-sensitivity8/test_execution.desc b/regression/cbmc/array-cell-sensitivity8/test_execution.desc index 96db1c25647..6cbd3a308e8 100644 --- a/regression/cbmc/array-cell-sensitivity8/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity8/test_execution.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/byte_update14/test.desc b/regression/cbmc/byte_update14/test.desc index 8ae3cc84473..99e319ce543 100644 --- a/regression/cbmc/byte_update14/test.desc +++ b/regression/cbmc/byte_update14/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc index de9fedec0a0..60be5f3c51c 100644 --- a/regression/cbmc/compact-trace/test.desc +++ b/regression/cbmc/compact-trace/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --compact-trace activate-multi-line-match diff --git a/regression/cbmc/gcc_vector3/test.desc b/regression/cbmc/gcc_vector3/test.desc index 39d9265e8a7..9efefbc7362 100644 --- a/regression/cbmc/gcc_vector3/test.desc +++ b/regression/cbmc/gcc_vector3/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/json-interface1/test_wrong_flag.desc b/regression/cbmc/json-interface1/test_wrong_flag.desc index b75ff5551e7..b1210068e2e 100644 --- a/regression/cbmc/json-interface1/test_wrong_flag.desc +++ b/regression/cbmc/json-interface1/test_wrong_flag.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE --json-interface < test_wrong_flag.json ^EXIT=6$ diff --git a/regression/cbmc/json-interface1/test_wrong_option.desc b/regression/cbmc/json-interface1/test_wrong_option.desc index 6c799c51262..c1b57e8574b 100644 --- a/regression/cbmc/json-interface1/test_wrong_option.desc +++ b/regression/cbmc/json-interface1/test_wrong_option.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE --json-interface < test_wrong_option.json ^EXIT=6$ diff --git a/regression/cbmc/null6/test.desc b/regression/cbmc/null6/test.desc index b67aae7833b..b312cea5fe3 100644 --- a/regression/cbmc/null6/test.desc +++ b/regression/cbmc/null6/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=10$ diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index b188c0a0282..ab75c22cd93 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/regression/cbmc/pointer-primitive-check-01/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-primitive-check ^EXIT=10$ diff --git a/regression/cbmc/pointer-primitive-check-04/test.desc b/regression/cbmc/pointer-primitive-check-04/test.desc index b9dbbbb6893..dde92a4b2ab 100644 --- a/regression/cbmc/pointer-primitive-check-04/test.desc +++ b/regression/cbmc/pointer-primitive-check-04/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-primitive-check ^EXIT=10$ diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc index 6270581f4fd..eceab4a2d07 100644 --- a/regression/cbmc/stack-trace/test.desc +++ b/regression/cbmc/stack-trace/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --stack-trace activate-multi-line-match diff --git a/regression/cbmc/union15/test.desc b/regression/cbmc/union15/test.desc index 39d9265e8a7..9efefbc7362 100644 --- a/regression/cbmc/union15/test.desc +++ b/regression/cbmc/union15/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/union6/test.desc b/regression/cbmc/union6/test.desc index 7c7e749235e..0a5f3bc705f 100644 --- a/regression/cbmc/union6/test.desc +++ b/regression/cbmc/union6/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc index 58448e0655b..6450a89940a 100644 --- a/regression/cbmc/union7/test.desc +++ b/regression/cbmc/union7/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/va_list2/test.desc b/regression/cbmc/va_list2/test.desc index 39d9265e8a7..9efefbc7362 100644 --- a/regression/cbmc/va_list2/test.desc +++ b/regression/cbmc/va_list2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/variable-access-to-constant-array/test.desc b/regression/cbmc/variable-access-to-constant-array/test.desc index 7fa81e26cff..212fd7b6674 100644 --- a/regression/cbmc/variable-access-to-constant-array/test.desc +++ b/regression/cbmc/variable-access-to-constant-array/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=10$ diff --git a/regression/cbmc/void_pointer4/test.desc b/regression/cbmc/void_pointer4/test.desc index 59d65ddf9f7..6de79559914 100644 --- a/regression/cbmc/void_pointer4/test.desc +++ b/regression/cbmc/void_pointer4/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=10$