Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)

With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.

2 files changed, 28 insertions, 16 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a5bf3e819..441327b3a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2094,14 +2094,26 @@ add_custom_target(regress
 macro(cvc4_add_regression_test level file)
   add_test(${file}
     ${run_regress_script}
-    --cmake
     ${RUN_REGRESSION_ARGS}
     ${path_to_cvc4}/cvc4 ${CMAKE_CURRENT_LIST_DIR}/${file})
-  set_tests_properties(${file} PROPERTIES
-    LABELS "regress${level}"
-    SKIP_RETURN_CODE 77)
+  set_tests_properties(${file} PROPERTIES LABELS "regress${level}")
+
+  # For CMake 3.9.0 and newer, skipped tests do not count as a failure anymore:
+  # https://cmake.org/cmake/help/latest/release/3.9.html#other-changes
+  # This means that for newer versions, we can use the SKIP_RETURN_CODE to mark
+  # skipped tests as such.
+  if(NOT ${CMAKE_VERSION} VERSION_LESS "3.9.0")
+    set_tests_properties(${file} PROPERTIES SKIP_RETURN_CODE 77)
+  endif()
 endmacro()
 
+if(NOT ${CMAKE_VERSION} VERSION_LESS "3.9.0")
+  # For CMake 3.9.0 and newer, we want the regression script to return 77 for
+  # skipped tests, such that we can mark them as skipped. See the
+  # `cvc4_add_regression_test` macro for more details.
+  set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --use-skip-return-code)
+endif()
+
 foreach(file ${regress_0_tests})
   cvc4_add_regression_test(0 ${file})
 endforeach()
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 09ec8b7cf..759582afc 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -2,8 +2,8 @@
 """
 Usage:
 
-    run_regression.py [--enable-proof] [--with-lfsc] [--dump] [--cmake]
-        [wrapper] cvc4-binary
+    run_regression.py [--enable-proof] [--with-lfsc] [--dump]
+        [--use-skip-return-code] [wrapper] cvc4-binary
         [benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p]
 
 Runs benchmark and checks for correct exit status and output.
@@ -127,14 +127,14 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
     return (output.strip(), error.strip(), exit_status)
 
 
-def run_regression(unsat_cores, proofs, dump, cmake, wrapper, cvc4_binary,
-                   benchmark_path, timeout):
+def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
+                   cvc4_binary, benchmark_path, timeout):
     """Determines the expected output for a benchmark, runs CVC4 on it and then
     checks whether the output corresponds to the expected output. Optionally
     uses a wrapper `wrapper`, tests unsat cores (if unsat_cores is true),
     checks proofs (if proofs is true), or dumps a benchmark and uses that as
-    the input (if dump is true). `cmake` enables/disables CMake-specific
-    behavior."""
+    the input (if dump is true). `use_skip_return_code` enables/disables
+    returning 77 when a test is skipped."""
 
     if not os.access(cvc4_binary, os.X_OK):
         sys.exit(
@@ -234,7 +234,7 @@ def run_regression(unsat_cores, proofs, dump, cmake, wrapper, cvc4_binary,
         print(
             '1..0 # Skipped regression: unsat cores not supported without proof support'
         )
-        return (EXIT_SKIP if cmake else EXIT_OK)
+        return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
 
     for req_feature in requires:
         if req_feature.startswith("no-"):
@@ -242,11 +242,11 @@ def run_regression(unsat_cores, proofs, dump, cmake, wrapper, cvc4_binary,
             if inv_feature in cvc4_features:
                 print('1..0 # Skipped regression: not valid with {}'.format(
                     inv_feature))
-                return (EXIT_SKIP if cmake else EXIT_OK)
+                return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
         elif req_feature not in cvc4_features:
             print('1..0 # Skipped regression: {} not supported'.format(
                 req_feature))
-            return (EXIT_SKIP if cmake else EXIT_OK)
+            return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
 
     if not command_lines:
         command_lines.append('')
@@ -353,7 +353,7 @@ def main():
     parser.add_argument('--enable-proof', action='store_true')
     parser.add_argument('--with-lfsc', action='store_true')
     parser.add_argument('--dump', action='store_true')
-    parser.add_argument('--cmake', action='store_true')
+    parser.add_argument('--use-skip-return-code', action='store_true')
     parser.add_argument('wrapper', nargs='*')
     parser.add_argument('cvc4_binary')
     parser.add_argument('benchmark')
@@ -367,8 +367,8 @@ def main():
     timeout = float(os.getenv('TEST_TIMEOUT', 600.0))
 
     return run_regression(args.enable_proof, args.with_lfsc, args.dump,
-                          args.cmake, wrapper, cvc4_binary, args.benchmark,
-                          timeout)
+                          args.use_skip_return_code, wrapper, cvc4_binary,
+                          args.benchmark, timeout)
 
 
 if __name__ == "__main__":