From 73df0f9f414fbcc26849ea5d772283ed1552d33c Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 23 Mar 2011 03:17:02 +0000 Subject: [PATCH] If there are unapplied substitutions before starting unconstrained variable elimination. Then apply then. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1228 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/RemoveUnconstrained.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp index f15a1e8..78798ea 100644 --- a/src/simplifier/RemoveUnconstrained.cpp +++ b/src/simplifier/RemoveUnconstrained.cpp @@ -26,7 +26,6 @@ namespace BEEV const bool debug_unconstrained = false; - // There should be no unapplied simplifications. ASTNode RemoveUnconstrained::topLevel(const ASTNode &n, Simplifier *simplifier) { @@ -35,7 +34,9 @@ namespace BEEV bm.GetRunTimes()->start(RunTimes::RemoveUnconstrained); //All the simplifications should be written through before we get here. - assert(result == simplifier->applySubstitutionMap(result)); + + if(simplifier->hasUnappliedSubstitutions()) + result = simplifier->applySubstitutionMap(result); result = topLevel_other(result, simplifier); -- 2.47.3