From 367cc4b77f4ae283790556b848be31390a8e22c6 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sat, 22 Apr 2017 13:36:09 -0400
Subject: [PATCH 1/3] check result of unsat core validation

---
 src/smt/smt_context.cpp | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 225a0d58d..32fb492ad 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3281,13 +3281,21 @@ namespace smt {
                 TRACE("after_internalization", display(tout););
                 if (inconsistent()) {
                     VERIFY(!resolve_conflict()); // build the proof
-                    mk_unsat_core();
-                    r = l_false;
+                    lbool result = mk_unsat_core();
+                    if (result == l_undef) {
+                        r = l_undef;
+                    } else {
+                        r = l_false;
+                    }
                 }
                 else {
                     r = search();
-                    if (r == l_false)
-                        mk_unsat_core();
+                    if (r == l_false) {
+                        lbool result = mk_unsat_core();
+                        if (result == l_undef) {
+                            r = l_undef;
+                        }
+                    }
                 }
             }
         }

From 5068d2083dc0609801f572a0e3d14df753d36a03 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 22 Apr 2017 11:36:03 -0700
Subject: [PATCH 2/3] tidy

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 15 ++++-----------
 src/smt/smt_context.h   |  2 +-
 2 files changed, 5 insertions(+), 12 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 32fb492ad..6a3c036ca 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3156,7 +3156,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);
@@ -3223,7 +3223,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) {
@@ -3243,16 +3243,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();
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 4f0c14f5a..abdba86d1 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1059,7 +1059,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();
 

From ce67c8277c62b10cbb295266c0c6cc939dc86910 Mon Sep 17 00:00:00 2001
From: Bruce Collie <bsc28@cam.ac.uk>
Date: Mon, 24 Apr 2017 12:59:44 +0000
Subject: [PATCH 3/3] Return check result in fixedpoint object

This is a small change to fix a missing return statement.
---
 src/api/c++/z3++.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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());