Merge branch 'upstream-master' into develop

scripts/mk_util.py

@@ -2685,8 +2685,8 @@ def get_full_version_string(major, minor, build, revision):
     if GIT_HASH:
         res += " " + GIT_HASH
     if GIT_DESCRIBE:
-        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long'])
+        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
-        res += " master " + check_output(['git', 'describe'])
+        res += " " + branch + " " + check_output(['git', 'describe'])
     return '"' + res + '"'
 
 # Update files with the version number

src/api/api_quant.cpp

@@ -69,14 +69,17 @@ extern "C" {
         }
         expr * const* ps = reinterpret_cast<expr * const*>(patterns);
         expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
-        pattern_validator v(mk_c(c)->m());
+        symbol qid = to_symbol(quantifier_id);
-        for (unsigned i = 0; i < num_patterns; i++) {
+        bool is_rec = mk_c(c)->m().rec_fun_qid() == qid;
-            if (!v(num_decls, ps[i], 0, 0)) {
+        if (!is_rec) {
-                SET_ERROR_CODE(Z3_INVALID_PATTERN);
+            pattern_validator v(mk_c(c)->m());
-                return 0;
+            for (unsigned i = 0; i < num_patterns; i++) {
+                if (!v(num_decls, ps[i], 0, 0)) {
+                    SET_ERROR_CODE(Z3_INVALID_PATTERN);
+                    return 0;
+                }
             }
         }
-
         sort* const* ts = reinterpret_cast<sort * const*>(sorts);
         svector<symbol> names;
         for (unsigned i = 0; i < num_decls; ++i) {
@@ -88,7 +91,7 @@ extern "C" {
                 (0 != is_forall),
                 names.size(), ts, names.c_ptr(), to_expr(body),
                 weight,
-                to_symbol(quantifier_id),
+                qid,
                 to_symbol(skolem_id),
                 num_patterns, ps,
                 num_no_patterns, no_ps

src/api/python/z3/z3.py

@@ -3701,12 +3701,8 @@ def Extract(high, low, a):
         high = StringVal(high)
     if is_seq(high):
         s = high
-        offset = _py2expr(low, high.ctx)
+        offset, length = _coerce_exprs(low, a, s.ctx)
-        length = _py2expr(a, high.ctx)
+        return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
-
-        if __debug__:
-            _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers")
-            return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
     if __debug__:
         _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
         _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")

src/ast/arith_decl_plugin.cpp

@@ -35,7 +35,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
 
     ~algebraic_numbers_wrapper() {
     }
-    
+
     unsigned mk_id(algebraic_numbers::anum const & val) {
         SASSERT(!m_amanager.is_rational(val));
         unsigned new_id = m_id_gen.mk();
@@ -121,7 +121,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_int_decl = m->mk_sort(symbol("Int"), sort_info(id, INT_SORT));
     m->inc_ref(m_int_decl);
     sort * i = m_int_decl;
-    
+
     sort * b = m->mk_bool_sort();
 
 #define MK_PRED(FIELD, NAME, KIND, SORT) {                      \
@@ -140,7 +140,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     MK_PRED(m_i_ge_decl, ">=", OP_GE, i);
     MK_PRED(m_i_lt_decl, "<",  OP_LT, i);
     MK_PRED(m_i_gt_decl, ">",  OP_GT, i);
-    
+
 #define MK_AC_OP(FIELD, NAME, KIND, SORT) {                             \
         func_decl_info info(id, KIND);                                  \
         info.set_associative();                                         \
@@ -205,7 +205,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     MK_UNARY(m_asinh_decl, "asinh", OP_ASINH, r);
     MK_UNARY(m_acosh_decl, "acosh", OP_ACOSH, r);
     MK_UNARY(m_atanh_decl, "atanh", OP_ATANH, r);
-    
+
     func_decl * pi_decl = m->mk_const_decl(symbol("pi"), r, func_decl_info(id, OP_PI));
     m_pi = m->mk_const(pi_decl);
     m->inc_ref(m_pi);
@@ -213,7 +213,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     func_decl * e_decl  = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E));
     m_e = m->mk_const(e_decl);
     m->inc_ref(m_e);
-    
+
     func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
     m_0_pw_0_int = m->mk_const(z_pw_z_int);
     m->inc_ref(m_0_pw_0_int);
@@ -221,7 +221,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
     m_0_pw_0_real = m->mk_const(z_pw_z_real);
     m->inc_ref(m_0_pw_0_real);
-    
+
     MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
     MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
     MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
@@ -285,7 +285,8 @@ arith_decl_plugin::arith_decl_plugin():
     m_idiv_0_decl(0),
     m_mod_0_decl(0),
     m_u_asin_decl(0),
-    m_u_acos_decl(0) {
+    m_u_acos_decl(0),
+    m_convert_int_numerals_to_real(false) {
 }
 
 arith_decl_plugin::~arith_decl_plugin() {
@@ -418,7 +419,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
     if (val.is_unsigned()) {
         unsigned u_val = val.get_unsigned();
         if (u_val < MAX_SMALL_NUM_TO_CACHE) {
-            if (is_int) {
+            if (is_int && !m_convert_int_numerals_to_real) {
                 app * r = m_small_ints.get(u_val, 0);
                 if (r == 0) {
                     parameter p[2] = { parameter(val), parameter(1) };
@@ -442,7 +443,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
     }
     parameter p[2] = { parameter(val), parameter(static_cast<int>(is_int)) };
     func_decl * decl;
-    if (is_int) 
+    if (is_int && !m_convert_int_numerals_to_real)
         decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
     else
         decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
@@ -479,14 +480,14 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args
 }
 
 static bool is_const_op(decl_kind k) {
-    return 
+    return
-        k == OP_PI || 
+        k == OP_PI ||
         k == OP_E  ||
         k == OP_0_PW_0_INT ||
         k == OP_0_PW_0_REAL;
 }
-    
+
-func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
     if (k == OP_NUM)
         return mk_num_decl(num_parameters, parameters, arity);
@@ -503,7 +504,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     }
 }
 
-func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned num_args, expr * const * args, sort * range) {
     if (k == OP_NUM)
         return mk_num_decl(num_parameters, parameters, num_args);
@@ -521,9 +522,17 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
 }
 
 void arith_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
-    // TODO: only define Int and Real in the right logics
+    if (logic == "NRA" ||
-    sort_names.push_back(builtin_name("Int", INT_SORT));
+        logic == "QF_NRA" ||
-    sort_names.push_back(builtin_name("Real", REAL_SORT));
+        logic == "QF_UFNRA") {
+        m_convert_int_numerals_to_real = true;
+        sort_names.push_back(builtin_name("Real", REAL_SORT));
+    }
+    else {
+        // TODO: only define Int and Real in the right logics
+        sort_names.push_back(builtin_name("Int", INT_SORT));
+        sort_names.push_back(builtin_name("Real", REAL_SORT));
+    }
 }
 
 void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
@@ -563,16 +572,16 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
 }
 
 bool arith_decl_plugin::is_value(app * e) const {
-    return 
+    return
-        is_app_of(e, m_family_id, OP_NUM) || 
+        is_app_of(e, m_family_id, OP_NUM) ||
         is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) ||
         is_app_of(e, m_family_id, OP_PI) ||
         is_app_of(e, m_family_id, OP_E);
 }
 
 bool arith_decl_plugin::is_unique_value(app * e) const {
-    return 
+    return
-        is_app_of(e, m_family_id, OP_NUM) || 
+        is_app_of(e, m_family_id, OP_NUM) ||
         is_app_of(e, m_family_id, OP_PI) ||
         is_app_of(e, m_family_id, OP_E);
 }
@@ -671,7 +680,7 @@ expr_ref arith_util::mk_mul_simplify(expr_ref_vector const& args) {
 }
 expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) {
     expr_ref result(m_manager);
-    
+
     switch (sz) {
     case 0:
         result = mk_numeral(rational(1), true);
@@ -681,7 +690,7 @@ expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) {
         break;
     default:
         result = mk_mul(sz, args);
-        break;                    
+        break;
     }
     return result;
 }
@@ -692,7 +701,7 @@ expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) {
 }
 expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
     expr_ref result(m_manager);
