Rename checkValid/query to checkEntailed. (#4191)

This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.

30 files changed, 104 insertions, 98 deletions

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index e77a5e99f..798dc08af 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -55,8 +55,9 @@ public class SimpleVC {
       new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
       impExpr(new Expr(twox_plus_y_geq_3));
 
-    System.out.println("Checking validity of formula " + formula + " with CVC4.");
-    System.out.println("CVC4 should report VALID.");
-    System.out.println("Result from CVC4 is: " + smt.query(formula));
+    System.out.println(
+        "Checking entailment of formula " + formula + " with CVC4.");
+    System.out.println("CVC4 should report ENTAILED.");
+    System.out.println("Result from CVC4 is: " + smt.checkEntailed(formula));
   }
 }
diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml
index c89341dc8..d9d78586b 100644
--- a/examples/SimpleVC.ml
+++ b/examples/SimpleVC.ml
@@ -79,13 +79,13 @@ let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3)
 
 let bformula = new_Expr(formula) in
 
-print_string "Checking validity of formula " ;
+print_string "Checking entailment of formula " ;
 print_string (get_string (formula->toString ())) ;
 print_string " with CVC4." ;
 print_newline () ;
-print_string "CVC4 should report VALID." ;
+print_string "CVC4 should report ENTAILED." ;
 print_newline () ;
 print_string "Result from CVC4 is: " ;
-print_string (get_string (smt->query(bformula)->toString ())) ;
+print_string (get_string (smt->checkEntailed(bformula)->toString ())) ;
 print_newline ()
 ;;
diff --git a/examples/SimpleVC.php b/examples/SimpleVC.php
index 329446703..031c0a1c5 100755
--- a/examples/SimpleVC.php
+++ b/examples/SimpleVC.php
@@ -50,7 +50,7 @@ my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
 
 my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
 
-print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
-print "CVC4 should report VALID.\n";
-print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n";
+print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n";
+print "CVC4 should report ENTAILED.\n";
+print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n";
 
diff --git a/examples/SimpleVC.pl b/examples/SimpleVC.pl
index 998c28bb0..20ad6c737 100755
--- a/examples/SimpleVC.pl
+++ b/examples/SimpleVC.pl
@@ -50,7 +50,7 @@ my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
 
 my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
 
-print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
-print "CVC4 should report VALID.\n";
-print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n";
+print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n";
+print "CVC4 should report ENTAILED.\n";
+print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n";
 
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index 4c21d35c0..5550974c9 100755
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -53,9 +53,9 @@ def main():
 
   formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3))
 
-  print("Checking validity of formula " + formula.toString() + " with CVC4.")
-  print("CVC4 should report VALID.")
-  print("Result from CVC4 is: " + smt.query(formula).toString())
+  print("Checking entailment of formula " + formula.toString() + " with CVC4.")
+  print("CVC4 should report ENTAILED .")
+  print("Result from CVC4 is: " + smt.checkEntailed(formula).toString())
 
   return 0
 
diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb
index 0d19ef49f..4f289d34f 100755
--- a/examples/SimpleVC.rb
+++ b/examples/SimpleVC.rb
@@ -49,9 +49,9 @@ twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three)
 
 formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3))
 
-puts "Checking validity of formula " + formula.toString + " with CVC4."
-puts "CVC4 should report VALID."
-puts "Result from CVC4 is: " + smt.query(formula).toString
+puts "Checking entailment of formula " + formula.toString + " with CVC4."
+puts "CVC4 should report ENTAILED."
+puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString
 
 exit
 
diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl
index ed0decb26..4e1c76c5a 100755
--- a/examples/SimpleVC.tcl
+++ b/examples/SimpleVC.tcl
@@ -48,7 +48,7 @@ set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three]
 
 set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
 
-puts "Checking validity of formula [Expr_toString $formula] with CVC4."
-puts "CVC4 should report VALID."
-puts "Result from CVC4 is: [Result_toString [SmtEngine_query smt $formula]]"
+puts "Checking entailment of formula [Expr_toString $formula] with CVC4."
+puts "CVC4 should report ENTAILED."
+puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]"
 
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 4578da733..ebb8ee7ee 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -87,9 +87,9 @@ int main()
   slv.assertFormula(assignment1);
   Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_);
 
-  cout << " Check validity assuming: " << new_x_eq_new_x_ << endl;
-  cout << " Expect valid. " << endl;
-  cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl;
+  cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl;
+  cout << " Expect ENTAILED. " << endl;
+  cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
   cout << " Popping context. " << endl;
   slv.pop();
 
@@ -103,15 +103,15 @@ int main()
   cout << "Asserting " << assignment2 << " to CVC4 " << endl;
   slv.assertFormula(assignment2);
 
