From eaa01d355abd0e69bfec9d5b61f1330f42ff1fe8 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Mon, 5 Apr 2010 04:01:35 +0000
Subject: STP: Remove stray semi-colons.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100391 91177308-0d34-0410-b5e6-96231b3b80d8
---
 stp/sat/Global.h       | 6 +++---
 stp/sat/Heap.h         | 2 +-
 stp/sat/Simplifier.cpp | 2 +-
 stp/sat/Solver.cpp     | 4 ++--
 stp/sat/Solver.h       | 2 +-
 stp/sat/SolverTypes.h  | 2 +-
 stp/sat/Sort.h         | 2 +-
 stp/sat/VarOrder.h     | 2 +-
 8 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'stp/sat')

diff --git a/stp/sat/Global.h b/stp/sat/Global.h
index a428975c..deaf8c24 100644
--- a/stp/sat/Global.h
+++ b/stp/sat/Global.h
@@ -194,7 +194,7 @@ template<class V, class T>
 void remove(V& ts, const T& t)
 {
     int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
+    for (; j < ts.size() && ts[j] != t; j++) ;
     assert(j < ts.size());
     for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
     ts.pop();
@@ -205,7 +205,7 @@ template<class V, class T>
 bool find(V& ts, const T& t)
 {
     int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
+    for (; j < ts.size() && ts[j] != t; j++) ;
     return j < ts.size();
 }
 
@@ -251,5 +251,5 @@ template <class T> static inline bool operator >= (const T& x, const T& y) { ret
 
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/Heap.h b/stp/sat/Heap.h
index acfa1c1e..e3a82dd0 100644
--- a/stp/sat/Heap.h
+++ b/stp/sat/Heap.h
@@ -147,5 +147,5 @@ class Heap {
 };
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/Simplifier.cpp b/stp/sat/Simplifier.cpp
index 1c192e20..2e709066 100644
--- a/stp/sat/Simplifier.cpp
+++ b/stp/sat/Simplifier.cpp
@@ -539,4 +539,4 @@ bool Solver::eliminate()
 
     return true;
 }
-};
+}
diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp
index 0fcb6149..13a9ae08 100644
--- a/stp/sat/Solver.cpp
+++ b/stp/sat/Solver.cpp
@@ -316,7 +316,7 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
         }
 
         // Select next clause to look at:
-        while (!seen[var(trail[index--])]);
+        while (!seen[var(trail[index--])]) ;
         p     = trail[index+1];
         confl = reason[var(p)];
         seen[var(p)] = 0;
@@ -808,4 +808,4 @@ bool Solver::solve(const vec<Lit>& assumps)
     cancelUntil(0);
     return status == l_True;
 }
-};//end of MINISAT namespace
+} //end of MINISAT namespace
diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h
index 829194cc..8826fac7 100644
--- a/stp/sat/Solver.h
+++ b/stp/sat/Solver.h
@@ -355,5 +355,5 @@ static inline int64 memUsed(void) {
 #endif
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/SolverTypes.h b/stp/sat/SolverTypes.h
index 90e7a9bd..29c3b95d 100644
--- a/stp/sat/SolverTypes.h
+++ b/stp/sat/SolverTypes.h
@@ -124,5 +124,5 @@ class TrailPos {
     bool operator <   (TrailPos other) const { return tp <  other.tp; }
 };
 
-};
+}
 #endif
diff --git a/stp/sat/Sort.h b/stp/sat/Sort.h
index a7011edb..9def2990 100644
--- a/stp/sat/Sort.h
+++ b/stp/sat/Sort.h
@@ -129,5 +129,5 @@ template <class T> void sortUnique(vec<T>& v) {
 
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/VarOrder.h b/stp/sat/VarOrder.h
index 6ad1bfb1..6d2a40f0 100644
--- a/stp/sat/VarOrder.h
+++ b/stp/sat/VarOrder.h
@@ -142,5 +142,5 @@ namespace MINISAT {
   
   
   //=================================================================================================
-};
+}
 #endif
-- 
cgit 1.4.1