diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 67625556b..109c8dbe5 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -617,6 +617,9 @@ void SMTChecker::checkCondition(
 	case smt::CheckResult::UNKNOWN:
 		m_errorReporter.warning(_location, _description + " might happen here." + loopComment);
 		break;
+	case smt::CheckResult::CONFLICTING:
+		m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
+		break;
 	case smt::CheckResult::ERROR:
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
 		break;
@@ -644,6 +647,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 
 	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
 		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
+	else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
+		m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
 	else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
 	{
 		// everything fine.
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 257957389..64806097e 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -92,7 +92,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr)
  * This comment explains how this result is decided.
  *
  * When a solver is queried, there are four possible answers:
- *   SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, ERROR
+ *   SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR
  * We say that a solver _answered_ the query if it returns either:
  *   SAT or UNSAT
  * A solver did not answer the query if it returns either:
@@ -107,7 +107,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr)
  *   because one buggy solver/integration shouldn't break the portfolio.
  *
  * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy
- * and the result is conflicting and we abort.
+ * and the result is CONFLICTING.
  *   In the future if we have more than 2 solvers enabled we could go with the majority.
  *
  * 3) If NO solver answers the query:
@@ -135,7 +135,8 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
 			}
 			else if (lastResult != result)
 			{
-				solAssert(false, "At least two SMT solvers gave opposing results.");
+				lastResult = CheckResult::CONFLICTING;
+				break;
 			}
 		}
 		else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR)
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index f8a2bebba..8bbd04173 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -39,7 +39,7 @@ namespace smt
 
 enum class CheckResult
 {
-	SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
+	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
 enum class Sort