From b0dd3f3238b32adc70454c112f114bc005185668 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Feb 2017 13:58:12 -0800
Subject: [PATCH 01/23] add recursive function graphs to model, adapt rewriter
 to bypass branches whose evaluation is redundant

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h | 11 ++++++++
 src/smt/smt_context.cpp         | 45 +++++++++++++++++++++++++++++++++
 src/smt/smt_context.h           |  5 ++++
 src/smt/smt_quantifier.h        |  2 ++
 4 files changed, 63 insertions(+)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 61d177809..dddb02dfd 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -184,9 +184,20 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
         unsigned num_args = t->get_num_args();
         while (fr.m_i < num_args) {
             expr * arg = t->get_arg(fr.m_i);
+            if (fr.m_i >= 1 && m().is_ite(t) && !ProofGen) {
+                expr * cond = result_stack()[fr.m_spos].get();
+                if (m().is_true(cond)) {
+                    arg = t->get_arg(1);
+                }
+                else if (m().is_false(cond)) {
+                    arg = t->get_arg(2);
+                }
+            }
             fr.m_i++;
             if (!visit<ProofGen>(arg, fr.m_max_depth))
                 return;
+
+
         }
         func_decl * f = t->get_decl();
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 3c88a75a2..d6a837d37 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4123,6 +4123,7 @@ namespace smt {
         if (fcs == FC_DONE) {
             mk_proto_model(l_true);
             m_model = m_proto_model->mk_model();
+            add_rec_funs_to_model();            
         }
             
         return fcs == FC_DONE;
@@ -4175,8 +4176,52 @@ namespace smt {
         return m_last_search_failure; 
     }
 
+    void context::add_rec_funs_to_model() {
+        ast_manager& m = m_manager;
+        SASSERT(m_model);
+        for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
+            expr* e = m_asserted_formulas.get_formula(i);
+            if (is_quantifier(e)) {
+                quantifier* q = to_quantifier(e);
+                std::cout << mk_pp(q, m) << "\n";
+                if (!m.is_rec_fun_def(q)) continue;
+                SASSERT(q->get_num_patterns() == 1);
+                expr* fn = to_app(q->get_pattern(0))->get_arg(0);
+                SASSERT(is_app(fn));
+                func_decl* f = to_app(fn)->get_decl();
+                expr* eq = q->get_expr();
+                expr_ref body(m);
+                if (is_fun_def(fn, q->get_expr(), body)) {
+                    func_interp* fi = alloc(func_interp, m, f->get_arity());
+                    fi->set_else(body);
+                    m_model->register_decl(f, fi);
+                }
+            }
+        }
+    }
+
+    bool context::is_fun_def(expr* f, expr* body, expr_ref& result) {
+        expr* t1, *t2, *t3;
+        if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) {
+            if (t1 == f) return result = t2, true;
+            if (t2 == f) return result = t1, true;
+            return false;
+        }
+        if (m_manager.is_ite(body, t1, t2, t3)) {
+            expr_ref body1(m_manager), body2(m_manager);
+            if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) {
+                // f is not free in t1
+                result = m_manager.mk_ite(t1, body1, body2);
+                return true;
+            }
+        }
+        return false;
+    }
+
+
 };
 
+
 #ifdef Z3DEBUG
 void pp(smt::context & c) {
     c.display(std::cout);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index b9b068442..c1c684fec 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -209,6 +209,7 @@ namespace smt {
             ~scoped_mk_model() {
                 if (m_ctx.m_proto_model.get() != 0) {
                     m_ctx.m_model = m_ctx.m_proto_model->mk_model();
+                    m_ctx.add_rec_funs_to_model();            
                     m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
                 }
             }
@@ -1156,6 +1157,10 @@ namespace smt {
 
         bool propagate();
 
+        void add_rec_funs_to_model();
+
+        bool is_fun_def(expr* f, expr* q, expr_ref& body);
+
     public:
         bool can_propagate() const;
 
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index bc731bf9c..bc249ed1a 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -165,6 +165,8 @@ namespace smt {
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
 
+        
+
     };
 };
 

From 8f14cfadd26051189f0c8356228047064d6d72bd Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 7 Mar 2017 18:10:03 +0000
Subject: [PATCH 02/23] Tabs, whitespace

---
 src/ast/fpa_decl_plugin.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index d8bf70e80..e039bcbd9 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -836,7 +836,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
 
     case OP_FPA_INTERNAL_BVWRAP:
-        return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);    
+        return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_INTERNAL_BV2RM:
         return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range);
 
@@ -915,7 +915,7 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED));
 
     /* Extensions */
-	op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
+    op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
     op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV));
 }
 

From 41e6fafc58f44e379a04e0650ddbb25c84350350 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Mar 2017 10:07:31 +0100
Subject: [PATCH 03/23] fix bug for bit-vector optimization. Issue #919

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ebe56381a..d1a3ddb8a 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1002,7 +1002,8 @@ namespace opt {
             TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
             return false;
         }
-        if (!m_arith.is_numeral(val, r)) {
+        unsigned bv_size;
+        if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) {
             TRACE("opt", tout << "model does not evaluate objective to a value\n";);
             return false;
         }

From 829519b83747992056953cd4d5a69163982e4aac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Mar 2017 10:19:35 +0100
Subject: [PATCH 04/23] fix bug for bit-vector optimization. Issue #928

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index d1a3ddb8a..cd40944b2 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1002,8 +1002,8 @@ namespace opt {
             TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
             return false;
         }
-        unsigned bv_size;
-        if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) {
+        unsigned bvsz;
+        if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) {
             TRACE("opt", tout << "model does not evaluate objective to a value\n";);
             return false;
         }

From fcda4cee9fde8fa129637d87a261d683ff3ca3a2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Mar 2017 05:29:56 +0100
Subject: [PATCH 05/23] ensure evaluation of array equalities is enabled for
 external facing evaluator. Issue #917

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp            | 11 ++++++++++-
 src/model/model_evaluator.h              |  1 +
 src/model/model_evaluator_params.pyg     |  3 ++-
 src/smt/proto_model/proto_model.cpp      |  1 +
 src/smt/smt_model_checker.cpp            |  7 +++++--
 src/tactic/extension_model_converter.cpp |  1 +
 6 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index af2253801..61da4b3a0 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -50,6 +50,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     unsigned                        m_max_steps;
     bool                            m_model_completion;
     bool                            m_cache;
+    bool                            m_array_equalities;
 
     evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
         m_model(md),
@@ -81,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_max_steps        = p.max_steps();
         m_model_completion = p.completion();
         m_cache            = p.cache();
+        m_array_equalities = p.array_equalities();
     }
 
     ast_manager & m() const { return m_model.get_manager(); }
@@ -264,11 +266,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
-        return BR_FAILED;
         if (a == b) {
             result = m().mk_true();
             return BR_DONE;
         }
+        if (!m_array_equalities) {
+            return BR_FAILED;
+        }
+
         // disabled until made more efficient
         vector<expr_ref_vector> stores1, stores2;
         bool args_are_unique1, args_are_unique2;
@@ -508,6 +513,10 @@ void model_evaluator::set_model_completion(bool f) {
     m_imp->cfg().m_model_completion = f;
 }
 
+void model_evaluator::set_expand_array_equalities(bool f) {
+    m_imp->cfg().m_array_equalities = f;
+}
+
 unsigned model_evaluator::get_num_steps() const {
     return m_imp->get_num_steps();
 }
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index 3f4da5c96..ba55e96ba 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -35,6 +35,7 @@ public:
 
     ast_manager & m () const;
     void set_model_completion(bool f);
+    void set_expand_array_equalities(bool f);
 
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);
diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg
index b68d5c3ad..b6417f7fc 100644
--- a/src/model/model_evaluator_params.pyg
+++ b/src/model/model_evaluator_params.pyg
@@ -3,6 +3,7 @@ def_module_params('model_evaluator',
                   params=(max_memory_param(),
                           max_steps_param(),
                           ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
-                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator')
+                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
+                          ('array_equalities', BOOL, True, 'evaluate array equalities')
                           ))
 
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index a7875e99e..129bed87e 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -93,6 +93,7 @@ bool proto_model::is_select_of_model_value(expr* e) const {
 
 bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
     m_eval.set_model_completion(model_completion);
+    m_eval.set_expand_array_equalities(false);
     try {
         m_eval(e, result);
 #if 0
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 5329cd80f..093d215b6 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -290,7 +290,7 @@ namespace smt {
 
         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";);
+            TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);                
             if (r != l_true)
                 break; 
             model_ref cex;
@@ -300,7 +300,7 @@ namespace smt {
             }
             num_new_instances++;
             if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
-                TRACE("model_checker", tout << "Add blocking clause failed\n";);
+                TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";);
                 // add_blocking_clause failed... stop the search for new counter-examples...
                 break; 
             }
@@ -407,6 +407,7 @@ namespace smt {
                 found_relevant = true;
                 if (m.is_rec_fun_def(q)) {
                     if (!check_rec_fun(q)) {
+                        TRACE("model_checker", tout << "checking recursive function failed\n";);
                         num_failures++;
                     }
                 }
@@ -414,6 +415,7 @@ namespace smt {
                     if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
                         verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
                     }
+                    TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
                     num_failures++;
                 }
             }
