From 3d817b296f5f60cbdc230a42b721755b24c2a090 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 1 Aug 2009 17:46:10 +0000 Subject: [PATCH] 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 --- AST/Transform.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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; } } -- 2.47.3