diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index d40aa93e9..3b8d2364d 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -809,8 +809,12 @@ class env {
                 r = terms[0] / terms[1];
             }
             else if (!strcmp(ch,"$distinct")) {
-                check_arity(terms.size(), 2);
-                r = terms[0] != terms[1];
+                if (terms.size() == 2) {
+                    r = terms[0] != terms[1];
+                }
+                else {
+                    r = distinct(terms);
+                }
             }
             else if (!strcmp(ch,"$floor") || !strcmp(ch,"$to_int")) {
                 check_arity(terms.size(), 1);
@@ -1089,12 +1093,11 @@ class env {
     }
 
     z3::sort mk_sort(char const* s) {
-        z3::symbol sym = symbol(s);
-        return mk_sort(sym);
+        return m_context.uninterpreted_sort(s);
     }
 
     z3::sort mk_sort(z3::symbol& s) {
-        return z3::sort(m_context, Z3_mk_uninterpreted_sort(m_context, s));
+        return m_context.uninterpreted_sort(s);
     }
     
 public:
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 4bccdf6bb..b9641c869 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -55,7 +55,6 @@ def init_project_def():
     add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
-    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic'], 'tactic/fpa')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
     add_lib('qe', ['smt','sat'], 'qe')
     add_lib('duality', ['smt', 'interp', 'qe'])
@@ -71,6 +70,7 @@ def init_project_def():
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
     add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
     add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
+    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 051e8fced..0d57a29ac 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -568,10 +568,12 @@ def mk_java():
     java_native.write('  public static class ObjArrayPtr { public long[] value; }\n')
     java_native.write('  public static class UIntArrayPtr { public int[] value; }\n')
     java_native.write('  public static native void setInternalErrorHandler(long ctx);\n\n')
-    if IS_WINDOWS or os.uname()[0]=="CYGWIN":
-        java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name)
-    else:
-        java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
+
+    java_native.write('  static {\n')
+    java_native.write('    try { System.loadLibrary("z3java"); }\n')
+    java_native.write('    catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n')
+    java_native.write('  }\n')
+
     java_native.write('\n')
     for name, result, params in _dotnet_decls:
         java_native.write('  protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name)))
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index e57050e82..ca15762f5 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -355,6 +355,10 @@ extern "C" {
         init_solver(c, s);
         Z3_stats_ref * st = alloc(Z3_stats_ref);
         to_solver_ref(s)->collect_statistics(st->m_stats);
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        st->m_stats.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
+        st->m_stats.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 0c5b34fb1..cd47d6900 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -203,7 +203,12 @@ namespace z3 {
            and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
         */
         sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
-        
+        /**
+           \brief create an uninterpreted sort with the name given by the string or symbol.
+         */
+        sort uninterpreted_sort(char const* name);
+        sort uninterpreted_sort(symbol const& name);
+
         func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(symbol const&  name, sort_vector const& domain, sort const& range);
@@ -678,7 +683,7 @@ namespace z3 {
 
         friend expr operator+(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 Z3_ast args[2] = { a, b };
                 r = Z3_mk_add(a.ctx(), 2, args);
@@ -698,7 +703,7 @@ namespace z3 {
 
         friend expr operator*(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 Z3_ast args[2] = { a, b };
                 r = Z3_mk_mul(a.ctx(), 2, args);
@@ -725,7 +730,7 @@ namespace z3 {
 
         friend expr operator/(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_div(a.ctx(), a, b);
             }
@@ -743,7 +748,7 @@ namespace z3 {
         friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
 
         friend expr operator-(expr const & a) {
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith()) {
                 r = Z3_mk_unary_minus(a.ctx(), a);
             }
@@ -760,7 +765,7 @@ namespace z3 {
 
         friend expr operator-(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 Z3_ast args[2] = { a, b };
                 r = Z3_mk_sub(a.ctx(), 2, args);
@@ -780,7 +785,7 @@ namespace z3 {
 
         friend expr operator<=(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_le(a.ctx(), a, b);
             }
@@ -799,7 +804,7 @@ namespace z3 {
 
         friend expr operator>=(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_ge(a.ctx(), a, b);
             }
@@ -818,7 +823,7 @@ namespace z3 {
 
         friend expr operator<(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_lt(a.ctx(), a, b);
             }
@@ -837,7 +842,7 @@ namespace z3 {
         
         friend expr operator>(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_gt(a.ctx(), a, b);
             }
@@ -1184,7 +1189,7 @@ namespace z3 {
         
         expr eval(expr const & n, bool model_completion=false) const {
             check_context(*this, n);
-            Z3_ast r;
+            Z3_ast r = 0;
             Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
             check_error();
             if (status == Z3_FALSE)
@@ -1637,6 +1642,13 @@ namespace z3 {
         for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
         return s;
     }
+    inline sort context::uninterpreted_sort(char const* name) {
+        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
+        return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
+    }
+    inline sort context::uninterpreted_sort(symbol const& name) {
+        return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
+    }
 
     inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
         array<Z3_sort> args(arity);
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index ddce9ee33..05746af5d 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -108,7 +108,8 @@ public class InterpolationContext extends Context
         res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
         if (res.status == Z3_lbool.Z3_L_FALSE)
             res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
-        if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
+        if (res.status == Z3_lbool.Z3_L_TRUE) 
+            res.model = new Model(this, n_m.value);
         return res;
     }
 
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 16d2eb6ba..f6a617317 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -5617,7 +5617,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> len(st)
-        2
+        4
         """
         return int(Z3_stats_size(self.ctx.ref(), self.stats))
 
@@ -5631,7 +5631,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> len(st)
-        2
+        4
         >>> st[0]
         ('nlsat propagations', 2)
         >>> st[1]
@@ -5655,7 +5655,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> st.keys()
-        ['nlsat propagations', 'nlsat stages']
+        ['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
         """
         return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
 
@@ -5692,7 +5692,7 @@ class Statistics:
         sat
         >>> st = s.statistics() 
         >>> st.keys()
-        ['nlsat propagations', 'nlsat stages']
+        ['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
         >>> st.nlsat_propagations
         2
         >>> st.nlsat_stages
@@ -8194,23 +8194,24 @@ def FP(name, fpsort, ctx=None):
     >>> eq(x, x2)
     True
     """ 
-    ctx = fpsort.ctx
+    if isinstance(fpsort, FPSortRef):
+        ctx = fpsort.ctx
+    else:
+        ctx = _get_ctx(ctx)
     return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
 
 def FPs(names, fpsort, ctx=None):
     """Return an array of floating-point constants.
     
-    >>> x, y, z = BitVecs('x y z', 16)
-    >>> x.size()
-    16
+    >>> x, y, z = FPs('x y z', FPSort(8, 24))
     >>> x.sort()
-    BitVec(16)
-    >>> Sum(x, y, z)
-    0 + x + y + z
-    >>> Product(x, y, z)
-    1*x*y*z
-    >>> simplify(Product(x, y, z))
-    x*y*z
+    FPSort(8, 24)
+    >>> x.sbits()
+    24
+    >>> x.ebits()
+    8
+    >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
+    fpMul(RNE(), fpAdd(RNE(), x, y), z)
     """
     ctx = z3._get_ctx(ctx)
     if isinstance(names, str):
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 0d319af39..c74b4f185 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -341,22 +341,22 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
     }
     else {
         SASSERT(u.is_irrational_algebraic_numeral(t));
-        anum const & val = u.to_irrational_algebraic_numeral(t);
+        anum const & val2 = u.to_irrational_algebraic_numeral(t);
         algebraic_numbers::manager & am = u.am();
         format * vf;
         std::ostringstream buffer;
         bool is_neg = false;
         if (decimal) {
             scoped_anum abs_val(am);
-            am.set(abs_val, val);
-            if (am.is_neg(val)) {
+            am.set(abs_val, val2);
+            if (am.is_neg(val2)) {
                 is_neg = true;
                 am.neg(abs_val);
             }
             am.display_decimal(buffer, abs_val, decimal_prec);
         }
         else {
-            am.display_root_smt2(buffer, val); 
+            am.display_root_smt2(buffer, val2); 
         }
         vf = mk_string(get_manager(), buffer.str().c_str());
         return is_neg ? mk_neg(vf) : vf;
diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
index d77deca01..79f8f740e 100644
--- a/src/ast/ast_util.cpp
+++ b/src/ast/ast_util.cpp
@@ -44,12 +44,12 @@ app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned nu
     return mk_list_assoc_app(m, decl, num_args, args);
 }
 
-bool is_well_formed_vars(ptr_vector<sort>& bound, expr* e) {
+bool is_well_formed_vars(ptr_vector<sort>& bound, expr * top) {
     ptr_vector<expr> todo;
     ast_mark mark;
-    todo.push_back(e);
+    todo.push_back(top);
     while (!todo.empty()) {
-        expr* e = todo.back();
+        expr * e = todo.back();
         todo.pop_back();
         if (mark.is_marked(e)) {
             continue;
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index b056ded36..f65462d1b 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -501,13 +501,17 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     func_decl * r = mk_func_decl(k, bv_size);
     if (r != 0) {
         if (arity != r->get_arity()) {
-            m_manager->raise_exception("declared arity mismatches supplied arity");
-            return 0;            
+            if (r->get_info()->is_associative())
+                arity = r->get_arity();
+            else {
+                m_manager->raise_exception("declared arity mismatches supplied arity");
+                return 0;
+            }
         }
         for (unsigned i = 0; i < arity; ++i) {
             if (domain[i] != r->get_domain(i)) {
                 m_manager->raise_exception("declared sorts do not match supplied sorts");
-                return 0;            
+                return 0;
             }
         }
         return r;
@@ -566,6 +570,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
 
 func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                          unsigned num_args, expr * const * args, sort * range) {
+    ast_manager& m = *m_manager;
     int bv_size;
     if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
         // bv_size is filled in.
@@ -589,11 +594,35 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
     }
     else if (num_args == 0 || !get_bv_size(args[0], bv_size)) {
-        m_manager->raise_exception("operator is applied to arguments of the wrong sort");
+        m.raise_exception("operator is applied to arguments of the wrong sort");
         return 0;
     }
     func_decl * r = mk_func_decl(k, bv_size);
     if (r != 0) {
+        if (num_args != r->get_arity()) {
+            if (r->get_info()->is_associative()) {
+                sort * fs = r->get_domain(0);
+                for (unsigned i = 0; i < num_args; ++i) {
+                    if (m.get_sort(args[i]) != fs) {
+                        m_manager->raise_exception("declared sorts do not match supplied sorts");
+                        return 0;
+                    }
+                }
+                return r;
+            }
+            else {
+                m.raise_exception("declared arity mismatches supplied arity");
+                return 0;
+            }
+        }
+        for (unsigned i = 0; i < num_args; ++i) {
+            if (m.get_sort(args[i]) != r->get_domain(i)) {
+                std::ostringstream buffer;
+                buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
+                m.raise_exception(buffer.str().c_str());
+                return 0;
+            }
+        }
         return r;
     }
     return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index d707f0178..c185540b7 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -149,10 +149,10 @@ enum status {
 */
 static bool is_recursive_datatype(parameter const * parameters) {
     unsigned num_types          = parameters[0].get_int();
-    unsigned tid                = parameters[1].get_int();
+    unsigned top_tid            = parameters[1].get_int();
     buffer<status>    already_found(num_types, WHITE);
     buffer<unsigned>  todo;
-    todo.push_back(tid);
+    todo.push_back(top_tid);
     while (!todo.empty()) {
         unsigned tid = todo.back();
         if (already_found[tid] == BLACK) {
@@ -198,11 +198,11 @@ static bool is_recursive_datatype(parameter const * parameters) {
 */
 static sort_size get_datatype_size(parameter const * parameters) {
     unsigned num_types          = parameters[0].get_int();
-    unsigned tid                = parameters[1].get_int();
+    unsigned top_tid            = parameters[1].get_int();
     buffer<sort_size> szs(num_types, sort_size());
     buffer<status>    already_found(num_types, WHITE);
     buffer<unsigned>  todo;
-    todo.push_back(tid);
+    todo.push_back(top_tid);
     while (!todo.empty()) {
         unsigned tid  = todo.back();
         if (already_found[tid] == BLACK) {
@@ -280,7 +280,7 @@ static sort_size get_datatype_size(parameter const * parameters) {
             }
         }
     }
-    return szs[tid];
+    return szs[top_tid];
 }
 
 /**
@@ -657,8 +657,8 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const {
     for (unsigned tid = 0; tid < num_types; tid++) {
         unsigned o                 = parameters[2 + 2*tid + 1].get_int(); // constructor offset
         unsigned num_constructors  = parameters[o].get_int();
-        for (unsigned s = 1; s <= num_constructors; s++) {
-            unsigned k_i           = parameters[o + s].get_int();
+        for (unsigned si = 1; si <= num_constructors; si++) {
+            unsigned k_i           = parameters[o + si].get_int();
             unsigned num_accessors = parameters[k_i + 2].get_int();
             unsigned r = 0;
             for (; r < num_accessors; r++) {
diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp
index fbabcb150..097d77cbc 100644
--- a/src/ast/expr2polynomial.cpp
+++ b/src/ast/expr2polynomial.cpp
@@ -367,16 +367,16 @@ struct expr2polynomial::imp {
             begin_loop:
                 checkpoint();
                 frame & fr = m_frame_stack.back();
-                app * t = fr.m_curr;
-                TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(t, m()) << "\n";);
-                unsigned num_args = t->get_num_args();
+                app * a = fr.m_curr;
+                TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(a, m()) << "\n";);
+                unsigned num_args = a->get_num_args();
                 while (fr.m_idx < num_args) {
-                    expr * arg = t->get_arg(fr.m_idx);
+                    expr * arg = a->get_arg(fr.m_idx);
                     fr.m_idx++;
                     if (!visit(arg)) 
                         goto begin_loop;
                 }
-                process_app(t);
+                process_app(a);
                 m_frame_stack.pop_back();
             }
         }
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 2c32e7f1a..11c6f8bf6 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
     split_fp(x, x_sgn, x_exp, x_sig);
     split_fp(y, y_sgn, y_exp, y_sig);
 
-    expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);    
+    expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
     mk_is_zero(x, x_is_zero);
     mk_is_zero(y, y_is_zero);
     m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
@@ -1079,12 +1079,16 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
     mk_is_nan(y, y_is_nan);
     mk_pzero(f, pzero);
 
+    expr_ref sgn_diff(m);
+    sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
+
     expr_ref lt(m);
     mk_float_lt(f, num, args, lt);
     
     result = y;
     mk_ite(lt, x, result, result);
     mk_ite(both_zero, y, result, result);
+    mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
     mk_ite(y_is_nan, x, result, result);
     mk_ite(x_is_nan, y, result, result);
 
@@ -1109,12 +1113,16 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
     mk_is_nan(y, y_is_nan);
     mk_pzero(f, pzero);
 
+    expr_ref sgn_diff(m);
+    sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
+
     expr_ref gt(m);
     mk_float_gt(f, num, args, gt);
 
     result = y;
     mk_ite(gt, x, result, result);
-    mk_ite(both_zero, y, result, result);
+    mk_ite(both_zero, y, result, result);    
+    mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
     mk_ite(y_is_nan, x, result, result);
     mk_ite(x_is_nan, y, result, result);
 
@@ -2211,13 +2219,13 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
         SASSERT(sz == 3);
         BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
 
-        mpf_rounding_mode rm;
+        mpf_rounding_mode mrm;
         switch (bv_rm) {
-        case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
-        case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
-        case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break;
-        case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break;
-        case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break;
+        case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
+        case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;
+        case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break;
+        case BV_RM_TO_POSITIVE: mrm = MPF_ROUND_TOWARD_POSITIVE; break;
+        case BV_RM_TO_ZERO: mrm = MPF_ROUND_TOWARD_ZERO; break;
         default: UNREACHABLE();
         }
 
@@ -2229,17 +2237,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
             return mk_pzero(f, result);
         else {
             scoped_mpf v(m_mpf_manager);
-            m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
+            m_util.fm().set(v, ebits, sbits, mrm, q.to_mpq());
 
-
-
-            expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
+            expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
-            s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
+            sig = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
-            mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, exp);
 
-            mk_fp(sgn, e, s, result);
+            mk_fp(sgn, exp, sig, result);
         }
     }
     else if (m_util.au().is_numeral(x)) {
@@ -2267,44 +2273,45 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
 
             expr_ref v1(m), v2(m), v3(m), v4(m);
 
-            expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
+            expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1);
-            s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
+            sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
-            mk_bias(unbiased_exp, e);
-            mk_fp(sgn, e, s, v1);
+            mk_bias(unbiased_exp, exp);
+            mk_fp(sgn, exp, sig, v1);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
-            s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
+            sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
-            mk_bias(unbiased_exp, e);
-            mk_fp(sgn, e, s, v2);
+            mk_bias(unbiased_exp, exp);
+            mk_fp(sgn, exp, sig, v2);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
-            s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
+            sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
-            mk_bias(unbiased_exp, e);
-            mk_fp(sgn, e, s, v3);
+            mk_bias(unbiased_exp, exp);
+            mk_fp(sgn, exp, sig, v3);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
-            s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
+            sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
-            mk_bias(unbiased_exp, e);
-            mk_fp(sgn, e, s, v4);
+            mk_bias(unbiased_exp, exp);
+            mk_fp(sgn, exp, sig, v4);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
-            s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
+            sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
-            mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, exp);
 
-            mk_fp(sgn, e, s, result);
+            mk_fp(sgn, exp, sig, result);
             mk_ite(rm_tn, v4, result, result);
             mk_ite(rm_tp, v3, result, result);
             mk_ite(rm_nte, v2, result, result);
             mk_ite(rm_nta, v1, result, result);
         }
     }
-    else {        
+    else {
+        SASSERT(!m_arith_util.is_numeral(x));
         bv_util & bu = m_bv_util;
         arith_util & au = m_arith_util;
 
@@ -2322,12 +2329,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
         expr_ref rme(rm, m);
         round(s, rme, sgn, sig, exp, result);
         
-        expr_ref c0(m);
-        mk_is_zero(x, c0);
-        mk_ite(c0, x, result, result);
-
         expr * e = m.mk_eq(m_util.mk_to_real(result), x);
-        m_extra_assertions.push_back(e);        
+        m_extra_assertions.push_back(e);
     }
 
     SASSERT(is_well_sorted(m, result));
@@ -2950,9 +2953,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
     SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
     SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
-    SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
-    dbg_decouple("fpa2bv_to_sbv_shift", shift);
-    dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
+    SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);    
+    dbg_decouple("fpa2bv_to_sbv_shift", shift);    
 
     // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long    
     //           [1][ ... sig ... ][r][g][ ... s ...]
@@ -2961,34 +2963,48 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
     shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
     SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
+    dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
 
     expr_ref c_in_limits(m);
     c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2));
     dbg_decouple("fpa2bv_to_sbv_in_limits", c_in_limits);
 
-    expr_ref shifted_sig(m);
-    shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
-    dbg_decouple("fpa2bv_to_sbv_shifted_sig", shifted_sig);
+    expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m);
+    huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz));
+    huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs);
+    huge_shifted_sig = m_bv_util.mk_bv_lshr(huge_sig, huge_shift);
+    dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig);
+    SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz);
+
+    expr_ref upper_hss(m), lower_hss(m);
+    upper_hss = m_bv_util.mk_extract(2 * sig_sz - 1, sig_sz + 1, huge_shifted_sig);    
+    lower_hss = m_bv_util.mk_extract(sig_sz, 0, huge_shifted_sig);
+    SASSERT(m_bv_util.get_bv_size(upper_hss) == sig_sz - 1);
+    SASSERT(m_bv_util.get_bv_size(lower_hss) == sig_sz + 1);
+    dbg_decouple("fpa2bv_to_sbv_upper_hss", upper_hss);
+    dbg_decouple("fpa2bv_to_sbv_lower_hss", lower_hss);
 
     expr_ref last(m), round(m), sticky(m);
-    last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig);
-    round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, shifted_sig);
-    sticky = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(sig_sz - bv_sz - 2, 0, shifted_sig),
-        m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)),
-        bv0,
-        bv1);
+    last = m_bv_util.mk_extract(1, 1, upper_hss);
+    round = m_bv_util.mk_extract(0, 0, upper_hss);    
+    sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss.get());
     dbg_decouple("fpa2bv_to_sbv_last", last);
     dbg_decouple("fpa2bv_to_sbv_round", round);
     dbg_decouple("fpa2bv_to_sbv_sticky", sticky);
 
+    expr_ref upper_hss_w_sticky(m);
+    upper_hss_w_sticky = m_bv_util.mk_concat(upper_hss, sticky);
+    dbg_decouple("fpa2bv_to_sbv_upper_hss_w_sticky", upper_hss_w_sticky);
+    SASSERT(m_bv_util.get_bv_size(upper_hss_w_sticky) == sig_sz);
+
     expr_ref rounding_decision(m);
     rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
     SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
     dbg_decouple("fpa2bv_to_sbv_rounding_decision", rounding_decision);
 
     expr_ref unrounded_sig(m), pre_rounded(m), inc(m);
-    unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, shifted_sig));
-    inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision));
+    unrounded_sig = m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz - 1, upper_hss_w_sticky);
+    inc = m_bv_util.mk_zero_extend(bv_sz, rounding_decision);
     pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc);
     dbg_decouple("fpa2bv_to_sbv_inc", inc);
     dbg_decouple("fpa2bv_to_sbv_unrounded_sig", unrounded_sig);
@@ -3345,7 +3361,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
             // the maximum shift is `sbits', because after that the mantissa
             // would be zero anyways. So we can safely cut the shift variable down,
             // as long as we check the higher bits.            
-            expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m);
+            expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m);
             zero_s = m_bv_util.mk_numeral(0, sbits-1);
             sbits_s = m_bv_util.mk_numeral(sbits, sbits);
             sh = m_bv_util.mk_extract(ebits-1, sbits, shift);            
@@ -3406,6 +3422,17 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
 }
 
 expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) {
+    expr_ref rmr(rm, m);
+    expr_ref sgnr(sgn, m);
+    expr_ref lastr(last, m);
+    expr_ref roundr(round, m);
+    expr_ref stickyr(sticky, m);
+    dbg_decouple("fpa2bv_rnd_dec_rm", rmr);
+    dbg_decouple("fpa2bv_rnd_dec_sgn", sgnr);
+    dbg_decouple("fpa2bv_rnd_dec_last", lastr);
+    dbg_decouple("fpa2bv_rnd_dec_round", roundr);
+    dbg_decouple("fpa2bv_rnd_dec_sticky", stickyr);
+
     expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m);
     expr * last_sticky[2] = { last, sticky };
     expr * round_sticky[2] = { round, sticky };
@@ -3443,6 +3470,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la
     m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
     m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res);
     
+    dbg_decouple("fpa2bv_rnd_dec_res", res);
     return res;
 }
 
diff --git a/src/ast/func_decl_dependencies.cpp b/src/ast/func_decl_dependencies.cpp
index 162efb0dd..d53c2d9b1 100644
--- a/src/ast/func_decl_dependencies.cpp
+++ b/src/ast/func_decl_dependencies.cpp
@@ -145,24 +145,24 @@ class func_decl_dependencies::top_sort {
             return false;
         m_todo.push_back(f);
         while (!m_todo.empty()) {
-            func_decl * f = m_todo.back();
+            func_decl * cf = m_todo.back();
             
-            switch (get_color(f)) {
+            switch (get_color(cf)) {
             case CLOSED:                
                 m_todo.pop_back();
                 break;
             case OPEN:
-                set_color(f, IN_PROGRESS);
-                if (visit_children(f)) {
-                    SASSERT(m_todo.back() == f);
+                set_color(cf, IN_PROGRESS);
+                if (visit_children(cf)) {
+                    SASSERT(m_todo.back() == cf);
                     m_todo.pop_back();
-                    set_color(f, CLOSED);
+                    set_color(cf, CLOSED);
                 }
                 break;
             case IN_PROGRESS: 
-                if (all_children_closed(f)) {
-                    SASSERT(m_todo.back() == f);
-                    set_color(f, CLOSED);
+                if (all_children_closed(cf)) {
+                    SASSERT(m_todo.back() == cf);
+                    set_color(cf, CLOSED);
                 } else {
                     m_todo.reset();
                     return true;
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index e97933921..9284ff420 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -464,18 +464,18 @@ void bit_blaster_tpl<Cfg>::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr
         // update p
         if (i < sz - 1) {
             for (unsigned j = sz - 1; j > 0; j--) {
-                expr_ref i(m());
-                mk_ite(q, t.get(j-1), p.get(j-1), i); 
-                p.set(j, i);
+                expr_ref ie(m());
+                mk_ite(q, t.get(j-1), p.get(j-1), ie); 
+                p.set(j, ie);
             }
             p.set(0, a_bits[sz - i - 2]);
         }
         else {
             // last step: p contains the remainder
             for (unsigned j = 0; j < sz; j++) {
-                expr_ref i(m());
-                mk_ite(q, t.get(j), p.get(j), i);
-                p.set(j, i);
+                expr_ref ie(m());
+                mk_ite(q, t.get(j), p.get(j), ie);
+                p.set(j, ie);
             }
         }
     }
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 37c42b494..07a39bcae 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -143,9 +143,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
 
 br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
     if (m_hi_fp_unspecified)
-        result = m_util.au().mk_numeral(0, false);
-    else
         // The "hardware interpretation" is 0.
+        result = m_util.au().mk_numeral(rational(0), false);
+    else
         result = m_util.mk_internal_to_real_unspecified();
 
     return BR_DONE;    
@@ -243,7 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
                 !m_util.au().is_numeral(args[2], r2))
                 return BR_FAILED;
 
-            TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);            
+            TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
             m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator());
             result = m_util.mk_value(v);
             return BR_DONE;
@@ -420,11 +420,15 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
                         arg2,
                         m().mk_ite(mk_eq_nan(arg2),
                         arg1,
+                        // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
+                                              m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
+                        m_util.mk_pzero(m().get_sort(arg1)),
                         m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
                         arg2,
                         m().mk_ite(m_util.mk_lt(arg1, arg2),
                         arg1,
-                        arg2))));
+                        arg2)))));
     return BR_REWRITE_FULL;
 }
 
@@ -445,12 +449,16 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
     result = m().mk_ite(mk_eq_nan(arg1),
                         arg2,
                         m().mk_ite(mk_eq_nan(arg2),
-                        arg1,
+                        arg1,                        
+                        // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), 
+                                              m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
+                        m_util.mk_pzero(m().get_sort(arg1)),
                         m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
                         arg2,
                         m().mk_ite(m_util.mk_gt(arg1, arg2),
                         arg1,
-                        arg2))));
+                        arg2)))));
     return BR_REWRITE_FULL;
 }
 
@@ -583,6 +591,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_fm);
+
     if (m_util.is_numeral(arg1, v)) {
         result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false();
         return BR_DONE;
@@ -593,6 +602,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
 
 br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_fm);
+
     if (m_util.is_numeral(arg1, v)) {
         result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false();
         return BR_DONE;
@@ -603,6 +613,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
 
 br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_fm);
+
     if (m_util.is_numeral(arg1, v)) {
         result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false();
         return BR_DONE;
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 92f06679d..be3bfbd0a 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -324,7 +324,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                     }
                     result_stack().push_back(def);
                     TRACE("get_macro", tout << "bindings:\n";
-                          for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
+                          for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";);
                     begin_scope();
                     m_num_qvars = 0;
                     m_root      = def;
diff --git a/src/ast/shared_occs.h b/src/ast/shared_occs.h
index e135fea84..b522f4a4d 100644
--- a/src/ast/shared_occs.h
+++ b/src/ast/shared_occs.h
@@ -75,7 +75,7 @@ public:
     iterator end_shared() const { return m_shared.end(); }
     void reset();
     void cleanup();
-    void display(std::ostream & out, ast_manager & m) const;
+    void display(std::ostream & out, ast_manager & mgr) const;
 };
 
 #endif
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 80aa10cde..50afc1735 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -40,6 +40,7 @@ Notes:
 #include"for_each_expr.h"
 #include"scoped_timer.h"
 #include"interpolant_cmds.h"
+#include"model_smt2_pp.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -528,6 +529,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "LRA" || 
         s == "QF_FP" ||
         s == "QF_FPBV" ||
+        s == "QF_BVFP" ||
         s == "HORN";
 }
 
@@ -547,6 +549,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
         s == "QF_AUFBV" ||
         s == "QF_BVRE" ||
         s == "QF_FPBV" ||
+        s == "QF_BVFP" ||
         s == "HORN";
 }
 
@@ -1402,6 +1405,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
                 was_pareto = true;
                 get_opt()->display_assignment(regular_stream());
                 regular_stream() << "\n";
+                if (get_opt()->print_model()) {
+                    model_ref mdl;
+                    get_opt()->get_model(mdl);
+                    if (mdl) {
+                        regular_stream() << "(model " << std::endl;
+                        model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2);
+                        regular_stream() << ")" << std::endl;                    
+                    }
+                }
                 r = get_opt()->optimize();
             }
         }
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 148bb61d9..795b3a65a 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -124,6 +124,7 @@ public:
     virtual void display_assignment(std::ostream& out) = 0;
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
+    virtual bool print_model() const = 0;
 };
 
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 78dd6f174..268085090 100755
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -616,6 +616,30 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& r
     extract_lcd(rats);
 }
 
+void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& coeffs){
+    std::vector<rational> rats;
+    get_gomory_cut_coeffs(proof,rats);
+    coeffs.resize(rats.size());
+    for(unsigned i = 0; i < rats.size(); i++){
+        coeffs[i] = make_int(rats[i]);
+    }
+}
+
+void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats){
+    symb s = sym(proof);
+    int numps = s->get_num_parameters();
+    rats.resize(numps-2);
+    for(int i = 2; i < numps; i++){
+        rational r;
+        bool ok = s->get_parameter(i).is_rational(r);
+        if(!ok)
+            throw "Bad Farkas coefficient";
+        rats[i-2] = r;
+    }
+    abs_rat(rats);
+    extract_lcd(rats);
+}
+
 void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& coeffs){
     std::vector<rational> rats;
     get_assign_bounds_rule_coeffs(proof,rats);
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 8d4479f8f..dcbe08817 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -396,7 +396,7 @@ class iz3mgr  {
         return UnknownTheory;
     }
 
-    enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
+    enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,GomoryCutKind,ArithMysteryKind,UnknownKind};
 
     lemma_kind get_theory_lemma_kind(const ast &proof){
         symb s = sym(proof);
@@ -417,6 +417,8 @@ class iz3mgr  {
             return AssignBoundsKind;
         if(foo == "eq-propagate")
             return EqPropagateKind;
+        if(foo == "gomory-cut")
+            return GomoryCutKind;
         return UnknownKind;
     }
 
@@ -434,6 +436,10 @@ class iz3mgr  {
   
     void get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& rats);
 
+    void get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats);
+
+    void get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& rats);
+
     bool is_farkas_coefficient_negative(const ast &proof, int n);
 
     bool is_true(ast t){
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 2debdaf42..3620f0ad1 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1182,6 +1182,31 @@ public:
         return res;
     }
 
+    ast GomoryCutRule2Farkas(const ast &proof, const ast &con, std::vector<Iproof::node> prems){
+        std::vector<Iproof::node>  my_prems = prems;
+        std::vector<ast>  my_coeffs;
+        std::vector<Iproof::node>  my_prem_cons;
+        get_gomory_cut_coeffs(proof,my_coeffs);
+        int nargs = num_prems(proof);
+        if(nargs != (int)(my_coeffs.size()))
+            throw "bad gomory-cut theory lemma";
+        for(int i = 0; i < nargs; i++)
+            my_prem_cons.push_back(conc(prem(proof,i)));
+        ast my_con = normalize_inequality(sum_inequalities(my_coeffs,my_prem_cons));
+        Iproof::node hyp = iproof->make_hypothesis(mk_not(my_con));
+        my_prems.push_back(hyp);
+        my_coeffs.push_back(make_int("1"));
+        my_prem_cons.push_back(mk_not(my_con));
+        Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_prem_cons,my_coeffs);
+        ast t = arg(my_con,0);
+        ast c = arg(my_con,1);
+        ast d = gcd_of_coefficients(t);
+        t = z3_simplify(mk_idiv(t,d));
+        c = z3_simplify(mk_idiv(c,d));
+        ast cut_con = make(op(my_con),t,c);
+        return iproof->make_cut_rule(my_con,d,cut_con,res);
+    }
+
     Iproof::node RewriteClause(Iproof::node clause, const ast &rew){
         if(pr(rew) == PR_MONOTONICITY){
             int nequivs = num_prems(rew);
@@ -1912,6 +1937,13 @@ public:
                             res = AssignBounds2Farkas(proof,conc(proof));
                         break;
                     }
+                    case GomoryCutKind: {
+                        if(args.size() > 0)
+                            res =  GomoryCutRule2Farkas(proof, conc(proof), args);
+                        else
+                            throw unsupported();
+                        break;
+                    }
                     case EqPropagateKind: {
                         std::vector<ast> prems(nprems);
                         for(unsigned i = 0; i < nprems; i++)
diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp
index 02ff1591e..9225a87ee 100644
--- a/src/math/euclid/euclidean_solver.cpp
+++ b/src/math/euclid/euclidean_solver.cpp
@@ -609,6 +609,7 @@ struct euclidean_solver::imp {
             // neg coeffs... to make sure that m_next_x is -1
             neg_coeffs(eq.m_as);
             neg_coeffs(eq.m_bs);
+            m().neg(eq.m_c);
         }
         unsigned sz = eq.size();
         for (unsigned i = 0; i < sz; i++) {
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index bd70c06ef..3555e5bdc 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -945,6 +945,10 @@ namespace datalog {
         if (m_engine) {
             m_engine->collect_statistics(st);
         }
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        st.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
+        st.update("memory", static_cast<double>(mem)/(1024.0*1024.0));        
     }
 
 
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 5d1aff44e..455e02e45 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -194,7 +194,6 @@ void rule_properties::operator()(app* n) {
         }
     }
     else {
-        std::cout << mk_pp(n, m) << "\n";
     }
 
 }
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 9e8ead241..59ba260a4 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -85,7 +85,7 @@ namespace datalog {
             removed_cols.size(), removed_cols.c_ptr(), result));
     }
 
-    void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
+    void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
             reg_idx & result, bool reuse, instruction_block & acc) {
         relation_signature res_sig;
         relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
@@ -139,7 +139,7 @@ namespace datalog {
         return r;
     }
 
-    compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) {
+    compiler::reg_idx compiler::get_single_column_register(const relation_sort s) {
         relation_signature singl_sig;
         singl_sig.push_back(s);
         return get_fresh_register(singl_sig);
@@ -165,7 +165,7 @@ namespace datalog {
         }
     }
 
-    void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val,
+    void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val,
             reg_idx & result, bool & dealloc, instruction_block & acc) {
         reg_idx singleton_table;
         if(!m_constant_registers.find(s, val, singleton_table)) {
@@ -185,7 +185,7 @@ namespace datalog {
         }
     }
 
-    void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, 
+    void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
             bool & dealloc, instruction_block & acc) {
         
         TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
@@ -862,9 +862,11 @@ namespace datalog {
         ast_manager& m = m_context.get_manager();
         unsigned pt_len = r->get_positive_tail_size();
         unsigned ut_len = r->get_uninterpreted_tail_size();
-        if (pt_len == ut_len) {
+
+        // no negated predicates
+        if (pt_len == ut_len)
             return;
-        }
+
         // populate negative variables:
         for (unsigned i = pt_len; i < ut_len; ++i) {
             app * neg_tail = r->get_tail(i);
diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h
index 8c33f987c..4902b9387 100644
--- a/src/muz/rel/dl_compiler.h
+++ b/src/muz/rel/dl_compiler.h
@@ -135,7 +135,7 @@ namespace datalog {
 
         reg_idx get_fresh_register(const relation_signature & sig);
         reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r);
-        reg_idx get_single_column_register(const relation_sort & s);
+        reg_idx get_single_column_register(const relation_sort s);
 
         /**
            \brief Allocate registers for predicates in \c pred and add them into the \c regs map.
@@ -150,7 +150,7 @@ namespace datalog {
             const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
         void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
             const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc);
-        void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
+        void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
             reg_idx & result, bool reuse, instruction_block & acc);
         /**
            \brief Create add an union or widen operation and put it into \c acc.
@@ -174,10 +174,10 @@ namespace datalog {
 
         void make_dealloc_non_void(reg_idx r, instruction_block & acc);
 
-        void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val,
+        void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val,
             reg_idx & result, bool & dealloc, instruction_block & acc);
 
-        void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, 
+        void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
             bool & dealloc, instruction_block & acc);
         void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 
             instruction_block & acc);
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 537f4bf22..01324fc67 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -323,12 +323,8 @@ private:
 
     void display_statistics(cmd_context& ctx) {
         statistics stats;
-        unsigned long long max_mem = memory::get_max_used_memory();
-        unsigned long long mem = memory::get_allocation_size();
-        stats.update("time", ctx.get_seconds());
-        stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
-        stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
         get_opt(ctx).collect_statistics(stats);
+        stats.update("time", ctx.get_seconds());
         stats.display_smt2(ctx.regular_stream());        
     }
 };
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 857b57296..bf8a9dd7f 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -254,6 +254,12 @@ namespace opt {
         }
     }
 
+
+    bool context::print_model() const {
+        opt_params optp(m_params);
+        return optp.print_model();
+    }
+
     void context::get_base_model(model_ref& mdl) {
         mdl = m_model;
     }
@@ -1179,6 +1185,10 @@ namespace opt {
         for (; it != end; ++it) {
             it->m_value->collect_statistics(stats);
         }        
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
+        stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
     }
 
     void context::collect_param_descrs(param_descrs & r) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 59868dd1e..eabc2550f 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -180,6 +180,7 @@ namespace opt {
         virtual void cancel() { set_cancel(true); }
         virtual void set_hard_constraints(ptr_vector<expr> & hard);
         virtual lbool optimize();
+        virtual bool print_model() const;
         virtual void get_model(model_ref& _m);
         virtual void set_model(model_ref& _m);
         virtual void fix_model(model_ref& _m);
diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h
new file mode 100644
index 000000000..11bceef0b
--- /dev/null
+++ b/src/qe/qe_mbp.h
@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qe_mbp.h
+
+Abstract:
+
+    Model-based projection utilities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#ifndef __QE_MBP_H__
+#define __QE_MBP_H__
+
+#include "ast.h"
+#include "params.h"
+
+namespace qe {
+    class mbp {
+        class impl;
+        impl * m_impl;
+    public:
+        mbp(ast_manager& m);
+        
+        ~mbp();
+        
+        /**
+           \brief
+           Apply model-based qe on constants provided as vector of variables. 
+           Return the updated formula and updated set of variables that were not eliminated.
+           
+        */
+        void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml);
+        
+        void set_cancel(bool f);
+    };
+}
+
+#endif 
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
new file mode 100644
index 000000000..4c736bc31
--- /dev/null
+++ b/src/qe/qsat.cpp
@@ -0,0 +1,281 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qsat.cpp
+
+Abstract:
+
+    Quantifier Satisfiability Solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#include "qsat.h"
+#include "smt_kernel.h"
+#include "qe_mbp.h"
+#include "smt_params.h"
+#include "ast_util.h"
+
+using namespace qe;
+
+struct qdef_t {
+    expr_ref        m_pred;
+    expr_ref        m_expr;
+    expr_ref_vector m_vars;
+    bool            m_is_forall;
+    qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall):
+        m_pred(p), 
+        m_expr(e),
+        m_vars(vars),
+        m_is_forall(is_forall) {}
+};
+
+typedef vector<qdef_t> qdefs_t;
+
+struct pdef_t {
+    expr_ref  m_pred;
+    expr_ref  m_atom;
+    pdef_t(expr_ref& p, expr* a):
+        m_pred(p),
+        m_atom(a, p.get_manager())
+    {}
+};
+
+class qsat::impl {
+    ast_manager&      m;
+    qe::mbp           mbp;
+    smt_params        m_smtp;
+    smt::kernel       m_kernel;
+    expr_ref          m_fml_pred;  // predicate that encodes top-level formula
+    expr_ref_vector   m_atoms;     // predicates that encode atomic subformulas
+
+
+    lbool check_sat() {        
+        // TBD main procedure goes here.
+        return l_undef;
+    }
+
+    /**
+       \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate.
+     */
+    void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) {
+        
+    }
+
+    /** 
+        \brief create propositional abstration of formula by replacing atomic sub-formulas by fresh 
+        propositional variables, and adding definitions for each propositional formula on the side.
+        Assumption is that the formula is quantifier-free.
+    */
+    void mk_abstract(expr_ref& fml, vector<pdef_t>& pdefs) {
+        expr_ref_vector todo(m), trail(m);
+        obj_map<expr,expr*> cache;
+        ptr_vector<expr> args;
+        expr_ref r(m);
+        todo.push_back(fml);
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            if (cache.contains(e)) {
+                todo.pop_back();
+                continue;
+            }
+            SASSERT(is_app(e));
+            app* a = to_app(e);
+            if (a->get_family_id() == m.get_basic_family_id()) {
+                unsigned sz = a->get_num_args();
+                args.reset();
+                for (unsigned i = 0; i < sz; ++i) {
+                    expr* f = a->get_arg(i);
+                    if (cache.find(f, f)) {
+                        args.push_back(f);
+                    }
+                    else {
+                        todo.push_back(f);
+                    }
+                } 
+                if (args.size() == sz) {
+                    r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+                    cache.insert(e, r);
+                    trail.push_back(r);
+                    todo.pop_back();
+                }
+            }
+            else if (is_uninterp_const(a)) {
+                cache.insert(e, e);
+            }
+            else {
+                // TBD: nested Booleans.    
+
+                r = m.mk_fresh_const("p",m.mk_bool_sort());
+                trail.push_back(r);
+                cache.insert(e, r);
+                pdefs.push_back(pdef_t(r, e));
+            }
+        }
+        fml = cache.find(fml);
+    }
+
+    /** 
+        \brief use dual propagation to minimize model.
+    */
+    bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) {        
+        bool result = false;
+        assignment.push_back(not_fml);
+        lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
+        switch (res) {
+        case l_true:
+            UNREACHABLE();
+            break;
+        case l_undef:
+            break;
+        case l_false: 
+            result = true;
+            get_core(assignment, not_fml);
+            break;
+        }
+        return result;
+    }
+
+    lbool check_sat(expr_ref_vector& assignment, expr* fml) {
+        assignment.push_back(fml);
+        lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
+        switch (res) {
+        case l_true: {
+            model_ref mdl;
+            expr_ref tmp(m);
+            assignment.reset();
+            m_kernel.get_model(mdl);
+            for (unsigned i = 0; i < m_atoms.size(); ++i) {
+                expr* p = m_atoms[i].get();
+                if (mdl->eval(p, tmp)) {
+                    if (m.is_true(tmp)) {
+                        assignment.push_back(p);
+                    }
+                    else if (m.is_false(tmp)) {
+                        assignment.push_back(m.mk_not(p));
+                    }
+                }                
+            }
+            expr_ref not_fml = mk_not(fml);
+            if (!minimize_assignment(assignment, not_fml)) {
+                res = l_undef;
+            }
+            break;
+        }
+        case l_undef:            
+            break;
+        case l_false:
+            get_core(assignment, fml);
+            break;
+        }
+        return res;
+    }
+
+    void get_core(expr_ref_vector& core, expr* exclude) {
+        unsigned sz = m_kernel.get_unsat_core_size();
+        core.reset();
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* e = m_kernel.get_unsat_core_expr(i);
+            if (e != exclude) {
+                core.push_back(e);
+            } 
+        }        
+    }
+
+    expr_ref mk_not(expr* e) {
+        return expr_ref(::mk_not(m, e), m);
+    }
+
+public:
+    impl(ast_manager& m):
+        m(m),
+        mbp(m),
+        m_kernel(m, m_smtp),
+        m_fml_pred(m), 
+        m_atoms(m) {}
+    
+    void updt_params(params_ref const & p) {
+    }
+
+    void collect_param_descrs(param_descrs & r) {
+    }
+
+    void operator()(/* in */  goal_ref const & in, 
+                    /* out */ goal_ref_buffer & result, 
+                    /* out */ model_converter_ref & mc, 
+                    /* out */ proof_converter_ref & pc,
+                    /* out */ expr_dependency_ref & core) {
+
+    }
+
+    void collect_statistics(statistics & st) const {
+
+    }
+    void reset_statistics() {
+    }
+
+    void cleanup() {
+    }
+
+    void set_logic(symbol const & l) {
+    }
+
+    void set_progress_callback(progress_callback * callback) {
+    }
+
+    tactic * translate(ast_manager & m) {
+        return 0;
+    }
+
+};
+
+qsat::qsat(ast_manager& m) {
+    m_impl = alloc(impl, m);
+}
+
+qsat::~qsat() {
+    dealloc(m_impl);
+}
+
+void qsat::updt_params(params_ref const & p) {
+    m_impl->updt_params(p);
+}
+void qsat::collect_param_descrs(param_descrs & r) {
+    m_impl->collect_param_descrs(r);
+}
+void qsat::operator()(/* in */  goal_ref const & in, 
+                      /* out */ goal_ref_buffer & result, 
+                      /* out */ model_converter_ref & mc, 
+                      /* out */ proof_converter_ref & pc,
+                      /* out */ expr_dependency_ref & core) {
+    (*m_impl)(in, result, mc, pc, core);
+}
+
+void qsat::collect_statistics(statistics & st) const {
+    m_impl->collect_statistics(st);
+}
+void qsat::reset_statistics() {
+    m_impl->reset_statistics();
+}
+void qsat::cleanup() {
+    m_impl->cleanup();
+}
+void qsat::set_logic(symbol const & l) {
+    m_impl->set_logic(l);
+}
+void qsat::set_progress_callback(progress_callback * callback) {
+    m_impl->set_progress_callback(callback);
+}
+tactic * qsat::translate(ast_manager & m) {
+    return m_impl->translate(m);
+}
+
+
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
new file mode 100644
index 000000000..2fc071c76
--- /dev/null
+++ b/src/qe/qsat.h
@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qsat.h
+
+Abstract:
+
+    Quantifier Satisfiability Solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#ifndef __QE_QSAT_H__
+#define __QE_QSAT_H__
+
+#include "tactic.h"
+
+namespace qe {
+    class qsat : public tactic {
+        class impl;
+        impl * m_impl;
+    public:
+        qsat(ast_manager& m);
+        ~qsat();
+        
+        virtual void updt_params(params_ref const & p);
+        virtual void collect_param_descrs(param_descrs & r);
+        virtual void operator()(/* in */  goal_ref const & in, 
+                                /* out */ goal_ref_buffer & result, 
+                                /* out */ model_converter_ref & mc, 
+                                /* out */ proof_converter_ref & pc,
+                                /* out */ expr_dependency_ref & core);
+        
+        virtual void collect_statistics(statistics & st) const;
+        virtual void reset_statistics();
+        virtual void cleanup() = 0;
+        virtual void set_logic(symbol const & l);
+        virtual void set_progress_callback(progress_callback * callback);
+        virtual tactic * translate(ast_manager & m);
+        
+    };
+};
+
+#endif 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 74f2e09fa..4f810727a 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1411,6 +1411,10 @@ namespace smt {
     
     void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) {
         justification * js = 0; 
+        TRACE("mk_th_axiom", 
+              display_literals_verbose(tout, num_lits, lits);
+              tout << "\n";);
+
         if (m_manager.proofs_enabled()) {
             js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params));
         }
@@ -1425,13 +1429,11 @@ namespace smt {
     
     void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) {
         literal ls[2] = { l1, l2 };
-        TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << "\n";);
         mk_th_axiom(tid, 2, ls, num_params, params);
     }
 
     void context::mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
         literal ls[3] = { l1, l2, l3 };
-        TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << " "; display_literal(tout, l3); tout << "\n";);
         mk_th_axiom(tid, 3, ls, num_params, params);
     }
 
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index d4c0e1efb..98ad5e51a 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -116,7 +116,7 @@ namespace smt {
             setup_LRA();
         else if (m_logic == "QF_FP")
             setup_QF_FP();
-        else if (m_logic == "QF_FPBV")
+        else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
             setup_QF_FPBV();
         else
             setup_unknown();
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 660a11faa..db4b01395 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -245,6 +245,8 @@ namespace smt {
             parameter* params(char const* name);
         };
 
+        class gomory_cut_justification;
+
         class bound { 
         protected:
             theory_var  m_var;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index f481e35d0..65105e65b 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -439,6 +439,7 @@ namespace smt {
                     j += rational(1);
                 }
                 ctx.mk_th_axiom(get_id(), lits.size(), lits.begin());
+                
 #else
                 // performs slightly worse.
                 literal_buffer lits;
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 893b5d87a..cc69bb533 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -460,13 +460,16 @@ namespace smt {
         SASSERT(is_well_sorted(get_manager(), result));
     }
 
-    class gomory_cut_justification : public ext_theory_propagation_justification {
+    template<typename Ext>
+    class theory_arith<Ext>::gomory_cut_justification : public ext_theory_propagation_justification {
     public:
-        gomory_cut_justification(family_id fid, region & r, 
+         gomory_cut_justification(family_id fid, region & r, 
                                  unsigned num_lits, literal const * lits, 
                                  unsigned num_eqs, enode_pair const * eqs,
+                                 antecedents& bounds, 
                                  literal consequent):
-            ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent) {
+        ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent,
+                                             bounds.num_params(), bounds.params("gomory-cut")) {
         }
         // Remark: the assignment must be propagated back to arith
         virtual theory_id get_from_theory() const { return null_theory_id; } 
@@ -530,7 +533,7 @@ namespace smt {
                         }
                         // k += new_a_ij * lower_bound(x_j).get_rational();
                         k.addmul(new_a_ij, lower_bound(x_j).get_rational());
-                        lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                        lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                     }
                     else {
                         SASSERT(at_upper(x_j));
@@ -546,7 +549,7 @@ namespace smt {
                         }
                         // k += new_a_ij * upper_bound(x_j).get_rational();
                         k.addmul(new_a_ij, upper_bound(x_j).get_rational());
-                        upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                        upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                     }
                     pol.push_back(row_entry(new_a_ij, x_j));
                 }
@@ -571,7 +574,7 @@ namespace smt {
                             }
                             // k += new_a_ij * lower_bound(x_j).get_rational();
                             k.addmul(new_a_ij, lower_bound(x_j).get_rational());
-                            lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                            lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                         }
                         else {
                             SASSERT(at_upper(x_j));
@@ -584,7 +587,7 @@ namespace smt {
                             new_a_ij.neg(); // the upper terms are inverted
                             // k += new_a_ij * upper_bound(x_j).get_rational();
                             k.addmul(new_a_ij, upper_bound(x_j).get_rational());
-                            upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                            upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                         }
                         TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
                         pol.push_back(row_entry(new_a_ij, x_j));
@@ -600,7 +603,7 @@ namespace smt {
         if (pol.empty()) {
             SASSERT(k.is_pos());
             // conflict 0 >= k where k is positive
-            set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory_cut");
+            set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory-cut");
             return true;
         }
         else if (pol.size() == 1) {
@@ -652,7 +655,7 @@ namespace smt {
                        gomory_cut_justification(
                            get_id(), ctx.get_region(), 
                            ante.lits().size(), ante.lits().c_ptr(), 
-                           ante.eqs().size(), ante.eqs().c_ptr(), l)));
+                           ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
         return true;
     }
     
@@ -1061,6 +1064,7 @@ namespace smt {
                 }
                 if (!failed) {
                     m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j);
+                    TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";);
                 }
                 else {
                     TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";);
@@ -1191,7 +1195,8 @@ namespace smt {
                 if (l != 0) {
                     rational l_old = l->get_value().get_rational().to_rational();
                     rational l_new = g*ceil((l_old - c2)/g) + c2;
-                    TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";);
+                    TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";
+                          tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";);
                     if (l_new > l_old) {
                         propagated = true;
                         mk_lower(v, l_new, l, m_js);
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 28314c421..4e169a8be 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -208,6 +208,8 @@ namespace smt {
         theory_array::reset_eh();
         std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
         m_var_data_full.reset();
+        m_eqs.reset();
+        m_eqsv.reset();
     }
 
     void theory_array_full::display_var(std::ostream & out, theory_var v) const {
@@ -223,7 +225,6 @@ namespace smt {
     }
     
     theory_var theory_array_full::mk_var(enode * n) {
-
         theory_var r = theory_array::mk_var(n);
         SASSERT(r == static_cast<int>(m_var_data_full.size()));
         m_var_data_full.push_back(alloc(var_data_full));
@@ -512,7 +513,7 @@ namespace smt {
         
         TRACE("array_map_bug",
               tout << "select-map axiom\n" << mk_ismt2_pp(sel1, m) << "\n=\n" << mk_ismt2_pp(sel2,m) << "\n";);
-        
+
         return try_assign_eq(sel1, sel2);
     }
 
@@ -760,37 +761,36 @@ namespace smt {
                     r = FC_CONTINUE;
             }
         }
+        while (!m_eqsv.empty()) {
+            literal eq = m_eqsv.back();
+            m_eqsv.pop_back();
+            get_context().mark_as_relevant(eq);            
+            assert_axiom(eq);
+            r = FC_CONTINUE;
+        }
         if (r == FC_DONE && m_found_unsupported_op)
             r = FC_GIVEUP;
         return r;
     }
 
+
     bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
-        context& ctx = get_context();
-        enode* n1 = ctx.get_enode(v1);
-        enode* n2 = ctx.get_enode(v2);
-        if (n1->get_root() == n2->get_root()) {
-            return false;
-        }
         TRACE("array", 
               tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" 
               << mk_bounded_pp(v2, get_manager()) << "\n";);
-
-#if 0
-        if (m.proofs_enabled()) {
-#endif
-            literal eq(mk_eq(v1,v2,true));
-            ctx.mark_as_relevant(eq);
-            assert_axiom(eq);
-#if 0
+        context& ctx = get_context();
+        if (m_eqs.contains(v1, v2)) {
+            return false;
         }
         else {
-            ctx.mark_as_relevant(n1);
-            ctx.mark_as_relevant(n2);
-            ctx.assign_eq(n1, n2, eq_justification::mk_axiom());
+            m_eqs.insert(v1, v2, true);
+            literal eq(mk_eq(v1, v2, true));
+            get_context().mark_as_relevant(eq);            
+            assert_axiom(eq);
+
+            // m_eqsv.push_back(eq);
+            return true;
         }
-#endif
-        return true;
     }
 
     void theory_array_full::pop_scope_eh(unsigned num_scopes) {
@@ -798,6 +798,8 @@ namespace smt {
         theory_array::pop_scope_eh(num_scopes);
         std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc<var_data_full>());
         m_var_data_full.shrink(num_old_vars);        
+        m_eqs.reset();
+        m_eqsv.reset();
     }
 
     void theory_array_full::collect_statistics(::statistics & st) const {
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 7c066f765..bbbf35408 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -38,12 +38,12 @@ namespace smt {
 
         ast2ast_trailmap<sort,app> m_sort2epsilon;
         simplifier*                m_simp;
+        obj_pair_map<expr,expr,bool> m_eqs;
+        svector<literal>             m_eqsv;
 
     protected:
 
-#if 0
-        virtual final_check_status final_check_eh();
-#endif
+        //virtual final_check_status final_check_eh();
         virtual void reset_eh();
 
         virtual void set_prop_upward(theory_var v);
@@ -84,6 +84,7 @@ namespace smt {
 
 
         bool try_assign_eq(expr* n1, expr* n2);
+        void assign_eqs();
 
         
     public:
diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp
index 0de507183..dc24a625b 100644
--- a/src/tactic/arith/arith_bounds_tactic.cpp
+++ b/src/tactic/arith/arith_bounds_tactic.cpp
@@ -34,8 +34,8 @@ struct arith_bounds_tactic : public tactic {
         bounds_arith_subsumption(in, result);
     }
     
-    virtual tactic* translate(ast_manager& m) {
-        return alloc(arith_bounds_tactic, m);
+    virtual tactic* translate(ast_manager & mgr) {
+        return alloc(arith_bounds_tactic, mgr);
     }
     
     void checkpoint() {
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 933b687b4..7c715e6e7 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -488,7 +488,7 @@ public:
         unsigned size = g->size();
         expr_ref new_f1(m), new_f2(m);
         proof_ref new_pr1(m), new_pr2(m);
-        for (unsigned idx = 0; idx < size; idx++) {
+        for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
             m_rw1(g->form(idx), new_f1, new_pr1);
             TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
             m_rw2.rewrite(new_f1, new_f2);
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 4854b3c07..fbce1668e 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -23,9 +23,47 @@ Notes:
 #include"fpa2bv_tactic.h"
 #include"smt_tactic.h"
 #include"propagate_values_tactic.h"
+#include"probe_arith.h"
+#include"qfnra_tactic.h"
 
 #include"qffp_tactic.h"
 
+
+struct has_fp_to_real_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       bu;
+    fpa_util      fu;
+    arith_util    au;
+
+    has_fp_to_real_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        sort * s = get_sort(n);
+        if (au.is_real(s) && n->get_family_id() == fu.get_family_id() &&
+            is_app(n) && to_app(n)->get_decl_kind() == OP_FPA_TO_REAL)
+            throw found();
+    }
+};
+
+class has_fp_to_real_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<has_fp_to_real_predicate>(g);
+    }
+
+    virtual ~has_fp_to_real_probe() {}
+};
+
+probe * mk_has_fp_to_real_probe() {
+    return alloc(has_fp_to_real_probe);
+}
+
+
 tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
     params_ref simp_p = p;
     simp_p.set_bool("arith_lhs", true);
@@ -40,10 +78,13 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
                                      mk_propagate_values_tactic(m, p),
                                      using_params(mk_simplify_tactic(m, p), simp_p),                                 
                                      mk_bit_blaster_tactic(m, p),
-                                     using_params(mk_simplify_tactic(m, p), simp_p),                                 
+                                     using_params(mk_simplify_tactic(m, p), simp_p),
                                      cond(mk_is_propositional_probe(),
                                         mk_sat_tactic(m, p),
-                                        mk_smt_tactic(p)),
+                                        cond(mk_has_fp_to_real_probe(),
+                                            mk_qfnra_tactic(m, p),
+                                            mk_smt_tactic(p))
+                                        ),
                                      mk_fail_if_undecided_tactic())));
 
     st->updt_params(p);
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index b28c8cf3d..687771a30 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -81,7 +81,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_ufbv_tactic(m, p);
     else if (logic=="QF_FP")
         return mk_qffp_tactic(m, p);
-    else if (logic == "QF_FPBV")
+    else if (logic == "QF_FPBV" || logic == "QF_BVFP")
         return mk_qffpbv_tactic(m, p);
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 9765bced5..149cbc272 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -709,8 +709,6 @@ public:
             tactic_ref_vector              ts2;
             goal_ref_vector                g_copies;
 
-            ast_manager & m = in->m();
-
             for (unsigned i = 0; i < r1_size; i++) {
                 ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode());
                 managers.push_back(new_m);
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 1521a8f87..57e5b56b5 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1229,7 +1229,11 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
 }
 
 void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
-    if (is_nan(x) || (is_zero(x) && is_zero(y)))
+    if (is_nan(x))
+        set(o, y);
+    else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
+        mk_pzero(x.ebits, x.sbits, o);
+    else if (is_zero(x) && is_zero(y))
         set(o, y);
     else if (is_nan(y))
         set(o, x);
@@ -1240,7 +1244,11 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
 }
 
 void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) {
-    if (is_nan(x) || (is_zero(x) && is_zero(y)))
+    if (is_nan(x))
+        set(o, y);
+    else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
+        mk_pzero(x.ebits, x.sbits, o);
+    else if (is_zero(x) && is_zero(y))
         set(o, y);
     else if (is_nan(y))
         set(o, x);