Clear the simplify maps after each transformation of div/mod/rem. This reverts back...

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

diff --git a/AST/Transform.cpp b/AST/Transform.cpp
index d3b73fdd49bbef2c10de3759e921c8cec614f2fd..10a56d0af7206ea8b375b5fbf692d04942a7b15b 100644 (file)
--- a/AST/Transform.cpp
+++ b/AST/Transform.cpp
@@ -52,7 +52,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 
                //put everything together, simplify, and return
                ASTNode n = CreateTerm(ITE, len, cond_dividend, minus_modnode, modnode);
-               return SimplifyTerm(n);
+               return SimplifyTerm_TopLevel(n);
        }
 
        // This is the modulus of dividing rounding to -infinity.
@@ -95,7 +95,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
                ASTNode ite2 = CreateTerm(ITE, len, CreateNode(AND, isSNeg, isTPos), branch2, ite3);
                ASTNode ite1 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTPos), branch1, ite2);
 
-               return SimplifyTerm(ite1);
+               return SimplifyTerm_TopLevel(ite1);
        }
        else if (SBVDIV == in.GetKind())
        {
@@ -131,7 +131,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
                ASTNode minus_divnode3 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), CreateTerm(BVUMINUS, len, divisor));
                ASTNode n = CreateTerm(ITE, len, cond1, minus_divnode1, CreateTerm(ITE, len, cond2, minus_divnode2, CreateTerm(ITE, len, cond3,
                                minus_divnode3, divnode)));
-               return SimplifyTerm(n);
+               return SimplifyTerm_TopLevel(n);
        }
 
        FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in);