-  cout << " Check validity assuming: " << new_x_eq_new_x_ << endl;
-  cout << " Expect valid. " << endl;
-  cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl;
+  cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl;
+  cout << " Expect ENTAILED. " << endl;
+  cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
 
   Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm();
   std::vector<Term> v{new_x_eq_new_x_, x_neq_x};
-  cout << " Check Validity Assuming: " << v << endl;
-  cout << " Expect invalid. " << endl;
-  cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
+  cout << " Check entailment assuming: " << v << endl;
+  cout << " Expect NOT_ENTAILED. " << endl;
+  cout << " CVC4: " << slv.checkEntailed(v) << endl;
 
   // Assert that a is odd
   Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index 259eb48ff..494a45abc 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -87,8 +87,8 @@ int main() {
   Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_);
 
   cout << " Querying: " << new_x_eq_new_x_ << endl;
-  cout << " Expect valid. " << endl;
-  cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
+  cout << " Expect entailed. " << endl;
+  cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl;
   cout << " Popping context. " << endl;
   smt.pop();
 
@@ -103,14 +103,14 @@ int main() {
   smt.assertFormula(assignment2);
 
   cout << " Querying: " << new_x_eq_new_x_ << endl;
-  cout << " Expect valid. " << endl;
-  cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
+  cout << " Expect ENTAILED. " << endl;
+  cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl;
 
   Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr();
   std::vector<Expr> v{new_x_eq_new_x_, x_neq_x};
   cout << " Querying: " << v << endl;
-  cout << " Expect invalid. " << endl;
-  cout << " CVC4: " << smt.query(v) << endl;
+  cout << " Expect NOT_ENTAILED. " << endl;
+  cout << " CVC4: " << smt.checkEntailed(v) << endl;
 
   // Assert that a is odd 
   Expr extract_op = em.mkConst(BitVectorExtract(0, 0));
diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 5284a0119..546d9ee9c 100644
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -82,9 +82,10 @@ int main()
   cout << "Given the following assertions:" << endl
        << assertions << endl << endl;
 
-  cout << "Prove x /= y is valid. " << endl
-       << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y))
-       << "." << endl << endl;
+  cout << "Prove x /= y is entailed. " << endl
+       << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "."
+       << endl
+       << endl;
 
   cout << "Call checkSat to show that the assertions are satisfiable. "
        << endl
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 646e6b17a..2e972a543 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -86,8 +86,8 @@ int main() {
 
   cout << "Given the following assumptions:" << endl
        << assumptions << endl
-       << "Prove x /= y is valid. "
-       << "CVC4 says: " << smt.query(em.mkExpr(kind::DISTINCT, x, y))
+       << "Prove x /= y is entailed. "
+       << "CVC4 says: " << smt.checkEntailed(em.mkExpr(kind::DISTINCT, x, y))
        << "." << endl;
 
   cout << "Now we call checksat on a trivial query to show that" << endl
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 0f0f8243a..705cdd90f 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -47,9 +47,9 @@ int main()
   slv.assertFormula(eq);
 
   Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0);
-  cout << " Check validity assuming: " << eq2 << endl;
-  cout << " Expect valid. " << endl;
-  cout << " CVC4: " << slv.checkValidAssuming(eq2) << endl;
+  cout << " Check entailment assuming: " << eq2 << endl;
+  cout << " Expect ENTAILED. " << endl;
+  cout << " CVC4: " << slv.checkEntailed(eq2) << endl;
 
   return 0;
 }
diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp
index a008ec718..e2558df28 100644
--- a/examples/api/extract.cpp
+++ b/examples/api/extract.cpp
@@ -48,8 +48,8 @@ int main() {
 
   Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0);
   cout << " Querying: " << eq2 << endl;
-  cout << " Expect valid. " << endl;
-  cout << " CVC4: " << smt.query(eq2) << endl;
+  cout << " Expect entailed. " << endl;
+  cout << " CVC4: " << smt.checkEntailed(eq2) << endl;
 
   return 0;
 }
diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp
index ab869f03c..f442c1412 100644
--- a/examples/api/helloworld-new.cpp
+++ b/examples/api/helloworld-new.cpp
@@ -24,7 +24,7 @@ int main()
 {
   Solver slv;
   Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
-  std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld)
+  std::cout << helloworld << " is " << slv.checkEntailed(helloworld)
             << std::endl;
   return 0;
 }
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index befeaa7bd..49a334504 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -23,6 +23,7 @@ int main() {
   ExprManager em;
   Expr helloworld = em.mkVar("Hello World!", em.booleanType());
   SmtEngine smt(&em);
-  std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
+  std::cout << helloworld << " is " << smt.checkEntailed(helloworld)
+            << std::endl;
   return 0;
 }
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 17111b63a..bb2245a6f 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -86,8 +86,8 @@ public class BitVectors {
     Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_);
 
     System.out.println(" Querying: " + new_x_eq_new_x_);
