OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (...

[cvc5.git] / examples / api / bitvectors-new.cpp

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 58912a1bb3ec1722250889113d29af6ab9d32d17..4578da7335e6f26eb3f29b3f0570b7a7b73a23bf 100644 (file)
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -114,8 +114,8 @@ int main()
   cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
 
   // Assert that a is odd
-  OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
-  Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a);
+  Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+  Term lsb_of_a = slv.mkTerm(extract_op, a);
   cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
   Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
   cout << "Assert " << a_odd << endl;