From e12861071152231ab75909b0489705135b13fc4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Sep 2014 10:29:55 -0700 Subject: [PATCH] chore(tests): use option -t 100000 to speedup tests --- src/shell/CMakeLists.txt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 4718d0a07..47d781c4e 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -44,7 +44,7 @@ FOREACH(T ${LEANRUNTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) ENDFOREACH(T) if("${MULTI_THREAD}" MATCHES "ON") @@ -54,7 +54,7 @@ FOREACH(T ${LEANITTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanittest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) ENDFOREACH(T) endif() @@ -64,7 +64,7 @@ FOREACH(T ${LEANSLOWTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanslowtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive") ENDFOREACH(T)