From 8e0a2c9e77edf0e8afc87a1f95abce23417df349 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Dec 2020 11:29:13 -0800
Subject: [PATCH] fix #4910

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/pb2bv_rewriter.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index a7c273bba..ee3f8f8b6 100644
--- 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;