diff --git a/regression/cbmc/Quantifiers-simplify/main.c b/regression/cbmc/Quantifiers-simplify/main.c
new file mode 100644
index 00000000000..3230c0d9a87
--- /dev/null
+++ b/regression/cbmc/Quantifiers-simplify/main.c
@@ -0,0 +1,11 @@
+int main()
+{
+  __CPROVER_assert(
+    !__CPROVER_forall {
+      int i;
+      i >= 0
+    },
+    "simplify");
+
+  return 0;
+}
diff --git a/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc b/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc
new file mode 100644
index 00000000000..7e9a2db9699
--- /dev/null
+++ b/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--program-only
+ASSERT\(exists \{ signed int i!0#0; !\(i!0#0 >= 0\) \}\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-simplify/test.desc b/regression/cbmc/Quantifiers-simplify/test.desc
new file mode 100644
index 00000000000..e549bceca6a
--- /dev/null
+++ b/regression/cbmc/Quantifiers-simplify/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h
index b4536737256..226aba5552a 100644
--- a/src/util/mathematical_expr.h
+++ b/src/util/mathematical_expr.h
@@ -337,6 +337,24 @@ class forall_exprt : public quantifier_exprt
   }
 };
 
+inline const forall_exprt &to_forall_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<const forall_exprt &>(expr);
+}
+
+inline forall_exprt &to_forall_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<forall_exprt &>(expr);
+}
+
 /// \brief An exists expression
 class exists_exprt : public quantifier_exprt
 {
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 9642a95d68d..9bcd53ec73a 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -222,6 +222,15 @@ bool simplify_exprt::simplify_not(exprt &expr)
     expr = rewritten_op;
     return false;
   }
+  else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
+  {
+    auto const &op_as_forall = to_forall_expr(op);
+    exists_exprt rewritten_op(
+      op_as_forall.symbol(), not_exprt(op_as_forall.where()));
+    simplify_node(rewritten_op.where());
+    expr = rewritten_op;
+    return false;
+  }
 
   return true;
 }