1 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress0/ho/ho-matching-nested-app.smt2 b/test/regress/regress0/ho/ho-matching-nested-app.smt2
new file mode 100644
index 000000000..d6de559e6
--- /dev/null
+++ b/test/regress/regress0/ho/ho-matching-nested-app.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun p (Int) Bool)
+(declare-fun g (Int) Int)
+
+(assert (not (p (g 0))))
+;(assert (= 0 (g 0)))
+
+(assert (forall ((f (-> Int Int)) (y Int)) (p (f (f (f (f (f y))))))))
+
+(check-sat)
+(exit)