From a475e7cf5a14a20724d57e297dd65d04656b5b00 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 20 Nov 2020 11:09:44 -0800
Subject: [PATCH] Add gcd test to bv-rewriter

---
 src/ast/rewriter/bv_rewriter.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index a0115cc9b..385906ac2 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2616,6 +2616,11 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
         std::swap(lhs, rhs);
     }
 
+    if (!gcd_test(lhs, rhs)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }        
+
     br_status st;
     if (m_bit2bool) {
         st = mk_bit2bool(lhs, rhs, result);