1 files changed, 0 insertions, 12 deletions
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index a7b3e149d..78d7f8c38 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -202,18 +202,6 @@ class BooleanSimplification {
   }
 
   /**
-   * Negates an Expr, doing all the double-negation elimination that's
-   * possible.
-   *
-   * @param e the Expr to negate (cannot be the null Expr)
-   */
-  static Expr negate(Expr e)
-  {
-    ExprManagerScope ems(e);
-    return negate(Node::fromExpr(e)).toExpr();
-  }
-
-  /**
    * Simplify an OR, AND, or IMPLIES.  This function is the identity
    * for all other kinds.
    */