update rewite modality

NikolajBjorner · NikolajBjorner · commit 470e87afe9bd · 2020-04-24T01:12:06.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -1271,7 +1271,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
             a1 = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a);
             result = m_util.str.mk_index(a1, b, m_autil.mk_int(r));
             result = m().mk_ite(m_autil.mk_ge(result, zero()), m_autil.mk_add(m_autil.mk_int(i), result), minus_one());
-            return BR_REWRITE2;
+            return BR_REWRITE_FULL;
         }
     }
     bool is_zero = m_autil.is_numeral(c, r) && r.is_zero();
@@ -1288,7 +1288,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
         result = m_util.str.mk_index(
             m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a), b, c);
         result = m().mk_ite(m_autil.mk_ge(result, zero()), m_autil.mk_add(m_autil.mk_int(i), result), minus_one());
-        return BR_REWRITE1;
+        return BR_REWRITE_FULL;
     }
 
     switch (compare_lengths(as, bs)) {

Original file line number	Diff line number	Diff line change
`@@ -1271,7 +1271,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result`
`1271`	`1271`	`a1 = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a);`
`1272`	`1272`	`result = m_util.str.mk_index(a1, b, m_autil.mk_int(r));`
`1273`	`1273`	`result = m().mk_ite(m_autil.mk_ge(result, zero()), m_autil.mk_add(m_autil.mk_int(i), result), minus_one());`
`1274`		`- return BR_REWRITE2;`
	`1274`	`+ return BR_REWRITE_FULL;`
`1275`	`1275`	`}`
`1276`	`1276`	`}`
`1277`	`1277`	`bool is_zero = m_autil.is_numeral(c, r) && r.is_zero();`
`@@ -1288,7 +1288,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result`
`1288`	`1288`	`result = m_util.str.mk_index(`
`1289`	`1289`	`m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a), b, c);`
`1290`	`1290`	`result = m().mk_ite(m_autil.mk_ge(result, zero()), m_autil.mk_add(m_autil.mk_int(i), result), minus_one());`
`1291`		`- return BR_REWRITE1;`
	`1291`	`+ return BR_REWRITE_FULL;`
`1292`	`1292`	`}`
`1293`	`1293`
`1294`	`1294`	`switch (compare_lengths(as, bs)) {`