1 files changed, 30 insertions, 17 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index e88189bcc..fa273dfa5 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -13,6 +13,7 @@
 #include "expr/expr.h"
 #include "expr_value.h"
 #include "expr_builder.h"
+#include "util/Assert.h"
 
 using namespace CVC4::expr;
 
@@ -33,70 +34,82 @@ Expr::Expr() :
 
 Expr::Expr(ExprValue* ev)
   : d_ev(ev) {
-  if(d_ev != 0)
-    d_ev->inc();
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
+  d_ev->inc();
 }
 
 Expr::Expr(const Expr& e) {
-  if((d_ev = e.d_ev) && d_ev != 0)
-    d_ev->inc();
+  Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!");
+  d_ev = e.d_ev;
+  d_ev->inc();
 }
 
 Expr::~Expr() {
-  if(d_ev)
-    d_ev->dec();
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
+  d_ev->dec();
+}
+
+void Expr::assignExprValue(ExprValue* ev) {
+  d_ev = ev;
+  d_ev->inc();
 }
 
 Expr& Expr::operator=(const Expr& e) {
-  if(d_ev)
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
+  if(this != &e && d_ev != e.d_ev) {
     d_ev->dec();
-  if((d_ev = e.d_ev))
+    d_ev = e.d_ev;
     d_ev->inc();
+  }
   return *this;
 }
 
-ExprValue* Expr::operator->() const {
+ExprValue const* Expr::operator->() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
   return d_ev;
 }
 
 uint64_t Expr::hash() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
   return d_ev->hash();
 }
 
 Expr Expr::eqExpr(const Expr& right) const {
-  return ExprBuilder(*this).eqExpr(right);
+  return ExprManager::currentEM()->mkExpr(EQUAL, *this, right);
 }
 
 Expr Expr::notExpr() const {
-  return ExprBuilder(*this).notExpr();
+  return ExprManager::currentEM()->mkExpr(NOT, *this);
 }
 
+// FIXME: What does this do and why?
 Expr Expr::negate() const { // avoid double-negatives
   return ExprBuilder(*this).negate();
 }
 
+
 Expr Expr::andExpr(const Expr& right) const {
-  return ExprBuilder(*this).andExpr(right);
+  return ExprManager::currentEM()->mkExpr(AND, *this, right);
 }
 
 Expr Expr::orExpr(const Expr& right) const {
-  return ExprBuilder(*this).orExpr(right);
+  return ExprManager::currentEM()->mkExpr(OR, *this, right);
 }
 
 Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
-  return ExprBuilder(*this).iteExpr(thenpart, elsepart);
+  return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
 }
 
 Expr Expr::iffExpr(const Expr& right) const {
-  return ExprBuilder(*this).iffExpr(right);
+  return ExprManager::currentEM()->mkExpr(IFF, *this, right);
 }
 
 Expr Expr::impExpr(const Expr& right) const {
-  return ExprBuilder(*this).impExpr(right);
+  return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right);
 }
 
 Expr Expr::xorExpr(const Expr& right) const {
-  return ExprBuilder(*this).xorExpr(right);
+  return ExprManager::currentEM()->mkExpr(XOR, *this, right);
 }
 
 }/* CVC4 namespace */