Removed an assertion, unneeded header file

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e51900a942cbbcd8008ab6e0d8a07adae044b46..6771b8cd5f27489151f5e9ec534151471c9b4da5 100644 (file)
--- 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 dd3848e7ffd2df2fc961841d62705066b1f4cbb2..11467c8db8d1714c787f901f96d0359704f4309e 100644 (file)
--- 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 {