diff options
| -rw-r--r-- | src/theory/uf/ho_extension.cpp | 15 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 | ||||
| -rw-r--r-- | test/unit/api/solver_black.cpp | 16 |
3 files changed, 26 insertions, 7 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 096a47c86..fd7cd467e 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -43,13 +43,16 @@ HoExtension::HoExtension(Env& env, Node HoExtension::ppRewrite(Node node) { // convert HO_APPLY to APPLY_UF if fully applied - if (node[0].getType().getNumChildren() == 2) + if (node.getKind() == HO_APPLY) { - Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; - Node ret = getApplyUfForHoApply(node); - Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret - << std::endl; - return ret; + if (node[0].getType().getNumChildren() == 2) + { + Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; + Node ret = getApplyUfForHoApply(node); + Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret + << std::endl; + return ret; + } } return node; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index cd974d3e4..ca7dc6a73 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -212,7 +212,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node << std::endl; Kind k = node.getKind(); - if (k == kind::HO_APPLY) + if (k == kind::HO_APPLY || (node.isVar() && node.getType().isFunction())) { if (!logicInfo().isHigherOrder()) { 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 |