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.