diff options
| author | Anurag Dashputre <anurag4u80@gmail.com> | 2018-09-30 15:10:38 +0800 |
|---|---|---|
| committer | Anurag Dashputre <anurag4u80@gmail.com> | 2018-09-30 15:10:38 +0800 |
| commit | 3321000f67add785383adb4ec544aad121552751 (patch) | |
| tree | 716675d37af1010521d53f7713a7ba4c5bcb38ee /libsolidity/formal | |
| parent | b86cea033bc3a31c15356b46e28e0f303490d52d (diff) | |
| download | dexon-solidity-3321000f67add785383adb4ec544aad121552751.tar dexon-solidity-3321000f67add785383adb4ec544aad121552751.tar.gz dexon-solidity-3321000f67add785383adb4ec544aad121552751.tar.bz2 dexon-solidity-3321000f67add785383adb4ec544aad121552751.tar.lz dexon-solidity-3321000f67add785383adb4ec544aad121552751.tar.xz dexon-solidity-3321000f67add785383adb4ec544aad121552751.tar.zst dexon-solidity-3321000f67add785383adb4ec544aad121552751.zip | |
Removing extra default cases to force compile time error, instead of runtime.
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 2 | ||||
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 49c90405..19785817 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -639,8 +639,6 @@ void SMTChecker::checkCondition( case smt::CheckResult::ERROR: m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; - default: - solAssert(false, ""); } m_interface->pop(); } diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 747c9172..9a0ccf48 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -91,8 +91,6 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _ case z3::check_result::unknown: result = CheckResult::UNKNOWN; break; - default: - solAssert(false, ""); } if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) |