diff --git a/regression/cbmc/Quantifiers-statement-expression/main.c b/regression/cbmc/Quantifiers-statement-expression/main.c
index 98e0233f268..efd5c55f9ca 100644
--- a/regression/cbmc/Quantifiers-statement-expression/main.c
+++ b/regression/cbmc/Quantifiers-statement-expression/main.c
@@ -3,10 +3,8 @@ int main()
   // clang-format off
   // no side effects!
   int j = 0;
-  //assert(j++);
-  //assert(({int i = 0; while(i <3) i++; i <3;}));
   int a[5] = {0 , 0, 0, 0, 0};
-  assert(__CPROVER_forall { int i;  ({ int j = i; i=i; if(i < 0 || i >4) i = 1;  ( a[i] < 5); }) });
+  assert(__CPROVER_forall { int i;  ({ int j = i; int cond = i < 0 || i >4; if(cond) i = 1;  ( a[i] < 5); }) });
   // clang-format on
 
   return 0;
diff --git a/regression/cbmc/Quantifiers-statement-expression3/main.c b/regression/cbmc/Quantifiers-statement-expression3/main.c
new file mode 100644
index 00000000000..8a0ae9db277
--- /dev/null
+++ b/regression/cbmc/Quantifiers-statement-expression3/main.c
@@ -0,0 +1,11 @@
+int main()
+{
+  // clang-format off
+  // no side effects!
+  int j;
+  int a[5] = {0 , 0, 0, 0, 0};
+  assert(__CPROVER_forall { int i;  ({ ( 0 <= i && i < 4) ==> ({ int k = j; if(j < 0 || j > i) k = 1;  ( a[k] == 0); }); }) });
+  // clang-format on
+
+  return 0;
+}
diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
index 4b7545d030b..4a605141902 100644
--- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp
+++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
@@ -43,6 +43,14 @@ static symbol_exprt find_base_symbol(const exprt &expr)
   {
     return find_base_symbol(to_dereference_expr(expr).pointer());
   }
+  else if(expr.id() == ID_typecast)
+  {
+    return find_base_symbol(to_typecast_expr(expr).op());
+  }
+  else if(expr.id() == ID_address_of)
+  {
+    return find_base_symbol(to_address_of_expr(expr).op());
+  }
   else
   {
     throw "unsupported expression type for finding base symbol";
@@ -63,6 +71,10 @@ static exprt convert_statement_expression(
   INVARIANT(
     natural_loops.loop_map.size() == 0, "quantifier must not contain loops");
 
+  std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
+  // All bound variables are local.
+  declared_symbols.insert(qex.variables().begin(), qex.variables().end());
+
   // `last` is the instruction corresponding to the last expression in the
   // statement expression.
   goto_programt::const_targett last = where.instructions.end();
@@ -75,6 +87,11 @@ static exprt convert_statement_expression(
     {
       last = it;
     }
+
+    if(it->is_decl())
+    {
+      declared_symbols.insert(it->decl_symbol());
+    }
   }
 
   DATA_INVARIANT(
@@ -82,6 +99,12 @@ static exprt convert_statement_expression(
     "expression statements must contain a terminator expression");
 
   auto last_expr = to_code_expression(last->get_other()).expression();
+  if(
+    last_expr.id() == ID_typecast &&
+    to_typecast_expr(last_expr).type().id() == ID_empty)
+  {
+    to_typecast_expr(last_expr).type() = bool_typet();
+  }
 
   struct pathst
   {
@@ -139,10 +162,6 @@ static exprt convert_statement_expression(
     {1, where.instructions.begin()},
     {1, std::make_pair(true_exprt(), replace_mapt())});
 
-  std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
-  // All bound variables are local.
-  declared_symbols.insert(qex.variables().begin(), qex.variables().end());
-
   exprt res = true_exprt();
 
   // Visit the quantifier body along `paths`.
@@ -151,9 +170,12 @@ static exprt convert_statement_expression(
     auto &current_it = paths.back_it();
     auto &path_condition = paths.back_path_condition();
     auto &value_map = paths.back_value_map();
-    INVARIANT(
-      current_it != where.instructions.end(),
-      "Quantifier body must have a unique end expression.");
+
+    if(current_it == where.instructions.end())
+    {
+      paths.pop_back();
+      continue;
+    }
 
     switch(current_it->type())
     {
@@ -189,19 +211,16 @@ static exprt convert_statement_expression(
     // path_condition && cond.
     case goto_program_instruction_typet::GOTO:
     {
-      if(!current_it->condition().is_true())
+      exprt condition = current_it->condition();
+      replace_expr(value_map, condition);
+      if(!condition.is_true())
       {
         auto next_it = current_it->targets.front();
         exprt copy_path_condition = path_condition;
-        replace_mapt copy_symbol_map = value_map;
-        auto copy_condition = current_it->condition();
-        path_condition =
-          and_exprt(path_condition, not_exprt(current_it->condition()));
+        path_condition = and_exprt(path_condition, not_exprt(condition));
         current_it++;
         paths.push_back(
-          next_it,
-          and_exprt(copy_path_condition, copy_condition),
-          copy_symbol_map);
+          next_it, and_exprt(copy_path_condition, condition), value_map);
       }
       else
       {