Revert "BREAKING: Bool variables should not allow arithmetic comparison"

This commit is contained in:
chriseth
2018-05-02 15:56:59 +02:00
committed by GitHub
parent 42289b642f
commit 8debded743
5 changed files with 35 additions and 60 deletions
+5 -1
View File
@@ -472,7 +472,11 @@ 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::NotEqual ? (left != right) :
op == Token::LessThan ? (!left && right) :
op == Token::LessThanOrEqual ? (!left || right) :
op == Token::GreaterThan ? (left && !right) :
/*op == Token::GreaterThanOrEqual*/ (left || !right)
);
}
// TODO: check that other values for op are not possible.