From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Jun 2010 14:12:16 +0000 (+0000)
Subject: Short cut on constant evaluation
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4e73d8ad8f7a531a4681ddd14c54c5c821289a92;p=francis%2Fstp.git

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 8fbab60..b4465f3 100644
--- 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))