6 files changed, 25 insertions, 25 deletions
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index 773974cc7..8e4e1b682 100755
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -4,7 +4,7 @@
 #! \file bitvectors.py
  ## \verbatim
  ## Top contributors (to current version):
- ##   Makai Mann
+ ##   Makai Mann, Aina Niemetz
  ## This file is part of the CVC4 project.
  ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ## in the top-level source directory) and their institutional affiliations.
@@ -82,9 +82,9 @@ if __name__ == "__main__":
     slv.assertFormula(assignment1)
     new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_)
 
-    print("Checking validity assuming:", new_x_eq_new_x_)
-    print("Expect valid.")
-    print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_))
+    print("Checking entailment assuming:", new_x_eq_new_x_)
+    print("Expect ENTAILED.")
+    print("CVC4:", slv.checkEntailment(new_x_eq_new_x_))
     print("Popping context.")
     slv.pop()
 
@@ -98,16 +98,16 @@ if __name__ == "__main__":
     print("Asserting {} to CVC4".format(assignment2))
     slv.assertFormula(assignment2)
 
-    print("Checking validity assuming:", new_x_eq_new_x_)
-    print("Expect valid.")
-    print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_))
+    print("Checking entailment assuming:", new_x_eq_new_x_)
+    print("Expect ENTAILED.")
+    print("CVC4:", slv.checkEntailed(new_x_eq_new_x_))
 
 
     x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm()
     v = [new_x_eq_new_x_, x_neq_x]
-    print("Check Validity Assuming: ", v)
-    print("Expect invalid.")
-    print("CVC4:", slv.checkValidAssuming(v))
+    print("Check entailment assuming: ", v)
+    print("Expect NOT_ENTAILED.")
+    print("CVC4:", slv.checkEntailed(v))
 
     # Assert that a is odd
     extract_op = slv.mkOp(kinds.BVExtract, 0, 0)
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 1b488d7d5..7a8055bdf 100755
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -4,7 +4,7 @@
 #! \file combination.py
  ## \verbatim
  ## Top contributors (to current version):
- ##   Makai Mann
+ ##   Makai Mann, Aina Niemetz
  ## This file is part of the CVC4 project.
  ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ## in the top-level source directory) and their institutional affiliations.
@@ -69,8 +69,8 @@ if __name__ == "__main__":
     slv.assertFormula(assertions)
 
     print("Given the following assertions:", assertions, "\n")
-    print("Prove x /= y is valid.\nCVC4: ",
-          slv.checkValidAssuming(slv.mkTerm(kinds.Distinct, x, y)), "\n")
+    print("Prove x /= y is entailed.\nCVC4: ",
+          slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n")
 
     print("Call checkSat to show that the assertions are satisfiable")
     print("CVC4:", slv.checkSat(), "\n")
diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py
index 1bfdf652a..2b8714739 100755
--- a/examples/api/python/extract.py
+++ b/examples/api/python/extract.py
@@ -4,7 +4,7 @@
 #! \file extract.py
  ## \verbatim
  ## Top contributors (to current version):
- ##   Makai Mann
+ ##   Makai Mann, Aina Niemetz
  ## This file is part of the CVC4 project.
  ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ## in the top-level source directory) and their institutional affiliations.
@@ -46,6 +46,6 @@ if __name__ == "__main__":
     slv.assertFormula(eq)
 
     eq2 = slv.mkTerm(Equal, x_31_31, x_0_0)
-    print("Check validity assuming:", eq2)
-    print("Expect valid")
-    print("CVC4:", slv.checkValidAssuming(eq2))
+    print("Check entailment assuming:", eq2)
+    print("Expect ENTAILED")
+    print("CVC4:", slv.checkEntailed(eq2))
diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py
index 472cf945b..5607d7f83 100755
--- a/examples/api/python/helloworld.py
+++ b/examples/api/python/helloworld.py
@@ -4,7 +4,7 @@
 #! \file helloworld.py
 ## \verbatim
 ## Top contributors (to current version):
-##   Makai Mann
+##   Makai Mann, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
 ## in the top-level source directory) and their institutional affiliations.
@@ -18,4 +18,4 @@ from pycvc4 import kinds
 if __name__ == "__main__":
     slv = pycvc4.Solver()
     helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!")
-    print(helloworld, "is", slv.checkValidAssuming(helloworld))
+    print(helloworld, "is", slv.checkEntailed(helloworld))
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index 6ae6427b1..bab9680b3 100755
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -4,7 +4,7 @@
 #! \file linear_arith.py
 ## \verbatim
 ## Top contributors (to current version):
-##   Makai Mann
+##   Makai Mann, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
 ## in the top-level source directory) and their institutional affiliations.
@@ -54,9 +54,9 @@ if __name__ == "__main__":
     slv.push()
     diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds)
     print("Prove that", diff_leq_two_thirds, "with CVC4")
-    print("CVC4 should report VALID")
+    print("CVC4 should report ENTAILED")
     print("Result from CVC4 is:",
-          slv.checkValidAssuming(diff_leq_two_thirds))
+          slv.checkEntailed(diff_leq_two_thirds))
     slv.pop()
 
     print()
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 584880b2b..b69c56b56 100755
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -4,7 +4,7 @@
 #! \file sets.py
 ## \verbatim
 ## Top contributors (to current version):
-##   Makai Mann
+##   Makai Mann, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
 ## in the top-level source directory) and their institutional affiliations.
@@ -48,7 +48,7 @@ if __name__ == "__main__":
     theorem = slv.mkTerm(kinds.Equal, lhs, rhs)
 
     print("CVC4 reports: {} is {}".format(theorem,
-                                          slv.checkValidAssuming(theorem)))
+                                          slv.checkEntailed(theorem)))
 
     # Verify emptset is a subset of any set
 
@@ -58,7 +58,7 @@ if __name__ == "__main__":
     theorem = slv.mkTerm(kinds.Subset, emptyset, A)
 
     print("CVC4 reports: {} is {}".format(theorem,
-                                          slv.checkValidAssuming(theorem)))
+                                          slv.checkEntailed(theorem)))
 
     # Find me an element in 1, 2 intersection 2, 3, if there is one.