Check for higher-order variables in TheoryUF::ppRewrite (#7408)

Fixes #7000. That sequence of API calls now throws a logic exception.

1 files changed, 16 insertions, 0 deletions

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index d5137393e..a294ad6ca 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -2544,5 +2544,21 @@ TEST_F(TestApiBlackSolver, Output)
   ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
 }
 
+
+TEST_F(TestApiBlackSolver, issue7000)
+{
+  Sort s1 = d_solver.getIntegerSort();
+  Sort s2 = d_solver.mkFunctionSort(s1, s1);
+  Sort s3 = d_solver.getRealSort();
+  Term t4 = d_solver.mkPi();
+  Term t7 = d_solver.mkConst(s3, "_x5");
+  Term t37 = d_solver.mkConst(s2, "_x32");
+  Term t59 = d_solver.mkConst(s2, "_x51");
+  Term t72 = d_solver.mkTerm(EQUAL, t37, t59);
+  Term t74 = d_solver.mkTerm(GT, t4, t7);
+  // throws logic exception since logic is not higher order by default
+  ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5