1 files changed, 2 insertions, 0 deletions
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index e5c4ead6c..be39f69c1 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -22,6 +22,7 @@
 #include <vector>
 #include <algorithm>
 
+#include "expr/expr_manager_scope.h"
 #include "expr/node.h"
 #include "util/cvc4_assert.h"
 
@@ -202,6 +203,7 @@ public:
    * @param e the Expr to negate (cannot be the null Expr)
    */
   static Expr negate(Expr e) throw(AssertionException) {
+    ExprManagerScope ems(e);
     return negate(Node::fromExpr(e)).toExpr();
   }