From 0e0518e5ce29e9b385793666cc3a30c3fdd43db5 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 23 Jun 2022 15:18:34 +0200
Subject: [PATCH] Implement push and pop.

---
 tools/solsmt.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp
index 6750548bd..4daccb9b5 100644
--- a/tools/solsmt.cpp
+++ b/tools/solsmt.cpp
@@ -270,6 +270,18 @@ int main(int argc, char** argv)
 			solAssert(items.size() == 2);
 			solver.addAssertion(toSMTUtilExpression(items[1], variableSorts));
 		}
+		else if (cmd == "push")
+		{
+			// TODO what is the meaning of the numeric argument?
+			solAssert(items.size() == 2);
+			solver.push();
+		}
+		else if (cmd == "pop")
+		{
+			// TODO what is the meaning of the numeric argument?
+			solAssert(items.size() == 2);
+			solver.pop();
+		}
 		else if (cmd == "set-logic")
 		{
 			// ignore - could check the actual logic.