1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2
new file mode 100644
index 000000000..af8e0b948
--- /dev/null
+++ b/test/regress/regress0/smtlib/issue4552.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic UF)
+(set-option :global-declarations true)
+
+(push)
+(define a true)
+(define (f (b Bool)) b)
+(define-const a2 Bool true)
+
+(define-fun a3 () Bool true)
+
+(define-fun-rec b () Bool true)
+(define-funs-rec ((g ((b Bool)) Bool)) (b))
+(assert (or (not a) (not a2) (not a3) (not b) (g false)))
+(check-sat)
+(pop)
+
+(assert (or (not a) (not a2) (not a3) (not b) (g false)))
+(check-sat)
+
+(reset-assertions)
+
+(assert (or (not a) (not a2) (not a3) (not b) (g false)))
+(check-sat)