From f677b02c2a2951d5d222bce47f26ab9ee2a77587 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 4 May 2011 05:04:31 +0000 Subject: [PATCH] Replace variables before calling the interval analysis. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1308 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 1c5478f..7cfd170 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -99,13 +99,6 @@ namespace BEEV { bm->ASTNodeStats("After Removing Unconstrained: ", simplified_solved_InputToSAT); } - if (bm->UserFlags.isSet("use-intervals", "1")) - { - EstablishIntervals intervals(*bm); - simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT); - bm->ASTNodeStats("After Establishing Intervals: ", simplified_solved_InputToSAT); - } - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { @@ -114,6 +107,13 @@ namespace BEEV { bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT); } + if (bm->UserFlags.isSet("use-intervals", "1")) + { + EstablishIntervals intervals(*bm); + simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT); + bm->ASTNodeStats("After Establishing Intervals: ", simplified_solved_InputToSAT); + } + if (bm->UserFlags.bitConstantProp_flag) { bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); -- 2.47.3