lfsc_checker: fix some warnings reported by _both_ gcc and clang

3 files changed, 6 insertions, 6 deletions

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{