1 files changed, 28 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 26d554356..cb9dc85f7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -315,6 +315,34 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
   return sum;
 }
 
+RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
+  // Look for multiplications with a 0 argument and rewrite the whole
+  // thing as 0
+  if(n.getKind() == MULT) {
+    Rational ratZero;
+    Integer intZero;
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      if((*i).getKind() == CONST_RATIONAL) {
+        if((*i).getConst<Rational>() == ratZero) {
+          n = NodeManager::currentNM()->mkConst(ratZero);
+          break;
+        }
+      } else if((*i).getKind() == CONST_INTEGER) {
+        if((*i).getConst<Integer>() == intZero) {
+          if(n.getType().isInteger()) {
+            n = NodeManager::currentNM()->mkConst(intZero);
+            break;
+          } else {
+            n = NodeManager::currentNM()->mkConst(ratZero);
+            break;
+          }
+        }
+      }
+    }
+  }
+  return RewritingComplete(Node(n));
+}
+
 Node TheoryArith::rewrite(TNode n){
   Debug("arith") << "rewrite(" << n << ")" << endl;