HF RL Explorer

SMACK Floating-Point Issues

SMACK Floating-Point Issues: a task in LegoFlow-SWE (Harbor dataset). SMACK’s floating-point support currently has several bugs and missing features that prevent correct verification of programs using floating-point types. The following items need to be addressed:

The task

SMACK’s floating-point support currently has several bugs and missing features that prevent correct verification of programs using floating-point types. The following items need to be addressed:

Part of Lego-X/LegoFlow-SWE.