cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #13755 from ethereum/smt_fix_nondet

Browse Source 
Make isoltest not check SMTChecker counterexamples by default
This commit is contained in:
Kamil Śliwak 2022-11-28 22:45:07 +01:00 committed by GitHub
commit 7070a1721f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/SMTCheckerTest.cpp
View File

@ -63,7 +63,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none()) if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none())
m_shouldRun = false; m_shouldRun = false;
auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "no"); auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "yes");
if (ignoreCex == "no") if (ignoreCex == "no")
m_ignoreCex = false; m_ignoreCex = false;
else if (ignoreCex == "yes") else if (ignoreCex == "yes")
@ -129,5 +129,8 @@ void SMTCheckerTest::filterObtainedErrors()
}; };
if (m_ignoreCex) if (m_ignoreCex)
{
removeCex(m_expectations);
removeCex(m_errorList); removeCex(m_errorList);
}
} }