search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Crash when there are bitwise operations on vectors #735

Open shaobo-he opened 3 years ago

shaobo-he commented 3 years ago

https://github.com/smackers/smack/blob/465280b2433d3b61d1ebfc86f4ffb39ad0c047f3/lib/smack/SmackInstGenerator.cpp#L341-L344

We need to restrict the condition here.

zvonimir commented 3 years ago

Can you provide a regression?