From d87b1cd543efaf724255da2ab74ca959bc75f920 Mon Sep 17 00:00:00 2001
From: Allen Ho <b07901135@ntu.edu.tw>
Date: Mon, 4 Mar 2024 10:16:14 +0800
Subject: [PATCH] fixed some warnings in bsat2

---
 src/sat/bsat2/Options.cpp    | 2 ++
 src/sat/bsat2/Options.h      | 2 +-
 src/sat/bsat2/SimpSolver.cpp | 4 ++++
 src/sat/bsat2/Solver.cpp     | 4 ++--
 src/sat/bsat2/Vec.h          | 1 -
 5 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/sat/bsat2/Options.cpp b/src/sat/bsat2/Options.cpp
index f14059f67..a0a3817d8 100644
--- a/src/sat/bsat2/Options.cpp
+++ b/src/sat/bsat2/Options.cpp
@@ -45,10 +45,12 @@ int Minisat::parseOptions(int& argc, char** argv, bool strict)
             }
 
             if (!parsed_ok)
+            {
                 if (strict && match(argv[i], "-"))
                     { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } //  exit(0);
                 else
                     argv[j++] = argv[i];
+            }
         }
     }
 
diff --git a/src/sat/bsat2/Options.h b/src/sat/bsat2/Options.h
index 137b5a45e..00d46d352 100644
--- a/src/sat/bsat2/Options.h
+++ b/src/sat/bsat2/Options.h
@@ -62,7 +62,7 @@ class Option
     struct OptionLt {
         bool operator()(const Option* x, const Option* y) {
             int test1 = strcmp(x->category, y->category);
-            return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+            return test1 < 0 || ( test1 == 0 && strcmp(x->type_name, y->type_name) < 0 );
         }
     };
 
diff --git a/src/sat/bsat2/SimpSolver.cpp b/src/sat/bsat2/SimpSolver.cpp
index 59952d154..c07ec5b97 100644
--- a/src/sat/bsat2/SimpSolver.cpp
+++ b/src/sat/bsat2/SimpSolver.cpp
@@ -230,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
         if (var(qs[i]) != v){
             for (j = 0; j < ps.size(); j++)
                 if (var(ps[j]) == var(qs[i]))
+                {
                     if (ps[j] == ~qs[i])
                         return false;
                     else
                         goto next;
+                }
             out_clause.push(qs[i]);
         }
         next:;
@@ -264,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
         if (var(__qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
                 if (var(__ps[j]) == var(__qs[i]))
+                {
                     if (__ps[j] == ~__qs[i])
                         return false;
                     else
                         goto next;
+                }
             size++;
         }
         next:;
diff --git a/src/sat/bsat2/Solver.cpp b/src/sat/bsat2/Solver.cpp
index 1c45a4538..602692a8b 100644
--- a/src/sat/bsat2/Solver.cpp
+++ b/src/sat/bsat2/Solver.cpp
@@ -211,7 +211,7 @@ void Solver::cancelUntil(int level) {
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+            if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
                 polarity[x] = sign(trail[c]);
             insertVarOrder(x); }
         qhead = trail_lim[level];
@@ -659,7 +659,7 @@ lbool Solver::search(int nof_conflicts)
 
         }else{
             // NO CONFLICT
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            if ( (nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
                 cancelUntil(0);
diff --git a/src/sat/bsat2/Vec.h b/src/sat/bsat2/Vec.h
index aade19f13..f5f5499ea 100644
--- a/src/sat/bsat2/Vec.h
+++ b/src/sat/bsat2/Vec.h
@@ -93,7 +93,6 @@ public:
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };
 
-
 template<class T>
 void vec<T>::capacity(int min_cap) {
     if (cap >= min_cap) return;