diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index cdd7bdeec..890c60501 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2086,12 +2086,12 @@ class CppExampleComponent(ExampleComponent):
 
         exefile = '%s$(EXE_EXT)' % self.name
         out.write('%s: %s %s\n' % (exefile, dll, objfiles))
-        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
+        out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s ' % (exefile, objfiles))
         if IS_WINDOWS:
             out.write('%s.lib' % dll_name)
         else:
             out.write(dll)
-        out.write(' $(LINK_EXTRA_FLAGS)\n')
+        out.write(' $(SLINK_EXTRA_FLAGS)\n')
         out.write('_ex_%s: %s\n\n' % (self.name, exefile))
 
 class CExampleComponent(CppExampleComponent):
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 9ebdc5640..5329cd80f 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -53,8 +53,8 @@ namespace smt {
     }
 
     void model_checker::set_qm(quantifier_manager & qm) {
-        SASSERT(m_qm == 0);
-        SASSERT(m_context == 0);
+        SASSERT(m_qm == 0); 
+        SASSERT(m_context == 0); 
         m_qm = &qm;
         m_context = &(m_qm->get_context());
     }
@@ -112,7 +112,7 @@ namespace smt {
         if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
             return;
         }
-        TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
+        TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);        
         ptr_buffer<expr> subst_args;
         unsigned num_decls = q->get_num_decls();
         subst_args.resize(num_decls, 0);
@@ -139,7 +139,7 @@ namespace smt {
     bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
         if (cex == 0) {
             TRACE("model_checker", tout << "no model is available\n";);
-            return false;
+            return false; 
         }
         unsigned num_decls = q->get_num_decls();
         // Remark: sks were created for the flat version of q.
@@ -187,20 +187,20 @@ namespace smt {
             }
             bindings.set(num_decls - i - 1, sk_value);
         }
-
+        
         TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
               for (unsigned i = 0; i < num_decls; i++) {
                   tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
               }
               tout << "\n";);
-
+        
         max_generation = std::max(m_qm->get_generation(q), max_generation);
         add_instance(q, bindings, max_generation);
         return true;
     }
 
     void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
-        for (unsigned i = 0; i < bindings.size(); i++)
+        for (unsigned i = 0; i < bindings.size(); i++) 
             m_new_instances_bindings.push_back(bindings[i]);
         void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
         instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
@@ -260,42 +260,41 @@ namespace smt {
     bool model_checker::check(quantifier * q) {
         SASSERT(!m_aux_context->relevancy());
         m_aux_context->push();
-
+        
         quantifier * flat_q = get_flat_quantifier(q);
-        TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
+        TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << 
               mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
         expr_ref_vector sks(m);
 
         assert_neg_q_m(flat_q, sks);
-        TRACE("model_checker", tout << "skolems:\n";
+        TRACE("model_checker", tout << "skolems:\n"; 
               for (unsigned i = 0; i < sks.size(); i++) {
                   expr * sk = sks.get(i);
                   tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
               });
-
+        
         lbool r = m_aux_context->check();
         TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
         if (r != l_true) {
             m_aux_context->pop(1);
             return r == l_false; // quantifier is satisfied by m_curr_model
         }
-
+		
         model_ref complete_cex;
-        m_aux_context->get_model(complete_cex);
-
+        m_aux_context->get_model(complete_cex); 
+        
         // try to find new instances using instantiation sets.
         m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
-
+        
         unsigned num_new_instances = 0;
 
         while (true) {
             lbool r = m_aux_context->check();
             TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
             if (r != l_true)
-                break;
+                break; 
             model_ref cex;
             m_aux_context->get_model(cex);
-            TRACE("model_checker", tout << "[restricted] model-checker model cex:\n"; model_pp(tout, *cex););
             if (!add_instance(q, cex.get(), sks, true)) {
                 break;
             }
@@ -303,7 +302,7 @@ namespace smt {
             if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
                 TRACE("model_checker", tout << "Add blocking clause failed\n";);
                 // add_blocking_clause failed... stop the search for new counter-examples...
-                break;
+                break; 
             }
         }
 
@@ -397,7 +396,7 @@ namespace smt {
         for (; it != end; ++it) {
             quantifier * q = *it;
 	    if(!m_qm->mbqi_enabled(q)) continue;
-            TRACE("model_checker",
+            TRACE("model_checker", 
                   tout << "Check: " << mk_pp(q, m) << "\n";
                   tout << m_context->get_assignment(q) << "\n";);
 
@@ -419,12 +418,12 @@ namespace smt {
                 }
             }
         }
-
+        
         if (found_relevant)
             m_iteration_idx++;
 
         TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
-        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
+        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);        
         m_max_cexs += m_params.m_mbqi_max_cexs;
 
         if (num_failures == 0 && !m_context->validate_model()) {
@@ -493,7 +492,7 @@ namespace smt {
                           expr * b = inst->m_bindings[i];
                           tout << mk_pp(b, m) << "\n";
                       });
-                TRACE("model_checker_instance",
+                TRACE("model_checker_instance", 
                       expr_ref inst_expr(m);
                       instantiate(m, q, inst->m_bindings, inst_expr);
                       tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 3199b13ef..e9d108cec 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -795,8 +795,9 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
         set(o, z);
     }
     else if (is_zero(x) || is_zero(y)) {
-        if (is_zero(z) && rm != MPF_ROUND_TOWARD_NEGATIVE)
-            mk_pzero(x.ebits, x.sbits, o);
+        bool xy_sgn = is_neg(x) ^ is_neg(y);
+        if (is_zero(z) && xy_sgn ^ is_neg(z))
+            mk_zero(x.ebits, x.sbits, rm != MPF_ROUND_TOWARD_NEGATIVE, o);
         else
             set(o, z);
     }