1 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
new file mode 100644
index 000000000..d5effc083
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --incremental --fmf-fun
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l)))))
+
+(declare-fun input () Int)
+(declare-fun p () Bool)
+(declare-fun acc () Lst)
+(assert (and (= acc (ite (>= input 0) (cons input nil) nil))
+             (= p (>= (sum acc) 0))))
+
+
+; EXPECT: unsat
+(push 1)
+(assert (not p))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (not p))
+(check-sat)
+(pop 1)
+
+