Change datatype selector/constructor/tester to terms (#3773)

1 files changed, 9 insertions, 5 deletions

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 43f97796e..c5773fa72 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -36,9 +36,11 @@ void test(Solver& slv, Sort& consListSort)
   // which is equivalent to consList["cons"].getConstructor().  Note that
   // "nil" is a constructor too, so it needs to be applied with
   // APPLY_CONSTRUCTOR, even though it has no arguments.
-  Term t = slv.mkTerm(consList.getConstructorTerm("cons"),
-                      slv.mkReal(0),
-                      slv.mkTerm(consList.getConstructorTerm("nil")));
+  Term t = slv.mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      slv.mkReal(0),
+      slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
 
   std::cout << "t is " << t << std::endl
             << "sort of cons is "
@@ -51,7 +53,8 @@ void test(Solver& slv, Sort& consListSort)
   // Here we first get the DatatypeConstructor for cons (with
   // consList["cons"]) in order to get the "head" selector symbol
   // to apply.
-  Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t);
+  Term t2 =
+      slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
 
   std::cout << "t2 is " << t2 << std::endl
             << "simplify(t2) is " << slv.simplify(t2) << std::endl
@@ -116,7 +119,8 @@ void test(Solver& slv, Sort& consListSort)
   Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
-  Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a);
+  Term head_a = slv.mkTerm(
+      APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
   std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
             << std::endl
             << "sort of cons is "