From 649c8ee32826476600f67e2f879859563c92dc00 Mon Sep 17 00:00:00 2001 From: Maximilian Hubert <64627729+gap-editor@users.noreply.github.com> Date: Sat, 26 Apr 2025 17:40:13 +0200 Subject: [PATCH 1/2] Update SMTPortfolio.cpp --- libsmtutil/SMTPortfolio.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 94c92f390a53..e6f6e9913a59 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 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. From 76e80168f10e560f159309edf3448f48fb80dc0e Mon Sep 17 00:00:00 2001 From: Maximilian Hubert <64627729+gap-editor@users.noreply.github.com> Date: Mon, 28 Apr 2025 11:27:07 +0200 Subject: [PATCH 2/2] Update SMTPortfolio.cpp --- libsmtutil/SMTPortfolio.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index e6f6e9913a59..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 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.