Remove some assertions that don't necessarily hold.

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

diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 78798ea75002b65f8483a31bfc2e875406ce7a57..1f2862967eaffa2fffa096a01ba4724ee26e5dfe 100644 (file)
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -33,17 +33,14 @@ namespace BEEV
 
     bm.GetRunTimes()->start(RunTimes::RemoveUnconstrained);
 
-    //All the simplifications should be written through before we get here.
-
     if(simplifier->hasUnappliedSubstitutions())
       result = simplifier->applySubstitutionMap(result);
 
+    // In some rare cases, the simplifier might not have removed a term
+    // that can be substituted away. e.g. read(A,0), if read(A,0) == 1,
+    // in the substitution map.
     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."