diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:54:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:54:12 -0700 |
| commit | 8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d (patch) | |
| tree | 42d8239ad5b56e40640730e23889866870737f1c /src/sat/glucose/SimpSolver.cpp | |
| parent | 7ce7e9ec310db430078b7cbec538ea2a29b6d539 (diff) | |
| download | abc-8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d.tar.gz abc-8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d.tar.bz2 abc-8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d.zip | |
Compiler warnings.
Diffstat (limited to 'src/sat/glucose/SimpSolver.cpp')
| -rw-r--r-- | src/sat/glucose/SimpSolver.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index 1c3ee67b..566472fe 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/src/sat/glucose/SimpSolver.cpp @@ -241,15 +241,16 @@ 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; - int i; + int i, j; for (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])) + 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:; @@ -279,11 +280,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& 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 (var(__ps[j]) == var(__qs[i])) { if (__ps[j] == ~__qs[i]) return false; else goto next; + } size++; } next:; |