Short cut on constant evaluation

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

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index 8fbab6057289a07e0d112a8c6029ee1e3eb99cb8..b4465f3a24d588be0127e8418f22a48feda97f52 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -24,7 +24,10 @@ namespace BEEV
 // Const evaluator logical and arithmetic operations.
   ASTNode NonMemberBVConstEvaluator(const ASTNode& t)
   {
-    ASTNode OutputNode;
+    if (t.isConstant())
+               return t;
+
+       ASTNode OutputNode;
     Kind k = t.GetKind();
 
     STPMgr* _bm = t.GetSTPMgr();
@@ -694,6 +697,9 @@ namespace BEEV
 
   ASTNode Simplifier::BVConstEvaluator(const ASTNode& t)
   {
+         if (t.isConstant())
+               return t;
+
          ASTNode OutputNode;
 
          if (CheckSubstitutionMap(t, OutputNode))