Fix division by zero results. x % 0, now equals x.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 0c00bf2f31cafcb64d8d8f17bd8bf69422959dc1..668614a8923676e0cfa584680c0e98ce37425fad 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -469,7 +469,7 @@ namespace BEEV
                   result = TranslateSignedDivModRem(result);
                 }
 
-              if (bm->UserFlags.division_by_zero_returns_one_flag)
+              if (bm->UserFlags.division_by_zero_returns_one_flag && (k==SBVDIV || k == BVDIV))
                 {
                   // This is a difficult rule to introduce in other
                   // places because it's recursive. i.e.  result is

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index ee4cc5f39dfdc53fa3cc139984f6a4d947292f7b..1bdafbb1a1bb9294950aac3349a06ad8edc7e0c6 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -304,8 +304,12 @@ namespace BEEV
               && CONSTANTBV::BitVector_is_empty(tmp1))
             {
               // Expecting a division by zero. Just return one.
-              OutputNode = _bm->CreateOneConst(outputwidth);
-              CONSTANTBV::BitVector_Destroy(remainder);
+                 if (k==SBVREM)
+                         OutputNode = children[0];
+                 else
+                         OutputNode = _bm->CreateOneConst(outputwidth);
+
+                 CONSTANTBV::BitVector_Destroy(remainder);
               CONSTANTBV::BitVector_Destroy(quotient);
             }
           else
@@ -363,8 +367,8 @@ namespace BEEV
           if (_bm->UserFlags.division_by_zero_returns_one_flag
               && CONSTANTBV::BitVector_is_empty(tmp1))
             {
-              // Expecting a division by zero. Just return one.
-              OutputNode = _bm->CreateOneConst(outputwidth);
+              // Return the top for a division be zero.
+              OutputNode = children[0];
               CONSTANTBV::BitVector_Destroy(remainder);
             }
           else