From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Mar 2011 00:28:45 +0000 (+0000)
Subject: Now assume there will be no unapplied substitutions when unconstrained variable elimi... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=dbe6e9751bc3d6e0e4364bb51519985ca1a64f73;p=francis%2Fstp.git

Now assume there will be no unapplied substitutions when unconstrained variable elimination starts.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1225 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h
index 1969f4d..c2c8eec 100644
--- a/src/simplifier/MutableASTNode.h
+++ b/src/simplifier/MutableASTNode.h
@@ -36,7 +36,7 @@ private:
     // will be created after its children.
 public:
     static MutableASTNode *
-    build(ASTNode n, map<ASTNode, MutableASTNode *> & visited)
+    build(const ASTNode& n, map<ASTNode, MutableASTNode *> & visited)
     {
       if (visited.find(n) != visited.end())
         {
diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 0b1598d..f15a1e8 100644
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -26,6 +26,7 @@ namespace BEEV
 
   const bool debug_unconstrained = false;
 
+  // There should be no unapplied simplifications.
   ASTNode
   RemoveUnconstrained::topLevel(const ASTNode &n, Simplifier *simplifier)
   {
@@ -33,15 +34,15 @@ namespace BEEV
 
     bm.GetRunTimes()->start(RunTimes::RemoveUnconstrained);
 
-    // If there are substitutions still to write through, I suspect that'd be bad.
-    result = simplifier->applySubstitutionMap(result);
-    simplifier->haveAppliedSubstitutionMap();
+    //All the simplifications should be written through before we get here.
+    assert(result == simplifier->applySubstitutionMap(result));
 
     result = topLevel_other(result, simplifier);
 
     // There should be no unapplied substitutions.
     assert(result == simplifier->applySubstitutionMap(result));
 
+
     // It is idempotent if there are no big ANDS (we have a special hack), and,
     // if we don't introduced any new "disjoint extracts."