From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 1 Aug 2009 17:46:10 +0000 (+0000)
Subject: Hack to avoid some of the division by zero errors that occur when evaluating the... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3d817b296f5f60cbdc230a42b721755b24c2a090;p=francis%2Fstp.git

Hack to avoid some of the division by zero errors that occur when evaluating the models that are produced.



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

diff --git a/AST/Transform.cpp b/AST/Transform.cpp
index 10a56d0..4d18cf8 100644
--- a/AST/Transform.cpp
+++ b/AST/Transform.cpp
@@ -316,10 +316,26 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
 			result = CreateTerm(k, width, o);
 			result.SetIndexWidth(indexwidth);
 
+			Kind k = result.GetKind();
+
 			if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind())
 			{
 				result = TranslateSignedDivModRem(result);
 			}
+
+			////// Temporary hack so we don't get killed on the Spear benchmarks in SMTCOMP-2009
+			// This is a difficult rule to introduce in other places because it's recursive. i.e.
+			// result is imbedded unchanged inside the result. It's not
+			if (BVDIV==k || BVMOD==k || SBVDIV == k || SBVREM == k || SBVMOD == k)
+			{
+				unsigned inputValueWidth = result.GetValueWidth();
+				ASTNode zero = CreateZeroConst(inputValueWidth);
+				ASTNode one = CreateOneConst(inputValueWidth);
+				result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, result[1]), one, result);
+			}
+			////////////////////////////////////////////////////////////////////////////////////
+
+
 			break;
 		}
 	}