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/SymbolicIntVariable.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'libsolidity/formal/SymbolicIntVariable.h') diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index afa25f1b..eb36b899 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -33,7 +33,7 @@ class SymbolicIntVariable: public SymbolicVariable { public: SymbolicIntVariable( - Declaration const* _decl, + Declaration const& _decl, smt::SolverInterface& _interface ); -- 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/SymbolicIntVariable.h | 3 +++ 1 file changed, 3 insertions(+) (limited to 'libsolidity/formal/SymbolicIntVariable.h') diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index eb36b899..d591e8db 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -44,6 +44,9 @@ public: static smt::Expression minValue(IntegerType const& _t); static smt::Expression maxValue(IntegerType const& _t); + +protected: + smt::Expression valueAtSequence(int _seq) const; }; } -- cgit v1.2.3