diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index c9f6aaa40..5635e6d12 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1095,6 +1095,22 @@ void sudoku_example() {
     }
 }
 
+void param_descrs_example() {
+    std::cout << "parameter description example\n";
+    context c;
+    param_descrs p = param_descrs::simplify_param_descrs(c);
+    std::cout << p << "\n";
+    unsigned sz = p.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        symbol nm = p.name(i);
+        char const* kind = "other";
+        Z3_param_kind k = p.kind(nm);
+        if (k == Z3_PK_UINT) kind = "uint";
+        if (k == Z3_PK_BOOL) kind = "bool";
+        std::cout << nm << ": " << p.documentation(nm) << " kind: " << kind << "\n";
+    }
+}
+
 int main() {
 
     try {
@@ -1136,6 +1152,7 @@ int main() {
         substitute_example(); std::cout << "\n";
         opt_example(); std::cout << "\n";
         extract_example(); std::cout << "\n";
+        param_descrs_example(); std::cout << "\n";
         sudoku_example(); std::cout << "\n";
         std::cout << "done\n";
     }
diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 0c6e2fae4..5e70bac81 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -2341,6 +2341,46 @@ void unsat_core_and_proof_example() {
     Z3_del_context(ctx);
 }
 
+void interpolation_example() {
+    Z3_context ctx = mk_context();
+    Z3_ast pa = mk_bool_var(ctx, "PredA");
+    Z3_ast pb = mk_bool_var(ctx, "PredB");
+    Z3_ast pc = mk_bool_var(ctx, "PredC");
+    Z3_ast args1[2] = {pa,pb}, args2[2] = {Z3_mk_not(ctx,pb),pc};
+    Z3_ast args3[2] = {Z3_mk_interpolant(ctx,Z3_mk_and(ctx,2,args1)),Z3_mk_and(ctx,2,args2)};
+    Z3_ast f = Z3_mk_and(ctx,2,args3);
+    Z3_ast_vector interpolant = 0;
+    Z3_model m = 0;
+
+    printf("\ninterpolation_example\n");
+    LOG_MSG("interpolation_example");
+
+    Z3_lbool result = Z3_compute_interpolant(ctx,f,0,&interpolant,&m);
+
+    switch (result) {
+    case Z3_L_FALSE:
+        printf("unsat\n");
+        printf("interpolant: %s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, interpolant, 0)));
+        printf("\n");
+        break;
+    case Z3_L_UNDEF:
+        printf("unknown\n");
+        printf("potential model:\n");
+	if (m) Z3_model_inc_ref(ctx, m);
+        display_model(ctx, stdout, m);
+        break;
+    case Z3_L_TRUE:
+        printf("sat\n");
+	if (m) Z3_model_inc_ref(ctx, m);
+        display_model(ctx, stdout, m);
+        break;
+    }
+
+    /* delete logical context */
+    if (m) Z3_model_dec_ref(ctx, m);
+    Z3_del_context(ctx);
+}
+
 #define MAX_RETRACTABLE_ASSERTIONS 1024
 
 /**
@@ -2825,6 +2865,7 @@ int main() {
     binary_tree_example();
     enum_example();
     unsat_core_and_proof_example();
+    interpolation_example();
     incremental_example1();
     reference_counter_example();
     smt2parser_example();
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 9df1c9f9a..1e201c5b3 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -289,7 +289,7 @@ extern "C" {
             }
             catch (z3_exception & ex) {
                 mk_c(c)->handle_exception(ex);
-                return Z3_L_UNDEF;
+                RETURN_Z3_compute_interpolant Z3_L_UNDEF;
             }
         }
 
@@ -323,7 +323,7 @@ extern "C" {
 
         *out_interp = of_ast_vector(v);
 
-        return status;
+        RETURN_Z3_compute_interpolant status;
         Z3_CATCH_RETURN(Z3_L_UNDEF);
     }
 
diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
index 19634af32..f2dab4d77 100644
--- a/src/api/api_params.cpp
+++ b/src/api/api_params.cpp
@@ -179,6 +179,19 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s) {
+        Z3_TRY;
+        LOG_Z3_param_descrs_get_documentation(c, p, s);
+        RESET_ERROR_CODE();
+        char const* result = to_param_descrs_ptr(p)->get_descr(to_symbol(s));
+        if (result == 0) {
+            SET_ERROR_CODE(Z3_IOB);
+            RETURN_Z3(0);
+        }
+        return mk_c(c)->mk_external_string(result);
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) {
         Z3_TRY;
         LOG_Z3_param_descrs_to_string(c, p);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index b353499ad..341684ca6 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -49,6 +49,7 @@ namespace z3 {
     class context;
     class symbol;
     class params;
+    class param_descrs;
     class ast;
     class sort;
     class func_decl;
@@ -286,6 +287,9 @@ namespace z3 {
 
     };
 
+
+
+
     template<typename T>
     class array {
         T *      m_array;
@@ -338,6 +342,30 @@ namespace z3 {
     }
 
 
+    class param_descrs : public object {
+        Z3_param_descrs m_descrs;
+    public:
+        param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
+        param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
+        param_descrs& operator=(param_descrs const& o) {
+            Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
+            Z3_param_descrs_dec_ref(ctx(), m_descrs);
+            m_descrs = o.m_descrs;
+            m_ctx = o.m_ctx;
+            return *this;
+        }
+        ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
+        static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); }
+
+        unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
+        symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
+        Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
+        std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
+        std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
+    };
+
+    inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
+
     class params : public object {
         Z3_params m_params;
     public:
@@ -1572,6 +1600,8 @@ namespace z3 {
                                    fmls,
                                    fml));
         }
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
+
     };
     inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
 
@@ -1686,6 +1716,7 @@ namespace z3 {
         friend tactic repeat(tactic const & t, unsigned max);
         friend tactic with(tactic const & t, params const & p);
         friend tactic try_for(tactic const & t, unsigned ms);
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }
     };
 
     inline tactic operator&(tactic const & t1, tactic const & t2) {
diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs
index af2916faa..1809518e1 100644
--- a/src/api/dotnet/ParamDescrs.cs
+++ b/src/api/dotnet/ParamDescrs.cs
@@ -46,6 +46,15 @@ namespace Microsoft.Z3
             return (Z3_param_kind)Native.Z3_param_descrs_get_kind(Context.nCtx, NativeObject, name.NativeObject);
         }
 
+        /// <summary>
+        /// Retrieve documentation of parameter.
+        /// </summary>
+        public string GetDocumentation(Symbol name)
+        {
+            Contract.Requires(name != null);
+            return Native.Z3_param_descrs_get_documentation(Context.nCtx, NativeObject, name.NativeObject);
+        }
+
         /// <summary>
         /// Retrieve all names of parameters.
         /// </summary>
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 9c6fbd0dc..8f8c6df0b 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -44,6 +44,15 @@ public class ParamDescrs extends Z3Object
                 getContext().nCtx(), getNativeObject(), name.getNativeObject()));
     }
 
+    /**
+     * Retrieve documentation of parameter.
+     **/
+
+     public String getDocumentation(Symbol name)
+     {
+	 return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
+     }
+
     /**
      * Retrieve all names of parameters.
      * 
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 323e57c79..9f3b0a1b9 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -4649,6 +4649,11 @@ class ParamDescrsRef:
         """
         return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
 
+    def get_documentation(self, n):
+        """Return the documentation string of the parameter named `n`.
+        """
+        return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
+
     def __getitem__(self, arg):
         if _is_int(arg):
             return self.get_name(arg)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 99ca0abc9..55a1b93d9 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1666,6 +1666,13 @@ extern "C" {
     */
     Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
 
+    /**
+       \brief Retrieve documentation string corresponding to parameter name \c s.
+
+       def_API('Z3_param_descrs_get_documentation', STRING, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL)))
+     */
+    Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
+
     /**
        \brief Convert a parameter description set into a string. This function is mainly used for printing the
        contents of a parameter description set.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index c65f51144..c9745a46b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -83,7 +83,7 @@ eautomaton* re2automaton::operator()(expr* e) {
 
 eautomaton* re2automaton::re2aut(expr* e) {
     SASSERT(u.is_re(e));
-    expr* e1, *e2;
+    expr *e0, *e1, *e2;
     scoped_ptr<eautomaton> a, b;
     unsigned lo, hi;
     zstring s1, s2;
@@ -98,8 +98,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
     }
     else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
         a->add_final_to_init_moves();
-        a->add_init_to_final_states();
-        
+        a->add_init_to_final_states();        
         return a.detach();            
     }
     else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
@@ -116,8 +115,6 @@ eautomaton* re2automaton::re2aut(expr* e) {
             unsigned start = s1[0];
             unsigned stop = s2[0];
             unsigned nb = s1.num_bits();
-            sort_ref s(bv.mk_sort(nb), m);          
-            expr_ref v(m.mk_var(0, s), m);
             expr_ref _start(bv.mk_numeral(start, nb), m);
             expr_ref _stop(bv.mk_numeral(stop, nb), m);
             a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
@@ -127,6 +124,39 @@ eautomaton* re2automaton::re2aut(expr* e) {
             TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
         }
     }
+    else if (u.re.is_complement(e, e0)) {
+        if (u.re.is_range(e0, e1, e2) && u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
+            s1.length() == 1 && s2.length() == 1) {
+            unsigned start = s1[0];
+            unsigned stop = s2[0];
+            unsigned nb = s1.num_bits();
+            sort_ref s(bv.mk_sort(nb), m);          
+            expr_ref v(m.mk_var(0, s), m);
+            expr_ref _start(bv.mk_numeral(start, nb), m);
+            expr_ref _stop(bv.mk_numeral(stop, nb), m);
+            expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
+            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
+            return a.detach();
+        }
+        else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
+            unsigned nb = s1.num_bits();
+            sort_ref s(bv.mk_sort(nb), m);          
+            expr_ref v(m.mk_var(0, s), m);
+            expr_ref _ch(bv.mk_numeral(s1[0], nb), m);          
+            expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
+            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
+            return a.detach();
+        }
+        else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
+            expr_ref v(m.mk_var(0, m.get_sort(e2)), m);
+            expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
+            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
+            return a.detach();
+        }
+        else {
+            TRACE("seq", tout << "Complement expression is not handled: " << mk_pp(e, m) << "\n";);
+        }
+    }
     else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
         scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
         b = eautomaton::mk_epsilon(sm);
@@ -225,6 +255,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_INTERSECT:
         SASSERT(num_args == 2);
         return mk_re_inter(args[0], args[1], result);
+    case OP_RE_COMPLEMENT:
+        SASSERT(num_args == 1);
+        return mk_re_complement(args[0], result);
     case OP_RE_LOOP:
         return mk_re_loop(num_args, args, result);
     case OP_RE_EMPTY_SET:
@@ -967,6 +1000,26 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
+    expr* e1, *e2;
+    if (m_util.re.is_intersection(a, e1, e2)) {
+        result = m_util.re.mk_union(m_util.re.mk_complement(e1), m_util.re.mk_complement(e2));
+        return BR_REWRITE2;
+    }
+    if (m_util.re.is_union(a, e1, e2)) {
+        result = m_util.re.mk_inter(m_util.re.mk_complement(e1), m_util.re.mk_complement(e2));
+        return BR_REWRITE2;
+    }
+    if (m_util.re.is_empty(a)) {
+        result = m_util.re.mk_full(m().get_sort(a));
+        return BR_DONE;
+    }
+    if (m_util.re.is_full(a)) {
+        result = m_util.re.mk_empty(m().get_sort(a));
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
 
 /**
    (emp n r) = emp
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 2860f11a0..83dd8f653 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -96,6 +96,7 @@ class seq_rewriter {
     br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_re_union(expr* a, expr* b, expr_ref& result);
     br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
+    br_status mk_re_complement(expr* a, expr_ref& result);
     br_status mk_re_star(expr* a, expr_ref& result);
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 3215840bc..58355eb0e 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -456,6 +456,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_UNION]      = alloc(psig, m, "re.union",     1, 2, reAreA, reA);
     m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re.inter",     1, 2, reAreA, reA);
     m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re.loop",    1, 1, &reA, reA);
+    m_sigs[OP_RE_COMPLEMENT]     = alloc(psig, m, "re.complement", 1, 1, &reA, reA);
     m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re.empty", 1, 0, 0, reA);
     m_sigs[OP_RE_FULL_SET]       = alloc(psig, m, "re.all", 1, 0, 0, reA);
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA);
@@ -574,7 +575,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_STAR:
     case OP_RE_OPTION:
     case OP_RE_RANGE:
-    case OP_RE_EMPTY_SET:
     case OP_RE_OF_PRED:
     case OP_STRING_ITOS:
     case OP_STRING_STOI:
@@ -587,6 +587,15 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         }
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_FULL_SET));
+    case OP_RE_FULL_SET:
+        if (!range) range = m_re;
+        if (range == m_re) {
+            match(*m_sigs[k], arity, domain, range, rng);
+            return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, k));
+        }
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+        
+
     case _OP_REGEXP_EMPTY:
         if (!range) {
             range = m_re;
@@ -594,6 +603,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET));
 
+    case OP_RE_EMPTY_SET:
+        if (!range) range = m_re;
+        if (range == m_re) {
+            match(*m_sigs[k], arity, domain, range, rng);
+            return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, k));
+        }
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+
     case OP_RE_LOOP:
         switch (arity) {
         case 1:
@@ -624,6 +641,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_const_decl(m_stringc_sym, m_string,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
 
+    case OP_RE_COMPLEMENT:
     case OP_RE_UNION:
     case OP_RE_CONCAT:
     case OP_RE_INTERSECT:
@@ -825,6 +843,15 @@ app* seq_util::re::mk_loop(expr* r, unsigned lo, unsigned hi) {
     return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
 }
 
+app* seq_util::re::mk_full(sort* s) {
+    return m.mk_app(m_fid, OP_RE_FULL_SET, 0, 0, 0, 0, s);
+}
+
+app* seq_util::re::mk_empty(sort* s) {
+    return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, 0, 0, 0, s);    
+}
+
+
 bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi)  {
     if (is_loop(n)) {
         app const* a = to_app(n);
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 4739af84b..4100fe6cc 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -54,6 +54,7 @@ enum seq_op_kind {
     OP_RE_UNION,
     OP_RE_INTERSECT,
     OP_RE_LOOP,
+    OP_RE_COMPLEMENT,
     OP_RE_EMPTY_SET,
     OP_RE_FULL_SET,
     OP_RE_OF_PRED,
@@ -299,16 +300,20 @@ public:
         app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
         app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
         app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }
+        app* mk_complement(expr* r) { return m.mk_app(m_fid, OP_RE_COMPLEMENT, r); }
         app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); }
         app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); }
         app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
         app* mk_loop(expr* r, unsigned lo);
         app* mk_loop(expr* r, unsigned lo, unsigned hi);
+        app* mk_full(sort* s);
+        app* mk_empty(sort* s);
 
         bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
         bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_UNION); }
         bool is_intersection(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
+        bool is_complement(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_COMPLEMENT); }
         bool is_star(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_STAR); }
         bool is_plus(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_PLUS); }
         bool is_opt(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_OPTION); }
@@ -321,6 +326,7 @@ public:
         MATCH_BINARY(is_union);
         MATCH_BINARY(is_intersection);
         MATCH_BINARY(is_range);
+        MATCH_UNARY(is_complement);
         MATCH_UNARY(is_star);
         MATCH_UNARY(is_plus);
         MATCH_UNARY(is_opt);
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index 3963836f2..74a03b620 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -29,7 +29,8 @@ Revision History:
 #include<fenv.h>
 #endif
 
-#ifndef _M_IA64
+#if defined(__x86_64__) || defined(_M_X64) ||	\
+    defined(__i386) || defined(_M_IX86)
 #define USE_INTRINSICS
 #endif
 
@@ -47,7 +48,9 @@ Revision History:
 // Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
 #ifdef __clang__
 #undef USE_INTRINSICS
-#else
+#endif
+
+#ifdef USE_INTRINSICS
 #include <emmintrin.h>
 #endif