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 #5504 from ethereum/smt_fix_emscripten

Browse Source 
[SMTChecker] Fix crash when SMTLib2Interface reports unknow for constant checks
This commit is contained in:
chriseth 2018-11-26 16:14:02 +01:00 committed by GitHub
commit f6d8810103
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/SMTChecker.cpp
View File

@ -889,6 +889,10 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
{
// everything fine.
}
else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
{
// can't do anything.
}
else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
m_errorReporter.warning(_condition.location(), "Condition unreachable.");
else