@@ -452,6 +454,7 @@ namespace smt {
     }
 
     bool model_checker::has_new_instances() {
+        TRACE("model_checker", tout << "instances: " << m_new_instances.size() << "\n";);
         return !m_new_instances.empty();
     }
 
diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp
index ee6b8f691..18b5b6288 100644
--- a/src/tactic/extension_model_converter.cpp
+++ b/src/tactic/extension_model_converter.cpp
@@ -49,6 +49,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
     TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
     model_evaluator ev(*(md.get()));
     ev.set_model_completion(true);
+    ev.set_expand_array_equalities(false);
     expr_ref val(m());
     unsigned i = m_vars.size();
     while (i > 0) {

From 29969648ba7b2f567b5b35ae2330cae5a4803454 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Mar 2017 05:52:46 +0100
Subject: [PATCH 06/23] check that formulas are in lira before invoking qsat.
 Issue #919

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/smtlogics/quant_tactics.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 044511c33..7d428b369 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -28,6 +28,7 @@ Revision History:
 #include"ctx_simplify_tactic.h"
 #include"smt_tactic.h"
 #include"elim_term_ite_tactic.h"
+#include"probe_arith.h"
 
 static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
     params_ref pull_ite_p;
@@ -107,8 +108,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = and_then(mk_quant_preprocessor(m),
                            mk_qe_lite_tactic(m, p),
                            cond(mk_has_quantifier_probe(), 
-                                or_else(mk_qsat_tactic(m, p),
-                                        and_then(mk_qe_tactic(m), mk_smt_tactic())),
+                                cond(mk_is_lira_probe(),
+                                     or_else(mk_qsat_tactic(m, p),
+                                             and_then(mk_qe_tactic(m), mk_smt_tactic())),
+                                     mk_smt_tactic()),
                                 mk_smt_tactic()));
     st->updt_params(p);
     return st;

From e34996fa9d8dab9f90d66603f273c5767036c229 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Mar 2017 06:00:34 +0100
Subject: [PATCH 07/23] add notes to README based on feedback in #916

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 README.md | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e0821ac79..b03888e9d 100644
--- a/README.md
+++ b/README.md
@@ -168,7 +168,10 @@ python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/p
 
 If you do need to install to a non standard prefix a better approach is to use
 a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/)
-and install Z3 there.
+and install Z3 there. Python packages also work for Python3.
+Under Windows, recall to build inside the Visual C++ native command build environment.
+Note that the buit/python/z3 directory should be accessible from where python is used with Z3 
+and it depends on libz3.dll to be in the path.
 
 ```bash
 virtualenv venv
@@ -185,3 +188,10 @@ python -c 'import z3; print(z3.get_version_string())'
 ```
 
 See [``examples/python``](examples/python) for examples.
+
+
+Even though the build instruction says use python scripts/mk_make.py -x --python, this can build a package that works in python3.
+The building should take place inside the Visual C++ 2015 x64 Native Build Tools Prompt`.
+The z3.exe appears to be independent and can work anywhere, you can copy the built version wherever. The libz3.dll needs to be discoverable on the PATH. So you can copy both build/z3.exe and build/libz3.dll into somewhere on the PATH.
+Then the build/python/z3 directory should be copied into the site-packages directory of Python. On Windows, this isn't done automatically, instead you have to find your Windows site-packages: like python3 -c 'import site; print(site.getsitepackages())', then copy the entire directory there.
+Then to test if it finally all works run:
\ No newline at end of file

From 7b727fc7252fca67776964c64fea6759f43c70fb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Mar 2017 06:37:56 +0100
Subject: [PATCH 08/23] remove scratch notes from readme

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 README.md | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/README.md b/README.md
index b03888e9d..f4c6dd012 100644
--- a/README.md
+++ b/README.md
@@ -189,9 +189,3 @@ python -c 'import z3; print(z3.get_version_string())'
 
 See [``examples/python``](examples/python) for examples.
 
-
-Even though the build instruction says use python scripts/mk_make.py -x --python, this can build a package that works in python3.
-The building should take place inside the Visual C++ 2015 x64 Native Build Tools Prompt`.
-The z3.exe appears to be independent and can work anywhere, you can copy the built version wherever. The libz3.dll needs to be discoverable on the PATH. So you can copy both build/z3.exe and build/libz3.dll into somewhere on the PATH.
-Then the build/python/z3 directory should be copied into the site-packages directory of Python. On Windows, this isn't done automatically, instead you have to find your Windows site-packages: like python3 -c 'import site; print(site.getsitepackages())', then copy the entire directory there.
-Then to test if it finally all works run:
\ No newline at end of file

From 854bb2197f70b92eeae5e6291b22f4a85c9ddca1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Mar 2017 21:41:24 -0800
Subject: [PATCH 09/23] include recursive functions to models. Issue #898

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/combined_solver.cpp | 5 ++---
 src/util/vector.h              | 5 +++++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 1eb6be08e..d67643edf 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -228,7 +228,7 @@ public:
             if (m_inc_timeout == UINT_MAX) {
                 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);            
                 lbool r = m_solver2->check_sat(num_assumptions, assumptions);
-                if (r != l_undef || !use_solver1_when_undef()) {
+                if (r != l_undef || !use_solver1_when_undef() || get_manager().canceled()) {
                     return r;
                 }
             }
@@ -285,10 +285,9 @@ public:
     }
 
     virtual void collect_statistics(statistics & st) const {
+        m_solver2->collect_statistics(st);
         if (m_use_solver1_results)
             m_solver1->collect_statistics(st);
-        else
-            m_solver2->collect_statistics(st);
     }
 
     virtual void get_unsat_core(ptr_vector<expr> & r) {
diff --git a/src/util/vector.h b/src/util/vector.h
index 03c1d6019..7ffee2535 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -374,6 +374,11 @@ public:
         }
     }
 
+    void fill(unsigned sz, T const & elem) {
+        resize(sz);
+        fill(sz, elem);
+    }
+
     bool contains(T const & elem) const {
         const_iterator it  = begin();
         const_iterator e = end();

From fbf81c88a228975e1e593d27be2b90e041df4225 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Mar 2017 11:13:38 +0100
Subject: [PATCH 10/23] remove print breaking build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index d6a837d37..e816f5c73 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4183,7 +4183,6 @@ namespace smt {
             expr* e = m_asserted_formulas.get_formula(i);
             if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
-                std::cout << mk_pp(q, m) << "\n";
                 if (!m.is_rec_fun_def(q)) continue;
                 SASSERT(q->get_num_patterns() == 1);
                 expr* fn = to_app(q->get_pattern(0))->get_arg(0);

From 338193548b62cb8168dff0de89e2abc60b876c2f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 10 Mar 2017 22:52:55 +0100
Subject: [PATCH 11/23] fixing build break, adding fixedpoint object to C++ API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter.h     |  2 ++
 src/ast/rewriter/rewriter_def.h | 44 ++++++++++++++++++++++++++-------
 2 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index fc596cabd..2b4f4b14e 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -315,6 +315,8 @@ protected:
     template<bool ProofGen>
     void process_app(app * t, frame & fr);
 
+    bool constant_fold(app* t, frame& fr);
+
     template<bool ProofGen>
     void process_quantifier(quantifier * q, frame & fr);
 
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index dddb02dfd..aecc1c93a 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -174,6 +174,38 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     }
 }
 
