From 4e73d8ad8f7a531a4681ddd14c54c5c821289a92 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Jun 2010 14:12:16 +0000
Subject: [PATCH] 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
---
 src/simplifier/consteval.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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))
-- 
2.47.3