Remove plus_exprt_with_overflow_check

smowton · Apr 10, 2018 · ce4c008 · ce4c008
1 parent 4779b25
commit ce4c008
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 19 deletions.
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
@@ -177,8 +177,6 @@ class string_constraint_generatort final
   array_string_exprt
   fresh_string(const typet &index_type, const typet &char_type);
   array_string_exprt get_string_expr(const exprt &expr);
-  plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2);
-
 
   static constant_exprt constant_char(int i, const typet &char_type);
 

diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -145,23 +145,6 @@ exprt sum_overflows(const plus_exprt &sum)
     notequal_exprt(op1_negative, sum_negative));
 }
 
-/// Create a plus expression while adding extra constraints to axioms in order
-/// to prevent overflows.
-/// \param op1: First term of the sum
-/// \param op2: Second term of the sum
-/// \return A plus expression representing the sum of the arguments
-/// \deprecated
-plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check(
-  const exprt &op1, const exprt &op2)
-{
-  const plus_exprt sum(plus_exprt(op1, op2));
-  // We prevent overflows by adding the following constraint:
-  // If the signs of the two operands are the same, then the sign of the sum
-  // should also be the same.
-  lemmas.push_back(not_exprt(sum_overflows(sum)));
-  return sum;
-}
-
 /// Associate an actual finite length to infinite arrays
 /// \param s: array expression representing a string
 /// \return expression for the length of `s`