Replace new-smt-backend tag with inverted no-new-smt tag

This makes it somewhat more straight forward to find tests where the new
smt backend is not currently run. It also helps with testing with the
new smt support on new tests by default.

The tags in the `.desc` files are flipped using a one-off python script.
I am including it here below in the commit message body rather than in a
separate commit as it is intended for a singular usage and it may be
more straight forward to review the script than the `.desc` file
updates.

```
import os
import sys
from pathlib import Path

def usage():
    print("Usage " + sys.argv[0] + " [directory]")
    print("Processes all test tags within a [directory].")

def update_file(file_path) -> bool:
    with file_path.open("rt") as file:
        lines = file.readlines()
    if len(lines) == 0:
        print("File " + file_path + " is empty")
        return False
    if "CORE" not in lines[0]:
        return False
    if " new-smt-backend" not in lines[0] and " no-new-smt" not in lines[0]:
        lines[0] = lines[0].replace("\n", " no-new-smt\n")
    else:
        lines[0] = lines[0].replace(" new-smt-backend", "")
    with file_path.open("wt") as file:
        file.writelines(lines)
    return True

def main() -> int:
    if len(sys.argv) != 2:
        usage()
        return os.EX_USAGE
    directory = Path(sys.argv[1])
    if not directory.is_absolute():
        directory = Path(os.getcwd()) / directory
    print("Running against directory " + os.fspath(directory))
    if not directory.is_dir():
        print("Error - This is not a directory.")
        return os.EX_IOERR
    files = directory.glob("*/*.desc")
    tests_updated = 0
    for file_path in files:
        if not file_path.is_file():
            print(os.fspath(file_path) + " was expected to be a file but is "
                                         "not a file")
            continue
        if update_file(file_path):
            tests_updated += 1
    if tests_updated == 0:
        print("Error - No tests updated")
        return os.EX_NOTFOUND
    print(str(tests_updated) + " tests updated.")
    return os.EX_OK

if __name__ == '__main__':
    sys.exit(main())
```

Author: thomasspriggs

regression/book-examples/CMakeLists.txt

@@ -30,11 +30,11 @@ add_test_pl_profile(
     "CORE"
 )
 
-# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+# If `-I` (include flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "book-examples-new-smt-backend"
   "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-  "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
+  "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )
 

regression/book-examples/Makefile

@@ -31,7 +31,7 @@ test-paths-lifo:
 
 test-new-smt-backend:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
-					  -I new-smt-backend \
+					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 
 tests.log: ../test.pl test

regression/book-examples/abs/C1.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs
 ^EXIT=0$

regression/book-examples/abs/C13.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs --signed-overflow-check --show-goto-functions
 ^EXIT=0$

regression/book-examples/abs/C2.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs --signed-overflow-check
 ^EXIT=10$

regression/book-examples/abs/C3.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 abs.c
 --function abs --signed-overflow-check --trace
 ^EXIT=10$

regression/book-examples/binsearch/C4.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 binsearch.c
 --function binsearch --unwind 6 --bounds-check --unwinding-assertions
 ^EXIT=0$

regression/book-examples/lock/depth.desc

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

regression/book-examples/lock/unwind1.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 lock.c
 --unwind 1
 ^EXIT=0$

regression/book-examples/lock/unwind2.desc

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

regression/book-examples/login/C5.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --bounds-check
 ^EXIT=10$

regression/book-examples/login/C6.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --show-properties --bounds-check --pointer-check
 ^EXIT=0$

regression/book-examples/login/C7.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --show-vcc --bounds-check --pointer-check
 ^EXIT=0$

regression/book-examples/login/C8.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --bounds-check --pointer-check
 ^EXIT=10$

regression/book-examples/login/C9.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 login.c
 --unwind 20 --bounds-check --pointer-check --trace
 ^EXIT=10$

regression/book-examples/pid/C11.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-new-smt
 pid.c
 --cover mcdc --unwind 6
 ^EXIT=0$

regression/cbmc-primitives/CMakeLists.txt

@@ -5,11 +5,11 @@ if(Z3_EXISTS)
         "$<TARGET_FILE:cbmc>"
     )
 
-    # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+    # If `-X` (include flag) is passed, test.pl will exclude the tests matching the label following it.
     add_test_pl_profile(
             "cbmc-primitives-new-smt-backend"
             "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-            "-I;new-smt-backend;-s;new-smt-backend"
+            "-X;no-new-smt;-s;new-smt-backend"
             "CORE"
     )
 else()

regression/cbmc-primitives/Makefile

@@ -4,7 +4,7 @@ test:
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 test.smt2_incr:
-	@../test.pl -e -p -I new-smt-backend -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc

regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc

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

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc

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

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

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

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

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

regression/cbmc-primitives/exists_assume_6231/test.desc

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

regression/cbmc-primitives/exists_assume_6231/test2.desc

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

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-new-smt
 invalid_index_range.c
 --pointer-check
 ^EXIT=10$

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

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

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend no-new-smt
 smt_missing_range_check.c
 --pointer-check -z3
 ^EXIT=10$

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

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

regression/cbmc-primitives/forall_6231_1/test.desc

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

regression/cbmc-primitives/forall_6231_2/test.desc

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

regression/cbmc-primitives/forall_6231_3/test.desc

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

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

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

regression/cbmc-primitives/forall_6231_4/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 test.c
 --div-by-zero-check
 ^EXIT=10$

regression/cbmc-primitives/implication_statement_checks_1/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 --div-by-zero-check
 test.c
 ^EXIT=0$

regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc

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

regression/cbmc-primitives/pointer-offset-01/test.desc

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

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$

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

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

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc

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

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

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

regression/cbmc-primitives/r_w_ok_null/test.desc

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

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

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

regression/cbmc-primitives/r_w_ok_valid/test.desc

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

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

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

regression/cbmc-primitives/r_w_ok_valid_negated/test.desc

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

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

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

regression/cbmc-primitives/same-object-01/test.desc

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

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

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

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

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

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

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

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

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

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

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

regression/cbmc-primitives/same-object-04/test.desc

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

regression/cbmc/ACSL/operators.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-new-smt
 operators.c
 
 ^EXIT=0$

regression/cbmc/ACSL/quantifier-precedence.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 quantifier-precedence.c
 
 ^EXIT=0$

regression/cbmc/ASHR1/test.desc

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

regression/cbmc/Address_of1/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --stop-on-fail
 ^\[main\.assertion

regression/cbmc/Address_of2/test.desc

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

regression/cbmc/Anonymous_Struct1/test.desc

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

regression/cbmc/Anonymous_Struct2/test.desc

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

regression/cbmc/Anonymous_Struct3/test.desc

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

regression/cbmc/Array_Access1/test.desc

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

regression/cbmc/Array_Access2/test.desc

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