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(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);