From 9f42338de86f1da7560fbfd14c355874b3ef6dc0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Apr 2020 14:43:27 -0700
Subject: [PATCH] fix #3926

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 60 ++++++++++++++++++++++++++++++-
 src/ast/rewriter/seq_rewriter.h   |  2 ++
 2 files changed, 61 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d6ee47b5022..fcf26817721 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -673,7 +673,60 @@ bool seq_rewriter::is_suffix(expr* s, expr* offset, expr* len) {
     rational a, b;
     return 
         get_lengths(len, lens, a) && 
-        (a.neg(), m_autil.is_numeral(offset, b) && b.is_pos() && a == b);
+        (a.neg(), m_autil.is_numeral(offset, b) && 
+         b.is_pos() && 
+         a == b && 
+         lens.size() == 1 && 
+         lens[0] == s);
+}
+
+bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
+    s = sign_zero;
+    if (m_autil.is_add(e)) {
+        for (expr* arg : *to_app(e)) {
+            sign s1;
+            if (!sign_is_determined(arg, s1))
+                return false;
+            if (s == sign_zero) 
+                s = s1;
+            else if (s1 == sign_zero)
+                continue;
+            else if (s1 != s)
+                return false;
+        }
+        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;
+            if (!sign_is_determined(arg, s1))
+                return false;
+            if (s1 == sign_zero) {
+                s = sign_zero;
+                return true;
+            }
+            if (s == sign_zero)
+                s = s1;
+            else if (s != s1)
+                s = sign_neg;
+            else 
+                s = sign_pos;
+        }
+        return true;
+    }
+    return true;
 }
 
 br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {
@@ -686,6 +739,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool constantLen = m_autil.is_numeral(c, len);
     bool lengthPos   = m_util.str.is_length(b) || m_autil.is_add(b);
 
+    sign sg;
+    if (sign_is_determined(c, sg) && sg == sign_neg) {
+        result = m_util.str.mk_empty(m().get_sort(a));
+        return BR_DONE;
+    }
     
     // case 1: pos<0 or len<=0
     // rewrite to ""
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index ad31af15906..b149864e0a9 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -24,6 +24,7 @@ Module Name:
 #include "ast/rewriter/rewriter_types.h"
 #include "util/params.h"
 #include "util/lbool.h"
+#include "util/sign.h"
 #include "math/automata/automaton.h"
 #include "math/automata/symbolic_automata.h"
 
@@ -141,6 +142,7 @@ class seq_rewriter {
     bool cannot_contain_suffix(expr* a, expr* b);
 
     bool is_suffix(expr* s, expr* offset, expr* len);
+    bool sign_is_determined(expr* len, sign& s);
 
     bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r,