From 8f094e2cefca3855d87b1e2c69ac5d6f08268498 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 6 Jun 2018 12:41:48 +0100
Subject: [PATCH] added model for FreeBSD __flt_rounds

---
 src/ansi-c/library/float.c | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/ansi-c/library/float.c b/src/ansi-c/library/float.c
index 204ad8d9627..a2ba36e4daa 100644
--- a/src/ansi-c/library/float.c
+++ b/src/ansi-c/library/float.c
@@ -83,3 +83,13 @@ inline int __builtin_flt_rounds(void)
          __CPROVER_rounding_mode==3?0: // to zero
          -1;
 }
+
+/* FUNCTION: __flt_rounds */
+
+int __builtin_flt_rounds(void);
+
+inline int __flt_rounds(void)
+{
+  // Spotted on FreeBSD
+  return __builtin_flt_rounds();
+}