From 9351d80a4d8b0748382648453b38e4232c7d4f8f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 10 Jan 2019 09:15:14 +0000
Subject: [PATCH] Fully rewrite nested forall during symbolic execution

This permits (correctly) solving another simple regression test.
---
 .../cbmc/Quantifiers-simplify/rewrite_forall.c | 18 ++++++++++++++++++
 .../Quantifiers-simplify/rewrite_forall.desc   |  8 ++++++++
 src/goto-symex/symex_main.cpp                  | 14 +++++++++++++-
 3 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Quantifiers-simplify/rewrite_forall.c
 create mode 100644 regression/cbmc/Quantifiers-simplify/rewrite_forall.desc

diff --git a/regression/cbmc/Quantifiers-simplify/rewrite_forall.c b/regression/cbmc/Quantifiers-simplify/rewrite_forall.c
new file mode 100644
index 00000000000..07924a5c7fa
--- /dev/null
+++ b/regression/cbmc/Quantifiers-simplify/rewrite_forall.c
@@ -0,0 +1,18 @@
+int main()
+{
+  // clang-format off
+  __CPROVER_assert(
+    __CPROVER_forall {
+      int i;
+      // clang-format would rewrite the "==>" as "== >"
+      i >= 0 ==> __CPROVER_forall
+      {
+        int j;
+        j<0 ==> j < i
+      }
+    },
+    "rewrite");
+  // clang-format on
+
+  return 0;
+}
diff --git a/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc b/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc
new file mode 100644
index 00000000000..516527d0ce1
--- /dev/null
+++ b/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc
@@ -0,0 +1,8 @@
+CORE
+rewrite_forall.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index d5ebe73b7d5..9e038616303 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/make_unique.h>
 #include <util/mathematical_expr.h>
 #include <util/replace_symbol.h>
@@ -86,7 +87,12 @@ void goto_symext::vcc(
   exprt expr=vcc_expr;
 
   // we are willing to re-write some quantified expressions
-  rewrite_quantifiers(expr, state);
+  if(has_subexpr(expr, ID_exists) || has_subexpr(expr, ID_forall))
+  {
+    // have negation pushed inwards as far as possible
+    do_simplify(expr);
+    rewrite_quantifiers(expr, state);
+  }
 
   // now rename, enables propagation
   state.rename(expr, ns);
@@ -143,8 +149,14 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
       to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
     symex_decl(state, tmp0);
     exprt tmp = quant_expr.where();
+    rewrite_quantifiers(tmp, state);
     quant_expr.swap(tmp);
   }
+  else if(expr.id() == ID_or || expr.id() == ID_and)
+  {
+    for(auto &op : expr.operands())
+      rewrite_quantifiers(op, state);
+  }
 }
 
 void goto_symext::initialize_entry_point(