From 809bba4439c45ebf2fa446aec714659db0e1696a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 13 Apr 2011 04:30:17 +0000 Subject: [PATCH] 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 --- src/simplifier/RemoveUnconstrained.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) 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." -- 2.47.3