+template<typename Config>
+bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
+    if (fr.m_i == 1 && m().is_ite(t)) {
+        expr * cond = result_stack()[fr.m_spos].get();
+        expr* arg = 0;
+        if (m().is_true(cond)) {
+            arg = t->get_arg(1);
+        }
+        else if (m().is_false(cond)) {
+            arg = t->get_arg(2);
+        }
+        if (arg) {
+            result_stack().shrink(fr.m_spos);
+            result_stack().push_back(arg);
+            fr.m_state = REWRITE_BUILTIN;
+            unsigned max_depth = fr.m_max_depth;
+            if (visit<false>(arg, fr.m_max_depth)) {
+                m_r = result_stack().back();
+                result_stack().pop_back(); 
+                result_stack().pop_back();
+                result_stack().push_back(m_r);
+                cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
+                frame_stack().pop_back();
+                set_new_child_flag(t);
+            }
+            m_r = 0;
+            return true;
+        }
+    }
+    return false;
+}
+
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
@@ -183,16 +215,10 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
     case PROCESS_CHILDREN: {
         unsigned num_args = t->get_num_args();
         while (fr.m_i < num_args) {
-            expr * arg = t->get_arg(fr.m_i);
-            if (fr.m_i >= 1 && m().is_ite(t) && !ProofGen) {
-                expr * cond = result_stack()[fr.m_spos].get();
-                if (m().is_true(cond)) {
-                    arg = t->get_arg(1);
-                }
-                else if (m().is_false(cond)) {
-                    arg = t->get_arg(2);
-                }
+            if (!ProofGen && constant_fold(t, fr)) {
+                return;
             }
+            expr * arg = t->get_arg(fr.m_i);
             fr.m_i++;
             if (!visit<ProofGen>(arg, fr.m_max_depth))
                 return;

From 509f7409badc0e7834968511ca3c6b6f97fdaed6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 10 Mar 2017 23:01:43 +0100
Subject: [PATCH 12/23] adding fixedpoint object to C++ API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 21a3fedf4..bfd4eb2c4 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2175,6 +2175,50 @@ namespace z3 {
     };
     inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
 
+    class fixedpoint : public object {
+        Z3_fixedpoint m_fp;
+    public:
+        fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
+        ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
+        operator Z3_fixedpoint() const { return m_fp; }        
+        void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
+        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(func_decl_vector& relations) { 
+            array<Z3_func_decl> rs(relations);
+            Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr()); 
+            check_error(); 
+            return to_check_result(r); 
+        }
+        expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
+        std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
+        void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
+        unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
+        expr get_cover_delta(int level, func_decl& p) { 
+            Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p); 
+            check_error();  
+            return expr(ctx(), r);
+        }
+        void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error();  }
+        stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
+        void register_relation(func_decl& p) { Z3_fixedpoint_register_relation(ctx(), m_fp, p); }
+        expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
+        expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
+        void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
+        std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
+        std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
+        std::string to_string(expr_vector const& queries) {
+            array<Z3_ast> qs(queries);
+            return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr()); 
+        }
+        void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
+        void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
+    };
+    inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
+
     inline tactic fail_if(probe const & p) {
         Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
         p.check_error();

From 228111511c8293c7a4b35743b141693d4a3b6415 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 11 Mar 2017 18:41:36 +0100
Subject: [PATCH 13/23] fixing build break, addressing #935

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp |  1 +
 src/smt/mam.cpp                 |  2 +-
 src/smt/smt_context.cpp         | 40 +++++++++++++++++++++++++++++----
 src/smt/smt_context.h           |  8 +++++++
 src/smt/smt_quantifier.cpp      | 26 ++++++++++++++-------
 5 files changed, 64 insertions(+), 13 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 67b1df50c..2551f0aa0 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1551,6 +1551,7 @@ void cmd_context::validate_model() {
     p.set_uint("sort_store", true);
     p.set_bool("completion", true);
     model_evaluator evaluator(*(md.get()), p);
+    evaluator.set_expand_array_equalities(false);
     contains_array_op_proc contains_array(m());
     {
         scoped_rlimit _rlimit(m().limit(), 0);
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 5d03a3563..ba9f970a2 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -3942,7 +3942,7 @@ namespace smt {
 #endif
         
         virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) {
-            TRACE("trigger_bug", tout << "found match\n";);
+            TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
 #ifdef Z3DEBUG
             if (m_check_missing_instances) {
                 if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index e816f5c73..3fca7d04b 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -304,7 +304,6 @@ namespace smt {
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";              
               display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
               display(tout, j););
-        SASSERT(l.var() < static_cast<int>(m_b_internalized_stack.size()));
         m_assigned_literals.push_back(l);
         m_assignment[l.index()]    = l_true;
         m_assignment[(~l).index()] = l_false;
@@ -319,14 +318,23 @@ namespace smt {
         d.m_phase_available        = true;
         d.m_phase                  = !l.sign();
         TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
+
         TRACE("relevancy", 
-              tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";);
-        if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var()))))
+              tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
+        if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
             m_atom_propagation_queue.push_back(l);
 
         if (m_manager.has_trace_stream())
             trace_assign(l, j, decision);
         m_case_split_queue->assign_lit_eh(l);
+
+        // a unit is asserted at search level. Mark it as relevant.
+        // this addresses bug... where a literal becomes fixed to true (false)
+        // as a conflict gets assigned misses relevancy (and quantifier instantiation).
+        // 
+        if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) {
+            mark_as_relevant(l);
+        }
     }
     
     bool context::bcp() {
@@ -1634,7 +1642,7 @@ namespace smt {
                     m_atom_propagation_queue.push_back(literal(v, val == l_false));
             }
         }
-        TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << "\n";);
+        TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";);
 #ifndef SMTCOMP
         m_case_split_queue->relevant_eh(n);
 #endif
@@ -3737,7 +3745,9 @@ namespace smt {
             // I invoke pop_scope_core instead of pop_scope because I don't want
             // to reset cached generations... I need them to rebuild the literals
             // of the new conflict clause.
+            if (relevancy()) record_relevancy(num_lits, lits);
             unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl);
+            if (relevancy()) restore_relevancy(num_lits, lits);
             SASSERT(m_scope_lvl == new_lvl);
             // the logical context may still be in conflict after
             // clauses are reinitialized in pop_scope.
@@ -3850,6 +3860,28 @@ namespace smt {
         }
         return false;
     }
