workaround for #997

SMT's (div 0 0) == 0xffff, which is annoying
Usually it doesn't matter because we make it UB when divisor=0
But with undef, things get complicated when undef vars are not quantified.
We could fix this properly with either some quantifiers or by wrapping around div
But that's expensive, so we const fold (div 0 x) -> 0 only.

smt/expr.cpp

@@ -728,6 +728,9 @@ expr expr::sdiv(const expr &rhs) const {
   if (rhs.isZero())
     return rhs;
 
+  if (isZero())
+    return *this;
+
   if (isSMin() && rhs.isAllOnes())
     return mkUInt(0, sort());
 
@@ -741,6 +744,9 @@ expr expr::udiv(const expr &rhs) const {
   if (rhs.isZero())
     return rhs;
 
+  if (isZero())
+    return *this;
+
   return binop_fold(rhs, Z3_mk_bvudiv);
 }