321   for (size_t pcol = 0, prow = 0; pcol < ncols && prow < nrows; ++pcol, ++prow)  in gaussElim()  local
327       for (size_t k = 0; k < pcol; ++k) { Assert(lhs[j][k] == 0); }  in gaussElim()
330       lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime);  in gaussElim()
334         while (lhs[j][pcol] == 0)  in gaussElim()
338             lhs[k][pcol] = lhs[k][pcol].euclidianDivideRemainder(prime);  in gaussElim()
339             if (lhs[k][pcol] != 0)  in gaussElim()
346           if (pcol >= ncols - 1) break;  in gaussElim()
347           if (lhs[j][pcol] == 0)  in gaussElim()
349             pcol += 1;  in gaussElim()
350             if (lhs[j][pcol] != 0)  in gaussElim()
351               lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime);  in gaussElim()
356       if (lhs[j][pcol] != 0)  in gaussElim()
359         if (lhs[j][pcol] != 1)  in gaussElim()
361           Integer inv = lhs[j][pcol].modInverse(prime);  in gaussElim()
366           for (size_t k = pcol; k < ncols; ++k)  in gaussElim()
378           for (size_t k = pcol; k < ncols; ++k)  in gaussElim()
389       Integer mul = lhs[j][pcol];  in gaussElim()
392         for (size_t k = pcol; k < ncols; ++k)  in gaussElim()
404     size_t pcol = i;  in gaussElim()  local
405     while (pcol < ncols && lhs[i][pcol] == 0) ++pcol;  in gaussElim()
406     if (pcol >= ncols)  in gaussElim()
422       if (j > pcol && lhs[i][j] != 0)  in gaussElim()
660       for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows;  in gaussElimRewriteForUrem()  local
661            ++pcol, ++prow)  in gaussElimRewriteForUrem()
663         Assert(lhs[prow][pcol] == 0 || lhs[prow][pcol] == 1);  in gaussElimRewriteForUrem()
664         while (pcol < nvars && lhs[prow][pcol] == 0) pcol += 1;  in gaussElimRewriteForUrem()
665         if (pcol >= nvars)  in gaussElimRewriteForUrem()
670         if (lhs[prow][pcol] == 0)  in gaussElimRewriteForUrem()
675         Assert(lhs[prow][pcol] == 1);  in gaussElimRewriteForUrem()
677         for (size_t i = pcol + 1; i < nvars; ++i)  in gaussElimRewriteForUrem()
690           res[vvars[pcol]] = nm->mkConst<BitVector>(  in gaussElimRewriteForUrem()
691               BitVector(bv::utils::getSize(vvars[pcol]), rhs[prow]));  in gaussElimRewriteForUrem()
703                                  bv::utils::getSize(vvars[pcol]), rhs[prow]),  in gaussElimRewriteForUrem()
707           res[vvars[pcol]] = nm->mkNode(kind::BITVECTOR_UREM, tmp, prime);  in gaussElimRewriteForUrem()