From 99a91ee1169505844d46c83225892d17ea375312 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Dec 2019 07:38:47 +0300
Subject: [PATCH] fix #2793

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

diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h
index e4a7e012d..c2fe43644 100644
--- a/src/ast/rewriter/pb_rewriter_def.h
+++ b/src/ast/rewriter/pb_rewriter_def.h
@@ -164,6 +164,9 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
         }            
     }
 
+    if (is_eq && k.is_neg()) {
+        return l_false;
+    }
     if (is_eq) {
         TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
         return l_undef;