diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 3e4456676..bad51528f 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -65,7 +65,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', @@ -93,6 +93,7 @@ def parse_options(): DOTNET_ENABLED = False elif opt == '--dotnetcore': DOTNET_CORE_ENABLED = True + DOTNET_ENABLED = False elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': @@ -195,10 +196,8 @@ def mk_dist_dir(): build_path = BUILD_DIR dist_path = os.path.join(DIST_DIR, get_z3_name()) mk_dir(dist_path) - if DOTNET_CORE_ENABLED: - mk_util.DOTNET_CORE_ENABLED = True - else: - mk_util.DOTNET_ENABLED = DOTNET_ENABLED + mk_util.DOTNET_CORE_ENABLED = DOTNET_CORE_ENABLED + mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index e61a7714c..bd3cad18a 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -104,6 +104,7 @@ def parse_options(): DOTNET_ENABLED = False elif opt == '--dotnetcore': DOTNET_CORE_ENABLED = True + DOTNET_ENABLED = False elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index b4c3eee49..df1f1461f 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -308,7 +308,7 @@ extern "C" { \param c - context. \param f - fixedpoint context. - \param s - string containing SMT2 specification. + \param s - path to file containing SMT2 specification. def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING))) */ diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index f15d8ff9c..b1c01a386 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -252,7 +252,7 @@ extern "C" { \param c - context. \param o - optimize context. - \param s - string containing SMT2 specification. + \param s - path to file containing SMT2 specification. def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING))) */ diff --git a/src/solver/solver.h b/src/solver/solver.h index 5329161cd..7437a5a08 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -146,6 +146,8 @@ public: lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); } + lbool check_sat() { return check_sat(0, nullptr); } + /** \brief Check satisfiability modulo a cube and a clause. diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 4ba3b3b5c..9ab3123a2 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -520,7 +520,7 @@ public: try { symbol m, p; normalize(name, m, p); - std::cout << name << " " << m << " " << p << "\n"; + out << name << " " << m << " " << p << "\n"; param_descrs * d; if (m == symbol::null) { d = &get_param_descrs();