From 6ea45b4d65f36f0299007dc172477ec6e8478727 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Oct 2016 14:23:55 +0100 Subject: [PATCH 1/3] fix for Python API installation --- scripts/mk_util.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 309b08297..a86499149 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1505,6 +1505,9 @@ class PythonInstallComponent(Component): os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'), in_prefix=self.in_prefix_install ) + MakeRuleCmd.remove_installed_files(out, + os.path.join(self.pythonPkgDir, 'z3', 'lib', + self.libz3Component.dll_file())) def mk_makefile(self, out): return From 8c5c564d6ce49c1bfc80175a457712ee30691af7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Oct 2016 14:31:29 +0100 Subject: [PATCH 2/3] fixed initialization order warning in pb2bv_rewriter --- src/ast/rewriter/pb2bv_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 4f538867e..8871c3dd8 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -224,12 +224,12 @@ struct pb2bv_rewriter::imp { public: card2bv_rewriter(imp& i, ast_manager& m): + m_sort(*this), m(m), m_imp(i), au(m), pb(m), bv(m), - m_sort(*this), m_trail(m), m_args(m) {} From c7fddf80c2a84d5235ddf4325cd2194de66d0083 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Oct 2016 14:34:00 +0100 Subject: [PATCH 3/3] fixed unhandled case warning in test/qe_arith.cpp --- src/test/qe_arith.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 79495e24f..a73f7ed38 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -375,6 +375,9 @@ static void add_random_ineq( case opt::t_le: fml = a.mk_le(t1, t2); break; + case opt::t_mod: + NOT_IMPLEMENTED_YET(); + break; } fmls.push_back(fml); mbo.add_constraint(vars, rational(coeff), rel);