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()
"""
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.
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(
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-"):
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('')
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')
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__":