diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 77f7702f2..7ffa04709 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -972,6 +972,8 @@ void substitute_example() { std::cout << new_f << std::endl; } + + int main() { try { demorgan(); std::cout << "\n"; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9941e5082..b4e90f4f4 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1505,7 +1505,7 @@ namespace z3 { assert(e.is_bool()); return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0)); } - handle maximzie(expr const& e) { + handle maximize(expr const& e) { return handle(Z3_optimize_maximize(ctx(), m_opt, e)); } handle minimize(expr const& e) {