6 files changed, 34 insertions, 34 deletions
diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py
index 538c9f2ca..eae0ecad7 100644
--- a/test/api/python/issue4889.py
+++ b/test/api/python/issue4889.py
@@ -14,7 +14,7 @@
 ##
 
 import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
 
 slv = pycvc5.Solver()
 sort_int = slv.getIntegerSort()
@@ -25,7 +25,7 @@ sort_bool = slv.getBooleanSort()
 const0 = slv.mkConst(sort_fp32, "_c0")
 const1 = slv.mkConst(sort_fp32, "_c2")
 const2 = slv.mkConst(sort_bool, "_c4")
-ite = slv.mkTerm(kinds.Ite, const2, const1, const0)
-rem = slv.mkTerm(kinds.FPRem, ite, const1)
-isnan = slv.mkTerm(kinds.FPIsNan, rem)
+ite = slv.mkTerm(Kind.Ite, const2, const1, const0)
+rem = slv.mkTerm(Kind.FPRem, ite, const1)
+isnan = slv.mkTerm(Kind.FPIsNan, rem)
 slv.checkSatAssuming(isnan)
diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py
index 05fc84ad6..f07b5c8fa 100644
--- a/test/api/python/issue5074.py
+++ b/test/api/python/issue5074.py
@@ -14,12 +14,12 @@
 ##
 
 import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
 
 slv = pycvc5.Solver()
 c1 = slv.mkConst(slv.getIntegerSort())
-t6 = slv.mkTerm(kinds.StringFromCode, c1)
-t12 = slv.mkTerm(kinds.StringToRegexp, t6)
-t14 = slv.mkTerm(kinds.StringReplaceRe, [t6, t12, t6])
-t16 = slv.mkTerm(kinds.StringContains, [t14, t14])
+t6 = slv.mkTerm(Kind.StringFromCode, c1)
+t12 = slv.mkTerm(Kind.StringToRegexp, t6)
+t14 = slv.mkTerm(Kind.StringReplaceRe, [t6, t12, t6])
+t16 = slv.mkTerm(Kind.StringContains, [t14, t14])
 slv.checkEntailed(t16)
diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py
index 6a4ec3842..9bbda286c 100644
--- a/test/api/python/issue6111.py
+++ b/test/api/python/issue6111.py
@@ -14,7 +14,7 @@
 ##
 
 import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
 
 solver = pycvc5.Solver()
 solver.setLogic("QF_BV")
@@ -25,7 +25,7 @@ zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10)
 args1 = []
 args1.append(zero)
 args1.append(input2_1)
-bvult_res = solver.mkTerm(kinds.BVUlt, args1)
+bvult_res = solver.mkTerm(Kind.BVUlt, args1)
 solver.assertFormula(bvult_res)
 
 bvsort4 = solver.mkBitVectorSort(4)
@@ -36,13 +36,13 @@ concat_result_43 = solver.mkConst(bvsort8, "concat_result_43")
 args2 = []
 args2.append(concat_result_42)
 args2.append(
-    solver.mkTerm(solver.mkOp(kinds.BVExtract, 7, 4), [concat_result_43]))
-solver.assertFormula(solver.mkTerm(kinds.Equal, args2))
+    solver.mkTerm(solver.mkOp(Kind.BVExtract, 7, 4), [concat_result_43]))
+solver.assertFormula(solver.mkTerm(Kind.Equal, args2))
 
 args3 = []
 args3.append(concat_result_42)
 args3.append(
-    solver.mkTerm(solver.mkOp(kinds.BVExtract, 3, 0), [concat_result_43]))
-solver.assertFormula(solver.mkTerm(kinds.Equal, args3))
+    solver.mkTerm(solver.mkOp(Kind.BVExtract, 3, 0), [concat_result_43]))
+solver.assertFormula(solver.mkTerm(Kind.Equal, args3))
 
 print(solver.checkSat())
diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py
index 5d84f65b6..7dbdd6b41 100644
--- a/test/api/python/proj-issue306.py
+++ b/test/api/python/proj-issue306.py
@@ -13,7 +13,7 @@
 ##
 
 import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
 
 slv = pycvc5.Solver()
 slv.setOption("check-proofs", "true")
@@ -24,8 +24,8 @@ t1 = slv.mkConst(s3, "_x0")
 t3 = slv.mkConst(s1, "_x2")
 t11 = slv.mkString("")
 t14 = slv.mkConst(s3, "_x11")
