fix #4910

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 20, 2020 · 8e0a2c9 · 8e0a2c9
1 parent 8cb1dd2
commit 8e0a2c9
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -114,6 +114,8 @@ struct pb2bv_rewriter::imp {
                 if (g.is_one())
                     return;
             }
+            if (g.is_zero())
+                return;
             switch (is_le) {
             case l_undef:
                 if (!k.is_int())
@@ -123,7 +125,7 @@ struct pb2bv_rewriter::imp {
                     return;
                 k /= g;
                 break;
-            case l_true:
+            case l_true:              
                 k /= g;
                 k = floor(k);
                 break;