Turns some checks into DATA_INVARIANTs

Author: klaas

src/solvers/flattening/bv_pointers.cpp

@@ -47,19 +47,19 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
   }
   else if(expr.id()==ID_is_dynamic_object)
   {
-    if(operands.size()==1 &&
-       operands[0].type().id()==ID_pointer)
-    {
-      // we postpone
-      literalt l=prop.new_variable();
+    DATA_INVARIANT(operands.size() == 1 &&
+                   operands[0].type().id() == ID_pointer,
+                   std::string("is_dynamic_object_exprt should have one") +
+                   "operand, which should have pointer type.");
+    // we postpone
+    literalt l=prop.new_variable();
 
-      postponed_list.push_back(postponedt());
-      postponed_list.back().op=convert_bv(operands[0]);
-      postponed_list.back().bv.push_back(l);
-      postponed_list.back().expr=expr;
+    postponed_list.push_back(postponedt());
+    postponed_list.back().op=convert_bv(operands[0]);
+    postponed_list.back().bv.push_back(l);
+    postponed_list.back().expr=expr;
 
-      return l;
-    }
+    return l;
   }
   else if(expr.id()==ID_lt || expr.id()==ID_le ||
           expr.id()==ID_gt || expr.id()==ID_ge)

src/util/simplify_expr_pointer.cpp

@@ -510,8 +510,10 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
 
 bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 {
-  // This should hold as a result of the expr ID being is_dynamic_object.
-  PRECONDITION(expr.operands().size() == 1);
+  DATA_INVARIANT(expr.operands().size() == 1 &&
+                 expr.op0().type().id() == ID_pointer,
+                 std::string("is_dynamic_object_exprt should have one") +
+                 "operand, which should have pointer type.");
 
   exprt &op=expr.op0();