From ec84a7dc9b7ed9cfd5b562ee570c6ad13bdfbeb7 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Thu, 22 Nov 2018 14:48:31 +0100
Subject: [SMTChecker] Refactor setZeroValue and setUnknownValue

---
 libsolidity/formal/SymbolicVariables.cpp | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'libsolidity/formal/SymbolicVariables.cpp')

diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 399e18f8..efaeb97a 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -62,15 +62,6 @@ smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
 	return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
 }
 
-void SymbolicBoolVariable::setZeroValue()
-{
-	m_interface.addAssertion(currentValue() == smt::Expression(false));
-}
-
-void SymbolicBoolVariable::setUnknownValue()
-{
-}
-
 SymbolicIntVariable::SymbolicIntVariable(
 	TypePointer _type,
 	string const& _uniqueName,
@@ -86,19 +77,6 @@ smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
 	return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
 }
 
-void SymbolicIntVariable::setZeroValue()
-{
-	m_interface.addAssertion(currentValue() == 0);
-}
-
-void SymbolicIntVariable::setUnknownValue()
-{
-	auto intType = dynamic_cast<IntegerType const*>(m_type.get());
-	solAssert(intType, "");
-	m_interface.addAssertion(currentValue() >= minValue(*intType));
-	m_interface.addAssertion(currentValue() <= maxValue(*intType));
-}
-
 SymbolicAddressVariable::SymbolicAddressVariable(
 	string const& _uniqueName,
 	smt::SolverInterface& _interface
-- 
cgit v1.2.3