diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index dcb929385..edac9a828 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1515,11 +1515,11 @@ namespace z3 {
         Z3_ast r;
         if (a.is_int()) {
             expr zero = a.ctx().int_val(0);
-            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
+            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
         }
         else if (a.is_real()) {
             expr zero = a.ctx().real_val(0);
-            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
+            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
         }
         else {
             r = Z3_mk_fpa_abs(a.ctx(), a); 
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index bbb06f719..bad25ef71 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1210,7 +1210,7 @@ expr_ref pred_transformer::get_origin_summary (model &mdl,
         if (!is_quantifier(s) && !mdl.is_true(s)) {
             TRACE("spacer", tout << "Summary not true in the model: "
                   << mk_pp(s, m) << "\n";);
-            return expr_ref(m);
+            // return expr_ref(m);
         }
     }
 
diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp
index 7ade47458..4109d7fd9 100644
--- a/src/qe/qe_datatypes.cpp
+++ b/src/qe/qe_datatypes.cpp
@@ -77,6 +77,7 @@ namespace qe {
             ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
             for (unsigned i = 0; i < acc.size(); ++i) {
                 arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range());
+                vars.push_back(arg);
                 model.register_decl(arg->get_decl(), m_val->get_arg(i));
                 args.push_back(arg);
             }