From 2818e977b6b8ddec11a0bf6b79423dbfc241e964 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 29 Oct 2015 13:20:56 +0000
Subject: [PATCH] Fixed unused variable warnings in examples.

---
 examples/c++/example.cpp  |  3 +--
 examples/interp/iz3.cpp   |  2 +-
 examples/maxsat/maxsat.c  |  2 +-
 examples/tptp/tptp5.cpp   | 10 +++++-----
 examples/tptp/tptp5.tab.c |  2 +-
 5 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index af972a36b..c9f6aaa40 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -294,7 +294,7 @@ void error_example() {
 
     // Error using the C API can be detected using Z3_get_error_code.
     // 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) {
         std::cout << "last call failed.\n";
     }
@@ -999,7 +999,6 @@ void opt_example() {
     opt.add(x + y <= 11);
     optimize::handle h1 = opt.maximize(x);
     optimize::handle h2 = opt.maximize(y);
-    check_result r = sat;
     while (true) {
         if (sat == opt.check()) {
             std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n";
diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp
index 380658b09..21ea518a6 100755
--- a/examples/interp/iz3.cpp
+++ b/examples/interp/iz3.cpp
@@ -42,7 +42,7 @@ int main(int argc, const char **argv) {
 
   Z3_config cfg = Z3_mk_config();
   // Z3_interpolation_options options = Z3_mk_interpolation_options();
-  Z3_params options = 0;
+  // Z3_params options = 0;
 
   /* Parse the command line */
   int argn = 1;
diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c
index f04c25e2c..8f747cb98 100644
--- a/examples/maxsat/maxsat.c
+++ b/examples/maxsat/maxsat.c
@@ -598,7 +598,7 @@ int smtlib_maxsat(char * file_name, int approach)
     Z3_context ctx;
     unsigned num_hard_cnstrs, num_soft_cnstrs;
     Z3_ast * hard_cnstrs, * soft_cnstrs;
-    unsigned result;
+    unsigned result = 0;
     ctx = mk_context();
     Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
     hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 0ed92801d..6c355a4a9 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -261,7 +261,7 @@ class env {
         parse(inc_name.c_str(), fmls);
         while (name_list) {
             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);            
         }
     }
@@ -614,7 +614,7 @@ class env {
 
     void mk_mapping_sort(TreeNode* t, z3::sort_vector& domain, z3::sort& s) {
         char const* name = t->symbol();
-        char const* id = 0;
+        //char const* id = 0;
         if (!strcmp(name,"tff_top_level_type")) {
             mk_mapping_sort(t->child(0), domain, s);
         }
@@ -1832,7 +1832,7 @@ public:
     }
 
     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);
         std::vector<z3::sort> vars;
         get_free_vars(result, vars);
@@ -2119,7 +2119,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
     int i = 1;
     while (i < argc) {
         char* arg = argv[i];
-        char * eq = 0;
+        //char * eq = 0;
         char * opt_arg = 0;
         if (arg[0] == '-' || arg[0] == '/') {
             ++arg;
@@ -2467,7 +2467,7 @@ static void prove_tptp() {
 
 int main(int argc, char** argv) {
 
-    std::ostream* out = &std::cout;
+    //std::ostream* out = &std::cout;
     g_start_time = static_cast<double>(clock());
     signal(SIGINT, on_ctrl_c);
 
diff --git a/examples/tptp/tptp5.tab.c b/examples/tptp/tptp5.tab.c
index c97225f4c..086f6e622 100644
--- a/examples/tptp/tptp5.tab.c
+++ b/examples/tptp/tptp5.tab.c
@@ -139,7 +139,7 @@ pTree pToken(char* token, int symbolIndex) {
 
     //char pTokenBuf[8240];
     pTree ss;
-    char* symbol = tptp_lval[symbolIndex];
+    //char* symbol = tptp_lval[symbolIndex];
     char* safeSym = 0;
 
     //strncpy(pTokenBuf, token, 39);