1 files changed, 0 insertions, 30 deletions
diff --git a/test/regress/regress0/push-pop/quant-fun-proc.smt2 b/test/regress/regress0/push-pop/quant-fun-proc.smt2
deleted file mode 100644
index 2a12cb677..000000000
--- a/test/regress/regress0/push-pop/quant-fun-proc.smt2
+++ /dev/null
@@ -1,30 +0,0 @@
-; COMMAND-LINE: --incremental --fmf-fun --macros-quant --macros-quant-mode=ground --no-check-models
-(set-logic UFLIA)
-
-(define-fun f ((x Int)) Int x)
-
-(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
-
-(declare-fun h (Int) Int)
-(assert (forall ((x Int)) (= (h x) (+ x 3))))
-
-; EXPECT: sat
-(check-sat)
-
-; EXPECT: unsat
-(push 1)
-(assert (= (f 1) 2))
-(check-sat)
-(pop 1)
-
-; EXPECT: unsat
-(push 1)
-(assert (= (g 1) 5))
-(check-sat)
-(pop 1)
-
-; EXPECT: unsat
-(push 1)
-(assert (= (h 1) 5))
-(check-sat)
-(pop 1)