From bdf16e0cd5790fb06d28fed150ec8730432ccca7 Mon Sep 17 00:00:00 2001
From: ApolloLizhaoyu <apollo19990425@sjtu.edu.cn>
Date: Thu, 6 Aug 2020 12:58:07 +0800
Subject: [PATCH 1/2] fix a small bug.

---
 eval_env.py | 4 ++--
 serapi.py   | 7 +++++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/eval_env.py b/eval_env.py
index cd6c1cde..3991c03c 100644
--- a/eval_env.py
+++ b/eval_env.py
@@ -72,7 +72,7 @@ def step(self, command):
                 self.num_tactics_left -= 1
                 command = 'timeout %d (%s).' % (time_left, command[:-1])
             responses, _ = self.serapi.execute(command)
-            self.serapi.pull()  # delete the saved state if no error
+            states_cnt = self.serapi.pull()  # delete the saved state if no error
         except CoqExn as ex: 
             self.serapi.pop()  # restore the state
             return self.feedback('ERROR', error=ex)
@@ -97,7 +97,7 @@ def step(self, command):
             self.success = True
             return self.feedback('SUCCESS')
         elif shelved_goals + given_up_goals != []:
-            self.serapi.pop()
+            self.serapi.pop_n(states_cnt)
             return self.feedback('ERROR', error=(shelved_goals, given_up_goals))
         else:
             return self.feedback('PROVING', fg_goals=fg_goals, bg_goals=bg_goals, 
diff --git a/serapi.py b/serapi.py
index 4d3cbeb8..054c504b 100644
--- a/serapi.py
+++ b/serapi.py
@@ -358,12 +358,19 @@ def pull(self):
         'remove a checkpoint created by push'
         states = self.states_stack.pop()
         self.states_stack[-1].extend(states)
+        return len(states)
 
 
     def pop(self):
         'rollback to a checkpoint created by push'
         self.cancel(self.states_stack.pop())
 
+    def pop_n(self, cnt):
+        states = []
+        for i in range(cnt):
+            states.append(self.states_stack[-1].pop())
+        self.cancel(states)
+
 
     def clean(self):
         self.proc.sendeof()

From 7258f59846297f3dc6bf38a47dface8cef94b719 Mon Sep 17 00:00:00 2001
From: ApolloLizhaoyu <apollo19990425@sjtu.edu.cn>
Date: Thu, 6 Aug 2020 13:05:01 +0800
Subject: [PATCH 2/2] update

---
 serapi.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/serapi.py b/serapi.py
index 054c504b..e5fe1ad3 100644
--- a/serapi.py
+++ b/serapi.py
@@ -365,6 +365,7 @@ def pop(self):
         'rollback to a checkpoint created by push'
         self.cancel(self.states_stack.pop())
 
+
     def pop_n(self, cnt):
         states = []
         for i in range(cnt):