From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 16 May 2014 22:38:22 +0000 (-0400)
Subject: lfsc_checker: fix some warnings reported by _both_ gcc and clang
X-Git-Tag: cvc5-1.0.0~6901^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5820d0cd1ccabd04613a77d5fcb844a5b0463ea4;p=cvc5.git

lfsc_checker: fix some warnings reported by _both_ gcc and clang
---

diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
index 34c6c133b..ee143a710 100644
--- a/proofs/lfsc_checker/code.cpp
+++ b/proofs/lfsc_checker/code.cpp
@@ -1141,7 +1141,7 @@ Expr *run_code(Expr *_e) {
     if (!r1)
       return NULL;
 
-    bool cond;
+    bool cond = true;
     if( r1->getclass() == INT_EXPR ){
       if( e->getop() == IFNEG )
         cond = mpz_sgn( ((IntExpr *)r1)->n )<0;
@@ -1244,7 +1244,7 @@ Expr *run_code(Expr *_e) {
     vector<Expr *> args;
     Expr *hd = scrut->collect_args(args);
     Expr **cases = &e->kids[1];
-    CExpr *c;
+    // CExpr *c;
     Expr *c_or_default;
     while ((c_or_default = *cases++)) {
 
@@ -1382,4 +1382,4 @@ int read_index()
     index = atoi( v.c_str() );
   }
   return index;
-}
\ No newline at end of file
+}
diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp
index bf068c248..34cb00cc4 100644
--- a/proofs/lfsc_checker/print_smt2.cpp
+++ b/proofs/lfsc_checker/print_smt2.cpp
@@ -54,7 +54,7 @@ void print_smt2( Expr* p, std::ostream& s, short mode )
             s << " ";
             for( int a=0; a<(int)args.size(); a++ ){
               print_smt2( args[a], s, newMode );
-              if( a!=args.size()-1 )
+              if( a!=(int)args.size()-1 )
                 s << " ";
             }
             s << ")";
diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp
index cff762a08..22f26ec88 100644
--- a/proofs/lfsc_checker/scccode.cpp
+++ b/proofs/lfsc_checker/scccode.cpp
@@ -99,11 +99,11 @@ Expr* f_litpol( Expr* l ){
    e3 = e_neg;
    e3->inc();
    if( e1==e2 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
       e0 = e_tt;
       e0->inc();
    }else if( e1==e3 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
       e0 = e_ff;
       e0->inc();
    }else{