diff --git a/regression/cbmc/switch7/main.c b/regression/cbmc/switch7/main.c
new file mode 100644
index 000000000000..f2fb45e34900
--- /dev/null
+++ b/regression/cbmc/switch7/main.c
@@ -0,0 +1,23 @@
+// These need to be constant-folded at compile time
+
+#define C1 (int) ( 0. / 1. + 0.5)
+#define C2 (int) ( 1. / 1. + 0.5)
+
+int nondet_int();
+
+int main(void)
+{
+  int i=nondet_int();
+
+  switch(i)
+  {
+  case C1:
+    break;
+
+  case C2:
+    break;
+
+  default:
+    break;
+  }
+}
diff --git a/regression/cbmc/switch7/test.desc b/regression/cbmc/switch7/test.desc
new file mode 100644
index 000000000000..9efefbc7362d
--- /dev/null
+++ b/regression/cbmc/switch7/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index c33bcfbefa8b..f6763ee39ec6 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #include "builtin_factory.h"
 #include "c_typecast.h"
 #include "c_qualifiers.h"
@@ -3372,6 +3374,13 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
 
 void c_typecheck_baset::make_constant(exprt &expr)
 {
+  // Floating-point expressions may require a rounding mode.
+  // The compile-time rounding mode may differ from the
+  // run-time rounding mode.
+  const auto rounding_mode =
+    from_integer(config.ansi_c.rounding_mode, signed_int_type());
+  adjust_float_expressions(expr, rounding_mode);
+
   simplify(expr, *this);
 
   if(!expr.is_constant() &&