From be8b05e6bfed1cbf14c6caaae01085ced1984238 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Mon, 28 Nov 2022 18:59:51 +0100
Subject: [PATCH] Make isoltest not check SMTChecker counterexamples by
 default.

---
 test/libsolidity/SMTCheckerTest.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
index 1d6109176..e3e52491d 100644
--- a/test/libsolidity/SMTCheckerTest.cpp
+++ b/test/libsolidity/SMTCheckerTest.cpp
@@ -63,7 +63,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none())
 		m_shouldRun = false;
 
-	auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "no");
+	auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "yes");
 	if (ignoreCex == "no")
 		m_ignoreCex = false;
 	else if (ignoreCex == "yes")
@@ -129,5 +129,8 @@ void SMTCheckerTest::filterObtainedErrors()
 	};
 
 	if (m_ignoreCex)
+	{
+		removeCex(m_expectations);
 		removeCex(m_errorList);
+	}
 }