From 5bd9edb52d9f08e83f4410d7cfaa314230d41229 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 21 Oct 2014 20:18:14 -0700 Subject: Compiler problems. --- src/sat/bsat2/SimpSolver.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/sat/bsat2') diff --git a/src/sat/bsat2/SimpSolver.cpp b/src/sat/bsat2/SimpSolver.cpp index 20858543..5a7a006c 100644 --- a/src/sat/bsat2/SimpSolver.cpp +++ b/src/sat/bsat2/SimpSolver.cpp @@ -222,10 +222,11 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& ou bool ps_smallest = _ps.size() < _qs.size(); const Clause& ps = ps_smallest ? _qs : _ps; const Clause& qs = ps_smallest ? _ps : _qs; + int i, j; - for (int i = 0; i < qs.size(); i++){ + for (i = 0; i < qs.size(); i++){ if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) + for (j = 0; j < ps.size(); j++) if (var(ps[j]) == var(qs[i])) if (ps[j] == ~qs[i]) return false; @@ -472,12 +473,13 @@ bool SimpSolver::eliminateVar(Var v) assert(!frozen[v]); assert(!isEliminated(v)); assert(value(v) == l_Undef); + int i; // Split the occurrences into positive and negative: // const vec& cls = occurs.lookup(v); vec pos, neg; - for (int i = 0; i < cls.size(); i++) + for (i = 0; i < cls.size(); i++) (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no @@ -683,7 +685,8 @@ void SimpSolver::relocAll(ClauseAllocator& to) // All occurs lists: // - for (int i = 0; i < nVars(); i++){ + int i; + for (i = 0; i < nVars(); i++){ vec& cs = occurs[i]; for (int j = 0; j < cs.size(); j++) ca.reloc(cs[j], to); -- cgit v1.2.3