Multiple tests fail with "Option 'no-type-check' registered more than once!"

[TheBjoel2]

I was trying to build ikos (master branch) on Arch Linux. I did:

cmake \
-DCMAKE_BUILD_TYPE="Release" \
-DCMAKE_INSTALL_PREFIX="/usr" \
-DLLVM_CONFIG_EXECUTABLE="/usr/bin/llvm-config-14" \
-DAPPEND_GIT_VERSION=ON \
..

make

Which failed with a linker error:

[ 32%] Linking CXX executable ikos-pp
/usr/bin/ld: cannot find -lLLVMAggressiveInstCombine: No such file or directory
/usr/bin/ld: cannot find -lLLVMAnalysis: No such file or directory
/usr/bin/ld: cannot find -lLLVMAsmParser: No such file or directory
/usr/bin/ld: cannot find -lLLVMBitReader: No such file or directory
/usr/bin/ld: cannot find -lLLVMBitWriter: No such file or directory
/usr/bin/ld: cannot find -lLLVMCodeGen: No such file or directory
/usr/bin/ld: cannot find -lLLVMCore: No such file or directory
/usr/bin/ld: cannot find -lLLVMCoroutines: No such file or directory
/usr/bin/ld: cannot find -lLLVMInstCombine: No such file or directory
/usr/bin/ld: cannot find -lLLVMInstrumentation: No such file or directory
/usr/bin/ld: cannot find -lLLVMipo: No such file or directory
/usr/bin/ld: cannot find -lLLVMIRReader: No such file or directory
/usr/bin/ld: cannot find -lLLVMMC: No such file or directory
/usr/bin/ld: cannot find -lLLVMObjCARCOpts: No such file or directory
/usr/bin/ld: cannot find -lLLVMScalarOpts: No such file or directory
/usr/bin/ld: cannot find -lLLVMTarget: No such file or directory
/usr/bin/ld: cannot find -lLLVMTransformUtils: No such file or directory
/usr/bin/ld: cannot find -lLLVMVectorize: No such file or directory
collect2: error: ld returned 1 exit status

Reading through this, I assumed that the issue was the llvm built as one single shared library. Looking at how llvm is packaged on arch linux, that seemed to be true. By adding -DBUILD_SHARED_LIBS=ON and -DIKOS_LINK_LLVM_DYLIB=ON to ikos cmake parameters, and also including #include <array> into these files (There were several compiler errors):

core/test/unit/adt/patricia_tree/map.cpp
core/test/unit/domain/discrete_domain.cpp
core/test/unit/domain/numeric/congruence.cpp
core/test/unit/domain/numeric/constant.cpp
core/test/unit/domain/numeric/interval.cpp
core/test/unit/domain/numeric/interval_congruence.cpp

I was able to build it successfully. However, after running make check, multiple tests failed

69% tests passed, 18 tests failed out of 59

Total Test time (real) =   2.12 sec

The following tests FAILED:
         42 - import-no-optimization (Failed)
         43 - import-basic-optimization (Failed)
         44 - import-aggressive-optimization (Failed)
         45 - analysis-buffer-overflow (Failed)
         46 - analysis-division-by-zero (Failed)
         47 - analysis-memory (Failed)
         48 - analysis-null-pointer-dereference (Failed)
         49 - analysis-assert-prover (Failed)
         50 - analysis-uninitialized-variable (Failed)
         51 - analysis-unaligned-pointer (Failed)
         52 - analysis-signed-int-overflow (Failed)
         53 - analysis-unsigned-int-overflow (Failed)
         54 - analysis-shift-count (Failed)
         55 - analysis-pointer-overflow (Failed)
         56 - analysis-pointer-compare (Failed)
         57 - analysis-function-call (Failed)
         58 - analysis-double-free (Failed)
         59 - analysis-soundness (Failed)
Errors while running CTest

Looking at logs to see why they're not passing, they seem to fail with the same error:

: CommandLine Error: Option 'no-type-check' registered more than once!

Maybe that is related to https://github.com/NASA-SW-VnV/ikos/issues/61?

Also, it would be great if you tell us on which linux distro you build ikos so that we wouldn't have to deal with non-standard llvm distributions.