From 8c191781e70332cb399a07960567eb1bd841368f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Jun 2016 18:52:30 +0100 Subject: [PATCH 1/3] Fixed warning message --- examples/c++/example.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 5635e6d12..2753e1475 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -23,7 +23,7 @@ void demorgan() { expr x = c.bool_const("x"); expr y = c.bool_const("y"); - expr conjecture = !(x && y) == (!x || !y); + expr conjecture = (!(x && y)) == (!x || !y); solver s(c); // adding the negation of the conjecture as a constraint. From 89b1d7d8da9ff4dc10f62fc0e764f6f23f3a055c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Jun 2016 18:52:40 +0100 Subject: [PATCH 2/3] Fixed test case --- src/test/qe_arith.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index f14ccf3e2..f9cd9aa23 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -382,8 +382,7 @@ static void add_random_ineq( static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) { qe::arith_project_plugin plugin(m); - model mdl(m); - expr_ref bound(m); + model mdl(m); arith_util a(m); for (unsigned i = 0; i < num_vars; ++i) { app_ref var(m); @@ -391,7 +390,8 @@ static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned nu rational val = mbo.get_value(i); mdl.register_decl(var->get_decl(), a.mk_numeral(val, false)); } - opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, bound); + expr_ref ge(m), gt(m); + opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, ge, gt); opt::inf_eps value2 = mbo.maximize(); std::cout << "optimal: " << value1 << " " << value2 << "\n"; mbo.display(std::cout); From fad1dffbf07abef3abd7561eb25b16e04fc6f918 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Jun 2016 19:03:42 +0100 Subject: [PATCH 3/3] Added PATH info to successful build message --- scripts/mk_util.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a73a0e59c..b02e6e2b7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2472,7 +2472,8 @@ def mk_makefile(): out.write(' %s' % c.name) out.write('\n\t@echo Z3 was successfully built.\n') out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR) - out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR) + pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH" + out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH and %s environment variables.\"\n" % (BUILD_DIR, pathvar)) if not IS_WINDOWS: out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n") out.write('\t@echo " sudo make install"\n\n')