Skip to content

Commit c79f2cc

Browse files
authored
Merge pull request #16164 from phrwlk/fix/formal-encoding-context-clear-const
refactor(formal): remove unused `clear()`/`solver()` from `EncodingContext`
2 parents d8293de + 68364ab commit c79f2cc

File tree

1 file changed

+1
-9
lines changed

1 file changed

+1
-9
lines changed

libsolidity/formal/EncodingContext.h

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,6 @@ class EncodingContext
4444
void resetUniqueId();
4545
/// Returns the current fresh slack id and increments it.
4646
unsigned newUniqueId();
47-
/// Clears the entire context, erasing everything.
48-
/// To be used before a model checking engine starts.
49-
void clear();
5047

5148
/// Sets the current solver used by the current engine for
5249
/// SMT variable declaration.
@@ -139,12 +136,7 @@ class EncodingContext
139136
void pushSolver();
140137
void popSolver();
141138
void addAssertion(smtutil::Expression const& _e);
142-
size_t solverStackHeight() { return m_assertions.size(); } const
143-
smtutil::SolverInterface* solver()
144-
{
145-
solAssert(m_solver, "");
146-
return m_solver;
147-
}
139+
size_t solverStackHeight() const { return m_assertions.size(); }
148140
//@}
149141

150142
SymbolicState& state() { return m_state; }

0 commit comments

Comments
 (0)