Tests that require Z3 fail rather than being unsupported

[mikeurbach]

I've been dealing with something in my circt integration tests for a while, and it has been an annoyance, but not a major issue. However, it actually masked a problem in #8225. Basically, I haven't configured z3, and any test with // REQUIRES: libz3 fails, rather than being unsupported. Does anyone else see this?

Separately, I need to just get z3 set up so I can run these tests during these LLVM bumps, but the current behavior seems wrong.

I didn't see any open issue about this, but please redirect me if this is a dupe.

For completeness, here is how I configure things:

cmake -B build -G Ninja llvm/llvm \
    -DCMAKE_BUILD_TYPE=Debug \
    -DCMAKE_C_COMPILER=clang \
    -DCMAKE_CXX_COMPILER=clang++ \
    -DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
    -DLLVM_ENABLE_PROJECTS=mlir \
    -DLLVM_ENABLE_ASSERTIONS=ON \
    -DLLVM_EXTERNAL_PROJECTS=circt \
    -DLLVM_EXTERNAL_CIRCT_SOURCE_DIR=. \
    -DLLVM_TARGETS_TO_BUILD=host \
    -DLLVM_LIT_ARGS="-v --show-unsupported" \
    -DLLVM_USE_LINKER=gold \
    -DMLIR_ENABLE_BINDINGS_PYTHON=ON \
    -DCIRCT_BINDINGS_PYTHON_ENABLED=ON

I will note that I see this in the output:

CMake Warning at cmake/modules/FindZ3.cmake:116 (message):
  Failed to determine Z3 library version, defaulting to 0.0.0.
Call Stack (most recent call first):
  /scratch/verif/mikeu/circt/CMakeLists.txt:474 (find_package)


-- Could NOT find Z3 (missing: Z3_LIBRARIES Z3_INCLUDE_DIR) (found version "0.0.0")
-- Did NOT find z3.

[teqdruid]

I get that message at config time but I don't get a test failure as a result.

…

On Wed, Feb 12, 2025, 12:33 PM Mike Urbach ***@***.***> wrote: I've been dealing with something in my circt integration tests for a while, and it has been an annoyance, but not a major issue. However, it actually masked a problem in #8225 <#8225>. Basically, I haven't configured z3, and any test with // REQUIRES: libz3 fails, rather than being unsupported. Does anyone else see this? Separately, I need to just get z3 set up so I can run these tests during these LLVM bumps, but the current behavior seems wrong. I didn't see any open issue about this, but please redirect me if this is a dupe. For completeness, here is how I configure things: cmake -B build -G Ninja llvm/llvm \ -DCMAKE_BUILD_TYPE=Debug \ -DCMAKE_C_COMPILER=clang \ -DCMAKE_CXX_COMPILER=clang++ \ -DCMAKE_EXPORT_COMPILE_COMMANDS=ON \ -DLLVM_ENABLE_PROJECTS=mlir \ -DLLVM_ENABLE_ASSERTIONS=ON \ -DLLVM_EXTERNAL_PROJECTS=circt \ -DLLVM_EXTERNAL_CIRCT_SOURCE_DIR=. \ -DLLVM_TARGETS_TO_BUILD=host \ -DLLVM_LIT_ARGS="-v --show-unsupported" \ -DLLVM_USE_LINKER=gold \ -DMLIR_ENABLE_BINDINGS_PYTHON=ON \ -DCIRCT_BINDINGS_PYTHON_ENABLED=ON I will note that I see this in the output: CMake Warning at cmake/modules/FindZ3.cmake:116 (message): Failed to determine Z3 library version, defaulting to 0.0.0. Call Stack (most recent call first): /scratch/verif/mikeu/circt/CMakeLists.txt:474 (find_package) -- Could NOT find Z3 (missing: Z3_LIBRARIES Z3_INCLUDE_DIR) (found version "0.0.0") -- Did NOT find z3. — Reply to this email directly, view it on GitHub <#8231> or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALNXYGM7WXQWKFVGMNNTBT2POAWLBFKMF2HI4TJMJ2XIZLTSOBKK5TBNR2WLJDUOJ2WLJDOMFWWLO3UNBZGKYLEL5YGC4TUNFRWS4DBNZ2F6YLDORUXM2LUPGBKK5TBNR2WLJLJONZXKZNENZQW2ZNLORUHEZLBMRPXI6LQMWBKK5TBNR2WLJDUOJ2WLJDOMFWWLLTXMF2GG2C7MFRXI2LWNF2HTLDTOVRGUZLDORPXI6LQMWSUS43TOVS2M5DPOBUWG44SQKSHI6LQMWVHEZLQN5ZWS5DPOJ42K5TBNR2WLKJSGQ2TANZSGUYTJAVEOR4XAZNFNFZXG5LFUV3GC3DVMWVDEOBUHA4TGMRVGM3KO5DSNFTWOZLSUZRXEZLBORSQ> . You are receiving this email because you are subscribed to this thread. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub> .