From fe5a65e26b89a14b09ed15fd5eb4c8a1e5ff6340 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 6 Aug 2024 10:53:50 -0700 Subject: [PATCH] Reorganize issues in C++ API tests. (#11106) --- test/api/c/CMakeLists.txt | 103 +++++--------------- test/api/c/issues/CMakeLists.txt | 80 +++++++++++++++ test/api/c/{ => issues}/issue11069.c | 0 test/api/cpp/CMakeLists.txt | 93 ++++-------------- test/api/cpp/issues/CMakeLists.txt | 79 +++++++++++++++ test/api/cpp/{ => issues}/issue11069.cpp | 0 test/api/cpp/{ => issues}/issue4889.cpp | 0 test/api/cpp/{ => issues}/issue5074.cpp | 0 test/api/cpp/{ => issues}/issue5893.cpp | 0 test/api/cpp/{ => issues}/issue6111.cpp | 0 test/api/cpp/{ => issues}/issue7000.cpp | 0 test/api/cpp/{ => issues}/proj-issue306.cpp | 0 test/api/cpp/{ => issues}/proj-issue308.cpp | 0 test/api/cpp/{ => issues}/proj-issue334.cpp | 0 test/api/cpp/{ => issues}/proj-issue337.cpp | 0 test/api/cpp/{ => issues}/proj-issue344.cpp | 0 test/api/cpp/{ => issues}/proj-issue345.cpp | 1 - test/api/cpp/{ => issues}/proj-issue373.cpp | 0 test/api/cpp/{ => issues}/proj-issue377.cpp | 0 test/api/cpp/{ => issues}/proj-issue378.cpp | 0 test/api/cpp/{ => issues}/proj-issue379.cpp | 0 test/api/cpp/{ => issues}/proj-issue381.cpp | 0 test/api/cpp/{ => issues}/proj-issue382.cpp | 0 test/api/cpp/{ => issues}/proj-issue383.cpp | 0 test/api/cpp/{ => issues}/proj-issue386.cpp | 0 test/api/cpp/{ => issues}/proj-issue388.cpp | 4 +- test/api/cpp/{ => issues}/proj-issue395.cpp | 2 +- test/api/cpp/{ => issues}/proj-issue399.cpp | 0 test/api/cpp/{ => issues}/proj-issue413.cpp | 0 test/api/cpp/{ => issues}/proj-issue414.cpp | 0 test/api/cpp/{ => issues}/proj-issue416.cpp | 0 test/api/cpp/{ => issues}/proj-issue418.cpp | 3 +- test/api/cpp/{ => issues}/proj-issue420.cpp | 0 test/api/cpp/{ => issues}/proj-issue421.cpp | 0 test/api/cpp/{ => issues}/proj-issue422.cpp | 0 test/api/cpp/{ => issues}/proj-issue423.cpp | 0 test/api/cpp/{ => issues}/proj-issue426.cpp | 0 test/api/cpp/{ => issues}/proj-issue429.cpp | 0 test/api/cpp/{ => issues}/proj-issue431.cpp | 0 test/api/cpp/{ => issues}/proj-issue434.cpp | 0 test/api/cpp/{ => issues}/proj-issue435.cpp | 0 test/api/cpp/{ => issues}/proj-issue436.cpp | 0 test/api/cpp/{ => issues}/proj-issue440.cpp | 0 test/api/cpp/{ => issues}/proj-issue445.cpp | 0 test/api/cpp/{ => issues}/proj-issue455.cpp | 3 +- test/api/cpp/{ => issues}/proj-issue484.cpp | 0 test/api/cpp/{ => issues}/proj-issue538.cpp | 0 test/api/cpp/{ => issues}/proj-issue567.cpp | 0 test/api/cpp/{ => issues}/proj-issue570.cpp | 0 test/api/cpp/{ => issues}/proj-issue573.cpp | 0 test/api/cpp/{ => issues}/proj-issue574.cpp | 0 test/api/cpp/{ => issues}/proj-issue575.cpp | 0 test/api/cpp/{ => issues}/proj-issue576.cpp | 0 test/api/cpp/{ => issues}/proj-issue580.cpp | 0 test/api/cpp/{ => issues}/proj-issue581.cpp | 0 test/api/cpp/{ => issues}/proj-issue587.cpp | 0 test/api/cpp/{ => issues}/proj-issue600.cpp | 0 test/api/cpp/{ => issues}/proj-issue611.cpp | 0 test/api/cpp/{ => issues}/proj-issue612.cpp | 0 test/api/cpp/{ => issues}/proj-issue618.cpp | 0 test/api/cpp/{ => issues}/proj-issue621.cpp | 0 test/api/cpp/{ => issues}/proj-issue644.cpp | 0 test/api/cpp/{ => issues}/proj-issue646.cpp | 0 test/api/cpp/{ => issues}/proj-issue652.cpp | 0 test/api/cpp/{ => issues}/proj-issue654.cpp | 0 test/api/cpp/{ => issues}/proj-issue655.cpp | 0 test/api/cpp/{ => issues}/proj-issue656.cpp | 0 test/api/cpp/{ => issues}/proj-issue657.cpp | 0 test/api/cpp/{ => issues}/proj-issue666.cpp | 0 69 files changed, 205 insertions(+), 163 deletions(-) create mode 100644 test/api/c/issues/CMakeLists.txt rename test/api/c/{ => issues}/issue11069.c (100%) create mode 100644 test/api/cpp/issues/CMakeLists.txt rename test/api/cpp/{ => issues}/issue11069.cpp (100%) rename test/api/cpp/{ => issues}/issue4889.cpp (100%) rename test/api/cpp/{ => issues}/issue5074.cpp (100%) rename test/api/cpp/{ => issues}/issue5893.cpp (100%) rename test/api/cpp/{ => issues}/issue6111.cpp (100%) rename test/api/cpp/{ => issues}/issue7000.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue306.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue308.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue334.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue337.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue344.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue345.cpp (99%) rename test/api/cpp/{ => issues}/proj-issue373.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue377.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue378.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue379.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue381.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue382.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue383.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue386.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue388.cpp (98%) rename test/api/cpp/{ => issues}/proj-issue395.cpp (95%) rename test/api/cpp/{ => issues}/proj-issue399.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue413.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue414.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue416.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue418.cpp (98%) rename test/api/cpp/{ => issues}/proj-issue420.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue421.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue422.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue423.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue426.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue429.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue431.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue434.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue435.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue436.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue440.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue445.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue455.cpp (96%) rename test/api/cpp/{ => issues}/proj-issue484.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue538.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue567.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue570.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue573.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue574.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue575.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue576.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue580.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue581.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue587.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue600.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue611.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue612.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue618.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue621.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue644.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue646.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue652.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue654.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue655.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue656.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue657.cpp (100%) rename test/api/cpp/{ => issues}/proj-issue666.cpp (100%) diff --git a/test/api/c/CMakeLists.txt b/test/api/c/CMakeLists.txt index 44d3bde0512..a0e0a44bcca 100644 --- a/test/api/c/CMakeLists.txt +++ b/test/api/c/CMakeLists.txt @@ -31,87 +31,30 @@ add_custom_target(capitests set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST -Dcvc5_obj_EXPORTS) -macro(cvc5_add_capi_test name) - set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/c) - set(testname capi_${name}) - add_executable(${testname} ${name}.c) - target_link_libraries(${testname} PUBLIC main-test) - target_compile_definitions(${testname} PRIVATE ${CVC5_API_TEST_FLAGS}) - set_target_properties(${testname} +macro(cvc5_add_capi_test name dir) + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/c/${dir}) + set(cname capi_${name}) + add_executable(${cname} ${name}.c) + target_link_libraries(${cname} PUBLIC main-test) + target_compile_definitions(${cname} PRIVATE ${CVC5_API_TEST_FLAGS}) + set_target_properties(${cname} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) - add_test(api/c/${testname} ${ENV_PATH_CMD} ${test_bin_dir}/${testname}) - set_tests_properties(api/c/${testname} PROPERTIES LABELS "api capi") + if("${dir}" STREQUAL "") + set(testname api/c/${cname}) + else() + set(testname api/c/${dir}/${cname}) + endif() + add_test(${testname} ${ENV_PATH_CMD} ${test_bin_dir}/${cname}) + set_tests_properties(${testname} PROPERTIES LABELS "api capi") # set_tests_properties(api/cpp/${name} PROPERTIES FIXTURES_REQUIRED build_capitests_fixture) - add_dependencies(build-capitests ${testname}) + add_dependencies(build-capitests ${cname}) endmacro() -cvc5_add_capi_test(boilerplate) -cvc5_add_capi_test(ouroborous) -cvc5_add_capi_test(reset_assertions) -cvc5_add_capi_test(sep_log_api) -cvc5_add_capi_test(smt2_compliance) -cvc5_add_capi_test(two_solvers) -cvc5_add_capi_test(issue11069) -#cvc5_add_capi_test(issue5074) -#cvc5_add_capi_test(issue5893) -#cvc5_add_capi_test(issue4889) -#cvc5_add_capi_test(issue6111) -#cvc5_add_capi_test(issue7000) -#cvc5_add_capi_test(proj-issue306) -#cvc5_add_capi_test(proj-issue308) -#cvc5_add_capi_test(proj-issue334) -#cvc5_add_capi_test(proj-issue337) -#cvc5_add_capi_test(proj-issue344) -#cvc5_add_capi_test(proj-issue345) -#cvc5_add_capi_test(proj-issue373) -#cvc5_add_capi_test(proj-issue377) -#cvc5_add_capi_test(proj-issue378) -#cvc5_add_capi_test(proj-issue379) -#cvc5_add_capi_test(proj-issue381) -#cvc5_add_capi_test(proj-issue382) -#cvc5_add_capi_test(proj-issue383) -#cvc5_add_capi_test(proj-issue386) -#cvc5_add_capi_test(proj-issue388) -#cvc5_add_capi_test(proj-issue395) -#cvc5_add_capi_test(proj-issue399) -#cvc5_add_capi_test(proj-issue413) -#cvc5_add_capi_test(proj-issue414) -#cvc5_add_capi_test(proj-issue416) -#cvc5_add_capi_test(proj-issue418) -#cvc5_add_capi_test(proj-issue420) -#cvc5_add_capi_test(proj-issue421) -#cvc5_add_capi_test(proj-issue422) -#cvc5_add_capi_test(proj-issue423) -#cvc5_add_capi_test(proj-issue426) -#cvc5_add_capi_test(proj-issue429) -#cvc5_add_capi_test(proj-issue431) -#cvc5_add_capi_test(proj-issue434) -#cvc5_add_capi_test(proj-issue435) -#cvc5_add_capi_test(proj-issue436) -#cvc5_add_capi_test(proj-issue440) -#cvc5_add_capi_test(proj-issue445) -#cvc5_add_capi_test(proj-issue455) -#cvc5_add_capi_test(proj-issue484) -#cvc5_add_capi_test(proj-issue538) -#cvc5_add_capi_test(proj-issue567) -#cvc5_add_capi_test(proj-issue570) -#cvc5_add_capi_test(proj-issue573) -#cvc5_add_capi_test(proj-issue574) -#cvc5_add_capi_test(proj-issue575) -#cvc5_add_capi_test(proj-issue576) -#cvc5_add_capi_test(proj-issue580) -#cvc5_add_capi_test(proj-issue581) -#cvc5_add_capi_test(proj-issue587) -#cvc5_add_capi_test(proj-issue600) -#cvc5_add_capi_test(proj-issue611) -#cvc5_add_capi_test(proj-issue612) -#cvc5_add_capi_test(proj-issue618) -#cvc5_add_capi_test(proj-issue621) -#cvc5_add_capi_test(proj-issue644) -#cvc5_add_capi_test(proj-issue646) -#cvc5_add_capi_test(proj-issue652) -#cvc5_add_capi_test(proj-issue654) -#cvc5_add_capi_test(proj-issue655) -#cvc5_add_capi_test(proj-issue656) -#cvc5_add_capi_test(proj-issue657) -#cvc5_add_capi_test(proj-issue666) +cvc5_add_capi_test(boilerplate "") +cvc5_add_capi_test(ouroborous "") +cvc5_add_capi_test(reset_assertions "") +cvc5_add_capi_test(sep_log_api "") +cvc5_add_capi_test(smt2_compliance "") +cvc5_add_capi_test(two_solvers "") + +add_subdirectory(issues) diff --git a/test/api/c/issues/CMakeLists.txt b/test/api/c/issues/CMakeLists.txt new file mode 100644 index 00000000000..79422655aec --- /dev/null +++ b/test/api/c/issues/CMakeLists.txt @@ -0,0 +1,80 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. +## + +cvc5_add_capi_test(issue11069 "issues") + +#cvc5_add_capi_test(issue5074) +#cvc5_add_capi_test(issue5893) +#cvc5_add_capi_test(issue4889) +#cvc5_add_capi_test(issue6111) +#cvc5_add_capi_test(issue7000) +#cvc5_add_capi_test(proj-issue306) +#cvc5_add_capi_test(proj-issue308) +#cvc5_add_capi_test(proj-issue334) +#cvc5_add_capi_test(proj-issue337) +#cvc5_add_capi_test(proj-issue344) +#cvc5_add_capi_test(proj-issue345) +#cvc5_add_capi_test(proj-issue373) +#cvc5_add_capi_test(proj-issue377) +#cvc5_add_capi_test(proj-issue378) +#cvc5_add_capi_test(proj-issue379) +#cvc5_add_capi_test(proj-issue381) +#cvc5_add_capi_test(proj-issue382) +#cvc5_add_capi_test(proj-issue383) +#cvc5_add_capi_test(proj-issue386) +#cvc5_add_capi_test(proj-issue388) +#cvc5_add_capi_test(proj-issue395) +#cvc5_add_capi_test(proj-issue399) +#cvc5_add_capi_test(proj-issue413) +#cvc5_add_capi_test(proj-issue414) +#cvc5_add_capi_test(proj-issue416) +#cvc5_add_capi_test(proj-issue418) +#cvc5_add_capi_test(proj-issue420) +#cvc5_add_capi_test(proj-issue421) +#cvc5_add_capi_test(proj-issue422) +#cvc5_add_capi_test(proj-issue423) +#cvc5_add_capi_test(proj-issue426) +#cvc5_add_capi_test(proj-issue429) +#cvc5_add_capi_test(proj-issue431) +#cvc5_add_capi_test(proj-issue434) +#cvc5_add_capi_test(proj-issue435) +#cvc5_add_capi_test(proj-issue436) +#cvc5_add_capi_test(proj-issue440) +#cvc5_add_capi_test(proj-issue445) +#cvc5_add_capi_test(proj-issue455) +#cvc5_add_capi_test(proj-issue484) +#cvc5_add_capi_test(proj-issue538) +#cvc5_add_capi_test(proj-issue567) +#cvc5_add_capi_test(proj-issue570) +#cvc5_add_capi_test(proj-issue573) +#cvc5_add_capi_test(proj-issue574) +#cvc5_add_capi_test(proj-issue575) +#cvc5_add_capi_test(proj-issue576) +#cvc5_add_capi_test(proj-issue580) +#cvc5_add_capi_test(proj-issue581) +#cvc5_add_capi_test(proj-issue587) +#cvc5_add_capi_test(proj-issue600) +#cvc5_add_capi_test(proj-issue611) +#cvc5_add_capi_test(proj-issue612) +#cvc5_add_capi_test(proj-issue618) +#cvc5_add_capi_test(proj-issue621) +#cvc5_add_capi_test(proj-issue644) +#cvc5_add_capi_test(proj-issue646) +#cvc5_add_capi_test(proj-issue652) +#cvc5_add_capi_test(proj-issue654) +#cvc5_add_capi_test(proj-issue655) +#cvc5_add_capi_test(proj-issue656) +#cvc5_add_capi_test(proj-issue657) +#cvc5_add_capi_test(proj-issue666) diff --git a/test/api/c/issue11069.c b/test/api/c/issues/issue11069.c similarity index 100% rename from test/api/c/issue11069.c rename to test/api/c/issues/issue11069.c diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index 9d54630471d..2ef7a42859d 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -13,10 +13,8 @@ # The build system configuration. ## -include_directories(.) include_directories(${PROJECT_SOURCE_DIR}/src) include_directories(${PROJECT_SOURCE_DIR}/src/include) -include_directories(${CMAKE_BINARY_DIR}/src) #-----------------------------------------------------------------------------# # Add target 'apitests', builds and runs @@ -36,86 +34,29 @@ add_custom_target(apitests set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST -Dcvc5_obj_EXPORTS) -macro(cvc5_add_api_test name) - set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/cpp) +macro(cvc5_add_api_test name dir) + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/cpp/${dir}) add_executable(${name} ${name}.cpp) target_link_libraries(${name} PUBLIC main-test) target_compile_definitions(${name} PRIVATE ${CVC5_API_TEST_FLAGS}) set_target_properties(${name} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) - add_test(api/cpp/${name} ${ENV_PATH_CMD} ${test_bin_dir}/${name}) - set_tests_properties(api/cpp/${name} PROPERTIES LABELS "api") + if("${dir}" STREQUAL "") + set(test_name api/cpp/${name}) + else() + set(test_name api/cpp/${dir}/${name}) + endif() + add_test(${test_name} ${ENV_PATH_CMD} ${test_bin_dir}/${name}) + set_tests_properties(${test_name} PROPERTIES LABELS "api cppapi") # set_tests_properties(api/cpp/${name} PROPERTIES FIXTURES_REQUIRED build_apitests_fixture) add_dependencies(build-apitests ${name}) endmacro() -cvc5_add_api_test(boilerplate) -cvc5_add_api_test(ouroborous) -cvc5_add_api_test(reset_assertions) -cvc5_add_api_test(sep_log_api) -cvc5_add_api_test(smt2_compliance) -cvc5_add_api_test(two_solvers) -cvc5_add_api_test(issue11069) -cvc5_add_api_test(issue5074) -cvc5_add_api_test(issue5893) -cvc5_add_api_test(issue4889) -cvc5_add_api_test(issue6111) -cvc5_add_api_test(issue7000) -cvc5_add_api_test(proj-issue306) -cvc5_add_api_test(proj-issue308) -cvc5_add_api_test(proj-issue334) -cvc5_add_api_test(proj-issue337) -cvc5_add_api_test(proj-issue344) -cvc5_add_api_test(proj-issue345) -cvc5_add_api_test(proj-issue373) -cvc5_add_api_test(proj-issue377) -cvc5_add_api_test(proj-issue378) -cvc5_add_api_test(proj-issue379) -cvc5_add_api_test(proj-issue381) -cvc5_add_api_test(proj-issue382) -cvc5_add_api_test(proj-issue383) -cvc5_add_api_test(proj-issue386) -cvc5_add_api_test(proj-issue388) -cvc5_add_api_test(proj-issue395) -cvc5_add_api_test(proj-issue399) -cvc5_add_api_test(proj-issue413) -cvc5_add_api_test(proj-issue414) -cvc5_add_api_test(proj-issue416) -cvc5_add_api_test(proj-issue418) -cvc5_add_api_test(proj-issue420) -cvc5_add_api_test(proj-issue421) -cvc5_add_api_test(proj-issue422) -cvc5_add_api_test(proj-issue423) -cvc5_add_api_test(proj-issue426) -cvc5_add_api_test(proj-issue429) -cvc5_add_api_test(proj-issue431) -cvc5_add_api_test(proj-issue434) -cvc5_add_api_test(proj-issue435) -cvc5_add_api_test(proj-issue436) -cvc5_add_api_test(proj-issue440) -cvc5_add_api_test(proj-issue445) -cvc5_add_api_test(proj-issue455) -cvc5_add_api_test(proj-issue484) -cvc5_add_api_test(proj-issue538) -cvc5_add_api_test(proj-issue567) -cvc5_add_api_test(proj-issue570) -cvc5_add_api_test(proj-issue573) -cvc5_add_api_test(proj-issue574) -cvc5_add_api_test(proj-issue575) -cvc5_add_api_test(proj-issue576) -cvc5_add_api_test(proj-issue580) -cvc5_add_api_test(proj-issue581) -cvc5_add_api_test(proj-issue587) -cvc5_add_api_test(proj-issue600) -cvc5_add_api_test(proj-issue611) -cvc5_add_api_test(proj-issue612) -cvc5_add_api_test(proj-issue618) -cvc5_add_api_test(proj-issue621) -cvc5_add_api_test(proj-issue644) -cvc5_add_api_test(proj-issue646) -cvc5_add_api_test(proj-issue652) -cvc5_add_api_test(proj-issue654) -cvc5_add_api_test(proj-issue655) -cvc5_add_api_test(proj-issue656) -cvc5_add_api_test(proj-issue657) -cvc5_add_api_test(proj-issue666) +cvc5_add_api_test(boilerplate "") +cvc5_add_api_test(ouroborous "") +cvc5_add_api_test(reset_assertions "") +cvc5_add_api_test(sep_log_api "") +cvc5_add_api_test(smt2_compliance "") +cvc5_add_api_test(two_solvers "") + +add_subdirectory(issues) diff --git a/test/api/cpp/issues/CMakeLists.txt b/test/api/cpp/issues/CMakeLists.txt new file mode 100644 index 00000000000..b38b12a7b06 --- /dev/null +++ b/test/api/cpp/issues/CMakeLists.txt @@ -0,0 +1,79 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. +## + +cvc5_add_api_test(issue11069 "issues") +cvc5_add_api_test(issue5074 "issues") +cvc5_add_api_test(issue5893 "issues") +cvc5_add_api_test(issue4889 "issues") +cvc5_add_api_test(issue6111 "issues") +cvc5_add_api_test(issue7000 "issues") +cvc5_add_api_test(proj-issue306 "issues") +cvc5_add_api_test(proj-issue308 "issues") +cvc5_add_api_test(proj-issue334 "issues") +cvc5_add_api_test(proj-issue337 "issues") +cvc5_add_api_test(proj-issue344 "issues") +cvc5_add_api_test(proj-issue345 "issues") +cvc5_add_api_test(proj-issue373 "issues") +cvc5_add_api_test(proj-issue377 "issues") +cvc5_add_api_test(proj-issue378 "issues") +cvc5_add_api_test(proj-issue379 "issues") +cvc5_add_api_test(proj-issue381 "issues") +cvc5_add_api_test(proj-issue382 "issues") +cvc5_add_api_test(proj-issue383 "issues") +cvc5_add_api_test(proj-issue386 "issues") +cvc5_add_api_test(proj-issue388 "issues") +cvc5_add_api_test(proj-issue395 "issues") +cvc5_add_api_test(proj-issue399 "issues") +cvc5_add_api_test(proj-issue413 "issues") +cvc5_add_api_test(proj-issue414 "issues") +cvc5_add_api_test(proj-issue416 "issues") +cvc5_add_api_test(proj-issue418 "issues") +cvc5_add_api_test(proj-issue420 "issues") +cvc5_add_api_test(proj-issue421 "issues") +cvc5_add_api_test(proj-issue422 "issues") +cvc5_add_api_test(proj-issue423 "issues") +cvc5_add_api_test(proj-issue426 "issues") +cvc5_add_api_test(proj-issue429 "issues") +cvc5_add_api_test(proj-issue431 "issues") +cvc5_add_api_test(proj-issue434 "issues") +cvc5_add_api_test(proj-issue435 "issues") +cvc5_add_api_test(proj-issue436 "issues") +cvc5_add_api_test(proj-issue440 "issues") +cvc5_add_api_test(proj-issue445 "issues") +cvc5_add_api_test(proj-issue455 "issues") +cvc5_add_api_test(proj-issue484 "issues") +cvc5_add_api_test(proj-issue538 "issues") +cvc5_add_api_test(proj-issue567 "issues") +cvc5_add_api_test(proj-issue570 "issues") +cvc5_add_api_test(proj-issue573 "issues") +cvc5_add_api_test(proj-issue574 "issues") +cvc5_add_api_test(proj-issue575 "issues") +cvc5_add_api_test(proj-issue576 "issues") +cvc5_add_api_test(proj-issue580 "issues") +cvc5_add_api_test(proj-issue581 "issues") +cvc5_add_api_test(proj-issue587 "issues") +cvc5_add_api_test(proj-issue600 "issues") +cvc5_add_api_test(proj-issue611 "issues") +cvc5_add_api_test(proj-issue612 "issues") +cvc5_add_api_test(proj-issue618 "issues") +cvc5_add_api_test(proj-issue621 "issues") +cvc5_add_api_test(proj-issue644 "issues") +cvc5_add_api_test(proj-issue646 "issues") +cvc5_add_api_test(proj-issue652 "issues") +cvc5_add_api_test(proj-issue654 "issues") +cvc5_add_api_test(proj-issue655 "issues") +cvc5_add_api_test(proj-issue656 "issues") +cvc5_add_api_test(proj-issue657 "issues") +cvc5_add_api_test(proj-issue666 "issues") diff --git a/test/api/cpp/issue11069.cpp b/test/api/cpp/issues/issue11069.cpp similarity index 100% rename from test/api/cpp/issue11069.cpp rename to test/api/cpp/issues/issue11069.cpp diff --git a/test/api/cpp/issue4889.cpp b/test/api/cpp/issues/issue4889.cpp similarity index 100% rename from test/api/cpp/issue4889.cpp rename to test/api/cpp/issues/issue4889.cpp diff --git a/test/api/cpp/issue5074.cpp b/test/api/cpp/issues/issue5074.cpp similarity index 100% rename from test/api/cpp/issue5074.cpp rename to test/api/cpp/issues/issue5074.cpp diff --git a/test/api/cpp/issue5893.cpp b/test/api/cpp/issues/issue5893.cpp similarity index 100% rename from test/api/cpp/issue5893.cpp rename to test/api/cpp/issues/issue5893.cpp diff --git a/test/api/cpp/issue6111.cpp b/test/api/cpp/issues/issue6111.cpp similarity index 100% rename from test/api/cpp/issue6111.cpp rename to test/api/cpp/issues/issue6111.cpp diff --git a/test/api/cpp/issue7000.cpp b/test/api/cpp/issues/issue7000.cpp similarity index 100% rename from test/api/cpp/issue7000.cpp rename to test/api/cpp/issues/issue7000.cpp diff --git a/test/api/cpp/proj-issue306.cpp b/test/api/cpp/issues/proj-issue306.cpp similarity index 100% rename from test/api/cpp/proj-issue306.cpp rename to test/api/cpp/issues/proj-issue306.cpp diff --git a/test/api/cpp/proj-issue308.cpp b/test/api/cpp/issues/proj-issue308.cpp similarity index 100% rename from test/api/cpp/proj-issue308.cpp rename to test/api/cpp/issues/proj-issue308.cpp diff --git a/test/api/cpp/proj-issue334.cpp b/test/api/cpp/issues/proj-issue334.cpp similarity index 100% rename from test/api/cpp/proj-issue334.cpp rename to test/api/cpp/issues/proj-issue334.cpp diff --git a/test/api/cpp/proj-issue337.cpp b/test/api/cpp/issues/proj-issue337.cpp similarity index 100% rename from test/api/cpp/proj-issue337.cpp rename to test/api/cpp/issues/proj-issue337.cpp diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/issues/proj-issue344.cpp similarity index 100% rename from test/api/cpp/proj-issue344.cpp rename to test/api/cpp/issues/proj-issue344.cpp diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/issues/proj-issue345.cpp similarity index 99% rename from test/api/cpp/proj-issue345.cpp rename to test/api/cpp/issues/proj-issue345.cpp index 34dfefb0c71..0fd2adacdfb 100644 --- a/test/api/cpp/proj-issue345.cpp +++ b/test/api/cpp/issues/proj-issue345.cpp @@ -33,4 +33,3 @@ int main(void) Term query = tm.mkTerm(Kind::AND, {t154, t154, t154, t154}); slv.checkSatAssuming(query.notTerm()); } - diff --git a/test/api/cpp/proj-issue373.cpp b/test/api/cpp/issues/proj-issue373.cpp similarity index 100% rename from test/api/cpp/proj-issue373.cpp rename to test/api/cpp/issues/proj-issue373.cpp diff --git a/test/api/cpp/proj-issue377.cpp b/test/api/cpp/issues/proj-issue377.cpp similarity index 100% rename from test/api/cpp/proj-issue377.cpp rename to test/api/cpp/issues/proj-issue377.cpp diff --git a/test/api/cpp/proj-issue378.cpp b/test/api/cpp/issues/proj-issue378.cpp similarity index 100% rename from test/api/cpp/proj-issue378.cpp rename to test/api/cpp/issues/proj-issue378.cpp diff --git a/test/api/cpp/proj-issue379.cpp b/test/api/cpp/issues/proj-issue379.cpp similarity index 100% rename from test/api/cpp/proj-issue379.cpp rename to test/api/cpp/issues/proj-issue379.cpp diff --git a/test/api/cpp/proj-issue381.cpp b/test/api/cpp/issues/proj-issue381.cpp similarity index 100% rename from test/api/cpp/proj-issue381.cpp rename to test/api/cpp/issues/proj-issue381.cpp diff --git a/test/api/cpp/proj-issue382.cpp b/test/api/cpp/issues/proj-issue382.cpp similarity index 100% rename from test/api/cpp/proj-issue382.cpp rename to test/api/cpp/issues/proj-issue382.cpp diff --git a/test/api/cpp/proj-issue383.cpp b/test/api/cpp/issues/proj-issue383.cpp similarity index 100% rename from test/api/cpp/proj-issue383.cpp rename to test/api/cpp/issues/proj-issue383.cpp diff --git a/test/api/cpp/proj-issue386.cpp b/test/api/cpp/issues/proj-issue386.cpp similarity index 100% rename from test/api/cpp/proj-issue386.cpp rename to test/api/cpp/issues/proj-issue386.cpp diff --git a/test/api/cpp/proj-issue388.cpp b/test/api/cpp/issues/proj-issue388.cpp similarity index 98% rename from test/api/cpp/proj-issue388.cpp rename to test/api/cpp/issues/proj-issue388.cpp index c26ffd744e5..c5c15c49982 100644 --- a/test/api/cpp/proj-issue388.cpp +++ b/test/api/cpp/issues/proj-issue388.cpp @@ -28,7 +28,7 @@ int main(void) { return 0; } - { // Original + { // Original TermManager tm; Solver slv(tm); slv.setLogic("QF_NRA"); @@ -45,7 +45,7 @@ int main(void) slv.assertFormula(t9); slv.checkSat(); } - { // Minimized + { // Minimized TermManager tm; Solver slv(tm); slv.setOption("nl-cov", "true"); diff --git a/test/api/cpp/proj-issue395.cpp b/test/api/cpp/issues/proj-issue395.cpp similarity index 95% rename from test/api/cpp/proj-issue395.cpp rename to test/api/cpp/issues/proj-issue395.cpp index b4ba97f3251..fb5b8be8a75 100644 --- a/test/api/cpp/proj-issue395.cpp +++ b/test/api/cpp/issues/proj-issue395.cpp @@ -26,5 +26,5 @@ int main(void) Sort s1 = tm.getBooleanSort(); Sort s2 = tm.getIntegerSort(); Sort s5 = tm.mkFunctionSort({s2}, s1); - (void) s5.substitute({s1}, {s1}); + (void)s5.substitute({s1}, {s1}); } diff --git a/test/api/cpp/proj-issue399.cpp b/test/api/cpp/issues/proj-issue399.cpp similarity index 100% rename from test/api/cpp/proj-issue399.cpp rename to test/api/cpp/issues/proj-issue399.cpp diff --git a/test/api/cpp/proj-issue413.cpp b/test/api/cpp/issues/proj-issue413.cpp similarity index 100% rename from test/api/cpp/proj-issue413.cpp rename to test/api/cpp/issues/proj-issue413.cpp diff --git a/test/api/cpp/proj-issue414.cpp b/test/api/cpp/issues/proj-issue414.cpp similarity index 100% rename from test/api/cpp/proj-issue414.cpp rename to test/api/cpp/issues/proj-issue414.cpp diff --git a/test/api/cpp/proj-issue416.cpp b/test/api/cpp/issues/proj-issue416.cpp similarity index 100% rename from test/api/cpp/proj-issue416.cpp rename to test/api/cpp/issues/proj-issue416.cpp diff --git a/test/api/cpp/proj-issue418.cpp b/test/api/cpp/issues/proj-issue418.cpp similarity index 98% rename from test/api/cpp/proj-issue418.cpp rename to test/api/cpp/issues/proj-issue418.cpp index 777100996aa..dd2142b26c9 100644 --- a/test/api/cpp/proj-issue418.cpp +++ b/test/api/cpp/issues/proj-issue418.cpp @@ -45,6 +45,5 @@ int main(void) Term t785 = tm.mkTerm(Kind::FLOATINGPOINT_DIV, {t201, t436, t436}); Term t788 = tm.mkTerm(Kind::FLOATINGPOINT_IS_NAN, {t785}); slv.assertFormula({t788}); - (void) slv.simplify(t450); + (void)slv.simplify(t450); } - diff --git a/test/api/cpp/proj-issue420.cpp b/test/api/cpp/issues/proj-issue420.cpp similarity index 100% rename from test/api/cpp/proj-issue420.cpp rename to test/api/cpp/issues/proj-issue420.cpp diff --git a/test/api/cpp/proj-issue421.cpp b/test/api/cpp/issues/proj-issue421.cpp similarity index 100% rename from test/api/cpp/proj-issue421.cpp rename to test/api/cpp/issues/proj-issue421.cpp diff --git a/test/api/cpp/proj-issue422.cpp b/test/api/cpp/issues/proj-issue422.cpp similarity index 100% rename from test/api/cpp/proj-issue422.cpp rename to test/api/cpp/issues/proj-issue422.cpp diff --git a/test/api/cpp/proj-issue423.cpp b/test/api/cpp/issues/proj-issue423.cpp similarity index 100% rename from test/api/cpp/proj-issue423.cpp rename to test/api/cpp/issues/proj-issue423.cpp diff --git a/test/api/cpp/proj-issue426.cpp b/test/api/cpp/issues/proj-issue426.cpp similarity index 100% rename from test/api/cpp/proj-issue426.cpp rename to test/api/cpp/issues/proj-issue426.cpp diff --git a/test/api/cpp/proj-issue429.cpp b/test/api/cpp/issues/proj-issue429.cpp similarity index 100% rename from test/api/cpp/proj-issue429.cpp rename to test/api/cpp/issues/proj-issue429.cpp diff --git a/test/api/cpp/proj-issue431.cpp b/test/api/cpp/issues/proj-issue431.cpp similarity index 100% rename from test/api/cpp/proj-issue431.cpp rename to test/api/cpp/issues/proj-issue431.cpp diff --git a/test/api/cpp/proj-issue434.cpp b/test/api/cpp/issues/proj-issue434.cpp similarity index 100% rename from test/api/cpp/proj-issue434.cpp rename to test/api/cpp/issues/proj-issue434.cpp diff --git a/test/api/cpp/proj-issue435.cpp b/test/api/cpp/issues/proj-issue435.cpp similarity index 100% rename from test/api/cpp/proj-issue435.cpp rename to test/api/cpp/issues/proj-issue435.cpp diff --git a/test/api/cpp/proj-issue436.cpp b/test/api/cpp/issues/proj-issue436.cpp similarity index 100% rename from test/api/cpp/proj-issue436.cpp rename to test/api/cpp/issues/proj-issue436.cpp diff --git a/test/api/cpp/proj-issue440.cpp b/test/api/cpp/issues/proj-issue440.cpp similarity index 100% rename from test/api/cpp/proj-issue440.cpp rename to test/api/cpp/issues/proj-issue440.cpp diff --git a/test/api/cpp/proj-issue445.cpp b/test/api/cpp/issues/proj-issue445.cpp similarity index 100% rename from test/api/cpp/proj-issue445.cpp rename to test/api/cpp/issues/proj-issue445.cpp diff --git a/test/api/cpp/proj-issue455.cpp b/test/api/cpp/issues/proj-issue455.cpp similarity index 96% rename from test/api/cpp/proj-issue455.cpp rename to test/api/cpp/issues/proj-issue455.cpp index 25eb2bf1493..7d5ae17b44e 100644 --- a/test/api/cpp/proj-issue455.cpp +++ b/test/api/cpp/issues/proj-issue455.cpp @@ -64,7 +64,8 @@ int main(void) Term t26 = tm.mkVar(s1, "_f19_2"); Term t27 = tm.mkVar(s2, "_f19_3"); Term t28 = tm.mkVar(s1, "_f19_4"); - Term t29 = slv.defineFun("_f19", {t24, t25, t26, t27, t28}, t24.getSort(), t24); + Term t29 = + slv.defineFun("_f19", {t24, t25, t26, t27, t28}, t24.getSort(), t24); Term t30 = tm.mkTerm(Kind::DISTINCT, {t19, t20, t16}); Term t31 = tm.mkTerm(Kind::ITE, {t30, t9, t22}); Term t32 = tm.mkTerm(Kind::DIVISION, {t11, t6, t10}); diff --git a/test/api/cpp/proj-issue484.cpp b/test/api/cpp/issues/proj-issue484.cpp similarity index 100% rename from test/api/cpp/proj-issue484.cpp rename to test/api/cpp/issues/proj-issue484.cpp diff --git a/test/api/cpp/proj-issue538.cpp b/test/api/cpp/issues/proj-issue538.cpp similarity index 100% rename from test/api/cpp/proj-issue538.cpp rename to test/api/cpp/issues/proj-issue538.cpp diff --git a/test/api/cpp/proj-issue567.cpp b/test/api/cpp/issues/proj-issue567.cpp similarity index 100% rename from test/api/cpp/proj-issue567.cpp rename to test/api/cpp/issues/proj-issue567.cpp diff --git a/test/api/cpp/proj-issue570.cpp b/test/api/cpp/issues/proj-issue570.cpp similarity index 100% rename from test/api/cpp/proj-issue570.cpp rename to test/api/cpp/issues/proj-issue570.cpp diff --git a/test/api/cpp/proj-issue573.cpp b/test/api/cpp/issues/proj-issue573.cpp similarity index 100% rename from test/api/cpp/proj-issue573.cpp rename to test/api/cpp/issues/proj-issue573.cpp diff --git a/test/api/cpp/proj-issue574.cpp b/test/api/cpp/issues/proj-issue574.cpp similarity index 100% rename from test/api/cpp/proj-issue574.cpp rename to test/api/cpp/issues/proj-issue574.cpp diff --git a/test/api/cpp/proj-issue575.cpp b/test/api/cpp/issues/proj-issue575.cpp similarity index 100% rename from test/api/cpp/proj-issue575.cpp rename to test/api/cpp/issues/proj-issue575.cpp diff --git a/test/api/cpp/proj-issue576.cpp b/test/api/cpp/issues/proj-issue576.cpp similarity index 100% rename from test/api/cpp/proj-issue576.cpp rename to test/api/cpp/issues/proj-issue576.cpp diff --git a/test/api/cpp/proj-issue580.cpp b/test/api/cpp/issues/proj-issue580.cpp similarity index 100% rename from test/api/cpp/proj-issue580.cpp rename to test/api/cpp/issues/proj-issue580.cpp diff --git a/test/api/cpp/proj-issue581.cpp b/test/api/cpp/issues/proj-issue581.cpp similarity index 100% rename from test/api/cpp/proj-issue581.cpp rename to test/api/cpp/issues/proj-issue581.cpp diff --git a/test/api/cpp/proj-issue587.cpp b/test/api/cpp/issues/proj-issue587.cpp similarity index 100% rename from test/api/cpp/proj-issue587.cpp rename to test/api/cpp/issues/proj-issue587.cpp diff --git a/test/api/cpp/proj-issue600.cpp b/test/api/cpp/issues/proj-issue600.cpp similarity index 100% rename from test/api/cpp/proj-issue600.cpp rename to test/api/cpp/issues/proj-issue600.cpp diff --git a/test/api/cpp/proj-issue611.cpp b/test/api/cpp/issues/proj-issue611.cpp similarity index 100% rename from test/api/cpp/proj-issue611.cpp rename to test/api/cpp/issues/proj-issue611.cpp diff --git a/test/api/cpp/proj-issue612.cpp b/test/api/cpp/issues/proj-issue612.cpp similarity index 100% rename from test/api/cpp/proj-issue612.cpp rename to test/api/cpp/issues/proj-issue612.cpp diff --git a/test/api/cpp/proj-issue618.cpp b/test/api/cpp/issues/proj-issue618.cpp similarity index 100% rename from test/api/cpp/proj-issue618.cpp rename to test/api/cpp/issues/proj-issue618.cpp diff --git a/test/api/cpp/proj-issue621.cpp b/test/api/cpp/issues/proj-issue621.cpp similarity index 100% rename from test/api/cpp/proj-issue621.cpp rename to test/api/cpp/issues/proj-issue621.cpp diff --git a/test/api/cpp/proj-issue644.cpp b/test/api/cpp/issues/proj-issue644.cpp similarity index 100% rename from test/api/cpp/proj-issue644.cpp rename to test/api/cpp/issues/proj-issue644.cpp diff --git a/test/api/cpp/proj-issue646.cpp b/test/api/cpp/issues/proj-issue646.cpp similarity index 100% rename from test/api/cpp/proj-issue646.cpp rename to test/api/cpp/issues/proj-issue646.cpp diff --git a/test/api/cpp/proj-issue652.cpp b/test/api/cpp/issues/proj-issue652.cpp similarity index 100% rename from test/api/cpp/proj-issue652.cpp rename to test/api/cpp/issues/proj-issue652.cpp diff --git a/test/api/cpp/proj-issue654.cpp b/test/api/cpp/issues/proj-issue654.cpp similarity index 100% rename from test/api/cpp/proj-issue654.cpp rename to test/api/cpp/issues/proj-issue654.cpp diff --git a/test/api/cpp/proj-issue655.cpp b/test/api/cpp/issues/proj-issue655.cpp similarity index 100% rename from test/api/cpp/proj-issue655.cpp rename to test/api/cpp/issues/proj-issue655.cpp diff --git a/test/api/cpp/proj-issue656.cpp b/test/api/cpp/issues/proj-issue656.cpp similarity index 100% rename from test/api/cpp/proj-issue656.cpp rename to test/api/cpp/issues/proj-issue656.cpp diff --git a/test/api/cpp/proj-issue657.cpp b/test/api/cpp/issues/proj-issue657.cpp similarity index 100% rename from test/api/cpp/proj-issue657.cpp rename to test/api/cpp/issues/proj-issue657.cpp diff --git a/test/api/cpp/proj-issue666.cpp b/test/api/cpp/issues/proj-issue666.cpp similarity index 100% rename from test/api/cpp/proj-issue666.cpp rename to test/api/cpp/issues/proj-issue666.cpp