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

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 10a56d0af7206ea8b375b5fbf692d04942a7b15b..4d18cf85d065ed7818b0520258a7c9a21966a256 100644 (file)
--- 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;
                }
        }