From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 14 Jun 2012 17:55:08 +0000 (+0000)
Subject: Removed an assertion, unneeded header file
X-Git-Tag: cvc5-1.0.0~8014
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86b8b53afbbd2259e297709c99d594a79927184a;p=cvc5.git

Removed an assertion, unneeded header file
---

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 {