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

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 1969f4dd4702848833dffb0f898ce86328652cf7..c2c8eecf534b47703254a03e1346eaa44cb37e2e 100644 (file)
--- 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 0b1598d28b6b48c6b149e5844c8e115f2ad17beb..f15a1e8cf293aad71e2cf2c0e22df5bc20ae829a 100644 (file)
--- 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."