Adding a precondition to fill_in_array_with_expr

romainbrenguier · romainbrenguier · commit df3658321c5b · 2017-08-18T09:00:14.000+01:00
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -880,6 +880,7 @@ exprt string_refinementt::substitute_array_with_expr(
 exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)
 {
   PRECONDITION(expr.type().id()==ID_array);
+  PRECONDITION(expr.id()==ID_with || expr.id()==ID_array_of);
 
   // Nothing to do for empty array
   if(expr.id()==ID_array_of)

Original file line number	Diff line number	Diff line change
`@@ -880,6 +880,7 @@ exprt string_refinementt::substitute_array_with_expr(`
`880`	`880`	`exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)`
`881`	`881`	`{`
`882`	`882`	`PRECONDITION(expr.type().id()==ID_array);`
	`883`	`+ PRECONDITION(expr.id()==ID_with \|\| expr.id()==ID_array_of);`
`883`	`884`
`884`	`885`	`// Nothing to do for empty array`
`885`	`886`	`if(expr.id()==ID_array_of)`