aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
-rw-r--r--libsolidity/formal/SMTChecker.cpp6
1 files changed, 1 insertions, 5 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index c4dee22d..7facdf92 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -472,11 +472,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) :
- op == Token::NotEqual ? (left != right) :
- op == Token::LessThan ? (!left && right) :
- op == Token::LessThanOrEqual ? (!left || right) :
- op == Token::GreaterThan ? (left && !right) :
- /*op == Token::GreaterThanOrEqual*/ (left || !right)
+ /*op == Token::NotEqual*/ (left != right)
);
}
// TODO: check that other values for op are not possible.