diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index b6157f3ff..9d9982523 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2244,7 +2244,7 @@ namespace z3 {
         void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
         void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
         void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
-        check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); to_check_result(r); }
+        check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
         check_result query(func_decl_vector& relations) { 
             array<Z3_func_decl> rs(relations);
             Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr()); 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index bb48848ce..3d0652093 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3295,7 +3295,7 @@ namespace smt {
         setup_context(m_fparams.m_auto_config);
 
         expr_ref_vector theory_assumptions(m_manager);
-        get_theory_assumptions(theory_assumptions);
+        add_theory_assumptions(theory_assumptions);
         if (!theory_assumptions.empty()) {
             TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
             return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
@@ -3362,7 +3362,7 @@ namespace smt {
             (*it)->setup();
     }
 
-    void context::get_theory_assumptions(expr_ref_vector & theory_assumptions) {
+    void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
         ptr_vector<theory>::iterator it = m_theory_set.begin();
         ptr_vector<theory>::iterator end = m_theory_set.end();
         for (; it != end; ++it) {
@@ -3382,16 +3382,9 @@ namespace smt {
         if (!check_preamble(reset_cancel))
             return l_undef;
 
-        expr_ref_vector all_assumptions(m_manager);
-        for (unsigned i = 0; i < ext_num_assumptions; ++i) {
-            all_assumptions.push_back(ext_assumptions[i]);
-        }
+        expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
         if (!already_did_theory_assumptions) {
-            ptr_vector<theory>::iterator it = m_theory_set.begin();
-            ptr_vector<theory>::iterator end = m_theory_set.end();
-            for (; it != end; ++it) {
-                (*it)->add_theory_assumptions(all_assumptions);
-            }
+            add_theory_assumptions(all_assumptions);            
         }
 
         unsigned num_assumptions = all_assumptions.size();
@@ -3420,12 +3413,20 @@ namespace smt {
                 TRACE("after_internalization", display(tout););
                 if (inconsistent()) {
                     VERIFY(!resolve_conflict()); // build the proof
-                    r = mk_unsat_core();
+                    lbool result = mk_unsat_core();
+                    if (result == l_undef) {
+                        r = l_undef;
+                    } else {
+                        r = l_false;
+                    }
                 }
                 else {
                     r = search();
                     if (r == l_false) {
-                        r = mk_unsat_core(); // validation may change an l_false to l_undef here
+                        lbool result = mk_unsat_core();
+                        if (result == l_undef) {
+                            r = l_undef;
+                        }
                     }
                 }
             }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index c412ee669..1d7ce084e 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -226,9 +226,6 @@ namespace smt {
         literal2assumption         m_literal2assumption; // maps an expression associated with a literal to the original assumption
         expr_ref_vector            m_unsat_core;
 
-        // Unsat core assumption hint for theory_str
-        bool                       m_use_theory_str_overlap_assumption;
-
         // -----------------------------------
         //
         // Theory case split
@@ -1094,7 +1091,7 @@ namespace smt {
 
         void reset_assumptions();
 
-        void get_theory_assumptions(expr_ref_vector & theory_assumptions);
+        void add_theory_assumptions(expr_ref_vector & theory_assumptions);
 
         lbool mk_unsat_core();