From 777091e653f0674a81e374634da9e3195ef50cd1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Jan 2017 18:09:27 -0800
Subject: [PATCH] fix part 1 of #875

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp |  2 ++
 src/smt/theory_seq.cpp  | 28 +++++++++++++++-------------
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c7aecca88..3c88a75a2 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2031,11 +2031,13 @@ namespace smt {
         v.shrink(old_size);
     }
 
+#if 0
     void context::mark_as_deleted(clause * cls) {
         SASSERT(!cls->deleted());
         remove_cls_occs(cls);
         cls->mark_as_deleted(m_manager);
     }
+#endif
 
     /**
        \brief Undo variable assignments.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index ed95ef8d7..cdea02c48 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2958,22 +2958,19 @@ void theory_seq::tightest_prefix(expr* s, expr* x) {
   let i = Index(t, s, offset):
 
   offset >= len(t) => i = -1
-
-  offset fixed to 0:
-
   len(t) != 0 & !contains(t, s) => i = -1
-  len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
+
+
+  offset = 0 & len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
   tightest_prefix(x, s)
 
-  offset not fixed:
 
   0 <= offset < len(t) => xy = t &
                           len(x) = offset &
                           (-1 = indexof(y, s, 0) => -1 = i) &
                           (indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i)
 
-  if offset < 0
-     under specified
+  offset < 0 => i = -1
 
   optional lemmas:
    (len(s) > len(t)  -> i = -1)
@@ -2987,17 +2984,19 @@ void theory_seq::add_indexof_axiom(expr* i) {
     expr_ref minus_one(m_autil.mk_int(-1), m);
     expr_ref zero(m_autil.mk_int(0), m);
     expr_ref xsy(m);
+    
+    literal cnt = mk_literal(m_util.str.mk_contains(t, s));
+    literal i_eq_m1 = mk_eq(i, minus_one, false);
+    add_axiom(cnt,  i_eq_m1);
+    literal s_eq_empty = mk_eq_empty(s);
+    add_axiom(~s_eq_empty, mk_eq(i, zero, false));
+    add_axiom(s_eq_empty, ~mk_eq_empty(t), i_eq_m1);
 
     if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
         expr_ref x  = mk_skolem(m_indexof_left, t, s);
         expr_ref y  = mk_skolem(m_indexof_right, t, s);
         xsy         = mk_concat(x, s, y);
         expr_ref lenx(m_util.str.mk_length(x), m);
-        literal cnt = mk_literal(m_util.str.mk_contains(t, s));
-        literal s_eq_empty = mk_eq_empty(s);
-        add_axiom(cnt,  mk_eq(i, minus_one, false));
-        add_axiom(~s_eq_empty, mk_eq(i, zero, false));
-        add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
         add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
         add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
         tightest_prefix(s, x);
@@ -3024,10 +3023,13 @@ void theory_seq::add_indexof_axiom(expr* i) {
         add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
         add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false));
         add_axiom(~offset_ge_0, offset_ge_len,
-                  ~mk_eq(indexof0, minus_one, false), mk_eq(i, minus_one, false));
+                  ~mk_eq(indexof0, minus_one, false), i_eq_m1);
         add_axiom(~offset_ge_0, offset_ge_len,
                   ~mk_literal(m_autil.mk_ge(indexof0, zero)),
                   mk_eq(offset_p_indexof0, i, false));
+
+        // offset < 0 => -1 = i
+        add_axiom(offset_ge_0, i_eq_m1);
     }
 }