more to #3926

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 13, 2020 · e102779 · e102779
1 parent 7caae3f
commit e102779
Showing 1 changed file with 14 additions and 15 deletions.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -676,8 +676,7 @@ bool seq_rewriter::is_suffix(expr* s, expr* offset, expr* len) {
         (a.neg(), m_autil.is_numeral(offset, b) && 
          b.is_pos() && 
          a == b && 
-         lens.size() == 1 && 
-         lens[0] == s);
+         lens.contains(s));
 }
 
 bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
@@ -696,18 +695,6 @@ bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
         }
         return true;
     }
-    if (m_util.str.is_length(e)) {
-        s = sign_pos;
-        return true;
-    }
-    rational pos;
-    if (m_autil.is_numeral(e, pos)) {
-        if (pos.is_pos())
-            s = sign_pos;
-        else if (pos.is_neg())
-            s = sign_neg;
-        return true;
-    }
     if (m_autil.is_mul(e)) {
         for (expr* arg : *to_app(e)) {
             sign s1;
@@ -726,7 +713,19 @@ bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
         }
         return true;
     }
-    return true;
+    if (m_util.str.is_length(e)) {
+        s = sign_pos;
+        return true;
+    }
+    rational r;
+    if (m_autil.is_numeral(e, r)) {
+        if (r.is_pos())
+            s = sign_pos;
+        else if (r.is_neg())
+            s = sign_neg;
+        return true;
+    }
+    return false;
 }
 
 br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {