aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SymbolicBoolVariable.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp')
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.cpp8
1 files changed, 3 insertions, 5 deletions
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index 5e5aec8f..f65ecd37 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -17,8 +17,6 @@
#include <libsolidity/formal/SymbolicBoolVariable.h>
-#include <libsolidity/ast/AST.h>
-
using namespace std;
using namespace dev;
using namespace dev::solidity;
@@ -38,11 +36,11 @@ smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
return m_interface.newBool(uniqueSymbol(_seq));
}
-void SymbolicBoolVariable::setZeroValue(int _seq)
+void SymbolicBoolVariable::setZeroValue()
{
- m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false));
+ m_interface.addAssertion(current() == smt::Expression(false));
}
-void SymbolicBoolVariable::setUnknownValue(int)
+void SymbolicBoolVariable::setUnknownValue()
{
}