From 6c242695012e7af6b61a8570e7bf5a0bab341193 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 21 Mar 2011 03:59:42 +0000 Subject: [PATCH] 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 --- src/AST/ArrayTransformer.cpp | 2 +- src/simplifier/consteval.cpp | 12 ++++++++---- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 0c00bf2..668614a 100644 --- 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 ee4cc5f..1bdafbb 100644 --- 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 -- 2.47.3