1 files changed, 9 insertions, 9 deletions
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index 5444a7df3..44a3d66d2 100644
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -16,16 +16,16 @@
 # Darulova. This requires building cvc5 with symfpu.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
 
     if not slv.supportsFloatingPoint():
-        # CVC4 must be built with SymFPU to support the theory of
+        # cvc5 must be built with SymFPU to support the theory of
         # floating-point numbers
-        print("CVC4 was not built with floating-point support.")
+        print("cvc5 was not built with floating-point support.")
         exit()
 
     slv.setOption("produce-models", "true")
@@ -35,7 +35,7 @@ if __name__ == "__main__":
     fp32 = slv.mkFloatingPointSort(8, 24)
 
     # the standard rounding mode
-    rm = slv.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+    rm = slv.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
 
     # create a few single-precision variables
     x = slv.mkConst(fp32, 'x')
@@ -49,7 +49,7 @@ if __name__ == "__main__":
     slv.assertFormula(slv.mkTerm(kinds.Not, commutative))
     print("Checking floating-point commutativity")
     print("Expect SAT (property does not hold for NaN and Infinities).")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
     print("Model for x:", slv.getValue(x))
     print("Model for y:", slv.getValue(y))
 
@@ -61,7 +61,7 @@ if __name__ == "__main__":
 
     print("Checking floating-point commutativity assuming x and y are not NaN or Infinity")
     print("Expect UNSAT.")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
 
     # check floating-point arithmetic is not associative
     slv.pop()
@@ -84,7 +84,7 @@ if __name__ == "__main__":
 
     print("Checking floating-point associativity")
     print("Expect SAT.")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
     print("Model for x:", slv.getValue(x))
     print("Model for y:", slv.getValue(y))
     print("Model for z:", slv.getValue(z))