diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 94c92f390a53..fb82f3c69361 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -78,7 +78,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr) * Ideally all solvers answer the query and agree on what the answer is * (all say SAT or all say UNSAT). * - * The actual logic as as follows: + * The actual logic is as follows: * 1) If at least one solver answers the query, all the non-answer results are ignored. * Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR * because one buggy solver/integration shouldn't break the portfolio.