From b7164b45928fe5a03a6debb21e345948cb814d69 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Mon, 13 Dec 2021 11:47:40 -0600 Subject: [PATCH] Update Relations.java (#7796) --- examples/api/java/Relations.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index a3e2b2a7e..95aede591 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -152,10 +152,9 @@ public class Relations Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant); Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose); - // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor)))) + // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor)))) Term x = solver.mkVar(personSort, "x"); - DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); - Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x); + Term xxTuple = solver.mkTuple(new Sort[]{personSort, personSort}, new Term[] {x, x}); Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); -- 2.30.2