BoolExpr removed and replaced with Expr

2 files changed, 9 insertions, 9 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 878588d15..2d83b7960 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1770,7 +1770,7 @@ void SmtEnginePrivate::processAssertions() {
     // Push the simplified assertions to the dump output stream
     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
       Dump("assertions")
-        << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
+        << AssertCommand(d_assertionsToCheck[i].toExpr());
     }
   }
 
@@ -1812,7 +1812,7 @@ void SmtEnginePrivate::addFormula(TNode n)
   }
 }
 
-void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) {
+void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
   Type type = e.getType(options::typeChecking());
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
@@ -1824,7 +1824,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) {
   }
 }
 
-Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) {
 
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
@@ -1891,7 +1891,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
   return r;
 }/* SmtEngine::checkSat() */
 
-Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::query(const Expr& e) throw(TypeCheckingException) {
 
   Assert(!e.isNull());
   Assert(e.getExprManager() == d_exprManager);
@@ -1955,7 +1955,7 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
   return r;
 }/* SmtEngine::query() */
 
-Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::assertFormula(const Expr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f30a98935..df2e47b5b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -263,7 +263,7 @@ class CVC4_PUBLIC SmtEngine {
    * Fully type-check the argument, and also type-check that it's
    * actually Boolean.
    */
-  void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException);
+  void ensureBoolean(const Expr& e) throw(TypeCheckingException);
 
   void internalPush();
 
@@ -362,20 +362,20 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(const BoolExpr& e) throw(TypeCheckingException);
+  Result assertFormula(const Expr& e) throw(TypeCheckingException);
 
   /**
    * Check validity of an expression with respect to the current set
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const BoolExpr& e) throw(TypeCheckingException);
+  Result query(const Expr& e) throw(TypeCheckingException);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException);
+  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException);
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve