I broke the division family in #100. Fixing.

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

diff --git a/AST/Transform.cpp b/AST/Transform.cpp
index 4d18cf85d065ed7818b0520258a7c9a21966a256..baa9adb4ddce19e6103c94556bdcf05cf71fdfb1 100644 (file)
--- a/AST/Transform.cpp
+++ b/AST/Transform.cpp
@@ -318,26 +318,29 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
 
                        Kind k = result.GetKind();
 
-                       if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind())
+                       if (BVDIV == k || BVMOD == k || SBVDIV == k || SBVREM == k || SBVMOD == k)
                        {
-                               result = TranslateSignedDivModRem(result);
-                       }
+                               ASTNode bottom = result[1];
+
+                               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
 
-                       ////// 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);
+                               result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result);
                        }
+               }
                        ////////////////////////////////////////////////////////////////////////////////////
 
 
                        break;
-               }
        }
 
        TransformMap[term] = result;