1 files changed, 12 insertions, 34 deletions

diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index 0adb9d09..cf1a7486 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -17,6 +17,8 @@
 
 #include <libsolidity/formal/SymbolicIntVariable.h>
 
+#include <libsolidity/formal/SymbolicTypes.h>
+
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
@@ -28,47 +30,23 @@ SymbolicIntVariable::SymbolicIntVariable(
 ):
 	SymbolicVariable(_type, _uniqueName, _interface)
 {
-	solAssert(
-		_type.category() == Type::Category::Integer ||
-		_type.category() == Type::Category::Address,
-		""
-	);
-}
-
-smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
-{
-	return m_interface.newInteger(uniqueSymbol(_seq));
-}
-
-void SymbolicIntVariable::setZeroValue(int _seq)
-{
-	m_interface.addAssertion(valueAtSequence(_seq) == 0);
+	solAssert(isNumber(_type.category()), "");
 }
 
-void SymbolicIntVariable::setUnknownValue(int _seq)
+smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
 {
-	if (m_type.category() == Type::Category::Integer)
-	{
-		auto intType = dynamic_cast<IntegerType const*>(&m_type);
-		solAssert(intType, "");
-		m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
-		m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType));
-	}
-	else
-	{
-		solAssert(m_type.category() == Type::Category::Address, "");
-		IntegerType addrType{160};
-		m_interface.addAssertion(valueAtSequence(_seq) >= minValue(addrType));
-		m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(addrType));
-	}
+	return m_interface.newInteger(uniqueSymbol(_index));
 }
 
-smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
+void SymbolicIntVariable::setZeroValue()
 {
-	return smt::Expression(_t.minValue());
+	m_interface.addAssertion(currentValue() == 0);
 }
 
-smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
+void SymbolicIntVariable::setUnknownValue()
 {
-	return smt::Expression(_t.maxValue());
+	auto intType = dynamic_cast<IntegerType const*>(&m_type);
+	solAssert(intType, "");
+	m_interface.addAssertion(currentValue() >= minValue(*intType));
+	m_interface.addAssertion(currentValue() <= maxValue(*intType));
 }