3 files changed, 101 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 18e4d6c1b..29224803a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -922,6 +922,7 @@ set(regress_0_tests
   regress0/smtlib/issue4028.smt2
   regress0/smtlib/issue4077.smt2
   regress0/smtlib/issue4151.smt2
+  regress0/smtlib/issue4552.smt2
   regress0/smtlib/reason-unknown.smt2
   regress0/smtlib/reset.smt2
   regress0/smtlib/reset-assertions1.smt2
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)
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 3dcf18f78..257c28669 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -84,8 +84,11 @@ class SolverBlack : public CxxTest::TestSuite
   void testDeclareSort();
 
   void testDefineFun();
+  void testDefineFunGlobal();
   void testDefineFunRec();
+  void testDefineFunRecGlobal();
   void testDefineFunsRec();
+  void testDefineFunsRecGlobal();
 
   void testUFIteration();
 
@@ -1036,6 +1039,30 @@ void SolverBlack::testDefineFun()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testDefineFunGlobal()
+{
+  Sort bSort = d_solver->getBooleanSort();
+  Sort fSort = d_solver->mkFunctionSort({bSort}, bSort);
+
+  Term bTrue = d_solver->mkBoolean(true);
+  // (define-fun f () Bool true)
+  Term f = d_solver->defineFun("f", {}, bSort, bTrue, true);
+  Term b = d_solver->mkVar(bSort, "b");
+  Term gSym = d_solver->mkConst(fSort, "g");
+  // (define-fun g (b Bool) Bool b)
+  Term g = d_solver->defineFun(gSym, {b}, b, true);
+
+  // (assert (or (not f) (not (g true))))
+  d_solver->assertFormula(d_solver->mkTerm(
+      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+  d_solver->resetAssertions();
+  // (assert (or (not f) (not (g true))))
+  d_solver->assertFormula(d_solver->mkTerm(
+      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+}
+
 void SolverBlack::testDefineFunRec()
 {
   Sort bvSort = d_solver->mkBitVectorSort(32);
@@ -1090,6 +1117,31 @@ void SolverBlack::testDefineFunRec()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testDefineFunRecGlobal()
+{
+  Sort bSort = d_solver->getBooleanSort();
+  Sort fSort = d_solver->mkFunctionSort({bSort}, bSort);
+
+  d_solver->push();
+  Term bTrue = d_solver->mkBoolean(true);
+  // (define-fun f () Bool true)
+  Term f = d_solver->defineFunRec("f", {}, bSort, bTrue, true);
+  Term b = d_solver->mkVar(bSort, "b");
+  Term gSym = d_solver->mkConst(fSort, "g");
+  // (define-fun g (b Bool) Bool b)
+  Term g = d_solver->defineFunRec(gSym, {b}, b, true);
+
+  // (assert (or (not f) (not (g true))))
+  d_solver->assertFormula(d_solver->mkTerm(
+      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+  d_solver->pop();
+  // (assert (or (not f) (not (g true))))
+  d_solver->assertFormula(d_solver->mkTerm(
+      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+}
+
 void SolverBlack::testDefineFunsRec()
 {
   Sort uSort = d_solver->mkUninterpretedSort("u");
@@ -1162,6 +1214,27 @@ void SolverBlack::testDefineFunsRec()
       CVC4ApiException&);
 }
 
+void SolverBlack::testDefineFunsRecGlobal()
+{
+  Sort bSort = d_solver->getBooleanSort();
+  Sort fSort = d_solver->mkFunctionSort({bSort}, bSort);
+
+  d_solver->push();
+  Term bTrue = d_solver->mkBoolean(true);
+  Term b = d_solver->mkVar(bSort, "b");
+  Term gSym = d_solver->mkConst(fSort, "g");
+  // (define-funs-rec ((g ((b Bool)) Bool)) (b))
+  d_solver->defineFunsRec({gSym}, {{b}}, {b}, true);
+
+  // (assert (not (g true)))
+  d_solver->assertFormula(d_solver->mkTerm(APPLY_UF, gSym, bTrue).notTerm());
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+  d_solver->pop();
+  // (assert (not (g true)))
+  d_solver->assertFormula(d_solver->mkTerm(APPLY_UF, gSym, bTrue).notTerm());
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+}
+
 void SolverBlack::testUFIteration()
 {
   Sort intSort = d_solver->getIntegerSort();