-    System.out.println(" Expect valid. ");
-    System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_));
+    System.out.println(" Expect entailed. ");
+    System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_));
     System.out.println(" Popping context. ");
     smt.pop();
 
@@ -102,7 +102,7 @@ public class BitVectors {
     smt.assertFormula(assignment2);
 
     System.out.println(" Querying: " + new_x_eq_new_x_);
-    System.out.println(" Expect valid. ");
-    System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_));
+    System.out.println(" Expect entailed. ");
+    System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_));
   }
 }
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 0c9ca84d6..53b1fa92d 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -83,10 +83,9 @@ public class Combination {
 
     System.out.println("Given the following assumptions:");
     System.out.println(assumptions);
-    System.out.println("Prove x /= y is valid. " +
-                       "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) +
-                       ".");
-
+    System.out.println("Prove x /= y is entailed. "
+        + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y))
+        + ".");
 
     System.out.println("Now we call checksat on a trivial query to show that");
     System.out.println("the assumptions are satisfiable: " +
diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 393ce40f0..a08f3d452 100644
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -30,6 +30,6 @@ public class HelloWorld {
     Expr helloworld = em.mkVar("Hello World!", em.booleanType());
     SmtEngine smt = new SmtEngine(em);
 
-    System.out.println(helloworld + " is " + smt.query(helloworld));
+    System.out.println(helloworld + " is " + smt.checkEntailed(helloworld));
   }
 }
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 2ddf92584..e060263b4 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -61,8 +61,9 @@ public class LinearArith {
     smt.push();
     Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds);
     System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4.");
-    System.out.println("CVC4 should report VALID.");
-    System.out.println("Result from CVC4 is: " + smt.query(diff_leq_two_thirds));
+    System.out.println("CVC4 should report ENTAILED.");
+    System.out.println(
+        "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds));
     smt.pop();
 
     System.out.println();
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index a4ff9a2cc..887c35d24 100644
--- a/examples/api/linear_arith-new.cpp
+++ b/examples/api/linear_arith-new.cpp
@@ -62,9 +62,9 @@ int main()
   slv.push();
   Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds);
   cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
-  cout << "CVC4 should report VALID." << endl;
-  cout << "Result from CVC4 is: "
-       << slv.checkValidAssuming(diff_leq_two_thirds) << endl;
+  cout << "CVC4 should report ENTAILED." << endl;
+  cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds)
+       << endl;
   slv.pop();
 
   cout << endl;
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index f1c8b861c..9e605f85c 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -62,8 +62,9 @@ int main() {
   smt.push();
   Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds);
   cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
-  cout << "CVC4 should report VALID." << endl;
-  cout << "Result from CVC4 is: " << smt.query(diff_leq_two_thirds) << endl;
+  cout << "CVC4 should report ENTAILED." << endl;
+  cout << "Result from CVC4 is: " << smt.checkEntailed(diff_leq_two_thirds)
+       << endl;
   smt.pop();
 
   cout << endl;
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.
 
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 2ca3db9d2..21ef925df 100644
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -52,8 +52,8 @@ int main()
 
     Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
 
-    cout << "CVC4 reports: " << theorem << " is "
-         << slv.checkValidAssuming(theorem) << "." << endl;
+    cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+         << "." << endl;
   }
 
   // Verify emptset is a subset of any set
@@ -63,8 +63,8 @@ int main()
 
     Term theorem = slv.mkTerm(SUBSET, emptyset, A);
 
-    cout << "CVC4 reports: " << theorem << " is "
-         << slv.checkValidAssuming(theorem) << "." << endl;
+    cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+         << "." << endl;
   }
 
   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 9fb342431..eb6a5a350 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -55,7 +55,8 @@ int main() {
 
     Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs);
 
-    cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl;
+    cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem)
+         << "." << endl;
   }
 
   // Verify emptset is a subset of any set
@@ -65,7 +66,8 @@ int main() {
 
     Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A);
 
-    cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl;
+    cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem)
+         << "." << endl;
   }
 
   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 25a05a1a7..cfd14b089 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -50,9 +50,9 @@ int main() {
     em.mkExpr(kind::AND, x_positive, y_positive).
     impExpr(twox_plus_y_geq_3);
 
-  cout << "Checking validity of formula " << formula << " with CVC4." << endl;
-  cout << "CVC4 should report VALID." << endl;
-  cout << "Result from CVC4 is: " << smt.query(formula) << endl;
+  cout << "Checking entailment of formula " << formula << " with CVC4." << endl;
+  cout << "CVC4 should report ENTAILED." << endl;
+  cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl;
 
   return 0;
 }