-t42 = slv.mkTerm(kinds.Ite, t3, t14, t1)
-t58 = slv.mkTerm(kinds.StringLeq, t14, t11)
-t95 = slv.mkTerm(kinds.Equal, t14, t42)
+t42 = slv.mkTerm(Kind.Ite, t3, t14, t1)
+t58 = slv.mkTerm(Kind.StringLeq, t14, t11)
+t95 = slv.mkTerm(Kind.Equal, t14, t42)
 slv.assertFormula(t95)
 slv.checkSatAssuming([t58])
diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py
index 221f1c884..8c3a4e44c 100644
--- a/test/api/python/reset_assertions.py
+++ b/test/api/python/reset_assertions.py
@@ -19,7 +19,7 @@
 ##
 
 import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
 
 slv = pycvc5.Solver()
 slv.setOption("incremental", "true")
@@ -27,7 +27,7 @@ slv.setOption("incremental", "true")
 real = slv.getRealSort()
 x = slv.mkConst(real, "x")
 four = slv.mkInteger(4)
-xEqFour = slv.mkTerm(kinds.Equal, x, four)
+xEqFour = slv.mkTerm(Kind.Equal, x, four)
 slv.assertFormula(xEqFour)
 print(slv.checkSat())
 
@@ -37,8 +37,8 @@ elementType = slv.getIntegerSort()
 indexType = slv.getIntegerSort()
 arrayType = slv.mkArraySort(indexType, elementType)
 array = slv.mkConst(arrayType, "array")
-arrayAtFour = slv.mkTerm(kinds.Select, array, four)
+arrayAtFour = slv.mkTerm(Kind.Select, array, four)
 ten = slv.mkInteger(10)
-arrayAtFour_eq_ten = slv.mkTerm(kinds.Equal, arrayAtFour, ten)
+arrayAtFour_eq_ten = slv.mkTerm(Kind.Equal, arrayAtFour, ten)
 slv.assertFormula(arrayAtFour_eq_ten)
 print(slv.checkSat())
diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py
index 4e2fbb750..8bbef42fa 100644
--- a/test/api/python/sep_log_api.py
+++ b/test/api/python/sep_log_api.py
@@ -20,7 +20,7 @@
 ##
 
 import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
 
 
 # Test function to validate that we *cannot* obtain the heap/nil expressions
@@ -43,7 +43,7 @@ def validate_exception():
     y = slv.mkConst(integer, "y")
 
     # y > x
-    y_gt_x = slv.mkTerm(kinds.Gt, y, x)
+    y_gt_x = slv.mkTerm(Kind.Gt, y, x)
 
     # assert it
     slv.assertFormula(y_gt_x)
@@ -124,18 +124,18 @@ def validate_getters():
     p2 = slv.mkConst(integer, "p2")
 
     # Constraints on x and y
-    x_equal_const = slv.mkTerm(kinds.Equal, x, random_constant)
-    y_gt_x = slv.mkTerm(kinds.Gt, y, x)
+    x_equal_const = slv.mkTerm(Kind.Equal, x, random_constant)
+    y_gt_x = slv.mkTerm(Kind.Gt, y, x)
 
     # Points-to expressions
-    p1_to_x = slv.mkTerm(kinds.SepPto, p1, x)
-    p2_to_y = slv.mkTerm(kinds.SepPto, p2, y)
+    p1_to_x = slv.mkTerm(Kind.SepPto, p1, x)
+    p2_to_y = slv.mkTerm(Kind.SepPto, p2, y)
 
     # Heap -- the points-to have to be "starred"!
-    heap = slv.mkTerm(kinds.SepStar, p1_to_x, p2_to_y)
+    heap = slv.mkTerm(Kind.SepStar, p1_to_x, p2_to_y)
 
     # Constain "nil" to be something random
-    fix_nil = slv.mkTerm(kinds.Equal, nil, expr_nil_val)
+    fix_nil = slv.mkTerm(Kind.Equal, nil, expr_nil_val)
 
     # Add it all to the solver!
     slv.assertFormula(x_equal_const)
@@ -157,11 +157,11 @@ def validate_getters():
     nil_expr = slv.getValueSepNil()
 
     # If the heap is not a separating conjunction, bail-out
-    if (heap_expr.getKind() != kinds.SepStar):
+    if (heap_expr.getKind() != Kind.SepStar):
         return False
 
     # If nil is not a direct equality, bail-out
-    if (nil_expr.getKind() != kinds.Equal):
+    if (nil_expr.getKind() != Kind.Equal):
         return False
 
     # Obtain the values for our "pointers"
@@ -175,7 +175,7 @@ def validate_getters():
     # Walk all the children
     for child in heap_expr:
         # If we don't have a PTO operator, bail-out
-        if (child.getKind() != kinds.SepPto):
+        if (child.getKind() != Kind.SepPto):
             return False
 
         # Find both sides of the PTO operator