From 8b31f826cf672a2d79e377864d6a239b2679e133 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Sun, 15 May 2022 18:58:41 +0200
Subject: [PATCH] fix

---
 libsmtutil/CHCSmtLib2Interface.cpp | 3 ++-
 libsolidity/formal/CHC.cpp         | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index 07ef19fac..5ea710b5d 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -449,7 +449,8 @@ string CHCSmtLib2Interface::querySolver(string const& _input)
 			boost::process::child eld(
 				eldBin,
 				"-ssol",
-				"-scex",
+				//"-scex",
+				"-cex",
 				queryFileName,
 				boost::process::std_out > is
 			);
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index d8e669a4d..d9f832a73 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -1194,7 +1194,7 @@ void CHC::resetSourceAnalysis()
 #endif
 	if (!usesZ3)
 	{
-		solAssert(m_settings.solvers.smtlib2);
+		solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld);
 
 		if (!m_interface)
 			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);