From eacef5f3f9af67521137bf955b092114c749dc49 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Nov 2020 19:45:35 -0800 Subject: [PATCH] deal with warnings over unused variables and procedures Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 2 ++ examples/tptp/tptp5.cpp | 7 ------- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index dfced2796..d49fc45b3 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1057,6 +1057,8 @@ void opt_translate_example() { o1.add(x + y <= 11); optimize::handle h1 = o1.maximize(x); optimize::handle h2 = o1.maximize(y); + (void)h1; + (void)h2; optimize o2(c2, o1); expr z = c2.int_const("z"); expr x2 = c2.int_const("x"); diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 7323cad8e..fac922db8 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -2196,13 +2196,6 @@ static bool is_smt2_file(char const* filename) { return (len > 4 && !strcmp(filename + len - 5,".smt2")); } -static void check_error(z3::context& ctx) { - Z3_error_code e = Z3_get_error_code(ctx); - if (e != Z3_OK) { - std::cout << Z3_get_error_msg(ctx, e) << "\n"; - exit(1); - } -} static void display_tptp(std::ostream& out) { // run SMT2 parser, pretty print TFA format.