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.cpp6
1 files changed, 5 insertions, 1 deletions
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index e5c56e46..5cf22d7d 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -30,7 +30,11 @@ SymbolicBoolVariable::SymbolicBoolVariable(
SymbolicVariable(_decl, _interface)
{
solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
- m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool));
+}
+
+smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
+{
+ return m_interface.newBool(uniqueSymbol(_seq));
}
void SymbolicBoolVariable::setZeroValue(int _seq)