aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2018-11-26 23:14:02 +0800
committerGitHub <noreply@github.com>2018-11-26 23:14:02 +0800
commitf6d8810103c762d1f5a41bf1c29d33b771cfed50 (patch)
treea3d469810fa5faf8fa857ae2cd1d0a5074acefce /libsolidity
parent764d618c442c969e72ab73ffda8475060fca1299 (diff)
parentaaaa92012cdab9c11984dfab2d0d56a1c537a61e (diff)
downloaddexon-solidity-f6d8810103c762d1f5a41bf1c29d33b771cfed50.tar.gz
dexon-solidity-f6d8810103c762d1f5a41bf1c29d33b771cfed50.tar.zst
dexon-solidity-f6d8810103c762d1f5a41bf1c29d33b771cfed50.zip
Merge pull request #5504 from ethereum/smt_fix_emscripten
[SMTChecker] Fix crash when SMTLib2Interface reports unknow for constant checks
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SMTChecker.cpp4
1 files changed, 4 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 5b7807f7..477568a0 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -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