Adjust casting within quantifier handling

Author: ArenBabikian

src/goto-instrument/code_contracts.cpp

@@ -27,6 +27,7 @@ Date: February 2016
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
 #include <util/mathematical_types.h>
+#include <util/mathematical_expr.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -169,41 +170,44 @@ void code_contractst::add_quantified_variable(
   irep_idt mode)
 {
   if(
-    expression.id() == ID_not || expression.id() == ID_notequal ||
-    expression.id() == ID_typecast)
+    expression.id() == ID_not || expression.id() == ID_typecast)
   {
     // For unary connectives, recursively check for
     // nested quantified formulae in the term
-    exprt term = expression.operands().at(0);
+    unary_exprt unary_expression = to_unary_expr(expression);
+    exprt term = unary_expression.operands().at(0);
     add_quantified_variable(term, replace, mode);
   }
   if(
     expression.id() == ID_and || expression.id() == ID_or ||
-    expression.id() == ID_implies)
+    expression.id() == ID_notequal || expression.id() == ID_implies)
   {
     // For binary connectives, recursively check for
     // nested quantified formulae in the left and right terms
-    exprt left = expression.operands().at(0);
+    binary_exprt binary_expression = to_binary_expr(expression);
+    exprt left = binary_expression.operands().at(0);
     add_quantified_variable(left, replace, mode);
-    exprt right = expression.operands().at(1);
+    exprt right = binary_expression.operands().at(1);
     add_quantified_variable(right, replace, mode);
   }
   if(expression.id() == ID_if)
   {
     // For ternary connectives, recursively check for
     // nested quantified formulae in all three terms
-    exprt condition = expression.operands().at(0);
+    if_exprt if_expression = to_if_expr(expression);
+    exprt condition = if_expression.operands().at(0);
     add_quantified_variable(condition, replace, mode);
-    exprt first = expression.operands().at(1);
+    exprt first = if_expression.operands().at(1);
     add_quantified_variable(first, replace, mode);
-    exprt second = expression.operands().at(2);
+    exprt second = if_expression.operands().at(2);
     add_quantified_variable(second, replace, mode);
   }
   else if(expression.id() == ID_exists || expression.id() == ID_forall)
   {
-    // When a quantified expression is found,
+    // When a quantifier expression is found,
     // 1. get quantified symbol
-    exprt tuple = expression.operands().at(0);
+    quantifier_exprt quantifier_expression = to_quantifier_expr(expression);
+    exprt tuple = quantifier_expression.operands().at(0);
     exprt quantified_variable = tuple.operands().at(0);
     symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
 
@@ -222,7 +226,7 @@ void code_contractst::add_quantified_variable(
     replace.insert(q, new_symbol.symbol_expr());
 
     // 4. recursively check for nested quantified formulae
-    exprt quantified_expression = expression.operands().at(1);
+    exprt quantified_expression = quantifier_expression.operands().at(1);
     add_quantified_variable(quantified_expression, replace, mode);
   }
 }