further test for FP divider

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6353 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/Float-div3/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <math.h>
+
+float nondet_float (void);
+
+int main (void) {
+	float f = nondet_float();
+	__CPROVER_assume(f < +INFINITY);
+	__CPROVER_assume(f > 1.0f);
+
+	float g = nondet_float();
+	__CPROVER_assume(g < 1.0f);
+	__CPROVER_assume(g >= 0x1.0p-126f);
+	__CPROVER_assume(g > 0.0f);
+
+	float div = f / g;
+
+	assert(!(div == 0.0));
+
+	return 1;
+}

regression/cbmc/Float-div3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring