diff --git a/tests/dune.inc b/tests/dune.inc
index d94198034..8ac2f5252 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -205624,6 +205624,27 @@
      (package alt-ergo)
       (action
        (diff testfile-quoted1.dolmen.expected testfile-quoted1.dolmen_dolmen.output)))
+  (rule
+   (target testfile-push-pop2.dolmen_dolmen.output)
+   (deps (:input testfile-push-pop2.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-push-pop2.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-push-pop2.dolmen.expected testfile-push-pop2.dolmen_dolmen.output)))
   (rule
    (target testfile-push-pop1.err.dolmen_dolmen.output)
    (deps (:input testfile-push-pop1.err.dolmen.smt2))
diff --git a/tests/smtlib/testfile-push-pop2.dolmen.expected b/tests/smtlib/testfile-push-pop2.dolmen.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/smtlib/testfile-push-pop2.dolmen.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/smtlib/testfile-push-pop2.dolmen.smt2 b/tests/smtlib/testfile-push-pop2.dolmen.smt2
new file mode 100644
index 000000000..860996f73
--- /dev/null
+++ b/tests/smtlib/testfile-push-pop2.dolmen.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(push 1)
+(assert (> x 0))
+(push 1)
+(pop 1)
+(pop 1)
+(assert (< x 0))
+(check-sat)