+    
+    /*
+      \brief we record and restore relevancy information for literals in conflict clauses.
+      A literal may have been marked relevant within the scope that gets popped during
+      conflict resolution. In this case, the literal is no longer marked as relevant after
+      the pop. This can cause quantifier instantiation to miss relevant triggers and thereby
+      cause incmpleteness.
+     */
+    void context::record_relevancy(unsigned n, literal const* lits) {
+        m_relevant_conflict_literals.reset();
+        for (unsigned i = 0; i < n; ++i) {
+            m_relevant_conflict_literals.push_back(is_relevant(lits[i]));
+        }
+    }
+
+    void context::restore_relevancy(unsigned n, literal const* lits) {
+        for (unsigned i = 0; i < n; ++i) {
+            if (m_relevant_conflict_literals[i] && !is_relevant(lits[i])) {
+                mark_as_relevant(lits[i]);
+            }
+        }
+    }
 
     void context::get_relevant_labels(expr* cnstr, buffer<symbol> & result) {
         if (m_fparams.m_check_at_labels) {
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index c1c684fec..2a555e6b5 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1103,6 +1103,10 @@ namespace smt {
 
         bool is_relevant_core(expr * n) const { return m_relevancy_propagator->is_relevant(n); }
 
+        svector<bool>  m_relevant_conflict_literals;
+        void record_relevancy(unsigned n, literal const* lits);
+        void restore_relevancy(unsigned n, literal const* lits);
+
     public:
         // event handler for relevancy_propagator class
         void relevant_eh(expr * n);
@@ -1124,6 +1128,10 @@ namespace smt {
             return is_relevant(l.var());
         }
 
+        bool is_relevant_core(literal l) const {
+            return is_relevant_core(bool_var2expr(l.var()));
+        }
+
         void mark_as_relevant(expr * n) { m_relevancy_propagator->mark_as_relevant(n); m_relevancy_propagator->propagate(); }
 
         void mark_as_relevant(enode * n) { mark_as_relevant(n->get_owner()); }
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 2a56168f2..bad788f5d 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -52,8 +52,9 @@ namespace smt {
             m_qi_queue.setup();
         }
 
-        bool has_trace_stream() const { return m_context.get_manager().has_trace_stream(); }
-        std::ostream & trace_stream() { return m_context.get_manager().trace_stream(); }
+        ast_manager& m() const { return m_context.get_manager(); }
+        bool has_trace_stream() const { return m().has_trace_stream(); }
+        std::ostream & trace_stream() { return m().trace_stream(); }
 
         quantifier_stat * get_stat(quantifier * q) const {
             return m_quantifier_stat.find(q);
@@ -110,8 +111,9 @@ namespace smt {
                           unsigned max_top_generation,
                           ptr_vector<enode> & used_enodes) {
             max_generation = std::max(max_generation, get_generation(q));
-            if (m_num_instances > m_params.m_qi_max_instances)
+            if (m_num_instances > m_params.m_qi_max_instances) {
                 return false;
+            }
             get_stat(q)->update_max_generation(max_generation);
             fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
             if (f) {
@@ -132,9 +134,17 @@ namespace smt {
                 }
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
                 m_num_instances++;
-                return true;
             }
-            return false;
+            TRACE("quantifier", 
+                  tout << mk_pp(q, m()) << " ";
+                  for (unsigned i = 0; i < num_bindings; ++i) {
+                      tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
+                  }
+                  tout << "\n";
+                  tout << "inserted: " << (f != 0) << "\n";
+                  );
+
+            return f != 0;
         }
 
         void init_search_eh() {
@@ -186,7 +196,7 @@ namespace smt {
         }
 
         bool check_quantifier(quantifier* q) {
-            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m_context.get_manager().is_rec_fun_def(q);
+            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m().is_rec_fun_def(q);
         }
 
         bool quick_check_quantifiers() {
@@ -501,13 +511,13 @@ namespace smt {
                 SASSERT(m_context->get_manager().is_pattern(mp));
                 bool unary = (mp->get_num_args() == 1);
                 if (!unary && j >= num_eager_multi_patterns) {
-                    TRACE("assign_quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n"
+                    TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n"
                           << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns
                           << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";);
                     m_lazy_mam->add_pattern(q, mp);
                 }
                 else {
-                    TRACE("assign_quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";);
+                    TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";);
                     m_mam->add_pattern(q, mp);
                 }
                 if (!unary)

From 559c5e5ae63e13a0fbb18b7b6589d8a0b111debe Mon Sep 17 00:00:00 2001
From: James Bornholt <bornholt@cs.washington.edu>
Date: Sat, 11 Mar 2017 16:03:09 -0800
Subject: [PATCH 14/23] z3py: With tactical should not try to use context as a
 parameter

---
 src/api/python/z3/z3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a0aba95d6..16d7fbb5f 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7204,7 +7204,7 @@ def With(t, *args, **keys):
     >>> t((x + 1)*(y + 2) == 0)
     [[2*x + y + x*y == -2]]
     """
-    ctx = keys.get('ctx', None)
+    ctx = keys.pop('ctx', None)
     t = _to_tactic(t, ctx)
     p = args2params(args, keys, t.ctx)
     return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)

From 8bec1e25a83e8e3f8c9b48f1641b68b6df841f08 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Mar 2017 08:32:06 +0100
Subject: [PATCH 15/23] move restore relevancy until after literals have been
 replayed

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 3fca7d04b..9336322f7 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3747,7 +3747,6 @@ namespace smt {
             // of the new conflict clause.
             if (relevancy()) record_relevancy(num_lits, lits);
             unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl);
-            if (relevancy()) restore_relevancy(num_lits, lits);
             SASSERT(m_scope_lvl == new_lvl);
             // the logical context may still be in conflict after
             // clauses are reinitialized in pop_scope.
@@ -3778,6 +3777,7 @@ namespace smt {
                     }
                 }
             }
+            if (relevancy()) restore_relevancy(num_lits, lits);
             // Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core
             reset_cache_generation();
             TRACE("resolve_conflict_bug", 

From 2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 12 Mar 2017 12:29:26 +0100
Subject: [PATCH 16/23] [CMake] Support including Git hash and description into
 the build. CMake will automatically pick up changes in git's HEAD so that the
 necessary code is rebuilt when the build system is invoked.

Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been
added that enable/disable including the git hash and the output of `git
describe` respectively. By default if the source tree is a git
repository both options are on, otherwise they are false by default.

To support the `Z3GITHASH` macro a different implementation is used from
the old build system. In that build system the define is passed on the
command line. This would not work well for CMake because CMake
conservatively (and correctly) rebuilds *everything* if the flags given
to the compiler change. This would result in the entire project being
rebuilt everytime git's `HEAD` changed.  Instead in this implementation
a CMake specific version of `version.h.in` (named `version.h.cmake.in`)
is added that uses the `#cmakedefine` feature of CMake's
`configure_file()` command to define `Z3GITHASH` if it is available and
not define it otherwise. This way only object files that depend on
`version.h` get re-built rather than the whole project.

It is unfortunate that the build systems now have different `version.h`
file templates. However they are very simple and I don't want to
modify how templates are handled in the python/Makefile build system.
---
 CMakeLists.txt                        |  60 ++++++++-
 README-CMake.md                       |   2 +
 contrib/cmake/cmake/git_utils.cmake   | 173 ++++++++++++++++++++++++++
 contrib/cmake/src/util/CMakeLists.txt |   4 +-
 src/util/version.h.cmake.in           |   8 ++
 5 files changed, 245 insertions(+), 2 deletions(-)
 create mode 100644 contrib/cmake/cmake/git_utils.cmake
 create mode 100644 src/util/version.h.cmake.in

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 87bd07f31..8788cdaf4 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -35,8 +35,8 @@ set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 5)
 set(Z3_VERSION_PATCH 1)
 set(Z3_VERSION_TWEAK 0)
-set(Z3_FULL_VERSION 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
+set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
 message(STATUS "Z3 version ${Z3_VERSION}")
 
 ################################################################################
@@ -75,6 +75,64 @@ endif()
 ################################################################################
 list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules")
 
+################################################################################
+# Handle git hash and description
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/git_utils.cmake)
+macro(disable_git_describe)
+  message(WARNING "Disabling INCLUDE_GIT_DESCRIBE")
+  set(INCLUDE_GIT_DESCRIBE OFF CACHE BOOL "Include git describe output in version output" FORCE)
+endmacro()
+macro(disable_git_hash)
+  message(WARNING "Disabling INCLUDE_GIT_HASH")
+  set(INCLUDE_GIT_HASH OFF CACHE BOOL "Include git hash in version output" FORCE)
+  unset(Z3GITHASH) # Used in configure_file()
+endmacro()
+option(INCLUDE_GIT_HASH "Include git hash in version output" ON)
+option(INCLUDE_GIT_DESCRIBE "Include git describe output in version output" ON)
+
+set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git")
+if (EXISTS "${GIT_DIR}")
+  # Try to make CMake configure depend on the current git HEAD so that
+  # a re-configure is triggered when the HEAD changes.
+  add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
+  if (ADD_GIT_DEP_SUCCESS)
+    if (INCLUDE_GIT_HASH)
+      get_git_head_hash("${GIT_DIR}" Z3GITHASH)
+      if (NOT Z3GITHASH)
+        message(WARNING "Failed to get Git hash")
+        disable_git_hash()
+      endif()
+      message(STATUS "Using Git hash in version output: ${Z3GITHASH}")
+      # This mimics the behaviour of the old build system.
+      string(APPEND Z3_FULL_VERSION_STR " ${Z3GITHASH}")
+    else()
+      message(STATUS "Not using Git hash in version output")
+      unset(Z3GITHASH) # Used in configure_file()
+    endif()
+    if (INCLUDE_GIT_DESCRIBE)
+      get_git_head_describe("${GIT_DIR}" Z3_GIT_DESCRIPTION)
+      if (NOT Z3_GIT_DESCRIPTION)
+        message(WARNING "Failed to get Git description")
+        disable_git_describe()
+      endif()
+      message(STATUS "Using Git description in version output: ${Z3_GIT_DESCRIPTION}")
+      # This mimics the behaviour of the old build system.
+      string(APPEND Z3_FULL_VERSION_STR " ${Z3_GIT_DESCRIPTION}")
+    else()
+      message(STATUS "Not including git descrption in version")
+    endif()
+  else()
+    message(WARNING "Failed to add git dependency.")
+    disable_git_describe()
+    disable_git_hash()
+  endif()
+else()
+  message(STATUS "Failed to find git directory.")
+  disable_git_describe()
+  disable_git_hash()
+endif()
+
 ################################################################################
 # Useful CMake functions/Macros
 ################################################################################
diff --git a/README-CMake.md b/README-CMake.md
index 0943e7a7d..2a8317890 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -283,6 +283,8 @@ The following useful options can be passed to CMake whilst configuring.
 * ``INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings.
 * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
 * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
+* ``INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build.
+* ``INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 
diff --git a/contrib/cmake/cmake/git_utils.cmake b/contrib/cmake/cmake/git_utils.cmake
new file mode 100644
index 000000000..aa7f38825
--- /dev/null
+++ b/contrib/cmake/cmake/git_utils.cmake
@@ -0,0 +1,173 @@
+# add_git_dir_dependency(GIT_DIR SUCCESS_VAR)
+#
+# Adds a configure time dependency on the git directory such that if the HEAD
+# of the git directory changes CMake will be forced to re-run. This useful
+# for fetching the current git hash and including it in the build.
+#
+# `GIT_DIR` is the path to the git directory (i.e. the `.git` directory)
+# `SUCCESS_VAR` is the name of the variable to set. It will be set to TRUE
+# if the dependency was successfully added and FALSE otherwise.
+function(add_git_dir_dependency GIT_DIR SUCCESS_VAR)
+  if (NOT "${ARGC}" EQUAL 2)
+    message(FATAL_ERROR "Invalid number (${ARGC}) of arguments")
+  endif()
+
+  if (NOT IS_ABSOLUTE "${GIT_DIR}")
+    message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not an absolute path")
+  endif()
+
+  if (NOT IS_DIRECTORY "${GIT_DIR}")
+    message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not a directory")
+  endif()
+
+  set(GIT_HEAD_FILE "${GIT_DIR}/HEAD")
+  if (NOT EXISTS "${GIT_HEAD_FILE}")
+    message(AUTHOR_WARNING "Git head file \"${GIT_HEAD_FILE}\" cannot be found")
+    set(${SUCCESS_VAR} FALSE PARENT_SCOPE)
+    return()
+  endif()
+
+  # List of files in the git tree that CMake configuration should depend on
+  set(GIT_FILE_DEPS "${GIT_HEAD_FILE}")
+
+  # Examine the HEAD and workout what additional dependencies there are.
+  file(READ "${GIT_HEAD_FILE}" GIT_HEAD_DATA LIMIT 128)
+  string(STRIP "${GIT_HEAD_DATA}" GIT_HEAD_DATA_STRIPPED)
+
+  if ("${GIT_HEAD_DATA_STRIPPED}" MATCHES "^ref:[ ]*(.+)$")
+    # HEAD points at a reference.
+    set(GIT_REF "${CMAKE_MATCH_1}")
+    if (EXISTS "${GIT_DIR}/${GIT_REF}")
+      # Unpacked reference. The file contains the commit hash
+      # so add a dependency on this file so that if we stay on this
+      # reference (i.e. branch) but change commit CMake will be forced
+      # to reconfigure.
+      list(APPEND GIT_FILE_DEPS "${GIT_DIR}/${GIT_REF}")
+    elseif(EXISTS "${GIT_DIR}/packed-refs")
+      # The ref must be packed (see `man git-pack-refs`).
+      list(APPEND GIT_FILE_DEPS "${GIT_DIR}/packed-refs")
+    else()
+      # Fail
+      message(AUTHOR_WARNING "Unhandled git reference")
+      set(${SUCCESS_VAR} FALSE PARENT_SCOPE)
+      return()
+    endif()
+  else()
+    # Detached HEAD.
+    # No other dependencies needed
+  endif()
+
+  # FIXME:
+  # This is the directory we will copy (via `configure_file()`) git files
+  # into. This is a hack. It would be better to use the
+  # `CMAKE_CONFIGURE_DEPENDS` directory property but that feature is not
+  # available in CMake 2.8.12. So we use `configure_file()` to effectively
+  # do the same thing. When the source file to `configure_file()` changes
+  # it will trigger a re-run of CMake.
+  set(GIT_CMAKE_FILES_DIR "${CMAKE_CURRENT_BINARY_DIR}/git_cmake_files")
+  file(MAKE_DIRECTORY "${GIT_CMAKE_FILES_DIR}")
+
+  foreach (git_dependency ${GIT_FILE_DEPS})
+    message(STATUS "Adding git dependency \"${git_dependency}\"")
+    configure_file(
+      "${git_dependency}"
+      "${GIT_CMAKE_FILES_DIR}"
+      COPYONLY
+    )
+  endforeach()
+
+  set(${SUCCESS_VAR} TRUE PARENT_SCOPE)
+endfunction()
+
+# get_git_head_hash(GIT_DIR OUTPUT_VAR)
+#
+# Retrieve the current commit hash for a git working directory where `GIT_DIR`
+# is the `.git` directory in the root of the git working directory.
+#
+# `OUTPUT_VAR` should be the name of the variable to put the result in. If this
+# function fails then either a fatal error will be raised or `OUTPUT_VAR` will
+# contain a string with the suffix `NOTFOUND` which can be used in CMake `if()`
+# commands.
+function(get_git_head_hash GIT_DIR OUTPUT_VAR)
+  if (NOT "${ARGC}" EQUAL 2)
+    message(FATAL_ERROR "Invalid number of arguments")
+  endif()
+  if (NOT IS_DIRECTORY "${GIT_DIR}")
+    message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory")
+  endif()
+  if (NOT IS_ABSOLUTE "${GIT_DIR}")
+    message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path")
+  endif()
+  find_package(Git)
+  if (NOT Git_FOUND)
+    set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE)
+    return()
+  endif()
+  get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY)
+  execute_process(
+    COMMAND
+      "${GIT_EXECUTABLE}"
+      "rev-parse"
+      "-q" # Quiet
+      "HEAD"
+    WORKING_DIRECTORY
+      "${GIT_WORKING_DIR}"
+    RESULT_VARIABLE
+      GIT_EXIT_CODE
+    OUTPUT_VARIABLE
+      Z3_GIT_HASH
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+  )
+  if (NOT "${GIT_EXIT_CODE}" EQUAL 0)
+    message(WARNING "Failed to execute git")
+    set(${OUTPUT_VAR} NOTFOUND PARENT_SCOPE)
+    return()
+  endif()
+  set(${OUTPUT_VAR} "${Z3_GIT_HASH}" PARENT_SCOPE)
+endfunction()
+
+# get_git_head_describe(GIT_DIR OUTPUT_VAR)
+#
+# Retrieve the output of `git describe` for a git working directory where
+# `GIT_DIR` is the `.git` directory in the root of the git working directory.
+#
+# `OUTPUT_VAR` should be the name of the variable to put the result in. If this
+# function fails then either a fatal error will be raised or `OUTPUT_VAR` will
+# contain a string with the suffix `NOTFOUND` which can be used in CMake `if()`
+# commands.
+function(get_git_head_describe GIT_DIR OUTPUT_VAR)
+  if (NOT "${ARGC}" EQUAL 2)
+    message(FATAL_ERROR "Invalid number of arguments")
+  endif()
+  if (NOT IS_DIRECTORY "${GIT_DIR}")
+    message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory")
+  endif()
+  if (NOT IS_ABSOLUTE "${GIT_DIR}")
+    message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path")
+  endif()
+  find_package(Git)
+  if (NOT Git_FOUND)
+    set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE)
+    return()
+  endif()
+  get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY)
+  execute_process(
+    COMMAND
+      "${GIT_EXECUTABLE}"
+      "describe"
+      "--long"
+    WORKING_DIRECTORY
+      "${GIT_WORKING_DIR}"
+    RESULT_VARIABLE
+      GIT_EXIT_CODE
+    OUTPUT_VARIABLE
+      Z3_GIT_DESCRIPTION
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+  )
+  if (NOT "${GIT_EXIT_CODE}" EQUAL 0)
+    message(WARNING "Failed to execute git")
+    set(${OUTPUT_VAR} NOTFOUND PARENT_SCOPE)
+    return()
+  endif()
+  set(${OUTPUT_VAR} "${Z3_GIT_DESCRIPTION}" PARENT_SCOPE)
+endfunction()
diff --git a/contrib/cmake/src/util/CMakeLists.txt b/contrib/cmake/src/util/CMakeLists.txt
index c85076531..b76f909d0 100644
--- a/contrib/cmake/src/util/CMakeLists.txt
+++ b/contrib/cmake/src/util/CMakeLists.txt
@@ -3,7 +3,9 @@ if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
           ${z3_polluted_tree_msg}
   )
 endif()
-configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY)
+
+set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"")
+configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h)
 
 z3_add_component(util
   SOURCES
diff --git a/src/util/version.h.cmake.in b/src/util/version.h.cmake.in
new file mode 100644
index 000000000..af3a652a6
--- /dev/null
+++ b/src/util/version.h.cmake.in
@@ -0,0 +1,8 @@
+// automatically generated file.
+#define Z3_MAJOR_VERSION   @Z3_VERSION_MAJOR@
+#define Z3_MINOR_VERSION   @Z3_VERSION_MINOR@
+#define Z3_BUILD_NUMBER    @Z3_VERSION_PATCH@
+#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@
+
+#define Z3_FULL_VERSION    @Z3_FULL_VERSION@
+#cmakedefine Z3GITHASH @Z3GITHASH@

From 73614abf37feab15d4558cf65d0ab682ecd2e7f7 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 3 Mar 2017 19:39:53 +0000
Subject: [PATCH 17/23] [CMake] Implement generation of `Z3Config.cmake` and
 `Z3Target.cmake` file for the build and install tree.

These files allow users of CMake to use Z3 via a CMake config package.
Clients can do `find_package(Z3 CONFIG)` to get use the package from
their projects.

When generating the files for the install tree we try to generate
the files so that they are relocatable so that it shouldn't matter
if the installed files aren't in the CMAKE_INSTALL_PREFIX when
a user consumes them. As long as the relative locations of the files
aren't changed things should still work.

A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been
added so that the install location of the Z3 CMake package files can be
controlled.

This addresses #915 .
---
 CMakeLists.txt                        | 78 +++++++++++++++++++++++++++
 README-CMake.md                       |  1 +
 contrib/cmake/cmake/Z3Config.cmake.in | 30 +++++++++++
 contrib/cmake/src/CMakeLists.txt      |  1 +
 4 files changed, 110 insertions(+)
 create mode 100644 contrib/cmake/cmake/Z3Config.cmake.in

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8788cdaf4..72ea1143d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -398,10 +398,18 @@ set(CMAKE_INSTALL_PKGCONFIGDIR
   PATH
   "Directory to install pkgconfig files"
 )
+
+set(CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR
+  "${CMAKE_INSTALL_LIBDIR}/cmake/z3"
+  CACHE
+  PATH
+  "Directory to install Z3 CMake package files"
+)
 message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"")
 message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"")
 message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"")
 message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"")
+message(STATUS "CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: \"${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}\"")
 
 ################################################################################
 # Uninstall rule
@@ -449,6 +457,76 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake)
 include(${CMAKE_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake)
 add_subdirectory(src)
 
+################################################################################
+# Create `Z3Config.cmake` and related files for the build tree so clients can
+# use Z3 via CMake.
+################################################################################
+include(CMakePackageConfigHelpers)
+export(EXPORT Z3_EXPORTED_TARGETS
+  NAMESPACE z3::
+  FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake"
+)
+set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_BINARY_DIR}/src/api")
+set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api")
+set(Z3_CXX_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api/c++")
+set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT")
+set(CONFIG_FILE_TYPE "build tree")
+configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in"
+  "Z3Config.cmake"
+  INSTALL_DESTINATION "${CMAKE_BINARY_DIR}"
+  PATH_VARS
+    Z3_FIRST_PACKAGE_INCLUDE_DIR
+    Z3_SECOND_PACKAGE_INCLUDE_DIR
+    Z3_CXX_PACKAGE_INCLUDE_DIR
+  INSTALL_PREFIX "${CMAKE_BINARY_DIR}"
+)
+unset(Z3_FIRST_PACKAGE_INCLUDE_DIR)
+unset(Z3_SECOND_PACKAGE_INCLUDE_DIR)
+unset(Z3_CXX_PACKAGE_INCLUDE_DIR)
+unset(AUTO_GEN_MSG)
+unset(CONFIG_FILE_TYPE)
+# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version
+# of Z3 they want.
+
+################################################################################
+# Create `Z3Config.cmake` and related files for install tree so clients can use
+# Z3 via CMake.
+################################################################################
+install(EXPORT
+  Z3_EXPORTED_TARGETS
+  FILE "Z3Targets.cmake"
+  NAMESPACE z3::
+  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
+)
+set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${CMAKE_BINARY_DIR}/cmake/Z3Config.cmake")
+set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_INSTALL_INCLUDEDIR}")
+set(Z3_SECOND_INCLUDE_DIR "")
+set(Z3_CXX_PACKAGE_INCLUDE_DIR "")
+set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT")
+set(CONFIG_FILE_TYPE "install tree")
+# We use `configure_package_config_file()` to try and create CMake files
+# that are re-locatable so that it doesn't matter if the files aren't placed
+# in the original install prefix.
+configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in"
+  "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
+  INSTALL_DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
+  PATH_VARS Z3_FIRST_PACKAGE_INCLUDE_DIR
+)
+unset(Z3_FIRST_PACKAGE_INCLUDE_DIR)
+unset(Z3_SECOND_PACKAGE_INCLUDE_DIR)
+unset(Z3_CXX_PACKAGE_INCLUDE_DIR)
+unset(AUTO_GEN_MSG)
+unset(CONFIG_FILE_TYPE)
+
+# Add install rule to install ${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}
+install(
+  FILES "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
+  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
+)
+
+# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version
+# of Z3 they want.
+
 ################################################################################
 # Examples
 ################################################################################
diff --git a/README-CMake.md b/README-CMake.md
index 2a8317890..6a78b5d4c 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -267,6 +267,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``).
 * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files.
 * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute.
+* ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``).
 * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled.
 * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
 * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
diff --git a/contrib/cmake/cmake/Z3Config.cmake.in b/contrib/cmake/cmake/Z3Config.cmake.in
new file mode 100644
index 000000000..e7f604591
--- /dev/null
+++ b/contrib/cmake/cmake/Z3Config.cmake.in
@@ -0,0 +1,30 @@
+################################################################################
+# @AUTO_GEN_MSG@
+#
+# This file is intended to be consumed by clients who wish to use Z3 from CMake.
+# It can be use by doing `find_package(Z3 config)` from within a
+# `CMakeLists.txt` file. If CMake doesn't find this package automatically you
+# can give it a hint by passing `-DZ3_DIR=<path>` to the CMake invocation where
+# `<path>` is the path to the directory containing this file.
+#
+# This file was built for the @CONFIG_FILE_TYPE@.
+################################################################################
+
+# Exported targets
+include("${CMAKE_CURRENT_LIST_DIR}/Z3Targets.cmake")
+
+@PACKAGE_INIT@
+
+# Version information
+set(Z3_VERSION_MAJOR @Z3_VERSION_MAJOR@)
+set(Z3_VERSION_MINOR @Z3_VERSION_MINOR@)
+set(Z3_VERSION_PATCH @Z3_VERSION_PATCH@)
+set(Z3_VERSION_TWEAK @Z3_VERSION_TWEAK@)
+set(Z3_VERSION_STRING "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
+
+# NOTE: We can't use `set_and_check()` here because this a list of paths.
+# List of include directories
+set(Z3_C_INCLUDE_DIRS @PACKAGE_Z3_FIRST_PACKAGE_INCLUDE_DIR@ @PACKAGE_Z3_SECOND_PACKAGE_INCLUDE_DIR@)
+set(Z3_CXX_INCLUDE_DIRS @PACKAGE_Z3_CXX_PACKAGE_INCLUDE_DIR@ ${Z3_C_INCLUDE_DIRS})
+# List of libraries to link against
+set(Z3_LIBRARIES "z3::libz3")
diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt
index 65eef8094..548b59053 100644
--- a/contrib/cmake/src/CMakeLists.txt
+++ b/contrib/cmake/src/CMakeLists.txt
@@ -168,6 +168,7 @@ foreach (header ${libz3_public_headers})
 endforeach()
 
 install(TARGETS libz3
+  EXPORT Z3_EXPORTED_TARGETS
   LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
   ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
   RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake

From d9617841e085f8d62bafb5a6994db96807aacdcd Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 4 Mar 2017 13:07:36 +0000
Subject: [PATCH 18/23] [CMake] Python examples should only be copied over if
 python bindings are being built.

---
 contrib/cmake/examples/CMakeLists.txt | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt
index e596ed3dd..04df6e6b4 100644
--- a/contrib/cmake/examples/CMakeLists.txt
+++ b/contrib/cmake/examples/CMakeLists.txt
@@ -1,4 +1,6 @@
 add_subdirectory(c)
 add_subdirectory(c++)
 add_subdirectory(tptp)
-add_subdirectory(python)
+if (BUILD_PYTHON_BINDINGS)
+  add_subdirectory(python)
+endif()

From db5520c71d1dca4354ad82bbed4a7afad240dca1 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 4 Mar 2017 16:45:37 +0000
Subject: [PATCH 19/23] [CMake] Build `c_example`, `cpp_example` and `z3_tptp5`
 as external projects.

This works by giving each example it's own CMake build system and
then consuming Z3 via the Z3 CMake config package from the build
tree.
---
 contrib/cmake/examples/CMakeLists.txt      | 64 +++++++++++++++++++++-
 contrib/cmake/examples/c++/CMakeLists.txt  | 37 ++++++++++---
 contrib/cmake/examples/c/CMakeLists.txt    | 35 +++++++++---
 contrib/cmake/examples/tptp/CMakeLists.txt | 32 +++++++++--
 4 files changed, 144 insertions(+), 24 deletions(-)

diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt
index 04df6e6b4..3fa49f9e0 100644
--- a/contrib/cmake/examples/CMakeLists.txt
+++ b/contrib/cmake/examples/CMakeLists.txt
@@ -1,6 +1,64 @@
-add_subdirectory(c)
-add_subdirectory(c++)
-add_subdirectory(tptp)
+include(ExternalProject)
+# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject
+# that shipped with CMake >= 3.1.
+if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1"))
+  set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1)
+else()
+  set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
+endif()
+
+################################################################################
+# Build example project using libz3's C API as an external project
+################################################################################
+ExternalProject_Add(c_example
+  DEPENDS libz3
+  # Configure step
+  SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c"
+  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  # Build step
+  ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
+  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
+  # Install Step
+  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+)
+set_target_properties(c_example PROPERTIES EXCLUDE_FROM_ALL TRUE)
+
+
+################################################################################
+# Build example project using libz3's C++ API as an external project
+################################################################################
+ExternalProject_Add(cpp_example
+  DEPENDS libz3
+  # Configure step
+  SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++"
+  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  # Build step
+  ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
+  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir"
+  # Install Step
+  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+)
+set_target_properties(cpp_example PROPERTIES EXCLUDE_FROM_ALL TRUE)
+
+################################################################################
+# Build example tptp5 project using libz3's C++ API as an external project
+################################################################################
+ExternalProject_Add(z3_tptp5
+  DEPENDS libz3
+  # Configure step
+  SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp"
+  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  # Build step
+  ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
+  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir"
+  # Install Step
+  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+)
+set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE)
+
+################################################################################
+# Build Python examples
+################################################################################
 if (BUILD_PYTHON_BINDINGS)
   add_subdirectory(python)
 endif()
diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt
index fdc5cf387..b25bea533 100644
--- a/contrib/cmake/examples/c++/CMakeLists.txt
+++ b/contrib/cmake/examples/c++/CMakeLists.txt
@@ -1,9 +1,28 @@
-# FIXME: We should build this as an external project and consume
-# Z3 as `find_package(z3 CONFIG)`.
-add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp)
-target_link_libraries(cpp_example PRIVATE libz3)
-target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api")
-target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++")
-if (NOT BUILD_LIBZ3_SHARED)
-  z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
-endif()
+################################################################################
+# Example C++ project
+################################################################################
+project(Z3_C_EXAMPLE CXX)
+cmake_minimum_required(VERSION 2.8.12)
+find_package(Z3
+  REQUIRED
+  CONFIG
+  # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
+  # This should prevent us from accidently picking up an installed
+  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # this project. When making your own project you probably shouldn't
+  # use this option.
+  NO_DEFAULT_PATH
+)
+message(STATUS "Z3_FOUND: ${Z3_FOUND}")
+message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
+message(STATUS "Z3_DIR: ${Z3_DIR}")
+
+add_executable(cpp_example example.cpp)
+target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
+target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
+
+# FIXME: The Z3 package does not export information on the link flags
+# This is needed for when libz3 is built as a static library
+#if (NOT BUILD_LIBZ3_SHARED)
+#  z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+#endif()
diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt
index fc6eaee18..d51503e29 100644
--- a/contrib/cmake/examples/c/CMakeLists.txt
+++ b/contrib/cmake/examples/c/CMakeLists.txt
@@ -1,9 +1,28 @@
-# FIXME: We should build this as an external project and consume
-# Z3 as `find_package(z3 CONFIG)`.
-add_executable(c_example EXCLUDE_FROM_ALL test_capi.c)
-target_link_libraries(c_example PRIVATE libz3)
-target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api")
+################################################################################
+# Example C project
+################################################################################
+project(Z3_C_EXAMPLE C)
+cmake_minimum_required(VERSION 2.8.12)
+find_package(Z3
+  REQUIRED
+  CONFIG
+  # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
+  # This should prevent us from accidently picking up an installed
+  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # this project. When making your own project you probably shouldn't
+  # use this option.
+  NO_DEFAULT_PATH
+)
+message(STATUS "Z3_FOUND: ${Z3_FOUND}")
+message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
+message(STATUS "Z3_DIR: ${Z3_DIR}")
+
+add_executable(c_example test_capi.c)
+target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
+target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
+
+# FIXME: The Z3 package does not export information on the link flags
 # This is needed for when libz3 is built as a static library
-if (NOT BUILD_LIBZ3_SHARED)
-  z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS})
-endif()
+#if (NOT BUILD_LIBZ3_SHARED)
+#  z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS})
+#endif()
diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt
index 41fa9cc65..6a2858a9b 100644
--- a/contrib/cmake/examples/tptp/CMakeLists.txt
+++ b/contrib/cmake/examples/tptp/CMakeLists.txt
@@ -1,4 +1,28 @@
-add_executable(z3_tptp5 EXCLUDE_FROM_ALL tptp5.cpp tptp5.lex.cpp)
-target_link_libraries(z3_tptp5 PRIVATE libz3)
-target_include_directories(z3_tptp5 PRIVATE "${CMAKE_SOURCE_DIR}/src/api")
-target_include_directories(z3_tptp5 PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++")
+################################################################################
+# TPTP example
+################################################################################
+project(Z3_TPTP5 CXX)
+cmake_minimum_required(VERSION 2.8.12)
+find_package(Z3
+  REQUIRED
+  CONFIG
+  # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
+  # This should prevent us from accidently picking up an installed
+  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # this project. When making your own project you probably shouldn't
+  # use this option.
+  NO_DEFAULT_PATH
+)
+message(STATUS "Z3_FOUND: ${Z3_FOUND}")
+message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
+message(STATUS "Z3_DIR: ${Z3_DIR}")
+
+add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp)
+target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS})
+target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES})
+
+# FIXME: The Z3 package does not export information on the link flags
+# This is needed for when libz3 is built as a static library
+#if (NOT BUILD_LIBZ3_SHARED)
+#  z3_append_linker_flag_list_to_target(z3_tptp5 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+#endif()

From b20bf5169a5f9d7c6e235199b081993f210084c6 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 4 Mar 2017 16:49:19 +0000
Subject: [PATCH 20/23] [CMake] Fix typo handling OpenMP flags.

---
 CMakeLists.txt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 72ea1143d..6281f951b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -294,11 +294,11 @@ if (OPENMP_FOUND)
     # flag by MSVC and breaks the build
     if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR
         ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
-      list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_C_FLAGS})
+      list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS})
     endif()
     if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR
         ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU"))
-      list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_CXX_FLAGS})
+      list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_C_FLAGS})
     endif()
     unset(CMAKE_REQUIRED_FLAGS)
     message(STATUS "Using OpenMP")

From ac85c68ccb437590c2e6669d892eef146ba87d65 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 4 Mar 2017 19:01:23 +0000
Subject: [PATCH 21/23] [CMake] Fix examples linking against libz3 when it is
 built as a static library on Linux.

---
 CMakeLists.txt                             |  6 ------
 contrib/cmake/examples/c++/CMakeLists.txt  |  6 ------
 contrib/cmake/examples/c/CMakeLists.txt    | 12 +++++-------
 contrib/cmake/examples/tptp/CMakeLists.txt |  6 ------
 contrib/cmake/src/CMakeLists.txt           |  8 +++++++-
 contrib/cmake/src/api/java/CMakeLists.txt  |  1 -
 6 files changed, 12 insertions(+), 27 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6281f951b..cf46e7012 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -147,7 +147,6 @@ set(Z3_COMPONENT_CXX_FLAGS "")
 set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "")
 set(Z3_DEPENDENT_LIBS "")
 set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "")
-set(Z3_DEPENDENT_EXTRA_C_LINK_FLAGS "")
 
 ################################################################################
 # Build type
@@ -296,10 +295,6 @@ if (OPENMP_FOUND)
         ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
       list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS})
     endif()
-    if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR
-        ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU"))
-      list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_C_FLAGS})
-    endif()
     unset(CMAKE_REQUIRED_FLAGS)
     message(STATUS "Using OpenMP")
 else()
@@ -386,7 +381,6 @@ message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}")
 message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}")
 message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}")
 message(STATUS "Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}")
-message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}")
 
 ################################################################################
 # Z3 installation locations
diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt
index b25bea533..c37aa475d 100644
--- a/contrib/cmake/examples/c++/CMakeLists.txt
+++ b/contrib/cmake/examples/c++/CMakeLists.txt
@@ -20,9 +20,3 @@ message(STATUS "Z3_DIR: ${Z3_DIR}")
 add_executable(cpp_example example.cpp)
 target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
-
-# FIXME: The Z3 package does not export information on the link flags
-# This is needed for when libz3 is built as a static library
-#if (NOT BUILD_LIBZ3_SHARED)
-#  z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
-#endif()
diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt
index d51503e29..5ca985845 100644
--- a/contrib/cmake/examples/c/CMakeLists.txt
+++ b/contrib/cmake/examples/c/CMakeLists.txt
@@ -1,7 +1,11 @@
 ################################################################################
 # Example C project
 ################################################################################
-project(Z3_C_EXAMPLE C)
+# NOTE: Even though this is a C project, libz3 uses C++. When using libz3
+# as a static library if we don't configure this project to also support
+# C++ we will use the C linker rather than the C++ linker and will not link
+# the C++ standard library in resulting in a link failure.
+project(Z3_C_EXAMPLE C CXX)
 cmake_minimum_required(VERSION 2.8.12)
 find_package(Z3
   REQUIRED
@@ -20,9 +24,3 @@ message(STATUS "Z3_DIR: ${Z3_DIR}")
 add_executable(c_example test_capi.c)
 target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
-
-# FIXME: The Z3 package does not export information on the link flags
-# This is needed for when libz3 is built as a static library
-#if (NOT BUILD_LIBZ3_SHARED)
-#  z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS})
-#endif()
diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt
index 6a2858a9b..6cd814487 100644
--- a/contrib/cmake/examples/tptp/CMakeLists.txt
+++ b/contrib/cmake/examples/tptp/CMakeLists.txt
@@ -20,9 +20,3 @@ message(STATUS "Z3_DIR: ${Z3_DIR}")
 add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp)
 target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES})
-
-# FIXME: The Z3 package does not export information on the link flags
-# This is needed for when libz3 is built as a static library
-#if (NOT BUILD_LIBZ3_SHARED)
-#  z3_append_linker_flag_list_to_target(z3_tptp5 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
-#endif()
diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt
index 548b59053..66e34790a 100644
--- a/contrib/cmake/src/CMakeLists.txt
+++ b/contrib/cmake/src/CMakeLists.txt
@@ -143,7 +143,13 @@ endif()
 # so that if those are also shared libraries they are referenced by `libz3.so`.
 target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
 
-z3_append_linker_flag_list_to_target(libz3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+# This is currently only for the OpenMP flags. It needs to be set
+# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`
+# because when building the `libz3` as a static library when the target is exported
+# the link dependencies need to be exported too.
+foreach (flag_name ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+  target_link_libraries(libz3 PRIVATE ${flag_name})
+endforeach()
 
 # Declare which header file are the public header files of libz3
 # these will automatically installed when the libz3 target is installed
diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt
index b34277266..dce2bc4ea 100644
--- a/contrib/cmake/src/api/java/CMakeLists.txt
+++ b/contrib/cmake/src/api/java/CMakeLists.txt
@@ -44,7 +44,6 @@ target_link_libraries(z3java PRIVATE libz3)
 # Z3's components to build ``Native.cpp`` lets do the same for now.
 target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
 target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
-z3_append_linker_flag_list_to_target(z3java ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
 target_include_directories(z3java PRIVATE
   "${CMAKE_SOURCE_DIR}/src/api"
   "${CMAKE_BINARY_DIR}/src/api"

From 28493622c25e033a2db48bb99a4fba7d12e2fb7e Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 13 Mar 2017 12:37:29 +0000
Subject: [PATCH 22/23] [CMake] On Windows when building the examples copy the
 Z3 library into the directory of the example executable so that it works "out
 of the box".

---
 contrib/cmake/examples/c++/CMakeLists.txt  | 16 ++++++++++++++++
 contrib/cmake/examples/c/CMakeLists.txt    | 16 ++++++++++++++++
 contrib/cmake/examples/tptp/CMakeLists.txt | 17 +++++++++++++++++
 3 files changed, 49 insertions(+)

diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt
index c37aa475d..d60604924 100644
--- a/contrib/cmake/examples/c++/CMakeLists.txt
+++ b/contrib/cmake/examples/c++/CMakeLists.txt
@@ -20,3 +20,19 @@ message(STATUS "Z3_DIR: ${Z3_DIR}")
 add_executable(cpp_example example.cpp)
 target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
+
+if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+  # On Windows we need to copy the Z3 libraries
+  # into the same directory as the executable
+  # so that they can be found.
+  foreach (z3_lib ${Z3_LIBRARIES})
+    message(STATUS "Adding copy rule for ${z3_lib}")
+    add_custom_command(TARGET cpp_example
+      POST_BUILD
+      COMMAND
+        ${CMAKE_COMMAND} -E copy_if_different
+        $<TARGET_FILE:${z3_lib}>
+        $<TARGET_FILE_DIR:cpp_example>
+    )
+  endforeach()
+endif()
diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt
index 5ca985845..dd8fa6328 100644
--- a/contrib/cmake/examples/c/CMakeLists.txt
+++ b/contrib/cmake/examples/c/CMakeLists.txt
@@ -24,3 +24,19 @@ message(STATUS "Z3_DIR: ${Z3_DIR}")
 add_executable(c_example test_capi.c)
 target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
+
+if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+  # On Windows we need to copy the Z3 libraries
+  # into the same directory as the executable
+  # so that they can be found.
+  foreach (z3_lib ${Z3_LIBRARIES})
+    message(STATUS "Adding copy rule for ${z3_lib}")
+    add_custom_command(TARGET c_example
+      POST_BUILD
+      COMMAND
+        ${CMAKE_COMMAND} -E copy_if_different
+        $<TARGET_FILE:${z3_lib}>
+        $<TARGET_FILE_DIR:c_example>
+    )
+  endforeach()
+endif()
diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt
index 6cd814487..8e8dfb8ea 100644
--- a/contrib/cmake/examples/tptp/CMakeLists.txt
+++ b/contrib/cmake/examples/tptp/CMakeLists.txt
@@ -20,3 +20,20 @@ message(STATUS "Z3_DIR: ${Z3_DIR}")
 add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp)
 target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES})
+
+if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+  # On Windows we need to copy the Z3 libraries
+  # into the same directory as the executable
+  # so that they can be found.
+  foreach (z3_lib ${Z3_LIBRARIES})
+    message(STATUS "Adding copy rule for ${z3_lib}")
+    add_custom_command(TARGET z3_tptp5
+      POST_BUILD
+      COMMAND
+        ${CMAKE_COMMAND} -E copy_if_different
+        $<TARGET_FILE:${z3_lib}>
+        $<TARGET_FILE_DIR:z3_tptp5>
+    )
+  endforeach()
+endif()
+

From 5c9d7538a03c0e18b1e99df863058e5218cf0022 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 13 Mar 2017 14:39:12 -0400
Subject: [PATCH 23/23] add alternate str.at semantics check in seq_rewriter

this rewrites to empty string if the index is negative or beyond the length of the string,
which is consistent with CVC4's semantics for this term
---
 src/ast/rewriter/seq_rewriter.cpp | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 26c3e23e4..adb70c30c 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -598,14 +598,25 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+/*
+ * (str.at s i), constants s/i, i < 0 or i >= |s| ==> (str.at s i) = ""
+ */
 br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
     zstring c;
     rational r;
-    if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
-        unsigned j = r.get_unsigned();
-        if (j < c.length()) {
-            result = m_util.str.mk_string(c.extract(j, 1));
+    if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) {
+        if (r.is_neg()) {
+            result = m_util.str.mk_string(symbol(""));
             return BR_DONE;
+        } else if (r.is_unsigned()) {
+            unsigned j = r.get_unsigned();
+            if (j < c.length()) {
+                result = m_util.str.mk_string(c.extract(j, 1));
+                return BR_DONE;
+            } else {
+                result = m_util.str.mk_string(symbol(""));
+                return BR_DONE;
+            }
         }
     }
     return BR_FAILED;