summaryrefslogtreecommitdiff
path: root/src/util/boolean_simplification.h
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2013-09-30 13:56:51 -0400
committerLiana Hadarean <lianahady@gmail.com>2013-09-30 13:56:51 -0400
commit7d2265eb2b5dc96ddff04211959e208b1cb8a7f0 (patch)
tree26fb270349580c90efe163ca7767bccce6607902 /src/util/boolean_simplification.h
parentdb6df44574927f9b75db664e1e490f757725d13a (diff)
parent0c2eafec69b694a507ac914bf285fe0574be085f (diff)
merged golden
Diffstat (limited to 'src/util/boolean_simplification.h')
-rw-r--r--src/util/boolean_simplification.h2
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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback