From 93b947e946777aba0ce668fd9548a88421031f4f Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Tue, 26 Dec 2023 12:35:07 +0000
Subject: [PATCH] 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 | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/smt/expr.cpp b/smt/expr.cpp
index c97e27ab4..5abe5258e 100644
--- a/smt/expr.cpp
+++ b/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);
 }