fix regression with mainintaing signs for monotonicity lemmas

NikolajBjorner · NikolajBjorner · commit 2822922d3676 · 2020-05-16T11:17:40.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git 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) {

Original file line number	Diff line number	Diff line change
`@@ -1337,9 +1337,6 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e`
`1337`	`1337`	`return BR_REWRITE2;`
`1338`	`1338`	`}`
`1339`	`1339`
`1340`		`- if (r2.is_pos()) {`
`1341`		`-`
`1342`		`- }`
`1343`	`1340`	`}`
`1344`	`1341`
`1345`	`1342`	`if (hi_div0) {`