From 2822922d367600280a78a920e94fdb4ff56ac771 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 16 May 2020 11:17:13 -0700
Subject: [PATCH] fix regression with mainintaing signs for monotonicity lemmas

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_rewriter.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 8895ac855..9ba91a7e6 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1337,9 +1337,6 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
             return BR_REWRITE2;
         }
 
-        if (r2.is_pos()) {
-            
-        }
     }
 
     if (hi_div0) {