Removed an assertion, unneeded header file

2 files changed, 1 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e51900a9..6771b8cd5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1052,7 +1052,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
     SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin();
     for (; pos != d_topLevelSubstitutions.end(); ++pos) {
       Assert((*pos).first.isVar());
-      Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
+      //      Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
     }
     for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
       Assert((*pos).second.isConst());
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index dd3848e7f..11467c8db 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -24,7 +24,6 @@
 #define __CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
-#include "theory/substitutions.h"
 
 namespace CVC4 {