aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-04-18 18:52:04 +0800
committerLeonardo Alt <leo@ethereum.org>2018-04-18 19:17:59 +0800
commit78ba34608f9b587b5a481769ba6fee45a49fcf3a (patch)
treed3cae637e91e3550d14c5ce16710a0cfe6eb9ba7 /libsolidity/formal
parentf92574705033595b4a6bc20473c9f58e6f184f47 (diff)
downloaddexon-solidity-78ba34608f9b587b5a481769ba6fee45a49fcf3a.tar.gz
dexon-solidity-78ba34608f9b587b5a481769ba6fee45a49fcf3a.tar.zst
dexon-solidity-78ba34608f9b587b5a481769ba6fee45a49fcf3a.zip
[SMTChecker] Using solUnimplementedAssert instead of solAssert when applicable
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index da6b632c..777e57c3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -468,7 +468,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
}
else // Bool
{
- solAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "");
+ 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) :
@@ -839,7 +839,7 @@ void SMTChecker::createExpr(Expression const& _e)
m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break;
default:
- solAssert(false, "Type not implemented.");
+ solUnimplementedAssert(false, "Type not implemented.");
}
}
}