Fix compiler warnings. (#2555)

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 372f8eb04245f7c5b7ce5e99001951211184ddfb..a4b0248e0e3c52077adcf074735757315c74d7fe 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -357,8 +357,11 @@ void Solver::cancelUntil(int level) {
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
             if (marker[x] == 2) marker[x] = 1;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
-                polarity[x] = sign(trail[c]);
+            if (phase_saving > 1
+                || ((phase_saving == 1) && c > trail_lim.last()))
+            {
+              polarity[x] = sign(trail[c]);
+            }
             insertVarOrder(x); }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
@@ -1080,16 +1083,19 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               cancelUntil(assumptions.size()); 
               throw e; 
             }
-            
-            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts ||
-                !isWithinBudget) {
-                // Reached bound on number of conflicts:
-                Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
-                progress_estimate = progressEstimate();
-                cancelUntil(assumptions.size());
-                return l_Undef;
+
+            if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
+                 && conflictC >= nof_conflicts)
+                || !isWithinBudget)
+            {
+              // Reached bound on number of conflicts:
+              Debug("bvminisat::search")
+                  << OUTPUT_TAG << " restarting " << std::endl;
+              progress_estimate = progressEstimate();
+              cancelUntil(assumptions.size());
+              return l_Undef;
             }
- 
+
             // Simplify the set of problem clauses:
             if (decisionLevel() == 0 && !simplify()) {
                 Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;

diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 2fa8d472da36593a871b5b8a30c8a3ebdd2f7a8f..698d2a77643f5e7eea2323ca084aed6e80dfdae7 100644 (file)
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -255,17 +255,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     const Clause& ps  =  ps_smallest ? _qs : _ps;
     const Clause& qs  =  ps_smallest ? _ps : _qs;
 
-    for (int i = 0; i < qs.size(); i++){
-        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;
-            out_clause.push(qs[i]);
+    for (int i = 0; i < qs.size(); i++)
+    {
+      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;
+          }
         }
-        next:;
+        out_clause.push(qs[i]);
+      }
+    next:;
     }
 
     for (int i = 0; i < ps.size(); i++)
@@ -289,17 +295,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
 
     size = ps.size()-1;
 
-    for (int i = 0; i < qs.size(); i++){
-        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++;
+    for (int i = 0; i < qs.size(); i++)
+    {
+      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;
+          }
         }
-        next:;
+        size++;
+      }
+    next:;
     }
 
     return true;

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index dbe417dbc8c090484cea4e16446742db42c55867..c8a2e16c236766def4bb4b14031998b494b26a6b 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1349,15 +1349,16 @@ lbool Solver::search(int nof_conflicts)
               check_type = CHECK_WITH_THEORY;
             }
 
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts ||
-                !withinBudget(options::satConflictStep())) {
-                // Reached bound on number of conflicts:
-                progress_estimate = progressEstimate();
-                cancelUntil(0);
-                // [mdeters] notify theory engine of restarts for deferred
-                // theory processing
-                proxy->notifyRestart();
-                return l_Undef;
+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+                || !withinBudget(options::satConflictStep()))
+            {
+              // Reached bound on number of conflicts:
+              progress_estimate = progressEstimate();
+              cancelUntil(0);
+              // [mdeters] notify theory engine of restarts for deferred
+              // theory processing
+              proxy->notifyRestart();
+              return l_Undef;
             }
 
             // Simplify the set of problem clauses:

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 96fea214728dd94ac4ab7a10d6566b8481b193a9..a101a0c2d7307d968c15776f62aa570cdd2029f5 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -256,17 +256,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     const Clause& ps  =  ps_smallest ? _qs : _ps;
     const Clause& qs  =  ps_smallest ? _ps : _qs;
 
-    for (int i = 0; i < qs.size(); i++){
-        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;
-            out_clause.push(qs[i]);
+    for (int i = 0; i < qs.size(); i++)
+    {
+      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;
+          }
         }
-        next:;
+        out_clause.push(qs[i]);
+      }
+    next:;
     }
 
     for (int i = 0; i < ps.size(); i++)
@@ -290,17 +296,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
 
     size = ps.size()-1;
 
-    for (int i = 0; i < qs.size(); i++){
-        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++;
+    for (int i = 0; i < qs.size(); i++)
+    {
+      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;
+          }
         }
-        next:;
+        size++;
+      }
+    next:;
     }
 
     return true;

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f5c3eac0830245e061435814e7cd8b70c58da3f6..ff71f64323ea0a2e0089c002b00695b82209b919 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -711,9 +711,8 @@ bool Constraint::wellFormedFarkasProof() const {
   }
   Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
   // 0 = lhs <= rhs < 0
-  return
-    (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) &&
-    rhs.sgn() < 0;
+  return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
+         && rhs.sgn() < 0;
 
 #else  /* IS_PROOFS_BUILD */
   return true;