Question about Z3 solver used.

[tszdanger]

Hello, thanks for your fancy research and your code. There is one question bother me: I mention that you only deal with GCC Flags i n the source code of BinTuner, but in the paper, you use both GCC and Clang.

Both LLVM and GCC explicitly specify a set of constraints between optimization ?ags, including adverse interactions and dependency relationships.

I check their website and find that it's clear in GCC, but nobody mentioned this kind of interaction in LLVM.

So does that mean there's no such interaction? Or it's just so hard for us to figure it out?

I would appreciate it if you could help me with this.

[BinTuner]

Hi guys : ）

Thank you very much for your interest and feedback!

This question has been answered, let me close it for now and if you have other questions, feel free to open a new one.

All the best,