mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

deal with warnings over unused variables and procedures

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-29 19:45:35 -08:00
parent 64af8981ba
commit eacef5f3f9
2 changed files with 2 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
examples/c++/example.cpp
View file

@ -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");

7
examples/tptp/tptp5.cpp
View file

@ -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.