fix #4594

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/rewriter/bool_rewriter.cpp

@@ -813,12 +813,17 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         s = true;
     }
 
-    // (ite c (ite c t1 t2) t3)       ==> (ite c t1 t3)
+    // (ite c (ite c t1 t2) t3)       ==> (ite c t1 t3
     if (m().is_ite(t) && to_app(t)->get_arg(0) == c) {
         // Remark: (ite c (ite (not c) t1 t2) t3) ==> (ite c t2 t3) does not happen if applying rewrites bottom up
         t = to_app(t)->get_arg(1);
         s = true;
     }
+    // (ite c t1 (ite c2 t1 t2))      ==> (ite (or c c2) t1 t2)
+    if (m().is_ite(e) && to_app(e)->get_arg(1) == t) {
+        result = m().mk_ite(m().mk_or(c, to_app(e)->get_arg(0)), t, to_app(e)->get_arg(2));
+        return BR_REWRITE3;
+    }
 
     // (ite c t1 (ite c t2 t3))       ==> (ite c t1 t3)
     if (m().is_ite(e) && to_app(e)->get_arg(0) == c) {

src/ast/rewriter/seq_rewriter.cpp

@@ -824,6 +824,26 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = m_autil.mk_add(es.size(), es.c_ptr());
         return BR_REWRITE2;
     }
+#if 0
+    expr* s = nullptr, *offset = nullptr, *length = nullptr;
+    if (str().is_extract(a, s, offset, length)) {
+        expr_ref len_s(str().mk_length(s), m());
+        // if offset < 0 then 0
+        // elif length <= 0 then 0
+        // elif offset >= len(s) then 0
+        // elif offset + length > len(s) then len(s) - offset
+        // else length
+        expr_ref zero(m_autil.mk_int(0), m());
+        result = length;
+        result = m().mk_ite(m_autil.mk_gt(m_autil.mk_add(offset, length), len_s),
+                            m_autil.mk_sub(len_s, offset),
+                            result);
+        result = m().mk_ite(m().mk_or(m_autil.mk_ge(offset, len_s), m_autil.mk_le(length, zero), m_autil.mk_lt(offset, zero)),
+                            zero,
+                            result);
+        return BR_REWRITE_FULL;
+    }
+#endif
     return BR_FAILED;
 }
 

src/parsers/smt2/smt2scanner.cpp

@@ -271,6 +271,7 @@ namespace smt2 {
     }
 
     scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) :
+        ctx(ctx),
         m_interactive(interactive),
         m_spos(0),
         m_curr(0), // avoid Valgrind warning
@@ -283,7 +284,6 @@ namespace smt2 {
         m_stream(stream),
         m_cache_input(false) {
 
-        m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
 
         for (int i = 0; i < 256; ++i) {
             m_normalized[i] = (signed char) i;
@@ -366,7 +366,7 @@ namespace smt2 {
                 if (t == NULL_TOKEN) break;
                 return t;
             case '-':
-                if (m_smtlib2_compliant)
+                if (ctx.params().m_smtlib2_compliant)
                     return read_symbol();
                 else
                     return read_signed_number();

src/parsers/smt2/smt2scanner.h

@@ -30,6 +30,7 @@ namespace smt2 {
 
     class scanner {
     private:
+        cmd_context&       ctx;
         bool               m_interactive;
         int                m_spos; // position in the current line of the stream
         char               m_curr;  // current char;
@@ -54,7 +55,6 @@ namespace smt2 {
         svector<char>      m_cache;
         svector<char>      m_cache_result;
 
-        bool               m_smtlib2_compliant;
 
         char curr() const { return m_curr; }
         void new_line() { m_line++; m_spos = 0; }

src/smt/theory_seq.cpp

@@ -1579,6 +1579,8 @@ void theory_seq::add_length(expr* e, expr* l) {
    Add length limit restrictions to sequence s.
  */
 void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
+    if (m_sk.is_skolem(s))
+        return;
     expr_ref lim_e = m_ax.add_length_limit(s, k);
     unsigned k0 = 0;
     if (m_length_limit_map.find(s, k0)) {