From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 13 Apr 2011 04:30:17 +0000 (+0000)
Subject: Remove some assertions that don't necessarily hold.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=809bba4439c45ebf2fa446aec714659db0e1696a;p=francis%2Fstp.git

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 78798ea..1f28629 100644
--- 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."