From e1027790ae9e5e99ab98351c3a4953ae49661f5e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Apr 2020 16:04:44 -0700
Subject: [PATCH] more to #3926

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 29 ++++++++++++++---------------
 1 file changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index fcf26817721..39a04f6ec19 100644
--- 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) {