check for side effects in quantifiers

Author: Daniel Kroening

src/goto-programs/goto_clean_expr.cpp

@@ -93,8 +93,6 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
   // g1 = (i == 0)
   // g2 = (i > 10)
   // forall (i : int) (g1 || g2)
-  if(expr.id()==ID_forall || expr.id()==ID_exists)
-    return false;
 
   forall_operands(it, expr)
     if(needs_cleaning(*it))
@@ -409,7 +407,7 @@ void goto_convertt::clean_expr(
     // check if there are side-effects
     goto_programt tmp;
     clean_expr(expr.op1(), tmp, mode, true);
-    if(tmp.instructions.empty())
+    if(!tmp.instructions.empty())
     {
       error().source_location=expr.find_source_location();
       error() << "no side-effects in quantified expressions allowed"