Merge pull request ethereum#3922 from ethereum/smt_sol_unimplementeda…

…ssert [SMTChecker] Using solUnimplementedAssert instead of solAssert
terry2012 · Apr 18, 2018 · 377254d · 377254d
2 parents cd17c37 + 78ba346
commit 377254d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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.");
 		}
 	}
 }