From c2d26eb6a20a21f5fe4b5d78a39f8c23f7f3f5cb Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 9 Mar 2018 16:19:03 +0100 Subject: [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests. --- libsolidity/formal/SymbolicVariable.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'libsolidity/formal/SymbolicVariable.cpp') diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index 629049ea..d59b55b1 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -24,7 +24,7 @@ using namespace dev; using namespace dev::solidity; SymbolicVariable::SymbolicVariable( - Declaration const* _decl, + Declaration const& _decl, smt::SolverInterface& _interface ): m_declaration(_decl), @@ -34,7 +34,7 @@ SymbolicVariable::SymbolicVariable( string SymbolicVariable::uniqueSymbol() const { - return m_declaration->name() + "_" + to_string(m_declaration->id()); + return m_declaration.name() + "_" + to_string(m_declaration.id()); } -- cgit v1.2.3 From 8d087d1889826271a78ce537b8d1a2ceb11574dd Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 5 Apr 2018 12:20:41 +0200 Subject: [SMTChecker] Removing usage of UFs to access SSA indices --- libsolidity/formal/SymbolicVariable.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'libsolidity/formal/SymbolicVariable.cpp') diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index d59b55b1..caefa3a3 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -32,9 +32,9 @@ SymbolicVariable::SymbolicVariable( { } -string SymbolicVariable::uniqueSymbol() const +string SymbolicVariable::uniqueSymbol(int _seq) const { - return m_declaration.name() + "_" + to_string(m_declaration.id()); + return m_declaration.name() + "_" + to_string(m_declaration.id()) + "_" + to_string(_seq); } -- cgit v1.2.3