Для некоторых стандартных стандартных программ с двумя аргументами, верификация может игнорировать аргументы функции и предположить, что функция возвращает все возможные значения в своей области значений.
В этом коде первый assert оператор true, и второй assert оператор false. Однако, поскольку верификация принимает то fmodf и nextafterf возвращает значения полного диапазона, он считает, что assert операторы являются ложными, но только на части возможных путей выполнения. Поэтому User assertion проверяет assert операторы оранжевые.
#include <math.h>
int main() {
float val1=10.0, val2=3.0,res;
res = fmodf(val1/val2);
assert(res==1.0);
res = nextafterf(val2,val1);
assert(res<3.0);
}