-    
+
     switch (sz) {
     case 0:
         result = mk_numeral(rational(0), true);
@@ -702,7 +711,7 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
         break;
     default:
         result = mk_add(sz, args);
-        break;                    
+        break;
     }
     return result;
 }

src/ast/arith_decl_plugin.h

@@ -152,6 +152,8 @@ protected:
     ptr_vector<app> m_small_ints;
     ptr_vector<app> m_small_reals;
 
+    bool        m_convert_int_numerals_to_real;
+
     func_decl * mk_func_decl(decl_kind k, bool is_real);
     virtual void set_manager(ast_manager * m, family_id id);
     decl_kind fix_kind(decl_kind k, unsigned arity);

src/ast/bv_decl_plugin.h

@@ -406,11 +406,11 @@ public:
     app * mk_bv_not(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNOT, arg); }
     app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args);  }
     app * mk_bv_neg(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNEG, arg); }
-    app * mk_bv_urem(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); }
+    app * mk_bv_urem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); }
-    app * mk_bv_srem(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
+    app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
-    app * mk_bv_add(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
+    app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
-    app * mk_bv_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
+    app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
-    app * mk_bv_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
+    app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
     app * mk_zero_extend(unsigned n, expr* e) {
         parameter p(n);
         return m_manager.mk_app(get_fid(), OP_ZERO_EXT, 1, &p, 1, &e);

src/ast/decl_collector.cpp

@@ -23,8 +23,21 @@ void decl_collector::visit_sort(sort * n) {
     family_id fid = n->get_family_id();
     if (m().is_uninterp(n))
         m_sorts.push_back(n);
-    if (fid == m_dt_fid)
+    if (fid == m_dt_fid) {
         m_sorts.push_back(n);
+
+        unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
+        for (unsigned i = 0; i < num_cnstr; i++) {
+            func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
+            m_decls.push_back(cnstr);
+            ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
+            unsigned num_cas = cnstr_acc.size();
+            for (unsigned j = 0; j < num_cas; j++) {
+                func_decl * accsr = cnstr_acc.get(j);
+                m_decls.push_back(accsr);
+            }
+        }
+    }
 }
 
 bool decl_collector::is_bool(sort * s) {
@@ -38,14 +51,15 @@ void decl_collector::visit_func(func_decl * n) {
             m_preds.push_back(n);
         else
             m_decls.push_back(n);
-    }        
+    }
 }
 
 decl_collector::decl_collector(ast_manager & m, bool preds):
     m_manager(m),
-    m_sep_preds(preds) {
+    m_sep_preds(preds),
+    m_dt_util(m) {
     m_basic_fid = m_manager.get_basic_family_id();
-    m_dt_fid    = m_manager.mk_family_id("datatype");
+    m_dt_fid = m_dt_util.get_family_id();
 }
 
 void decl_collector::visit(ast* n) {
@@ -55,7 +69,7 @@ void decl_collector::visit(ast* n) {
         n = todo.back();
         todo.pop_back();
         if (!m_visited.is_marked(n)) {
-            m_visited.mark(n, true);                
+            m_visited.mark(n, true);
             switch(n->get_kind()) {
             case AST_APP: {
                 app * a = to_app(n);
@@ -64,7 +78,7 @@ void decl_collector::visit(ast* n) {
                 }
                 todo.push_back(a->get_decl());
                 break;
-            }                    
+            }
             case AST_QUANTIFIER: {
                 quantifier * q = to_quantifier(n);
                 unsigned num_decls = q->get_num_decls();
@@ -77,7 +91,7 @@ void decl_collector::visit(ast* n) {
                 }
                 break;
             }
-            case AST_SORT: 
+            case AST_SORT:
                 visit_sort(to_sort(n));
                 break;
             case AST_FUNC_DECL: {

src/ast/decl_collector.h

@@ -21,6 +21,7 @@ Revision History:
 #define SMT_DECL_COLLECTOR_H_
 
 #include"ast.h"
+#include"datatype_decl_plugin.h"
 
 class decl_collector {
     ast_manager &         m_manager;
@@ -28,9 +29,10 @@ class decl_collector {
     ptr_vector<sort>      m_sorts;
     ptr_vector<func_decl> m_decls;
     ptr_vector<func_decl> m_preds;
-    ast_mark m_visited;
+    ast_mark              m_visited;
-    family_id m_basic_fid;
+    family_id             m_basic_fid;
-    family_id m_dt_fid;
+    family_id             m_dt_fid;
+    datatype_util         m_dt_util;
 
     void visit_sort(sort* n);
     bool is_bool(sort* s);

src/ast/macros/macro_util.cpp

@@ -19,22 +19,22 @@ Revision History:
 --*/
 #include"macro_util.h"
 #include"occurs.h"
+#include"ast_util.h"
 #include"arith_simplifier_plugin.h"
-#include"basic_simplifier_plugin.h"
 #include"bv_simplifier_plugin.h"
 #include"var_subst.h"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"
-#include"ast_util.h"
 #include"for_each_expr.h"
 #include"well_sorted.h"
+#include"bool_rewriter.h"
 
 macro_util::macro_util(ast_manager & m, simplifier & s):
     m_manager(m),
+    m_bv(m),
     m_simplifier(s),
     m_arith_simp(0),
     m_bv_simp(0),
-    m_basic_simp(0),
     m_forbidden_set(0),
     m_curr_clause(0) {
 }
@@ -55,24 +55,17 @@ bv_simplifier_plugin * macro_util::get_bv_simp() const {
     return m_bv_simp;
 }
 
-basic_simplifier_plugin * macro_util::get_basic_simp() const {
-    if (m_basic_simp == 0) {
-        const_cast<macro_util*>(this)->m_basic_simp = static_cast<basic_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.get_basic_family_id()));
-    }
-    SASSERT(m_basic_simp != 0);
-    return m_basic_simp;
-}
 
 bool macro_util::is_bv(expr * n) const {
-    return get_bv_simp()->is_bv(n);
+    return m_bv.is_bv(n);
 }
 
 bool macro_util::is_bv_sort(sort * s) const {
-    return get_bv_simp()->is_bv_sort(s);
+    return m_bv.is_bv_sort(s);
 }
 
 bool macro_util::is_add(expr * n) const {
-    return get_arith_simp()->is_add(n) || get_bv_simp()->is_add(n);
+    return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n);
 }
 
 bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
@@ -80,11 +73,11 @@ bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
 }
 
 bool macro_util::is_le(expr * n) const {
-    return get_arith_simp()->is_le(n) || get_bv_simp()->is_le(n);
+    return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
 }
 
 bool macro_util::is_le_ge(expr * n) const {
-    return get_arith_simp()->is_le_ge(n) || get_bv_simp()->is_le_ge(n);
+    return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
 }
 
 poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const {
@@ -102,7 +95,7 @@ app * macro_util::mk_zero(sort * s) const {
 
 void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
     if (is_bv(t1)) {
-        get_bv_simp()->mk_sub(t1, t2, r);
+        r = m_bv.mk_bv_sub(t1, t2);
     }
     else {
         get_arith_simp()->mk_sub(t1, t2, r);
@@ -111,7 +104,7 @@ void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
 
 void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
     if (is_bv(t1)) {
-        get_bv_simp()->mk_add(t1, t2, r);
+        r = m_bv.mk_bv_add(t1, t2);
     }
     else {
         get_arith_simp()->mk_add(t1, t2, r);
@@ -429,7 +422,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
         new_args.push_back(new_var);
         new_conds.push_back(new_cond);
     }
-    get_basic_simp()->mk_and(new_conds.size(), new_conds.c_ptr(), cond);
+    bool_rewriter(m_manager).mk_and(new_conds.size(), new_conds.c_ptr(), cond);
     head = m_manager.mk_app(qhead->get_decl(), new_args.size(), new_args.c_ptr());
     num_decls = next_var_idx;
 }
@@ -687,7 +680,7 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def,
             if (cond == 0)
                 new_cond = extra_cond;
             else
-                get_basic_simp()->mk_and(cond, extra_cond, new_cond);
+                bool_rewriter(m_manager).mk_and(cond, extra_cond, new_cond);
         }
         else {
             hint_to_macro_head(m_manager, head, num_decls, new_head);
@@ -719,20 +712,19 @@ void macro_util::get_rest_clause_as_cond(expr * except_lit, expr_ref & extra_con
     if (m_curr_clause == 0)
         return;
     SASSERT(is_clause(m_manager, m_curr_clause));
-    basic_simplifier_plugin * bs = get_basic_simp();
     expr_ref_buffer neg_other_lits(m_manager);
     unsigned num_lits = get_clause_num_literals(m_manager, m_curr_clause);
     for (unsigned i = 0; i < num_lits; i++) {
         expr * l = get_clause_literal(m_manager, m_curr_clause, i);
         if (l != except_lit) {
             expr_ref neg_l(m_manager);
-            bs->mk_not(l, neg_l);
+            bool_rewriter(m_manager).mk_not(l, neg_l);
             neg_other_lits.push_back(neg_l);
         }
     }
     if (neg_other_lits.empty())
         return;
-    get_basic_simp()->mk_and(neg_other_lits.size(), neg_other_lits.c_ptr(), extra_cond);
+    bool_rewriter(m_manager).mk_and(neg_other_lits.size(), neg_other_lits.c_ptr(), extra_cond);
 }
 
 void macro_util::collect_poly_args(expr * n, expr * exception, ptr_buffer<expr> & args) {

src/ast/macros/macro_util.h

@@ -62,10 +62,10 @@ public:
 
 private:
     ast_manager &               m_manager;
+    bv_util                     m_bv;
     simplifier &                m_simplifier;
     arith_simplifier_plugin *   m_arith_simp;
     bv_simplifier_plugin    *   m_bv_simp;
-    basic_simplifier_plugin *   m_basic_simp;
     obj_hashtable<func_decl> *  m_forbidden_set;
 
     bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
@@ -99,7 +99,6 @@ public:
 
     arith_simplifier_plugin * get_arith_simp() const;
     bv_simplifier_plugin * get_bv_simp() const;
-    basic_simplifier_plugin * get_basic_simp() const;
 
     bool is_macro_head(expr * n, unsigned num_decls) const;
     bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;

src/ast/rewriter/rewriter_def.h

@@ -189,10 +189,9 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
             fr.m_state = REWRITE_BUILTIN;
-            unsigned max_depth = fr.m_max_depth;
             if (visit<false>(arg, fr.m_max_depth)) {
                 m_r = result_stack().back();
-                result_stack().pop_back(); 
+                result_stack().pop_back();
                 result_stack().pop_back();
                 result_stack().push_back(m_r);
                 cache_result<false>(t, m_r, m_pr, fr.m_cache_result);

src/ast/rewriter/seq_rewriter.cpp

@@ -12,6 +12,7 @@ Abstract:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2015-12-5
+    Murphy Berzish 2017-02-21
 
 Notes:
 
@@ -548,30 +549,56 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
 
-    // case 1: pos<0 or len<0
+    // case 1: pos<0 or len<=0
     // rewrite to ""
-    if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) {
+    if ( (constantPos && pos.is_neg()) || (constantLen && !len.is_pos()) ) {
         result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
     // case 1.1: pos >= length(base)
     // rewrite to ""
-    if (constantBase && constantPos && pos.get_unsigned() >= s.length()) {
+    if (constantBase && constantPos && pos >= rational(s.length())) {
         result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
 
+    constantPos &= pos.is_unsigned();
+    constantLen &= len.is_unsigned();
+
     if (constantBase && constantPos && constantLen) {
         if (pos.get_unsigned() + len.get_unsigned() >= s.length()) {
             // case 2: pos+len goes past the end of the string
             unsigned _len = s.length() - pos.get_unsigned() + 1;
             result = m_util.str.mk_string(s.extract(pos.get_unsigned(), _len));
-            return BR_DONE;
         } else {
             // case 3: pos+len still within string
             result = m_util.str.mk_string(s.extract(pos.get_unsigned(), len.get_unsigned()));
-            return BR_DONE;
         }
+        return BR_DONE;
+    }
+
+    if (constantPos && constantLen) {
+        unsigned _pos = pos.get_unsigned();
+        unsigned _len = len.get_unsigned();
+        SASSERT(_len > 0);
+        expr_ref_vector as(m()), bs(m());
+        m_util.str.get_concat(a, as);
+        for (unsigned i = 0; i < as.size() && _len > 0; ++i) {
+            if (m_util.str.is_unit(as[i].get())) {
+                if (_pos == 0) {
+                    bs.push_back(as[i].get());
+                    --_len;
+                }
+                else {
+                    --_pos;
+                }
+            }              
+            else {
+                return BR_FAILED;
+            }
+        }
+        result = m_util.str.mk_concat(bs);
+        return BR_DONE;
     }
 
     return BR_FAILED;
@@ -674,10 +701,33 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
             result = m_util.str.mk_empty(m().get_sort(a));
             return BR_DONE;
         }
-        if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) {
+        if (m_util.str.is_string(a, c)) {
-            result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1));
+            if (r.is_unsigned() && r < rational(c.length())) {
+                result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1));
+            }
+            else {
+                result = m_util.str.mk_empty(m().get_sort(a));
+            }
             return BR_DONE;
-        } 
+        }
+        if (r.is_unsigned()) {
+            len = r.get_unsigned();
+            expr_ref_vector as(m());
+            m_util.str.get_concat(a, as);
+            for (unsigned i = 0; i < as.size(); ++i) {
+                if (m_util.str.is_unit(as[i].get())) {
+                    if (len == 0) {
+                        result = as[i].get();
+                        return BR_DONE;
+                    }
+                    --len;
+                }         
+                else {
+                    return BR_FAILED;
+                }
+            }
+        }
+        
     }
     return BR_FAILED;
 }

src/cmd_context/basic_cmds.cpp

@@ -100,13 +100,34 @@ public:
 
 ATOMIC_CMD(exit_cmd, "exit", "exit.", ctx.print_success(); throw stop_parser_exception(););
 
-ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat command", {
+class get_model_cmd : public cmd {
-    if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
+    unsigned m_index;
-        throw cmd_exception("model is not available");
+public:
-    model_ref m;
+    get_model_cmd(): cmd("get-model"), m_index(0) {}
-    ctx.get_check_sat_result()->get_model(m);
+    virtual char const * get_usage() const { return "[<index of box objective>]"; }   
-    ctx.display_model(m);
+    virtual char const * get_descr(cmd_context & ctx) const { 
-});
+        return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; 
+    }
+    virtual unsigned get_arity() const { return VAR_ARITY; } 
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; }
+    virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }                           
+    virtual void execute(cmd_context & ctx) { 
+        if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
+            throw cmd_exception("model is not available");
+        model_ref m;
+        if (m_index > 0 && ctx.get_opt()) {
+            ctx.get_opt()->get_box_model(m, m_index);
+        }
+        else {
+            ctx.get_check_sat_result()->get_model(m);
+        }
+        ctx.display_model(m);
+    }                    
+    virtual void reset(cmd_context& ctx) {
+        m_index = 0;
+    }
+};
+
 
 ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
     if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)

