Can I take LLVM-IR in another language(such as solidity) as input to this tool?

[TheKingShun]

i want to verifiy solidity so i have llvm ir can i do this ?

[TheKingShun]

i have another question： Corral is currently the default back-end，why not Duality ,Duality builds upon Corral

[zvonimir]

Thanks for your interest in SMACK.

To answer your first question about solidity. Yes, you can verify (in theory at least) any LLVM IR program with SMACK no matter what the input language was. See for example:

• https://soarlab.org/publications/2020_vmcai_gbhr/
• https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-1_Kalra_paper.pdf

Now to your Duality question. Duality is basically a dead project that hasn't been updated or maintained for years at this point. Hence, we dropped our support for Duality in SMACK.

[TheKingShun]

@zvonimir Thank you very much indeed!!!!!