From aeeff0b11a81cf6600ca97bc4f398e27bd7b5562 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 25 Mar 2012 05:04:01 +0000
Subject: [PATCH] Improvement. Better propagation for division when division be
 zero is possible.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1610 e59a4935-1847-0410-ae03-e826735625c1
---
 .../constantBitP/ConstantBitP_Division.cpp    | 21 ++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
index d2e9b91..74d549a 100644
--- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
@@ -659,7 +659,26 @@ Result bvUnsignedDivisionBothWays(vector<FixedBits*>& children,
 		FixedBits& output, STPMgr* bm) {
 
         if (children[1]->containsZero())
-		return NO_CHANGE;
+          {
+            for (int i=children[0]->getWidth()-1; i > 0 ; i--)
+              {
+                if (children[0]->isFixedToZero(i))
+                  {
+                    if (output.isFixedToOne(i))
+                      return CONFLICT;
+                    else if (!output.isFixed(i))
+                      {
+                        output.setFixed(i,true);
+                        output.setValue(i,false);
+                      }
+                  }
+                else
+                  {
+                    break;
+                  }
+              }
+            return NOT_IMPLEMENTED;
+          }
 
 	Result r = bvUnsignedQuotientAndRemainder(children, output, bm,
 			QUOTIENT_IS_OUTPUT);
-- 
2.47.3