src/cmd_context/cmd_context.cpp

@@ -742,8 +742,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     lhs = m().mk_app(f, binding.size(), binding.c_ptr());
     eq  = m().mk_eq(lhs, e);
     if (!ids.empty()) {
-        expr* pat = m().mk_pattern(lhs);
+        if (!is_app(e)) {
-        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 1, &pat);
+            throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)");
+        }
+        expr* pats[2] = { m().mk_pattern(lhs), m().mk_pattern(to_app(e)) };
+        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 2, pats);
     }
 
     //

src/cmd_context/cmd_context.h

@@ -124,6 +124,7 @@ public:
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
     virtual bool print_model() const = 0;
+    virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
     virtual void updt_params(params_ref const& p) = 0;
 };
 

src/cmd_context/eval_cmd.cpp

@@ -38,6 +38,7 @@ public:
     virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
         model_evaluator::get_param_descrs(p);
         insert_timeout(p);
+        p.insert("model_index", CPK_UINT, "(default: 0) index of model from box optimization objective");
     }
 
     virtual void prepare(cmd_context & ctx) { 
@@ -58,9 +59,15 @@ public:
         if (!ctx.is_model_available())
             throw cmd_exception("model is not available");
         model_ref md;
+        unsigned index = m_params.get_uint("model_index", 0);
         check_sat_result * last_result = ctx.get_check_sat_result();
         SASSERT(last_result);
-        last_result->get_model(md);
+        if (index == 0 || !ctx.get_opt()) {
+            last_result->get_model(md);
+        }
+        else {
+            ctx.get_opt()->get_box_model(md, index);
+        }
         expr_ref r(ctx.m());
         unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
         unsigned rlimit  = m_params.get_uint("rlimit", 0);

src/opt/opt_context.cpp

@@ -273,7 +273,8 @@ namespace opt {
         display_benchmark();
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
         lbool is_sat = s.check_sat(0,0);
-        TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
+        TRACE("opt", tout << "initial search result: " << is_sat << "\n";
+              s.display(tout););
         if (is_sat != l_false) {
             s.get_model(m_model);
             s.get_labels(m_labels);
@@ -341,6 +342,14 @@ namespace opt {
         fix_model(mdl);
     }
 
+    void context::get_box_model(model_ref& mdl, unsigned index) {
+        if (index >= m_box_models.size()) {
+            throw default_exception("index into models is out of bounds");
+        }
+        mdl = m_box_models[index];
+        fix_model(mdl);
+    }
+
     lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
         if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index, is_max);
@@ -1037,6 +1046,10 @@ namespace opt {
             TRACE("opt", tout << "Purifying " << term << "\n";);
             term = purify(fm, term);
         }
+        else if (m.is_ite(term)) {
+            TRACE("opt", tout << "Purifying " << term << "\n";);
+            term = purify(fm, term);
+        }
         if (fm) {
             m_model_converter = concat(m_model_converter.get(), fm.get());
         }

src/opt/opt_context.h

@@ -186,6 +186,7 @@ namespace opt {
         virtual bool print_model() const;
         virtual void set_model(model_ref& _m) { m_model = _m; }
         virtual void get_model(model_ref& _m);
+        virtual void get_box_model(model_ref& _m, unsigned index);
         virtual void fix_model(model_ref& _m);
         virtual void collect_statistics(statistics& stats) const;
         virtual proof* get_proof() { return 0; }

src/opt/opt_solver.cpp

@@ -358,6 +358,7 @@ namespace opt {
         }
         smt::theory_opt& opt = get_optimizer();
         smt::theory_var v = m_objective_vars[var];
+        TRACE("opt", tout << "v" << var << " " << val << "\n";);
 
         if (typeid(smt::theory_inf_arith) == typeid(opt)) {
             smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt); 
@@ -387,8 +388,32 @@ namespace opt {
             smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
             return th.mk_ge(m_fm, v, val);
         }
+        
+        if (typeid(smt::theory_dense_i) == typeid(opt) &&
+            val.get_infinitesimal().is_zero()) {
+            smt::theory_dense_i& th = dynamic_cast<smt::theory_dense_i&>(opt);
+            return th.mk_ge(m_fm, v, val);
+        }
 
-        // difference logic?
+        if (typeid(smt::theory_dense_mi) == typeid(opt) &&
+            val.get_infinitesimal().is_zero()) {
+            smt::theory_dense_mi& th = dynamic_cast<smt::theory_dense_mi&>(opt);
+            return th.mk_ge(m_fm, v, val);
+        }
+
+        if (typeid(smt::theory_dense_si) == typeid(opt) &&
+            val.get_infinitesimal().is_zero()) {
+            smt::theory_dense_si& th = dynamic_cast<smt::theory_dense_si&>(opt);
+            return th.mk_ge(m_fm, v, val);
+        }
+
+        if (typeid(smt::theory_dense_smi) == typeid(opt) &&
+            val.get_infinitesimal().is_zero()) {
+            smt::theory_dense_smi& th = dynamic_cast<smt::theory_dense_smi&>(opt);
+            return th.mk_ge(m_fm, v, val);
+        }
+        
+        IF_VERBOSE(0, verbose_stream() << "WARNING: unhandled theory " << typeid(opt).name() << "\n";);
         return expr_ref(m.mk_true(), m);
     } 
 

src/sat/sat_solver.cpp

@@ -101,7 +101,7 @@ namespace sat {
                     if (!it->is_binary_non_learned_clause())
                         continue;
                     literal l2 = it->get_literal();
-                    if (l.index() > l2.index()) 
+                    if (l.index() > l2.index())
                         continue;
                     mk_clause_core(l, l2);
                 }
@@ -223,7 +223,7 @@ namespace sat {
         if (propagate_bin_clause(l1, l2)) {
             if (scope_lvl() == 0)
                 return;
-            if (!learned) 
+            if (!learned)
                 m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
         }
         m_stats.m_mk_bin_clause++;
@@ -248,7 +248,7 @@ namespace sat {
     void solver::push_reinit_stack(clause & c) {
         TRACE("sat_reinit", tout << "adding to reinit stack: " << c << "\n";);
         m_clauses_to_reinit.push_back(clause_wrapper(c));
-        c.set_reinit_stack(true);    
+        c.set_reinit_stack(true);
     }
 
 
@@ -257,7 +257,7 @@ namespace sat {
         clause * r = m_cls_allocator.mk_clause(3, lits, learned);
         bool reinit = attach_ter_clause(*r);
         if (reinit && !learned) push_reinit_stack(*r);
-        
+
         if (learned)
             m_learned.push_back(r);
         else
@@ -806,22 +806,22 @@ namespace sat {
             m_params.set_uint("random_seed", m_rand());
             if (i == 1 + num_threads/2) {
                 m_params.set_sym("phase", symbol("random"));
-            }                        
+            }
             solvers[i] = alloc(sat::solver, m_params, rlims[i], 0);
             solvers[i]->copy(*this);
             solvers[i]->set_par(&par);
-            scoped_rlimit.push_child(&solvers[i]->rlimit());            
+            scoped_rlimit.push_child(&solvers[i]->rlimit());
         }
         set_par(&par);
         m_params.set_sym("phase", saved_phase);
         int finished_id = -1;
         std::string        ex_msg;
-        par_exception_kind ex_kind;
+        par_exception_kind ex_kind = DEFAULT_EX;
         unsigned error_code = 0;
         lbool result = l_undef;
         #pragma omp parallel for
         for (int i = 0; i < num_threads; ++i) {
-            try {                
+            try {
                 lbool r = l_undef;
                 if (i < num_extra_solvers) {
                     r = solvers[i]->check(num_lits, lits);
@@ -851,7 +851,7 @@ namespace sat {
                             rlims[j].cancel();
                         }
                     }
-                }                
+                }
             }
             catch (z3_error & err) {
                 if (i == 0) {
@@ -871,7 +871,7 @@ namespace sat {
             m_stats = solvers[finished_id]->m_stats;
         }
 
-        for (int i = 0; i < num_extra_solvers; ++i) {            
+        for (int i = 0; i < num_extra_solvers; ++i) {
             dealloc(solvers[i]);
         }
         if (finished_id == -1) {
@@ -1140,7 +1140,7 @@ namespace sat {
             for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) {
                 assign(m_assumptions[i], justification());
             }
-            TRACE("sat", 
+            TRACE("sat",
                  for (unsigned i = 0; i < m_assumptions.size(); ++i) {
                      index_set s;
                      if (m_antecedents.find(m_assumptions[i].var(), s)) {
@@ -2037,7 +2037,7 @@ namespace sat {
             }
         }
 
-        literal consequent = m_not_l; 
+        literal consequent = m_not_l;
         justification js   = m_conflict;
 
 
@@ -3115,7 +3115,7 @@ namespace sat {
             literal_pair p(l1, l2);
             if (!seen_bc.contains(p)) {
                 seen_bc.insert(p);
-                mc.add_edge(l1.index(), l2.index());             
+                mc.add_edge(l1.index(), l2.index());
             }
         }
         vector<unsigned_vector> _mutexes;
@@ -3168,7 +3168,7 @@ namespace sat {
     }
 
     void solver::fixup_consequence_core() {
-        index_set s;        
+        index_set s;
         TRACE("sat", tout << m_core << "\n";);
         for (unsigned i = 0; i < m_core.size(); ++i) {
             TRACE("sat", tout << m_core[i] << ": "; display_index_set(tout, m_antecedents.find(m_core[i].var())) << "\n";);
@@ -3218,20 +3218,20 @@ namespace sat {
         while (true) {
             ++num_iterations;
             SASSERT(!inconsistent());
-            
+
             lbool r = bounded_search();
             if (r != l_undef) {
                 fixup_consequence_core();
                 return r;
             }
-            
+
             extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
 
             if (m_conflicts > m_config.m_max_conflicts) {
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";);
                 return l_undef;
             }
-            
+
             restart();
             simplify_problem();
             if (check_inconsistent()) {
@@ -3239,11 +3239,11 @@ namespace sat {
                 return l_false;
             }
             gc();
-            
+
             if (m_config.m_restart_max <= num_iterations) {
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
                 return l_undef;
-            }            
+            }
         }
     }
 

src/smt/smt_conflict_resolution.cpp

@@ -59,9 +59,9 @@ namespace smt {
         SASSERT(n->trans_reaches(n->get_root()));
         while (n) {
             if (Set)
-                n->set_mark();
+                n->set_mark2();
             else
-                n->unset_mark();
+                n->unset_mark2();
             n = n->m_trans.m_target;
         }
     }
@@ -84,7 +84,7 @@ namespace smt {
         mark_enodes_in_trans<true>(n1);
         while (true) {
             SASSERT(n2);
-            if (n2->is_marked()) {
+            if (n2->is_marked2()) {
                 mark_enodes_in_trans<false>(n1);
                 return n2;
             }

src/smt/smt_context.cpp

@@ -4372,42 +4372,21 @@ namespace smt {
         for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
             expr* e = m_asserted_formulas.get_formula(i);
             if (is_quantifier(e)) {
+                TRACE("context", tout << mk_pp(e, m) << "\n";);
                 quantifier* q = to_quantifier(e);
                 if (!m.is_rec_fun_def(q)) continue;
-                SASSERT(q->get_num_patterns() == 1);
+                SASSERT(q->get_num_patterns() == 2);
                 expr* fn = to_app(q->get_pattern(0))->get_arg(0);
+                expr* body = to_app(q->get_pattern(1))->get_arg(0);
                 SASSERT(is_app(fn));
                 func_decl* f = to_app(fn)->get_decl();
-                expr* eq = q->get_expr();
+                func_interp* fi = alloc(func_interp, m, f->get_arity());
-                expr_ref body(m);
+                fi->set_else(body);
-                if (is_fun_def(fn, q->get_expr(), body)) {
+                m_model->register_decl(f, fi);            
-                    func_interp* fi = alloc(func_interp, m, f->get_arity());
-                    fi->set_else(body);
-                    m_model->register_decl(f, fi);
-                }
             }
         }
     }
 
-    bool context::is_fun_def(expr* f, expr* body, expr_ref& result) {
-        expr* t1, *t2, *t3;
-        if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) {
-            if (t1 == f) return result = t2, true;
-            if (t2 == f) return result = t1, true;
-            return false;
-        }
-        if (m_manager.is_ite(body, t1, t2, t3)) {
-            expr_ref body1(m_manager), body2(m_manager);
-            if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) {
-                // f is not free in t1
-                result = m_manager.mk_ite(t1, body1, body2);
-                return true;
-            }
-        }
-        return false;
-    }
-
-
 };
 
 

src/smt/smt_context.h

@@ -1197,8 +1197,6 @@ namespace smt {
 
         void add_rec_funs_to_model();
 
-        bool is_fun_def(expr* f, expr* q, expr_ref& body);
-
     public:
         bool can_propagate() const;
 

src/smt/smt_context_pp.cpp

@@ -606,14 +606,14 @@ namespace smt {
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
-            if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
+            if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
             break;
         }
         case b_justification::JUSTIFICATION: {
             out << "justification ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals_verbose(out, lits.size(), lits.c_ptr());
+            display_literals(out, lits.size(), lits.c_ptr());
             break;
         }
         default:

src/smt/smt_model_checker.cpp

@@ -318,7 +318,7 @@ namespace smt {
 
     bool model_checker::check_rec_fun(quantifier* q) {
         TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
-        SASSERT(q->get_num_patterns() == 1);
+        SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
         expr* fn = to_app(q->get_pattern(0))->get_arg(0);
         SASSERT(is_app(fn));
         func_decl* f = to_app(fn)->get_decl();

src/smt/theory_dense_diff_logic_def.h

@@ -868,7 +868,8 @@ namespace smt {
                 e = ctx.get_enode(to_app(n));                
             }
             else {
-                e = ctx.mk_enode(to_app(n), false, false, true);
+                ctx.internalize(n, false);
+                e = ctx.get_enode(n);
             }            
             v = e->get_th_var(get_id());
             if (v == null_theory_var) {
@@ -1008,7 +1009,8 @@ namespace smt {
             inf_eps result(rational(0), r);
             blocker = mk_gt(v, result);
             IF_VERBOSE(10, verbose_stream() << blocker << "\n";);
-            return result;
+            r += m_objective_consts[v];
+            return inf_eps(rational(0), r);
         }
         default:
             TRACE("opt", tout << "unbounded\n"; );        
@@ -1019,6 +1021,7 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_dense_diff_logic<Ext>::add_objective(app* term) {
+        TRACE("opt", tout << mk_pp(term, get_manager()) << "\n";);
         objective_term objective;
         theory_var result = m_objectives.size();
         rational q(1), r(0);
@@ -1053,6 +1056,7 @@ namespace smt {
         ast_manager& m = get_manager();
         objective_term const& t = m_objectives[v];
         expr_ref e(m), f(m), f2(m);
+        TRACE("opt", tout << "mk_ineq " << v << " " << val << "\n";);
         if (t.size() == 1 && t[0].second.is_one()) {
             f = get_enode(t[0].first)->get_owner();
         }

src/smt/theory_seq.cpp

@@ -1981,6 +1981,7 @@ bool theory_seq::solve_nc(unsigned idx) {
     }
     if (c != n.contains()) {
         m_ncs.push_back(nc(c, deps));
+        m_new_propagation = true;
         return true;
     }
     return false;
@@ -2403,6 +2404,14 @@ void theory_seq::display(std::ostream & out) const {
         }
     }
 
+    if (!m_ncs.empty()) {
+        out << "Non contains:\n";
+        for (unsigned i = 0; i < m_ncs.size(); ++i) {
+            out << "not " << mk_pp(m_ncs[i].contains(), m) << "\n";
+            display_deps(out << "  <- ", m_ncs[i].deps()); out << "\n";
+        }
+    }
+
 }
 
 void theory_seq::display_equations(std::ostream& out) const {
@@ -3496,6 +3505,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
    let e = at(s, i)
 
    0 <= i < len(s) -> s = xey & len(x) = i & len(e) = 1
+   i < 0 \/ i >= len(s) -> e = empty
 
 */
 void theory_seq::add_at_axiom(expr* e) {
@@ -3509,13 +3519,18 @@ void theory_seq::add_at_axiom(expr* e) {
     expr_ref y = mk_skolem(m_post, s, mk_sub(mk_sub(len_s, i), one));
     expr_ref xey   = mk_concat(x, e, y);
     expr_ref len_x(m_util.str.mk_length(x), m);
+    expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
 
     literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
     literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
 
+
     add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
+
+    add_axiom(i_ge_0, mk_eq(s, emp, false));
+    add_axiom(~i_ge_len_s, mk_eq(s, emp, false));
 }
 
 /**

src/util/hwf.cpp

@@ -52,8 +52,10 @@ Revision History:
 
 #ifdef USE_INTRINSICS
 #include <emmintrin.h>
+#if defined(_MSC_VER) || defined(__SSE4_1__)
 #include <smmintrin.h>
 #endif
+#endif
 
 hwf_manager::hwf_manager() :
     m_mpz_manager(m_mpq_manager)
@@ -304,7 +306,9 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
     // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the
     // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
 #ifdef _WINDOWS
-#ifdef USE_INTRINSICS
+#if defined(USE_INTRINSICS) && \
+    (defined(_WINDOWS) && (defined(__AVX__) || defined(_M_X64))) || \
+    (!defined(_WINDOWS) && defined(__SSE4_1__))
     switch (rm) {
     case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break;
     case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break;