aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Beregszaszi <alex@rtfs.hu>2018-04-19 03:28:47 +0800
committerGitHub <noreply@github.com>2018-04-19 03:28:47 +0800
commit377254d5a89f3e24cd9c317fdef715101078edff (patch)
treeb0b55693756abc3fbee9264f1aa4ceb42dff1dc2
parentcd17c37fe6df143558a8aaadcec2495ff50f90df (diff)
parent78ba34608f9b587b5a481769ba6fee45a49fcf3a (diff)
downloaddexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.tar
dexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.tar.gz
dexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.tar.bz2
dexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.tar.lz
dexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.tar.xz
dexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.tar.zst
dexon-solidity-377254d5a89f3e24cd9c317fdef715101078edff.zip
Merge pull request #3922 from ethereum/smt_sol_unimplementedassert
[SMTChecker] Using solUnimplementedAssert instead of solAssert
-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.");
}
}
}