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

Fixed unused variable warnings in examples.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-29 13:20:56 +00:00
parent 5cb4b1d188
commit 2818e977b6
5 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -294,7 +294,7 @@ void error_example() {
// Error using the C API can be detected using Z3_get_error_code. // Error using the C API can be detected using Z3_get_error_code.
// The next call fails because x is a constant. // The next call fails because x is a constant.
Z3_ast arg = Z3_get_app_arg(c, x, 0); //Z3_ast arg = Z3_get_app_arg(c, x, 0);
if (Z3_get_error_code(c) != Z3_OK) { if (Z3_get_error_code(c) != Z3_OK) {
std::cout << "last call failed.\n"; std::cout << "last call failed.\n";
} }
@ -999,7 +999,6 @@ void opt_example() {
opt.add(x + y <= 11); opt.add(x + y <= 11);
optimize::handle h1 = opt.maximize(x); optimize::handle h1 = opt.maximize(x);
optimize::handle h2 = opt.maximize(y); optimize::handle h2 = opt.maximize(y);
check_result r = sat;
while (true) { while (true) {
if (sat == opt.check()) { if (sat == opt.check()) {
std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n"; std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n";

2
examples/interp/iz3.cpp
View file

@ -42,7 +42,7 @@ int main(int argc, const char **argv) {
Z3_config cfg = Z3_mk_config(); Z3_config cfg = Z3_mk_config();
// Z3_interpolation_options options = Z3_mk_interpolation_options(); // Z3_interpolation_options options = Z3_mk_interpolation_options();
Z3_params options = 0; // Z3_params options = 0;
/* Parse the command line */ /* Parse the command line */
int argn = 1; int argn = 1;

2
examples/maxsat/maxsat.c
View file

@ -598,7 +598,7 @@ int smtlib_maxsat(char * file_name, int approach)
Z3_context ctx; Z3_context ctx;
unsigned num_hard_cnstrs, num_soft_cnstrs; unsigned num_hard_cnstrs, num_soft_cnstrs;
Z3_ast * hard_cnstrs, * soft_cnstrs; Z3_ast * hard_cnstrs, * soft_cnstrs;
unsigned result; unsigned result = 0;
ctx = mk_context(); ctx = mk_context();
Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);

10
examples/tptp/tptp5.cpp
View file

@ -261,7 +261,7 @@ class env {
parse(inc_name.c_str(), fmls); parse(inc_name.c_str(), fmls);
while (name_list) { while (name_list) {
return mk_error(name_list, "name list (not handled)"); return mk_error(name_list, "name list (not handled)");
char const* name = name_list->child(0)->symbol(); //char const* name = name_list->child(0)->symbol();
name_list = name_list->child(2); name_list = name_list->child(2);
} }
} }
@ -614,7 +614,7 @@ class env {
void mk_mapping_sort(TreeNode* t, z3::sort_vector& domain, z3::sort& s) { void mk_mapping_sort(TreeNode* t, z3::sort_vector& domain, z3::sort& s) {
char const* name = t->symbol(); char const* name = t->symbol();
char const* id = 0; //char const* id = 0;
if (!strcmp(name,"tff_top_level_type")) { if (!strcmp(name,"tff_top_level_type")) {
mk_mapping_sort(t->child(0), domain, s); mk_mapping_sort(t->child(0), domain, s);
} }
@ -1832,7 +1832,7 @@ public:
} }
z3::expr get_proof_formula(z3::expr proof) { z3::expr get_proof_formula(z3::expr proof) {
unsigned na = proof.num_args(); // unsigned na = proof.num_args();
z3::expr result = proof.arg(proof.num_args()-1); z3::expr result = proof.arg(proof.num_args()-1);
std::vector<z3::sort> vars; std::vector<z3::sort> vars;
get_free_vars(result, vars); get_free_vars(result, vars);
@ -2119,7 +2119,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
int i = 1; int i = 1;
while (i < argc) { while (i < argc) {
char* arg = argv[i]; char* arg = argv[i];
char * eq = 0; //char * eq = 0;
char * opt_arg = 0; char * opt_arg = 0;
if (arg[0] == '-' || arg[0] == '/') { if (arg[0] == '-' || arg[0] == '/') {
++arg; ++arg;
@ -2467,7 +2467,7 @@ static void prove_tptp() {
int main(int argc, char** argv) { int main(int argc, char** argv) {
std::ostream* out = &std::cout; //std::ostream* out = &std::cout;
g_start_time = static_cast<double>(clock()); g_start_time = static_cast<double>(clock());
signal(SIGINT, on_ctrl_c); signal(SIGINT, on_ctrl_c);

2
examples/tptp/tptp5.tab.c
View file

@ -139,7 +139,7 @@ pTree pToken(char* token, int symbolIndex) {
//char pTokenBuf[8240]; //char pTokenBuf[8240];
pTree ss; pTree ss;
char* symbol = tptp_lval[symbolIndex]; //char* symbol = tptp_lval[symbolIndex];
char* safeSym = 0; char* safeSym = 0;
//strncpy(pTokenBuf, token, 39); //strncpy(pTokenBuf, token, 39);