From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 1 Apr 2020 01:12:16 +0000 (-0700)
Subject: Rename checkValid/query to checkEntailed. (#4191)
X-Git-Tag: cvc5-1.0.0~3416
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cfeaf40ed6a9d4d7fec925352e30d2470a1ca567;p=cvc5.git

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.
---

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;
 }
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index fa727088e..fff4bef85 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -768,22 +768,22 @@ bool Result::isSatUnknown(void) const
          && d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
 }
 
-bool Result::isValid(void) const
+bool Result::isEntailed(void) const
 {
-  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
-         && d_result->isValid() == CVC4::Result::VALID;
+  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+         && d_result->isEntailed() == CVC4::Result::ENTAILED;
 }
 
-bool Result::isInvalid(void) const
+bool Result::isNotEntailed(void) const
 {
-  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
-         && d_result->isValid() == CVC4::Result::INVALID;
+  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+         && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED;
 }
 
-bool Result::isValidUnknown(void) const
+bool Result::isEntailmentUnknown(void) const
 {
-  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
-         && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN;
+  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+         && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN;
 }
 
 bool Result::operator==(const Result& r) const
@@ -3585,7 +3585,7 @@ Term Solver::simplify(const Term& t)
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Result Solver::checkValid(void) const
+Result Solver::checkEntailed(Term term) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
@@ -3593,14 +3593,15 @@ Result Solver::checkValid(void) const
                  || CVC4::options::incrementalSolving())
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
+  CVC4_API_ARG_CHECK_NOT_NULL(term);
 
-  CVC4::Result r = d_smtEngine->query();
+  CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
   return Result(r);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Result Solver::checkValidAssuming(Term assumption) const
+Result Solver::checkEntailed(const std::vector<Term>& terms) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
@@ -3608,29 +3609,13 @@ Result Solver::checkValidAssuming(Term assumption) const
                  || CVC4::options::incrementalSolving())
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
-  CVC4_API_ARG_CHECK_NOT_NULL(assumption);
-
-  CVC4::Result r = d_smtEngine->query(*assumption.d_expr);
-  return Result(r);
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
-Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
-  CVC4_API_CHECK(!d_smtEngine->isQueryMade()
-                 || CVC4::options::incrementalSolving())
-      << "Cannot make multiple queries unless incremental solving is enabled "
-         "(try --incremental)";
-  for (const Term& assumption : assumptions)
+  for (const Term& term : terms)
   {
-    CVC4_API_ARG_CHECK_NOT_NULL(assumption);
+    CVC4_API_ARG_CHECK_NOT_NULL(term);
   }
 
-  std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
-  CVC4::Result r = d_smtEngine->query(eassumptions);
+  std::vector<Expr> exprs = termVectorToExprs(terms);
+  CVC4::Result r = d_smtEngine->checkEntailed(exprs);
   return Result(r);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 3c99d2480..1a1cd3b61 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -114,22 +114,21 @@ class CVC4_PUBLIC Result
   bool isSatUnknown() const;
 
   /**
-   * Return true if corresponding query was a valid checkValid() or
-   * checkValidAssuming() query.
+   * Return true if corresponding query was an entailed checkEntailed() query.
    */
-  bool isValid() const;
+  bool isEntailed() const;
 
   /**
-   * Return true if corresponding query was an invalid checkValid() or
-   * checkValidAssuming() query.
+   * Return true if corresponding query was a checkEntailed() query that is
+   * not entailed.
    */
-  bool isInvalid() const;
+  bool isNotEntailed() const;
 
   /**
-   * Return true if query was a checkValid() or checkValidAssuming() query
-   * and CVC4 was not able to determine (in)validity.
+   * Return true if query was a checkEntailed() () query and CVC4 was not able
+   * to determine if it is entailed.
    */
-  bool isValidUnknown() const;
+  bool isEntailmentUnknown() const;
 
   /**
    * Operator overloading for equality of two results.
@@ -2555,24 +2554,19 @@ class CVC4_PUBLIC Solver
   Result checkSatAssuming(const std::vector<Term>& assumptions) const;
 
   /**
-   * Check validity.
-   * @return the result of the validity check.
+   * Check entailment of the given formula w.r.t. the current set of assertions.
+   * @param term the formula to check entailment for
+   * @return the result of the entailment check.
    */
-  Result checkValid() const;
+  Result checkEntailed(Term term) const;
 
   /**
-   * Check validity assuming the given formula.
-   * @param assumption the formula to assume
-   * @return the result of the validity check.
-   */
-  Result checkValidAssuming(Term assumption) const;
-
-  /**
-   * Check validity assuming the given formulas.
-   * @param assumptions the formulas to assume
-   * @return the result of the validity check.
+   * Check entailment of the given set of given formulas w.r.t. the current
+   * set of assertions.
+   * @param terms the terms to check entailment for
+   * @return the result of the entailmentcheck.
    */
-  Result checkValidAssuming(const std::vector<Term>& assumptions) const;
+  Result checkEntailed(const std::vector<Term>& terms) const;
 
   /**
    * Create datatype sort.
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index bbff6f58b..d81d0c0bf 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -87,9 +87,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isSat() except +
         bint isUnsat() except +
         bint isSatUnknown() except +
-        bint isValid() except +
-        bint isInvalid() except +
-        bint isValidUnknown() except +
+        bint isEntailed() except +
+        bint isNotEntailed() except +
+        bint isEntailmentUnknown() except +
         string getUnknownExplanation() except +
         string toString() except +
 
@@ -168,8 +168,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         void assertFormula(Term term) except +
         Result checkSat() except +
         Result checkSatAssuming(const vector[Term]& assumptions) except +
-        Result checkValid() except +
-        Result checkValidAssuming(const vector[Term]& assumptions) except +
+        Result checkEntailed(const vector[Term]& assumptions) except +
         Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors)
         Term declareFun(const string& symbol, Sort sort) except +
         Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 188753122..60bd89cbd 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -749,19 +749,11 @@ cdef class Solver:
             explanation = r.getUnknownExplanation().decode()
         return  Result(name, explanation)
 
-    def checkValid(self):
-        cdef c_Result r = self.csolver.checkValid()
-        name = r.toString().decode()
-        explanation = ""
-        if r.isValidUnknown():
-            explanation = r.getUnknownExplanation().decode()
-        return Result(name, explanation)
-
     @expand_list_arg(num_req_args=0)
-    def checkValidAssuming(self, *assumptions):
+    def checkEntailed(self, *assumptions):
         '''
             Supports the following arguments:
-                 Result checkValidAssuming(List[Term] assumptions)
+                 Result checkEntailed(List[Term] assumptions)
 
                  where assumptions can also be comma-separated arguments of
                  type (boolean) Term
@@ -771,10 +763,10 @@ cdef class Solver:
         cdef vector[c_Term] v
         for a in assumptions:
             v.push_back((<Term?> a).cterm)
-        r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v)
+        r = self.csolver.checkEntailed(<const vector[c_Term]&> v)
         name = r.toString().decode()
         explanation = ""
-        if r.isValidUnknown():
+        if r.isEntailmentUnknown():
             explanation = r.getUnknownExplanation().decode()
         return Result(name, explanation)
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 79cc465ac..20f2dcff9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -513,7 +513,7 @@ void QueryCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    d_result = smtEngine->query(d_expr);
+    d_result = smtEngine->checkEntailed(d_expr);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 10fc76bf7..2e1716543 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1766,7 +1766,7 @@ Result SmtEngine::check() {
       resourceManager->out()) {
     Result::UnknownExplanation why = resourceManager->outOfResources() ?
                              Result::RESOURCEOUT : Result::TIMEOUT;
-    return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
+    return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
   }
 
   // Make sure the prop layer has all of the assertions
@@ -1791,7 +1791,8 @@ Result SmtEngine::check() {
 Result SmtEngine::quickCheck() {
   Assert(d_fullyInited);
   Trace("smt") << "SMT quickCheck()" << endl;
-  return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
+  return Result(
+      Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
 }
 
 theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
@@ -1807,7 +1808,8 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
   {
     std::stringstream ss;
     ss << "Cannot " << c
-       << " unless immediately preceded by SAT/INVALID or UNKNOWN response.";
+       << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
+          "response.";
     throw RecoverableModalException(ss.str().c_str());
   }
 
@@ -2380,35 +2382,34 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
   return checkSatisfiability(assumptions, inUnsatCore, false);
 }
 
-Result SmtEngine::query(const Expr& assumption, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore)
 {
-  Dump("benchmark") << QueryCommand(assumption, inUnsatCore);
-  return checkSatisfiability(assumption.isNull()
-                                 ? std::vector<Expr>()
-                                 : std::vector<Expr>{assumption},
-                             inUnsatCore,
-                             true)
-      .asValidityResult();
+  Dump("benchmark") << QueryCommand(expr, inUnsatCore);
+  return checkSatisfiability(
+             expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
+             inUnsatCore,
+             true)
+      .asEntailmentResult();
 }
 
-Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore)
 {
-  return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult();
+  return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult();
 }
 
 Result SmtEngine::checkSatisfiability(const Expr& expr,
                                       bool inUnsatCore,
-                                      bool isQuery)
+                                      bool isEntailmentCheck)
 {
   return checkSatisfiability(
       expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
       inUnsatCore,
-      isQuery);
+      isEntailmentCheck);
 }
 
 Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
                                       bool inUnsatCore,
-                                      bool isQuery)
+                                      bool isEntailmentCheck)
 {
   try
   {
@@ -2416,7 +2417,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
     finalOptionsAreSet();
     doPendingPops();
 
-    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
+    Trace("smt") << "SmtEngine::"
+                 << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
                  << assumptions << ")" << endl;
 
     if(d_queryMade && !options::incrementalSolving()) {
@@ -2434,7 +2436,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
 
     setProblemExtended();
 
-    if (isQuery)
+    if (isEntailmentCheck)
     {
       size_t size = assumptions.size();
       if (size > 1)
@@ -2540,8 +2542,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       d_smtMode = SMT_MODE_SAT_UNKNOWN;
     }
 
-    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
-                 << assumptions << ") => " << r << endl;
+    Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
+                 << "(" << assumptions << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {
@@ -2587,7 +2589,7 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void)
   {
     throw RecoverableModalException(
         "Cannot get unsat assumptions unless immediately preceded by "
-        "UNSAT/VALID response.");
+        "UNSAT/ENTAILED.");
   }
   finalOptionsAreSet();
   if (Dump.isOn("benchmark"))
@@ -2625,7 +2627,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
   }
   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
   d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv);
-  return quickCheck().asValidityResult();
+  return quickCheck().asEntailmentResult();
 }/* SmtEngine::assertFormula() */
 
 /*
@@ -3218,13 +3220,13 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
   Expr heap;
   Expr nil;
   Model* m = getAvailableModel("get separation logic heap and nil");
-  if (m->getHeapModel(heap, nil))
+  if (!m->getHeapModel(heap, nil))
   {
-    return std::make_pair(heap, nil);
+    InternalError()
+        << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
+           "expressions from theory model.";
   }
-  InternalError()
-      << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
-         "expressions from theory model.";
+  return std::make_pair(heap, nil);
 }
 
 std::vector<Expr> SmtEngine::getExpandedAssertions()
@@ -3294,8 +3296,8 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   if (d_smtMode != SMT_MODE_UNSAT)
   {
     throw RecoverableModalException(
-        "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
-        "response.");
+        "Cannot get an unsat core unless immediately preceded by "
+        "UNSAT/ENTAILED response.");
   }
 
   d_proofManager->traceUnsatCore();  // just to trigger core creation
@@ -3800,7 +3802,7 @@ const Proof& SmtEngine::getProof()
   if (d_smtMode != SMT_MODE_UNSAT)
   {
     throw RecoverableModalException(
-        "Cannot get a proof unless immediately preceded by UNSAT/VALID "
+        "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
         "response.");
   }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 2cb227fc9..37b89cfb7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -152,7 +152,9 @@ class CVC4_PUBLIC SmtEngine
    */
   bool isFullyInited() { return d_fullyInited; }
 
-  /** Return true if a query() or checkSat() has already been made.  */
+  /**
+   * Return true if a checkEntailed() or checkSatisfiability() has been made.
+   */
   bool isQueryMade() { return d_queryMade; }
 
   /** Return the user context level.  */
@@ -211,8 +213,8 @@ class CVC4_PUBLIC SmtEngine
   std::string getFilename() const;
 
   /**
-   * Get the model (only if immediately preceded by a SAT
-   * or INVALID query).  Only permitted if produce-models is on.
+   * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
+   * query).  Only permitted if produce-models is on.
    */
   Model* getModel();
 
@@ -230,9 +232,9 @@ class CVC4_PUBLIC SmtEngine
 
   /**
    * Block the current model values of (at least) the values in exprs.
-   * Can be called only if immediately preceded by a SAT or INVALID query. Only
-   * permitted if produce-models is on, and the block-models option is set to a
-   * mode other than "none".
+   * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query.
+   * Only permitted if produce-models is on, and the block-models option is set
+   * to a mode other than "none".
    *
    * This adds an assertion to the assertion stack of the form:
    *  (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
@@ -310,18 +312,21 @@ class CVC4_PUBLIC SmtEngine
   Result assertFormula(const Expr& e, bool inUnsatCore = true);
 
   /**
-   * Check validity of an expression with respect to the current set
-   * of assertions by asserting the query expression's negation and
-   * calling check().  Returns valid, invalid, or unknown result.
+   * Check if a given (set of) expression(s) is entailed with respect to the
+   * current set of assertions. We check this by asserting the negation of
+   * the (big AND over the) given (set of) expression(s).
+   * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result.
    *
    * @throw Exception
    */
-  Result query(const Expr& assumption = Expr(), bool inUnsatCore = true);
-  Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true);
+  Result checkEntailed(const Expr& assumption = Expr(),
+                       bool inUnsatCore = true);
+  Result checkEntailed(const std::vector<Expr>& assumptions,
+                       bool inUnsatCore = true);
 
   /**
    * Assert a formula (if provided) to the current context and call
-   * check().  Returns sat, unsat, or unknown result.
+   * check().  Returns SAT, UNSAT, or SAT_UNKNOWN result.
    *
    * @throw Exception
    */
@@ -456,9 +461,9 @@ class CVC4_PUBLIC SmtEngine
   Expr expandDefinitions(const Expr& e);
 
   /**
-   * Get the assigned value of an expr (only if immediately preceded
-   * by a SAT or INVALID query).  Only permitted if the SmtEngine is
-   * set to operate interactively and produce-models is on.
+   * Get the assigned value of an expr (only if immediately preceded by a SAT
+   * or NOT_ENTAILED query).  Only permitted if the SmtEngine is set to operate
+   * interactively and produce-models is on.
    *
    * @throw ModalException, TypeCheckingException, LogicException,
    *        UnsafeInterruptException
@@ -483,15 +488,15 @@ class CVC4_PUBLIC SmtEngine
 
   /**
    * Get the assignment (only if immediately preceded by a SAT or
-   * INVALID query).  Only permitted if the SmtEngine is set to
+   * NOT_ENTAILED query).  Only permitted if the SmtEngine is set to
    * operate interactively and produce-assignments is on.
    */
   std::vector<std::pair<Expr, Expr> > getAssignment();
 
   /**
-   * Get the last proof (only if immediately preceded by an UNSAT
-   * or VALID query).  Only permitted if CVC4 was built with proof
-   * support and produce-proofs is on.
+   * Get the last proof (only if immediately preceded by an UNSAT or ENTAILED
+   * query).  Only permitted if CVC4 was built with proof support and
+   * produce-proofs is on.
    *
    * The Proof object is owned by this SmtEngine until the SmtEngine is
    * destroyed.
@@ -624,9 +629,9 @@ class CVC4_PUBLIC SmtEngine
                                    std::vector<std::vector<Expr> >& tvecs);
 
   /**
-   * Get an unsatisfiable core (only if immediately preceded by an
-   * UNSAT or VALID query).  Only permitted if CVC4 was built with
-   * unsat-core support and produce-unsat-cores is on.
+   * Get an unsatisfiable core (only if immediately preceded by an UNSAT or
+   * ENTAILED query).  Only permitted if CVC4 was built with unsat-core support
+   * and produce-unsat-cores is on.
    */
   UnsatCore getUnsatCore();
 
@@ -714,8 +719,8 @@ class CVC4_PUBLIC SmtEngine
    *
    * Note that the cumulative timer only ticks away when one of the
    * SmtEngine's workhorse functions (things like assertFormula(),
-   * query(), checkSat(), and simplify()) are running.  Between calls,
-   * the timer is still.
+   * checkEntailed(), checkSat(), and simplify()) are running.
+   * Between calls, the timer is still.
    *
    * When an SmtEngine is first created, it has no time or resource
    * limits.
@@ -774,7 +779,10 @@ class CVC4_PUBLIC SmtEngine
   /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */
   void safeFlushStatistics(int fd) const;
 
-  /** Returns the most recent result of checkSat/query or (set-info :status). */
+  /**
+   * Returns the most recent result of checkSat/checkEntailed or
+   * (set-info :status).
+   */
   Result getStatusOfLastCommand() const { return d_status; }
 
   /**
@@ -881,7 +889,7 @@ class CVC4_PUBLIC SmtEngine
 
   /**
    * Internal method to get an unsatisfiable core (only if immediately preceded
-   * by an UNSAT or VALID query). Only permitted if CVC4 was built with
+   * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with
    * unsat-core support and produce-unsat-cores is on. Does not dump the
    * command.
    */
@@ -1007,13 +1015,13 @@ class CVC4_PUBLIC SmtEngine
                                 bool userVisible = true,
                                 const char* dumpTag = "declarations");
 
-  /* Check satisfiability (used for query and check-sat). */
+  /* Check satisfiability (used to check satisfiability and entailment). */
   Result checkSatisfiability(const Expr& assumption,
                              bool inUnsatCore,
-                             bool isQuery);
+                             bool isEntailmentCheck);
   Result checkSatisfiability(const std::vector<Expr>& assumptions,
                              bool inUnsatCore,
-                             bool isQuery);
+                             bool isEntailmentCheck);
 
   /**
    * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
@@ -1123,9 +1131,9 @@ class CVC4_PUBLIC SmtEngine
 
   /**
    * The list of assumptions from the previous call to checkSatisfiability.
-   * Note that if the last call to checkSatisfiability was a validity check,
-   * i.e., a call to query(a1, ..., an), then d_assumptions contains one single
-   * assumption ~(a1 AND ... AND an).
+   * Note that if the last call to checkSatisfiability was an entailment check,
+   * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
+   * one single assumption ~(a1 AND ... AND an).
    */
   std::vector<Expr> d_assumptions;
 
@@ -1189,10 +1197,10 @@ class CVC4_PUBLIC SmtEngine
   bool d_fullyInited;
 
   /**
-   * Whether or not a query() or checkSat() has already been made through
-   * this SmtEngine.  If true, and incrementalSolving is false, then
-   * attempting an additional query() or checkSat() will fail with a
-   * ModalException.
+   * Whether or not a checkEntailed() or checkSatisfiability() has already been
+   * made through this SmtEngine.  If true, and incrementalSolving is false,
+   * then attempting an additional checkEntailed() or checkSat() will fail with
+   * a ModalException.
    */
   bool d_queryMade;
 
@@ -1214,7 +1222,8 @@ class CVC4_PUBLIC SmtEngine
   bool d_globalNegation;
 
   /**
-   * Most recent result of last checkSat/query or (set-info :status).
+   * Most recent result of last checkSatisfiability/checkEntailed or
+   * (set-info :status).
    */
   Result d_status;
 
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 433dcbf29..916e16b4f 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -29,59 +29,68 @@ namespace CVC4 {
 
 Result::Result()
     : d_sat(SAT_UNKNOWN),
-      d_validity(VALIDITY_UNKNOWN),
+      d_entailment(ENTAILMENT_UNKNOWN),
       d_which(TYPE_NONE),
       d_unknownExplanation(UNKNOWN_REASON),
-      d_inputName("") {}
+      d_inputName("")
+{
+}
 
 Result::Result(enum Sat s, std::string inputName)
     : d_sat(s),
-      d_validity(VALIDITY_UNKNOWN),
+      d_entailment(ENTAILMENT_UNKNOWN),
       d_which(TYPE_SAT),
       d_unknownExplanation(UNKNOWN_REASON),
-      d_inputName(inputName) {
+      d_inputName(inputName)
+{
   PrettyCheckArgument(s != SAT_UNKNOWN,
                       "Must provide a reason for satisfiability being unknown");
 }
 
-Result::Result(enum Validity v, std::string inputName)
+Result::Result(enum Entailment e, std::string inputName)
     : d_sat(SAT_UNKNOWN),
-      d_validity(v),
-      d_which(TYPE_VALIDITY),
+      d_entailment(e),
+      d_which(TYPE_ENTAILMENT),
       d_unknownExplanation(UNKNOWN_REASON),
-      d_inputName(inputName) {
-  PrettyCheckArgument(v != VALIDITY_UNKNOWN,
-                      "Must provide a reason for validity being unknown");
+      d_inputName(inputName)
+{
+  PrettyCheckArgument(e != ENTAILMENT_UNKNOWN,
+                      "Must provide a reason for entailment being unknown");
 }
 
-Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
+Result::Result(enum Sat s,
+               enum UnknownExplanation unknownExplanation,
                std::string inputName)
     : d_sat(s),
-      d_validity(VALIDITY_UNKNOWN),
+      d_entailment(ENTAILMENT_UNKNOWN),
       d_which(TYPE_SAT),
       d_unknownExplanation(unknownExplanation),
-      d_inputName(inputName) {
+      d_inputName(inputName)
+{
   PrettyCheckArgument(s == SAT_UNKNOWN,
                       "improper use of unknown-result constructor");
 }
 
-Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+Result::Result(enum Entailment e,
+               enum UnknownExplanation unknownExplanation,
                std::string inputName)
     : d_sat(SAT_UNKNOWN),
-      d_validity(v),
-      d_which(TYPE_VALIDITY),
+      d_entailment(e),
+      d_which(TYPE_ENTAILMENT),
       d_unknownExplanation(unknownExplanation),
-      d_inputName(inputName) {
-  PrettyCheckArgument(v == VALIDITY_UNKNOWN,
+      d_inputName(inputName)
+{
+  PrettyCheckArgument(e == ENTAILMENT_UNKNOWN,
                       "improper use of unknown-result constructor");
 }
 
 Result::Result(const std::string& instr, std::string inputName)
     : d_sat(SAT_UNKNOWN),
-      d_validity(VALIDITY_UNKNOWN),
+      d_entailment(ENTAILMENT_UNKNOWN),
       d_which(TYPE_NONE),
       d_unknownExplanation(UNKNOWN_REASON),
-      d_inputName(inputName) {
+      d_inputName(inputName)
+{
   string s = instr;
   transform(s.begin(), s.end(), s.begin(), ::tolower);
   if (s == "sat" || s == "satisfiable") {
@@ -90,38 +99,56 @@ Result::Result(const std::string& instr, std::string inputName)
   } else if (s == "unsat" || s == "unsatisfiable") {
     d_which = TYPE_SAT;
     d_sat = UNSAT;
-  } else if (s == "valid") {
-    d_which = TYPE_VALIDITY;
-    d_validity = VALID;
-  } else if (s == "invalid") {
-    d_which = TYPE_VALIDITY;
-    d_validity = INVALID;
-  } else if (s == "incomplete") {
+  }
+  else if (s == "entailed")
+  {
+    d_which = TYPE_ENTAILMENT;
+    d_entailment = ENTAILED;
+  }
+  else if (s == "not_entailed")
+  {
+    d_which = TYPE_ENTAILMENT;
+    d_entailment = NOT_ENTAILED;
+  }
+  else if (s == "incomplete")
+  {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = INCOMPLETE;
-  } else if (s == "timeout") {
+  }
+  else if (s == "timeout")
+  {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = TIMEOUT;
-  } else if (s == "resourceout") {
+  }
+  else if (s == "resourceout")
+  {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = RESOURCEOUT;
-  } else if (s == "memout") {
+  }
+  else if (s == "memout")
+  {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = MEMOUT;
-  } else if (s == "interrupted") {
+  }
+  else if (s == "interrupted")
+  {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = INTERRUPTED;
-  } else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+  }
+  else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0)
+  {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
-  } else {
+  }
+  else
+  {
     IllegalArgument(s,
-                    "expected satisfiability/validity result, "
+                    "expected satisfiability/entailment result, "
                     "instead got `%s'",
                     s.c_str());
   }
@@ -142,37 +169,41 @@ bool Result::operator==(const Result& r) const {
     return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN ||
                                 d_unknownExplanation == r.d_unknownExplanation);
   }
-  if (d_which == TYPE_VALIDITY) {
-    return d_validity == r.d_validity &&
-           (d_validity != VALIDITY_UNKNOWN ||
-            d_unknownExplanation == r.d_unknownExplanation);
+  if (d_which == TYPE_ENTAILMENT)
+  {
+    return d_entailment == r.d_entailment
+           && (d_entailment != ENTAILMENT_UNKNOWN
+               || d_unknownExplanation == r.d_unknownExplanation);
   }
   return false;
 }
 
 bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; }
 
-bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; }
+bool operator==(enum Result::Entailment e, const Result& r) { return r == e; }
 bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); }
-bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); }
+bool operator!=(enum Result::Entailment e, const Result& r)
+{
+  return !(e == r);
+}
 
 Result Result::asSatisfiabilityResult() const {
   if (d_which == TYPE_SAT) {
     return *this;
   }
 
-  if (d_which == TYPE_VALIDITY) {
-    switch (d_validity) {
-      case INVALID:
-        return Result(SAT, d_inputName);
+  if (d_which == TYPE_ENTAILMENT)
+  {
+    switch (d_entailment)
+    {
+      case NOT_ENTAILED: return Result(SAT, d_inputName);
 
-      case VALID:
-        return Result(UNSAT, d_inputName);
+      case ENTAILED: return Result(UNSAT, d_inputName);
 
-      case VALIDITY_UNKNOWN:
+      case ENTAILMENT_UNKNOWN:
         return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
 
-      default: Unhandled() << d_validity;
+      default: Unhandled() << d_entailment;
     }
   }
 
@@ -180,28 +211,28 @@ Result Result::asSatisfiabilityResult() const {
   return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
 }
 
-Result Result::asValidityResult() const {
-  if (d_which == TYPE_VALIDITY) {
+Result Result::asEntailmentResult() const
+{
+  if (d_which == TYPE_ENTAILMENT)
+  {
     return *this;
   }
 
   if (d_which == TYPE_SAT) {
     switch (d_sat) {
-      case SAT:
-        return Result(INVALID, d_inputName);
+      case SAT: return Result(NOT_ENTAILED, d_inputName);
 
-      case UNSAT:
-        return Result(VALID, d_inputName);
+      case UNSAT: return Result(ENTAILED, d_inputName);
 
       case SAT_UNKNOWN:
-        return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
+        return Result(ENTAILMENT_UNKNOWN, d_unknownExplanation, d_inputName);
 
       default: Unhandled() << d_sat;
     }
   }
 
   // TYPE_NONE
-  return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
+  return Result(ENTAILMENT_UNKNOWN, NO_STATUS, d_inputName);
 }
 
 string Result::toString() const {
@@ -226,18 +257,14 @@ ostream& operator<<(ostream& out, enum Result::Sat s) {
   return out;
 }
 
-ostream& operator<<(ostream& out, enum Result::Validity v) {
-  switch (v) {
-    case Result::INVALID:
-      out << "INVALID";
-      break;
-    case Result::VALID:
-      out << "VALID";
-      break;
-    case Result::VALIDITY_UNKNOWN:
-      out << "VALIDITY_UNKNOWN";
-      break;
-    default: Unhandled() << v;
+ostream& operator<<(ostream& out, enum Result::Entailment e)
+{
+  switch (e)
+  {
+    case Result::NOT_ENTAILED: out << "NOT_ENTAILED"; break;
+    case Result::ENTAILED: out << "ENTAILED"; break;
+    case Result::ENTAILMENT_UNKNOWN: out << "ENTAILMENT_UNKNOWN"; break;
+    default: Unhandled() << e;
   }
   return out;
 }
@@ -301,14 +328,11 @@ void Result::toStreamDefault(std::ostream& out) const {
         break;
     }
   } else {
-    switch (isValid()) {
-      case Result::INVALID:
-        out << "invalid";
-        break;
-      case Result::VALID:
-        out << "valid";
-        break;
-      case Result::VALIDITY_UNKNOWN:
+    switch (isEntailed())
+    {
+      case Result::NOT_ENTAILED: out << "not_entailed"; break;
+      case Result::ENTAILED: out << "entailed"; break;
+      case Result::ENTAILMENT_UNKNOWN:
         out << "unknown";
         if (whyUnknown() != Result::UNKNOWN_REASON) {
           out << " (" << whyUnknown() << ")";
@@ -332,11 +356,17 @@ void Result::toStreamTptp(std::ostream& out) const {
     out << "Satisfiable";
   } else if (isSat() == Result::UNSAT) {
     out << "Unsatisfiable";
-  } else if (isValid() == Result::VALID) {
+  }
+  else if (isEntailed() == Result::ENTAILED)
+  {
     out << "Theorem";
-  } else if (isValid() == Result::INVALID) {
+  }
+  else if (isEntailed() == Result::NOT_ENTAILED)
+  {
     out << "CounterSatisfiable";
-  } else {
+  }
+  else
+  {
     out << "GaveUp";
   }
   out << " for " << getInputName();
diff --git a/src/util/result.h b/src/util/result.h
index f34a9bb5a..10df05388 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -38,9 +38,19 @@ class CVC4_PUBLIC Result {
  public:
   enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };
 
-  enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 };
+  enum Entailment
+  {
+    NOT_ENTAILED = 0,
+    ENTAILED = 1,
+    ENTAILMENT_UNKNOWN = 2
+  };
 
-  enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE };
+  enum Type
+  {
+    TYPE_SAT,
+    TYPE_ENTAILMENT,
+    TYPE_NONE
+  };
 
   enum UnknownExplanation {
     REQUIRES_FULL_CHECK,
@@ -57,7 +67,7 @@ class CVC4_PUBLIC Result {
 
  private:
   enum Sat d_sat;
-  enum Validity d_validity;
+  enum Entailment d_entailment;
   enum Type d_which;
   enum UnknownExplanation d_unknownExplanation;
   std::string d_inputName;
@@ -67,12 +77,13 @@ class CVC4_PUBLIC Result {
 
   Result(enum Sat s, std::string inputName = "");
 
-  Result(enum Validity v, std::string inputName = "");
+  Result(enum Entailment v, std::string inputName = "");
 
   Result(enum Sat s, enum UnknownExplanation unknownExplanation,
          std::string inputName = "");
 
-  Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+  Result(enum Entailment v,
+         enum UnknownExplanation unknownExplanation,
          std::string inputName = "");
 
   Result(const std::string& s, std::string inputName = "");
@@ -84,12 +95,13 @@ class CVC4_PUBLIC Result {
 
   enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; }
 
-  enum Validity isValid() const {
-    return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
+  enum Entailment isEntailed() const
+  {
+    return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN;
   }
 
   bool isUnknown() const {
-    return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
+    return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN;
   }
 
   Type getType() const { return d_which; }
@@ -101,7 +113,7 @@ class CVC4_PUBLIC Result {
   bool operator==(const Result& r) const;
   inline bool operator!=(const Result& r) const;
   Result asSatisfiabilityResult() const;
-  Result asValidityResult() const;
+  Result asEntailmentResult() const;
 
   std::string toString() const;
 
@@ -128,7 +140,7 @@ class CVC4_PUBLIC Result {
    * Write a Result out to a stream.
    *
    * The default implementation writes a reasonable string in lowercase
-   * for sat, unsat, valid, invalid, or unknown results.  This behavior
+   * for sat, unsat, entailed, not entailed, or unknown results.  This behavior
    * is overridable by each Printer, since sometimes an output language
    * has a particular preference for how results should appear.
    */
@@ -139,15 +151,15 @@ inline bool Result::operator!=(const Result& r) const { return !(*this == r); }
 
 std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out,
-                         enum Result::Validity v) CVC4_PUBLIC;
+                         enum Result::Entailment e) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out,
                          enum Result::UnknownExplanation e) CVC4_PUBLIC;
 
 bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
-bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
+bool operator==(enum Result::Entailment e, const Result& r) CVC4_PUBLIC;
 
 bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
-bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
+bool operator!=(enum Result::Entailment e, const Result& r) CVC4_PUBLIC;
 
 } /* CVC4 namespace */
 
diff --git a/src/util/result.i b/src/util/result.i
index b77bfd881..cb835fbb0 100644
--- a/src/util/result.i
+++ b/src/util/result.i
@@ -8,13 +8,13 @@
 %ignore CVC4::Result::operator!=(const Result& r) const;
 
 %ignore CVC4::operator<<(std::ostream&, enum Result::Sat);
-%ignore CVC4::operator<<(std::ostream&, enum Result::Validity);
+%ignore CVC4::operator<<(std::ostream&, enum Result::Entailment);
 %ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
 
 %ignore CVC4::operator==(enum Result::Sat, const Result&);
 %ignore CVC4::operator!=(enum Result::Sat, const Result&);
 
-%ignore CVC4::operator==(enum Result::Validity, const Result&);
-%ignore CVC4::operator!=(enum Result::Validity, const Result&);
+%ignore CVC4::operator==(enum Result::Entailment, const Result&);
+%ignore CVC4::operator!=(enum Result::Entailment, const Result&);
 
 %include "util/result.h"
diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc
index 1de397ab1..08d591590 100644
--- a/test/regress/regress0/arith/arith.01.cvc
+++ b/test/regress/regress0/arith/arith.01.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x : REAL;
 y : REAL;
 
diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc
index d7b0291f7..e0a48c357 100644
--- a/test/regress/regress0/arith/arith.02.cvc
+++ b/test/regress/regress0/arith/arith.02.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x : REAL;
 y : REAL;
 z : REAL;
diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc
index 288c341ef..ce54c8b7e 100644
--- a/test/regress/regress0/arith/arith.03.cvc
+++ b/test/regress/regress0/arith/arith.03.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x : REAL;
 y : REAL;
 
diff --git a/test/regress/regress0/arith/bug549.cvc b/test/regress/regress0/arith/bug549.cvc
index 54df5e62c..bfb3e75d5 100644
--- a/test/regress/regress0/arith/bug549.cvc
+++ b/test/regress/regress0/arith/bug549.cvc
@@ -1,3 +1,3 @@
-% EXPECT: valid
+% EXPECT: entailed
 a, b : REAL;
-QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
\ No newline at end of file
+QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc
index 265d18a84..84954a3ea 100644
--- a/test/regress/regress0/arith/integers/arith-int-014.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-014.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ;
 ASSERT  (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3;
diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc
index d2e2639ab..8f8b01fc9 100644
--- a/test/regress/regress0/arith/integers/arith-int-015.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-015.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ;
 ASSERT  (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28;
diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc
index 345c90899..66f02401b 100644
--- a/test/regress/regress0/arith/integers/arith-int-021.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-021.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12;
 QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc
index 01d51a226..b3d79e8ff 100644
--- a/test/regress/regress0/arith/integers/arith-int-023.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-023.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9;
 QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc
index 5a11212d5..e905da9a0 100644
--- a/test/regress/regress0/arith/integers/arith-int-025.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-025.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3;
 QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc
index c38231695..b6db26e86 100644
--- a/test/regress/regress0/arith/integers/arith-int-042.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-042.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ;
 ASSERT  (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc
index 77571e526..3fd20a0b6 100644
--- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x1: INT;
 x0: INT;
 QUERY NOT (((x0 * 6) + (x1 * 32)) = 1);
diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc
index 7fa2fc937..1739b3364 100644
--- a/test/regress/regress0/arith/integers/arith-int-079.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-079.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ;
 ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ;
diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc
index d79ec94a7..ed6cb747e 100644
--- a/test/regress/regress0/arith/integers/arith-interval.cvc
+++ b/test/regress/regress0/arith/integers/arith-interval.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x: INT;
 P: INT -> BOOLEAN;
 
diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc
index 9d1029cbf..07a2aa2f5 100644
--- a/test/regress/regress0/boolean-prec.cvc
+++ b/test/regress/regress0/boolean-prec.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of AND, <=>, NOT.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/bug310.cvc b/test/regress/regress0/bug310.cvc
index 0cb6cf0fe..12cb80494 100644
--- a/test/regress/regress0/bug310.cvc
+++ b/test/regress/regress0/bug310.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 b : BOOLEAN;
 DATATYPE D = c(s:INT) END;
 QUERY c(IF b THEN 1 ELSE 0 ENDIF) = IF b THEN c(1) ELSE c(0) ENDIF;
diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc
index 304dd6ec4..400f55885 100644
--- a/test/regress/regress0/bug32.cvc
+++ b/test/regress/regress0/bug32.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 a:BOOLEAN;
 b:BOOLEAN;
 ASSERT(a);
diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc
index fa9462f64..0e06cbc13 100644
--- a/test/regress/regress0/bug322b.cvc
+++ b/test/regress/regress0/bug322b.cvc
@@ -1,7 +1,7 @@
 % COMMAND-LINE: --incremental
-% EXPECT: valid
-% EXPECT: valid
-% EXPECT: valid
+% EXPECT: entailed
+% EXPECT: entailed
+% EXPECT: entailed
 x : INT;
 y : INT = x + 1;
 z : INT = -10;
diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc
index c51af4e24..665bcdafb 100644
--- a/test/regress/regress0/bug486.cvc
+++ b/test/regress/regress0/bug486.cvc
@@ -1,6 +1,6 @@
 % COMMAND-LINE: --finite-model-find -i
-% EXPECT: invalid
-% EXPECT: valid
+% EXPECT: not_entailed
+% EXPECT: entailed
 prin:TYPE;
 form:TYPE;
 
diff --git a/test/regress/regress0/bv/bvcomp.cvc b/test/regress/regress0/bv/bvcomp.cvc
index b9b4b8e17..17064a2f2 100644
--- a/test/regress/regress0/bv/bvcomp.cvc
+++ b/test/regress/regress0/bv/bvcomp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 x : BITVECTOR(10);
 
diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc
index dcacd643a..6bc649a03 100644
--- a/test/regress/regress0/bv/bvsimple.cvc
+++ b/test/regress/regress0/bv/bvsimple.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 % Some tests from the CVC3 user manual.
 % http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
diff --git a/test/regress/regress0/cvc-rerror-print.cvc b/test/regress/regress0/cvc-rerror-print.cvc
index dd05723d2..e134b5666 100644
--- a/test/regress/regress0/cvc-rerror-print.cvc
+++ b/test/regress/regress0/cvc-rerror-print.cvc
@@ -1,5 +1,5 @@
-% EXPECT: valid
-% EXPECT: Cannot get model unless immediately preceded by SAT/INVALID or UNKNOWN response.
+% EXPECT: entailed
+% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response.
 OPTION "logic" "ALL";
 OPTION "produce-models" true;
 x : INT;
diff --git a/test/regress/regress0/cvc3-bug15.cvc b/test/regress/regress0/cvc3-bug15.cvc
index 860ce38bd..779a2eab4 100644
--- a/test/regress/regress0/cvc3-bug15.cvc
+++ b/test/regress/regress0/cvc3-bug15.cvc
@@ -1,5 +1,5 @@
 %% This test borrowed from CVC3 regressions, bug15.cvc
-% EXPECT: valid
+% EXPECT: entailed
 x : REAL;
 y : REAL;
 f : REAL -> REAL;
diff --git a/test/regress/regress0/cvc3.userdoc.01.cvc b/test/regress/regress0/cvc3.userdoc.01.cvc
index 7c89de4ac..e3e9aaf0a 100644
--- a/test/regress/regress0/cvc3.userdoc.01.cvc
+++ b/test/regress/regress0/cvc3.userdoc.01.cvc
@@ -1,31 +1,31 @@
 % COMMAND-LINE: --incremental
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY 0bin0000111101010000  = 0hex0f50;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY 0bin01@0bin0          = 0bin010;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY 0bin0011[3:1]         = 0bin001;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY 0bin0011 << 3         = 0bin0011000;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY 0bin1000 >> 3         = 0bin0001;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY SX(0bin100, 5)        = 0bin11100;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY BVREPEAT(0bin10,3)    = 0bin101010;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY BVROTL(0bin101,1)     = 0bin011;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY BVROTR(0bin101,1)     = 0bin110;
diff --git a/test/regress/regress0/cvc3.userdoc.02.cvc b/test/regress/regress0/cvc3.userdoc.02.cvc
index b6329e953..e143ea275 100644
--- a/test/regress/regress0/cvc3.userdoc.02.cvc
+++ b/test/regress/regress0/cvc3.userdoc.02.cvc
@@ -2,6 +2,6 @@ x : BITVECTOR(5);
 y : BITVECTOR(4);
 yy : BITVECTOR(3);
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY
  BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;
diff --git a/test/regress/regress0/cvc3.userdoc.03.cvc b/test/regress/regress0/cvc3.userdoc.03.cvc
index 4fc6a5f8c..3b3829ebc 100644
--- a/test/regress/regress0/cvc3.userdoc.03.cvc
+++ b/test/regress/regress0/cvc3.userdoc.03.cvc
@@ -1,7 +1,7 @@
 bv : BITVECTOR(10);
 a : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY
  0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2]
  AND
diff --git a/test/regress/regress0/cvc3.userdoc.04.cvc b/test/regress/regress0/cvc3.userdoc.04.cvc
index 824690bcf..da8b1e82c 100644
--- a/test/regress/regress0/cvc3.userdoc.04.cvc
+++ b/test/regress/regress0/cvc3.userdoc.04.cvc
@@ -5,5 +5,5 @@ ASSERT x&y&t&z&q = x;
 ASSERT x|y = t;
 ASSERT BVXOR(x,~x) = t;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY  FALSE;
diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc
index 37da96b3c..85e0c2105 100644
--- a/test/regress/regress0/cvc3.userdoc.05.cvc
+++ b/test/regress/regress0/cvc3.userdoc.05.cvc
@@ -3,7 +3,7 @@ x, y : BITVECTOR(4);
 ASSERT x = 0hex5;
 ASSERT y = 0bin0101;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY
  BVMULT(8,x,y)=BVMULT(8,y,x)
  AND
diff --git a/test/regress/regress0/cvc3.userdoc.06.cvc b/test/regress/regress0/cvc3.userdoc.06.cvc
index 3801b6d53..3968365ad 100644
--- a/test/regress/regress0/cvc3.userdoc.06.cvc
+++ b/test/regress/regress0/cvc3.userdoc.06.cvc
@@ -6,8 +6,8 @@ z, t : BITVECTOR(12);
 ASSERT x = 0hexff;
 ASSERT z = 0hexff0;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY  z = x << 4;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY (z >> 4)[7:0] = x;
diff --git a/test/regress/regress0/datatypes/bug286.cvc b/test/regress/regress0/datatypes/bug286.cvc
index 501f5f737..33a320acd 100644
--- a/test/regress/regress0/datatypes/bug286.cvc
+++ b/test/regress/regress0/datatypes/bug286.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 DATATYPE foo = f(i:INT) END;
 x : foo;
 y : INT;
diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc
index 8e2818106..e28fc6305 100644
--- a/test/regress/regress0/datatypes/datatype-dump.cvc
+++ b/test/regress/regress0/datatypes/datatype-dump.cvc
@@ -10,7 +10,7 @@
 % EXPECT: END;
 % EXPECT: x : nat;
 % EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x));
-% EXPECT: invalid
+% EXPECT: not_entailed
 %
 
 DATATYPE nat = succ(pred : nat) | zero END;
diff --git a/test/regress/regress0/datatypes/datatype.cvc b/test/regress/regress0/datatypes/datatype.cvc
index 20fec4fdd..6a0e97fc3 100644
--- a/test/regress/regress0/datatypes/datatype.cvc
+++ b/test/regress/regress0/datatypes/datatype.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 
 DATATYPE nat = succ(pred : nat) | zero END;
 
diff --git a/test/regress/regress0/datatypes/datatype0.cvc b/test/regress/regress0/datatypes/datatype0.cvc
index 8fff50a86..0b9e41024 100644
--- a/test/regress/regress0/datatypes/datatype0.cvc
+++ b/test/regress/regress0/datatypes/datatype0.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 DATATYPE nat = succ(pred : nat) | zero END;
 
diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc
index 3934959f1..9e746c0e4 100644
--- a/test/regress/regress0/datatypes/datatype1.cvc
+++ b/test/regress/regress0/datatypes/datatype1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf
diff --git a/test/regress/regress0/datatypes/datatype13.cvc b/test/regress/regress0/datatypes/datatype13.cvc
index 91e582dbd..78d28be00 100644
--- a/test/regress/regress0/datatypes/datatype13.cvc
+++ b/test/regress/regress0/datatypes/datatype13.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 DATATYPE enum = enum1
 | enum2
diff --git a/test/regress/regress0/datatypes/datatype2.cvc b/test/regress/regress0/datatypes/datatype2.cvc
index 939dff197..64c84de45 100644
--- a/test/regress/regress0/datatypes/datatype2.cvc
+++ b/test/regress/regress0/datatypes/datatype2.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 DATATYPE
   nat = succ(pred : nat) | zero,
diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc
index fff1a5dd7..ce99edbb7 100644
--- a/test/regress/regress0/datatypes/datatype3.cvc
+++ b/test/regress/regress0/datatypes/datatype3.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf
diff --git a/test/regress/regress0/datatypes/datatype4.cvc b/test/regress/regress0/datatypes/datatype4.cvc
index 217777bdf..83962f49a 100644
--- a/test/regress/regress0/datatypes/datatype4.cvc
+++ b/test/regress/regress0/datatypes/datatype4.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 DATATYPE
    TypeGeneric = generic
 END;
diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc
index 4f6320028..b6950845e 100644
--- a/test/regress/regress0/datatypes/empty_tuprec.cvc
+++ b/test/regress/regress0/datatypes/empty_tuprec.cvc
@@ -7,15 +7,15 @@ b1, b2 : [##]; % empty records (a unit type)
 c1, c2 : [[]]; % 1-tuples of the empty tuple (a unit type)
 d1, d2 : [#x:[[##]],y:[#z:[]#]#]; % more complicated records (still a unit type)
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a1 = a2;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY b1 = b2;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY c1 = c2;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY d1 = d2;
 
diff --git a/test/regress/regress0/datatypes/mutually-recursive.cvc b/test/regress/regress0/datatypes/mutually-recursive.cvc
index b86b647b5..5bd857b6e 100644
--- a/test/regress/regress0/datatypes/mutually-recursive.cvc
+++ b/test/regress/regress0/datatypes/mutually-recursive.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 DATATYPE nat = succ(pred : nat2) | zero,
          nat2 = succ2(pred2 : nat) | zero2 END;
diff --git a/test/regress/regress0/datatypes/rec1.cvc b/test/regress/regress0/datatypes/rec1.cvc
index 79c9facda..b3e205985 100644
--- a/test/regress/regress0/datatypes/rec1.cvc
+++ b/test/regress/regress0/datatypes/rec1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 c : BOOLEAN;
 a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = (
           IF c THEN (# _a := 3, _b := 2 #)
diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc
index 44d523a46..56864c088 100644
--- a/test/regress/regress0/datatypes/rec2.cvc
+++ b/test/regress/regress0/datatypes/rec2.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 c : BOOLEAN;
 a16 : [# _a : INT, _b : INT #] = (
         IF c THEN (# _a := 3, _b := 2 #)
diff --git a/test/regress/regress0/datatypes/rec4.cvc b/test/regress/regress0/datatypes/rec4.cvc
index 08a9988ef..f7f29755f 100644
--- a/test/regress/regress0/datatypes/rec4.cvc
+++ b/test/regress/regress0/datatypes/rec4.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 a : BOOLEAN;
 a49 : BOOLEAN = (
           IF a THEN (# _a := 1 #)
diff --git a/test/regress/regress0/datatypes/rewriter.cvc b/test/regress/regress0/datatypes/rewriter.cvc
index 18f8b3441..e9b7662a0 100644
--- a/test/regress/regress0/datatypes/rewriter.cvc
+++ b/test/regress/regress0/datatypes/rewriter.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 % simple test for rewriter cases
 
diff --git a/test/regress/regress0/datatypes/tuple-record-bug.cvc b/test/regress/regress0/datatypes/tuple-record-bug.cvc
index 33c68dece..0e519a64f 100644
--- a/test/regress/regress0/datatypes/tuple-record-bug.cvc
+++ b/test/regress/regress0/datatypes/tuple-record-bug.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 
 Mem_0 : TYPE = ARRAY INT OF INT;
 
diff --git a/test/regress/regress0/datatypes/tuple.cvc b/test/regress/regress0/datatypes/tuple.cvc
index 366737525..00ab8d4db 100644
--- a/test/regress/regress0/datatypes/tuple.cvc
+++ b/test/regress/regress0/datatypes/tuple.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 );
 first_elem: REAL = x.0;
 third_elem: REAL = x.2;
diff --git a/test/regress/regress0/datatypes/typed_v10l30054.cvc b/test/regress/regress0/datatypes/typed_v10l30054.cvc
index ee414ed65..72c23d888 100644
--- a/test/regress/regress0/datatypes/typed_v10l30054.cvc
+++ b/test/regress/regress0/datatypes/typed_v10l30054.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/typed_v1l80005.cvc b/test/regress/regress0/datatypes/typed_v1l80005.cvc
index 988646f21..95b1a935f 100644
--- a/test/regress/regress0/datatypes/typed_v1l80005.cvc
+++ b/test/regress/regress0/datatypes/typed_v1l80005.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/typed_v2l30079.cvc b/test/regress/regress0/datatypes/typed_v2l30079.cvc
index f32c9e551..2295d1518 100644
--- a/test/regress/regress0/datatypes/typed_v2l30079.cvc
+++ b/test/regress/regress0/datatypes/typed_v2l30079.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/typed_v3l20092.cvc b/test/regress/regress0/datatypes/typed_v3l20092.cvc
index c6260e233..e067852df 100644
--- a/test/regress/regress0/datatypes/typed_v3l20092.cvc
+++ b/test/regress/regress0/datatypes/typed_v3l20092.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/typed_v5l30069.cvc b/test/regress/regress0/datatypes/typed_v5l30069.cvc
index 05d0247cc..f980acc69 100644
--- a/test/regress/regress0/datatypes/typed_v5l30069.cvc
+++ b/test/regress/regress0/datatypes/typed_v5l30069.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/v10l40099.cvc b/test/regress/regress0/datatypes/v10l40099.cvc
index 7b2da4b65..257bf2ccc 100644
--- a/test/regress/regress0/datatypes/v10l40099.cvc
+++ b/test/regress/regress0/datatypes/v10l40099.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/v2l40025.cvc b/test/regress/regress0/datatypes/v2l40025.cvc
index fc466f300..d3411e12e 100644
--- a/test/regress/regress0/datatypes/v2l40025.cvc
+++ b/test/regress/regress0/datatypes/v2l40025.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc
index b7019e7ae..ea27672d5 100644
--- a/test/regress/regress0/datatypes/v3l60006.cvc
+++ b/test/regress/regress0/datatypes/v3l60006.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/v5l30058.cvc b/test/regress/regress0/datatypes/v5l30058.cvc
index be101b8fb..d3db742ae 100644
--- a/test/regress/regress0/datatypes/v5l30058.cvc
+++ b/test/regress/regress0/datatypes/v5l30058.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 DATATYPE
   nat = succ(pred : nat) | zero,
   list = cons(car : tree, cdr : list) | null,
diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
index b0dbdc46e..67be78912 100644
--- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc
+++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 DATATYPE
   nat = succ(pred : nat) | zero
 END;
diff --git a/test/regress/regress0/fmf/bug-041417-set-options.cvc b/test/regress/regress0/fmf/bug-041417-set-options.cvc
index 16f59f78c..c4e9ba834 100644
--- a/test/regress/regress0/fmf/bug-041417-set-options.cvc
+++ b/test/regress/regress0/fmf/bug-041417-set-options.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 OPTION "finite-model-find";
 OPTION "fmf-fun";
 
diff --git a/test/regress/regress0/let.cvc b/test/regress/regress0/let.cvc
index 996b09d39..d0f5c5e1f 100644
--- a/test/regress/regress0/let.cvc
+++ b/test/regress/regress0/let.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 U: TYPE;
 a: U;
 b: U;
diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc
index 2c2ac2f79..305f2d396 100644
--- a/test/regress/regress0/logops.01.cvc
+++ b/test/regress/regress0/logops.01.cvc
@@ -1,3 +1,3 @@
 a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc
index 67415e95d..c74c11983 100644
--- a/test/regress/regress0/logops.02.cvc
+++ b/test/regress/regress0/logops.02.cvc
@@ -1,3 +1,3 @@
 a, b, c: BOOLEAN;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY NOT c AND b;
diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc
index 42298a8f4..1c86ce594 100644
--- a/test/regress/regress0/logops.03.cvc
+++ b/test/regress/regress0/logops.03.cvc
@@ -1,3 +1,3 @@
 a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc
index 89a9db320..254b0ed87 100644
--- a/test/regress/regress0/logops.04.cvc
+++ b/test/regress/regress0/logops.04.cvc
@@ -1,3 +1,3 @@
 a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY (a => b) <=> (NOT a OR b);
diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc
index 1ec94e5ae..2897dbc0c 100644
--- a/test/regress/regress0/logops.05.cvc
+++ b/test/regress/regress0/logops.05.cvc
@@ -1,4 +1,4 @@
 a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY TRUE XOR FALSE;
  
diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc
index 5115a90c1..3ede8d211 100644
--- a/test/regress/regress0/precedence/and-not.cvc
+++ b/test/regress/regress0/precedence/and-not.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of AND and NOT.
 
 A, B: BOOLEAN;
diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc
index 879becbbf..ec69087d1 100644
--- a/test/regress/regress0/precedence/and-xor.cvc
+++ b/test/regress/regress0/precedence/and-xor.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of XOR and AND.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/bool-cmp.cvc b/test/regress/regress0/precedence/bool-cmp.cvc
index b8729e92a..4f81c86ad 100644
--- a/test/regress/regress0/precedence/bool-cmp.cvc
+++ b/test/regress/regress0/precedence/bool-cmp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of comparisons and booleans
 
 x , y, z: INT;
diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc
index a7c07fe30..54ee7b8f8 100644
--- a/test/regress/regress0/precedence/cmp-plus.cvc
+++ b/test/regress/regress0/precedence/cmp-plus.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of comparisons and plus/minus
 
 x, y, z: INT;
diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc
index 9e581d514..af81ea10d 100644
--- a/test/regress/regress0/precedence/eq-fun.cvc
+++ b/test/regress/regress0/precedence/eq-fun.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of function application and =
 
 T : TYPE;
diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc
index 745cc7474..4643292b6 100644
--- a/test/regress/regress0/precedence/iff-assoc.cvc
+++ b/test/regress/regress0/precedence/iff-assoc.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right associativity of <=>
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc
index 947433c88..24181487d 100644
--- a/test/regress/regress0/precedence/iff-implies.cvc
+++ b/test/regress/regress0/precedence/iff-implies.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of <=> and =>.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc
index 1a7cef3b1..c6883c6ad 100644
--- a/test/regress/regress0/precedence/implies-assoc.cvc
+++ b/test/regress/regress0/precedence/implies-assoc.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right associativity of =>
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc
index 3de26eb18..9ebed72d4 100644
--- a/test/regress/regress0/precedence/implies-iff.cvc
+++ b/test/regress/regress0/precedence/implies-iff.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of <=> and =>.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc
index d724d33ef..883e7d4a1 100644
--- a/test/regress/regress0/precedence/implies-or.cvc
+++ b/test/regress/regress0/precedence/implies-or.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of => and OR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc
index fc671d7b5..579531ded 100644
--- a/test/regress/regress0/precedence/not-and.cvc
+++ b/test/regress/regress0/precedence/not-and.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of AND and NOT.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
index f658c127e..f8c7366be 100644
--- a/test/regress/regress0/precedence/not-eq.cvc
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of = and NOT.
 
 A, B: INT;
diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc
index 209df8559..746f142e4 100644
--- a/test/regress/regress0/precedence/or-implies.cvc
+++ b/test/regress/regress0/precedence/or-implies.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of => and OR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc
index 2a25bac63..405cb68b7 100644
--- a/test/regress/regress0/precedence/or-xor.cvc
+++ b/test/regress/regress0/precedence/or-xor.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of OR and XOR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc
index 5d980f90d..57b9b99cf 100644
--- a/test/regress/regress0/precedence/plus-mult.cvc
+++ b/test/regress/regress0/precedence/plus-mult.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of plus/minus and mult/divide
 
 a, b, c, d, e: INT;
diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc
index 68896db10..08c939c5e 100644
--- a/test/regress/regress0/precedence/xor-and.cvc
+++ b/test/regress/regress0/precedence/xor-and.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of XOR and AND.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc
index f31324a53..5f4646b1f 100644
--- a/test/regress/regress0/precedence/xor-assoc.cvc
+++ b/test/regress/regress0/precedence/xor-assoc.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for left associativity of XOR
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc
index 757286764..87abc0e73 100644
--- a/test/regress/regress0/precedence/xor-or.cvc
+++ b/test/regress/regress0/precedence/xor-or.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 % Simple test for right precedence of OR and XOR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc b/test/regress/regress0/preprocess/preprocess_00.cvc
index c86843535..2e51a42ad 100644
--- a/test/regress/regress0/preprocess/preprocess_00.cvc
+++ b/test/regress/regress0/preprocess/preprocess_00.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
 
diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc b/test/regress/regress0/preprocess/preprocess_02.cvc
index e2c93a359..0f94103f6 100644
--- a/test/regress/regress0/preprocess/preprocess_02.cvc
+++ b/test/regress/regress0/preprocess/preprocess_02.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
 
diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc b/test/regress/regress0/preprocess/preprocess_06.cvc
index 3e45c529a..abcc7a6ac 100644
--- a/test/regress/regress0/preprocess/preprocess_06.cvc
+++ b/test/regress/regress0/preprocess/preprocess_06.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 a0, a1, a2, a3, a4, a5: BOOLEAN;
 
diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc
index 8b26c0d08..9a6cd797c 100644
--- a/test/regress/regress0/preprocess/preprocess_13.cvc
+++ b/test/regress/regress0/preprocess/preprocess_13.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 
 a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
 
diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc
index 267a316e8..966668002 100644
--- a/test/regress/regress0/printer/tuples_and_records.cvc
+++ b/test/regress/regress0/printer/tuples_and_records.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 % EXPECT: ((r.a, "active"))
 % EXPECT: ((y.1, 9))
 OPTION "produce-models";
diff --git a/test/regress/regress0/push-pop/bug233.cvc b/test/regress/regress0/push-pop/bug233.cvc
index 2b9eedcdb..1a6049329 100644
--- a/test/regress/regress0/push-pop/bug233.cvc
+++ b/test/regress/regress0/push-pop/bug233.cvc
@@ -3,9 +3,9 @@
 
 a, b: BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY (a AND b) OR NOT (a AND b);
 
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY (a OR b);
 
diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc b/test/regress/regress0/push-pop/incremental-subst-bug.cvc
index 9b10ef843..657e74486 100644
--- a/test/regress/regress0/push-pop/incremental-subst-bug.cvc
+++ b/test/regress/regress0/push-pop/incremental-subst-bug.cvc
@@ -1,21 +1,21 @@
 % COMMAND-LINE: --incremental
 U : TYPE;
 x, y : U;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY x = y;
 ASSERT x = y;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY x = y;
 PUSH;
 z : U;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY x = y;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY x = z;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY z = x;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY z /= x;
 POP;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY z /= x;
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
index 63cf52fd6..d01d7b7d2 100644
--- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
+++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
@@ -1,2 +1,2 @@
-% EXPECT: valid
+% EXPECT: entailed
 QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;
diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc
index 6740faa8c..06d2b5049 100644
--- a/test/regress/regress0/sets/cvc-sample.cvc
+++ b/test/regress/regress0/sets/cvc-sample.cvc
@@ -4,7 +4,7 @@
 % EXPECT: unsat
 % EXPECT: unsat
 % EXPECT: unsat
-% EXPECT: invalid
+% EXPECT: not_entailed
 OPTION "incremental" true;
 OPTION "logic" "ALL_SUPPORTED";
 SetInt : TYPE = SET OF INT;
diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc
index 83d0225bd..def48254e 100644
--- a/test/regress/regress0/simple.cvc
+++ b/test/regress/regress0/simple.cvc
@@ -3,5 +3,5 @@ ASSERT x1 OR NOT x0;
 ASSERT x0 OR NOT x3;
 ASSERT x3 OR x2;
 ASSERT x1 AND NOT x1;
-% EXPECT: valid
+% EXPECT: entailed
 QUERY x2;
diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc
index bd732b4dc..dcb7c6f0d 100644
--- a/test/regress/regress0/smallcnf.cvc
+++ b/test/regress/regress0/smallcnf.cvc
@@ -4,6 +4,6 @@ ASSERT NOT a OR NOT b;
 ASSERT c OR b OR a;
 ASSERT b OR NOT a;
 ASSERT a OR NOT b OR c;
-% EXPECT: invalid
+% EXPECT: not_entailed
 QUERY FALSE;
 
diff --git a/test/regress/regress0/smtlib/set-info-status.smt2 b/test/regress/regress0/smtlib/set-info-status.smt2
index 489d686b3..4bfa1766a 100644
--- a/test/regress/regress0/smtlib/set-info-status.smt2
+++ b/test/regress/regress0/smtlib/set-info-status.smt2
@@ -1,4 +1,4 @@
-; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
+; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/ENTAILED response.")
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat
diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc
index 45052deeb..26dda442e 100644
--- a/test/regress/regress0/test11.cvc
+++ b/test/regress/regress0/test11.cvc
@@ -3,5 +3,5 @@ x, y : BOOLEAN;
 ASSERT (x OR y);
 ASSERT NOT (x OR y);
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY FALSE;
diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc
index bfe1a3285..7872f5a1a 100644
--- a/test/regress/regress0/test9.cvc
+++ b/test/regress/regress0/test9.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 P,Q:BOOLEAN;
 ASSERT (P OR Q);
 QUERY (P OR Q);
diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc
index 42b99cc44..6b0f93324 100644
--- a/test/regress/regress0/uf/simple.01.cvc
+++ b/test/regress/regress0/uf/simple.01.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 A: TYPE;
 B: TYPE;
 x, y: A;
diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc
index 1dd96fd1c..2bd0b1e1e 100644
--- a/test/regress/regress0/uf/simple.02.cvc
+++ b/test/regress/regress0/uf/simple.02.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 A: TYPE;
 B: TYPE;
 x, y: A;
diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc
index cc1721ca6..15fe5907c 100644
--- a/test/regress/regress0/uf/simple.03.cvc
+++ b/test/regress/regress0/uf/simple.03.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 A: TYPE;
 B: TYPE;
 x, y: A;
diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc
index 66223ca7b..0fc52bcca 100644
--- a/test/regress/regress0/uf/simple.04.cvc
+++ b/test/regress/regress0/uf/simple.04.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 A: TYPE;
 B: TYPE;
 x, y: A;
diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc
index 9de754284..b25d8a471 100644
--- a/test/regress/regress0/uf20-03.cvc
+++ b/test/regress/regress0/uf20-03.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;
diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc
index fb38fab65..1516503ff 100644
--- a/test/regress/regress0/wiki.01.cvc
+++ b/test/regress/regress0/wiki.01.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR (b OR c) <=> (a OR b) OR c;
diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc
index 93d555c96..ebeadee14 100644
--- a/test/regress/regress0/wiki.02.cvc
+++ b/test/regress/regress0/wiki.02.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND (b AND c) <=> (a AND b) AND c;
diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc
index 08b049c17..ca0e6a8d1 100644
--- a/test/regress/regress0/wiki.03.cvc
+++ b/test/regress/regress0/wiki.03.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR b <=> b OR a;
diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc
index b88de6144..75fe17238 100644
--- a/test/regress/regress0/wiki.04.cvc
+++ b/test/regress/regress0/wiki.04.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND b <=> b AND a;
diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
index 0fe647f7b..2f87e4ca0 100644
--- a/test/regress/regress0/wiki.05.cvc
+++ b/test/regress/regress0/wiki.05.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR (a AND b) <=> a;
diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc
index 1d466a86e..a4075bda3 100644
--- a/test/regress/regress0/wiki.06.cvc
+++ b/test/regress/regress0/wiki.06.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND (a OR b) <=> a;
diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc
index 146d92832..3b4527bdc 100644
--- a/test/regress/regress0/wiki.07.cvc
+++ b/test/regress/regress0/wiki.07.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc
index e9c7d3fa3..e15a21412 100644
--- a/test/regress/regress0/wiki.08.cvc
+++ b/test/regress/regress0/wiki.08.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc
index 478be2db9..5bc5faca5 100644
--- a/test/regress/regress0/wiki.09.cvc
+++ b/test/regress/regress0/wiki.09.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR NOT a;
diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc
index 226a3da82..613022e84 100644
--- a/test/regress/regress0/wiki.10.cvc
+++ b/test/regress/regress0/wiki.10.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND NOT a <=> FALSE;
diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc
index d615fef3b..8debef9cd 100644
--- a/test/regress/regress0/wiki.11.cvc
+++ b/test/regress/regress0/wiki.11.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR a <=> a;
diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc
index 209e512a6..2274fc78e 100644
--- a/test/regress/regress0/wiki.12.cvc
+++ b/test/regress/regress0/wiki.12.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND a <=> a;
diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc
index 2cc69f048..80b95802d 100644
--- a/test/regress/regress0/wiki.13.cvc
+++ b/test/regress/regress0/wiki.13.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR FALSE <=> a;
diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc
index 5a6c16248..7b8a14edb 100644
--- a/test/regress/regress0/wiki.14.cvc
+++ b/test/regress/regress0/wiki.14.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND TRUE <=> a;
diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc
index 6dc84f679..dfb4f13fc 100644
--- a/test/regress/regress0/wiki.15.cvc
+++ b/test/regress/regress0/wiki.15.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a OR TRUE <=> TRUE;
diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc
index 6b2bf4113..9c69baa52 100644
--- a/test/regress/regress0/wiki.16.cvc
+++ b/test/regress/regress0/wiki.16.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY a AND FALSE <=> FALSE;
diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc
index 7c6701acc..c58160bb9 100644
--- a/test/regress/regress0/wiki.17.cvc
+++ b/test/regress/regress0/wiki.17.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY NOT FALSE <=> TRUE;
diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc
index 7c1b1b8e4..17773b899 100644
--- a/test/regress/regress0/wiki.18.cvc
+++ b/test/regress/regress0/wiki.18.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY NOT TRUE <=> FALSE;
diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc
index d5812b5ea..46b6fc02e 100644
--- a/test/regress/regress0/wiki.19.cvc
+++ b/test/regress/regress0/wiki.19.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY NOT (a OR b) <=> NOT a AND NOT b;
diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc
index 8d2570620..42e114010 100644
--- a/test/regress/regress0/wiki.20.cvc
+++ b/test/regress/regress0/wiki.20.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY NOT (a AND b) <=> NOT a OR NOT b;
diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc
index d65cbcf65..bcc69beea 100644
--- a/test/regress/regress0/wiki.21.cvc
+++ b/test/regress/regress0/wiki.21.cvc
@@ -1,4 +1,4 @@
 a, b, c : BOOLEAN;
 
-% EXPECT: valid
+% EXPECT: entailed
 QUERY NOT NOT a <=> a;
diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc
index 03ed1a6ae..3fd528c11 100644
--- a/test/regress/regress1/arith/arith-int-001.cvc
+++ b/test/regress/regress1/arith/arith-int-001.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ;
 ASSERT  (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ;
diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc
index 849daba79..6cc4b2c5e 100644
--- a/test/regress/regress1/arith/arith-int-002.cvc
+++ b/test/regress/regress1/arith/arith-int-002.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ;
 ASSERT  (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ;
diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc
index 9c060c469..f294babe6 100644
--- a/test/regress/regress1/arith/arith-int-003.cvc
+++ b/test/regress/regress1/arith/arith-int-003.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ;
 ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ;
diff --git a/test/regress/regress1/arith/arith-int-004.cvc b/test/regress/regress1/arith/arith-int-004.cvc
index 314b76d18..15b060d92 100644
--- a/test/regress/regress1/arith/arith-int-004.cvc
+++ b/test/regress/regress1/arith/arith-int-004.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 
 x0, x1, x2, x3 : INT;
 ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ;
diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc
index 9b9776ad3..3701d60b4 100644
--- a/test/regress/regress1/arith/arith-int-005.cvc
+++ b/test/regress/regress1/arith/arith-int-005.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ;
 ASSERT  (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ;
diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc
index 999b4a5b4..53a80310a 100644
--- a/test/regress/regress1/arith/arith-int-006.cvc
+++ b/test/regress/regress1/arith/arith-int-006.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ;
 ASSERT  (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ;
diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc
index 4cb4d88ef..c0732e2b2 100644
--- a/test/regress/regress1/arith/arith-int-007.cvc
+++ b/test/regress/regress1/arith/arith-int-007.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ;
 ASSERT  (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ;
diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc
index 1ae22c993..1810d6f28 100644
--- a/test/regress/regress1/arith/arith-int-008.cvc
+++ b/test/regress/regress1/arith/arith-int-008.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ;
 ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ;
diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc
index 9bd7a2ce4..14b26da6c 100644
--- a/test/regress/regress1/arith/arith-int-009.cvc
+++ b/test/regress/regress1/arith/arith-int-009.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ;
 ASSERT  (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ;
diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc
index 4ac85a984..aa649ba4a 100644
--- a/test/regress/regress1/arith/arith-int-010.cvc
+++ b/test/regress/regress1/arith/arith-int-010.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ;
 ASSERT  (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ;
diff --git a/test/regress/regress1/arith/arith-int-011.cvc b/test/regress/regress1/arith/arith-int-011.cvc
index bd2fa2a0d..7de68533f 100644
--- a/test/regress/regress1/arith/arith-int-011.cvc
+++ b/test/regress/regress1/arith/arith-int-011.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ;
 ASSERT  (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9;
diff --git a/test/regress/regress1/arith/arith-int-012.cvc b/test/regress/regress1/arith/arith-int-012.cvc
index 11b0dab27..10922dd89 100644
--- a/test/regress/regress1/arith/arith-int-012.cvc
+++ b/test/regress/regress1/arith/arith-int-012.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ;
 ASSERT  (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24;
diff --git a/test/regress/regress1/arith/arith-int-013.cvc b/test/regress/regress1/arith/arith-int-013.cvc
index 329251cae..8a1f76add 100644
--- a/test/regress/regress1/arith/arith-int-013.cvc
+++ b/test/regress/regress1/arith/arith-int-013.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ;
 ASSERT  (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2;
diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc
index 6774dd2d1..951650461 100644
--- a/test/regress/regress1/arith/arith-int-016.cvc
+++ b/test/regress/regress1/arith/arith-int-016.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ;
 ASSERT  (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ;
diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc
index e9a06125a..48287249f 100644
--- a/test/regress/regress1/arith/arith-int-017.cvc
+++ b/test/regress/regress1/arith/arith-int-017.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ;
 ASSERT  (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ;
diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc
index 4cb97b77e..cae6fed72 100644
--- a/test/regress/regress1/arith/arith-int-018.cvc
+++ b/test/regress/regress1/arith/arith-int-018.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ;
 ASSERT  (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ;
diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc
index cf9ae2d70..a26bbac01 100644
--- a/test/regress/regress1/arith/arith-int-019.cvc
+++ b/test/regress/regress1/arith/arith-int-019.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ;
 ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ;
diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc
index 07a827465..c1416b38f 100644
--- a/test/regress/regress1/arith/arith-int-020.cvc
+++ b/test/regress/regress1/arith/arith-int-020.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ;
 ASSERT  (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ;
diff --git a/test/regress/regress1/arith/arith-int-022.cvc b/test/regress/regress1/arith/arith-int-022.cvc
index 584348da4..4612f72c9 100644
--- a/test/regress/regress1/arith/arith-int-022.cvc
+++ b/test/regress/regress1/arith/arith-int-022.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18;
 QUERY FALSE;
diff --git a/test/regress/regress1/arith/arith-int-024.cvc b/test/regress/regress1/arith/arith-int-024.cvc
index f57136dd1..73ae7c4ad 100644
--- a/test/regress/regress1/arith/arith-int-024.cvc
+++ b/test/regress/regress1/arith/arith-int-024.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5;
 QUERY FALSE;
diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc
index 9e69aa2d1..52f2478e0 100644
--- a/test/regress/regress1/arith/arith-int-026.cvc
+++ b/test/regress/regress1/arith/arith-int-026.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ;
 ASSERT  (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ;
diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc
index b45622fea..6c38642d2 100644
--- a/test/regress/regress1/arith/arith-int-027.cvc
+++ b/test/regress/regress1/arith/arith-int-027.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ;
 ASSERT  (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ;
diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc
index 61fee4203..7e8b78893 100644
--- a/test/regress/regress1/arith/arith-int-028.cvc
+++ b/test/regress/regress1/arith/arith-int-028.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ;
 ASSERT  (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ;
diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc
index ee49bbb68..ba49219d8 100644
--- a/test/regress/regress1/arith/arith-int-029.cvc
+++ b/test/regress/regress1/arith/arith-int-029.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ;
 ASSERT  (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ;
diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc
index 70b6a3785..a6348b107 100644
--- a/test/regress/regress1/arith/arith-int-030.cvc
+++ b/test/regress/regress1/arith/arith-int-030.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ;
 ASSERT  (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ;
diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc
index 86242f7aa..056ab622e 100644
--- a/test/regress/regress1/arith/arith-int-031.cvc
+++ b/test/regress/regress1/arith/arith-int-031.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ;
 ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ;
diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc
index 1ee4c9844..08c29108e 100644
--- a/test/regress/regress1/arith/arith-int-032.cvc
+++ b/test/regress/regress1/arith/arith-int-032.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ;
 ASSERT  (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ;
diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc
index 599ba4e9a..8259a7725 100644
--- a/test/regress/regress1/arith/arith-int-033.cvc
+++ b/test/regress/regress1/arith/arith-int-033.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ;
 ASSERT  (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ;
diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc
index ec615a785..2b5ae4f4f 100644
--- a/test/regress/regress1/arith/arith-int-034.cvc
+++ b/test/regress/regress1/arith/arith-int-034.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ;
 ASSERT  (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ;
diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc
index e7dee2484..1bad259e2 100644
--- a/test/regress/regress1/arith/arith-int-035.cvc
+++ b/test/regress/regress1/arith/arith-int-035.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ;
 ASSERT  (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ;
diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc
index 9594f9586..0eb783815 100644
--- a/test/regress/regress1/arith/arith-int-036.cvc
+++ b/test/regress/regress1/arith/arith-int-036.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ;
 ASSERT  (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ;
diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc
index 4d4422d3f..c3ed60011 100644
--- a/test/regress/regress1/arith/arith-int-037.cvc
+++ b/test/regress/regress1/arith/arith-int-037.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ;
 ASSERT  (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ;
diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc
index 476133b24..52ac2b1e3 100644
--- a/test/regress/regress1/arith/arith-int-038.cvc
+++ b/test/regress/regress1/arith/arith-int-038.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ;
 ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ;
diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc
index 9e9235ae8..cecb7f085 100644
--- a/test/regress/regress1/arith/arith-int-039.cvc
+++ b/test/regress/regress1/arith/arith-int-039.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ;
 ASSERT  (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ;
diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc
index 68502349f..f2dff7796 100644
--- a/test/regress/regress1/arith/arith-int-040.cvc
+++ b/test/regress/regress1/arith/arith-int-040.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ;
 ASSERT  (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ;
diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc
index a0c2dc0f9..9df03a9bd 100644
--- a/test/regress/regress1/arith/arith-int-041.cvc
+++ b/test/regress/regress1/arith/arith-int-041.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ;
 ASSERT  (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ;
diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc
index 7efea85e5..7a2d6d6af 100644
--- a/test/regress/regress1/arith/arith-int-043.cvc
+++ b/test/regress/regress1/arith/arith-int-043.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ;
 ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ;
diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc
index f933b014b..649532a4b 100644
--- a/test/regress/regress1/arith/arith-int-044.cvc
+++ b/test/regress/regress1/arith/arith-int-044.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 %%%% down from 24, up from 6, up from 39
 x0, x1, x2, x3 : INT;
 ASSERT  (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0;
diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc
index ca1a12ba6..2c552c915 100644
--- a/test/regress/regress1/arith/arith-int-045.cvc
+++ b/test/regress/regress1/arith/arith-int-045.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ;
 ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ;
diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc
index d4d206c6e..acf4dc9a9 100644
--- a/test/regress/regress1/arith/arith-int-046.cvc
+++ b/test/regress/regress1/arith/arith-int-046.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ;
 ASSERT  (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ;
diff --git a/test/regress/regress1/arith/arith-int-047.cvc b/test/regress/regress1/arith/arith-int-047.cvc
index 0763e5dc3..bb1225b9d 100644
--- a/test/regress/regress1/arith/arith-int-047.cvc
+++ b/test/regress/regress1/arith/arith-int-047.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10;
 ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ;
diff --git a/test/regress/regress1/arith/arith-int-048.cvc b/test/regress/regress1/arith/arith-int-048.cvc
index e7c05332d..ccc84f389 100644
--- a/test/regress/regress1/arith/arith-int-048.cvc
+++ b/test/regress/regress1/arith/arith-int-048.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ;
 ASSERT  (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ;
diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc
index 8eabc78a8..72e3b7f31 100644
--- a/test/regress/regress1/arith/arith-int-049.cvc
+++ b/test/regress/regress1/arith/arith-int-049.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ;
 ASSERT  (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ;
diff --git a/test/regress/regress1/arith/arith-int-050.cvc b/test/regress/regress1/arith/arith-int-050.cvc
index f0ba939b7..21dbfe09a 100644
--- a/test/regress/regress1/arith/arith-int-050.cvc
+++ b/test/regress/regress1/arith/arith-int-050.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ;
 ASSERT  (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ;
diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc
index 9a2497432..68654a7df 100644
--- a/test/regress/regress1/arith/arith-int-051.cvc
+++ b/test/regress/regress1/arith/arith-int-051.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ;
 ASSERT  (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ;
diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc
index 83fdc89c8..9c9433ede 100644
--- a/test/regress/regress1/arith/arith-int-052.cvc
+++ b/test/regress/regress1/arith/arith-int-052.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ;
 ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ;
diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc
index fa38fa3da..544d53fb9 100644
--- a/test/regress/regress1/arith/arith-int-053.cvc
+++ b/test/regress/regress1/arith/arith-int-053.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ;
 ASSERT  (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17;
diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc
index 9b0066966..5b4181a11 100644
--- a/test/regress/regress1/arith/arith-int-054.cvc
+++ b/test/regress/regress1/arith/arith-int-054.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ;
 ASSERT  (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ;
diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc
index 9729fb565..fdfa45848 100644
--- a/test/regress/regress1/arith/arith-int-055.cvc
+++ b/test/regress/regress1/arith/arith-int-055.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ;
 ASSERT  (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ;
diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc
index e1c3ee1da..394b3dd4e 100644
--- a/test/regress/regress1/arith/arith-int-056.cvc
+++ b/test/regress/regress1/arith/arith-int-056.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ;
 ASSERT  (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ;
diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc
index 4e7b939b4..252601514 100644
--- a/test/regress/regress1/arith/arith-int-057.cvc
+++ b/test/regress/regress1/arith/arith-int-057.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ;
 ASSERT  (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8;
diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc
index 4d964f1c6..7e2a04d45 100644
--- a/test/regress/regress1/arith/arith-int-058.cvc
+++ b/test/regress/regress1/arith/arith-int-058.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ;
 ASSERT  (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ;
diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc
index 841d9c8e1..87773679e 100644
--- a/test/regress/regress1/arith/arith-int-059.cvc
+++ b/test/regress/regress1/arith/arith-int-059.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ;
 ASSERT  (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ;
diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc
index 227cb49b1..74dd16dca 100644
--- a/test/regress/regress1/arith/arith-int-060.cvc
+++ b/test/regress/regress1/arith/arith-int-060.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ;
 ASSERT  (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ;
diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc
index 4a3cc28d0..b3bd247b2 100644
--- a/test/regress/regress1/arith/arith-int-061.cvc
+++ b/test/regress/regress1/arith/arith-int-061.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ;
 ASSERT  (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ;
diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc
index f9a3156a2..0a185eb68 100644
--- a/test/regress/regress1/arith/arith-int-062.cvc
+++ b/test/regress/regress1/arith/arith-int-062.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ;
 ASSERT  (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ;
diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc
index d88104688..13c4aae2e 100644
--- a/test/regress/regress1/arith/arith-int-063.cvc
+++ b/test/regress/regress1/arith/arith-int-063.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ;
 ASSERT  (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ;
diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc
index 21ca822e1..f50b3cd97 100644
--- a/test/regress/regress1/arith/arith-int-064.cvc
+++ b/test/regress/regress1/arith/arith-int-064.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ;
 ASSERT  (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ;
diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc
index b1b9e1b51..354eb981c 100644
--- a/test/regress/regress1/arith/arith-int-065.cvc
+++ b/test/regress/regress1/arith/arith-int-065.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ;
 ASSERT  (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ;
diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc
index 9532b4198..f53a254bd 100644
--- a/test/regress/regress1/arith/arith-int-066.cvc
+++ b/test/regress/regress1/arith/arith-int-066.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ;
 ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ;
diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc
index 5d7b52e69..61159e9aa 100644
--- a/test/regress/regress1/arith/arith-int-067.cvc
+++ b/test/regress/regress1/arith/arith-int-067.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ;
 ASSERT  (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ;
diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc
index 107a21a12..683d36801 100644
--- a/test/regress/regress1/arith/arith-int-068.cvc
+++ b/test/regress/regress1/arith/arith-int-068.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ;
 ASSERT  (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ;
diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc
index 3fab229b0..356a28013 100644
--- a/test/regress/regress1/arith/arith-int-069.cvc
+++ b/test/regress/regress1/arith/arith-int-069.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ;
 ASSERT  (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ;
diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc
index cd828da5f..791b3b8af 100644
--- a/test/regress/regress1/arith/arith-int-070.cvc
+++ b/test/regress/regress1/arith/arith-int-070.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ;
 ASSERT  (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ;
diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc
index ce5336476..d44b18b45 100644
--- a/test/regress/regress1/arith/arith-int-071.cvc
+++ b/test/regress/regress1/arith/arith-int-071.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ;
 ASSERT  (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ;
diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc
index 10222deae..fb13a6616 100644
--- a/test/regress/regress1/arith/arith-int-072.cvc
+++ b/test/regress/regress1/arith/arith-int-072.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ;
 ASSERT  (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ;
diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc
index 98e74be8f..784190cad 100644
--- a/test/regress/regress1/arith/arith-int-073.cvc
+++ b/test/regress/regress1/arith/arith-int-073.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ;
 ASSERT  (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ;
diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc
index 28cc48186..914cbe8e3 100644
--- a/test/regress/regress1/arith/arith-int-074.cvc
+++ b/test/regress/regress1/arith/arith-int-074.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ;
 ASSERT  (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ;
diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc
index 3b5131e8b..d3851e284 100644
--- a/test/regress/regress1/arith/arith-int-075.cvc
+++ b/test/regress/regress1/arith/arith-int-075.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ;
 ASSERT  (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ;
diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc
index 2c8de7cdf..25a3a7d35 100644
--- a/test/regress/regress1/arith/arith-int-076.cvc
+++ b/test/regress/regress1/arith/arith-int-076.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ;
 ASSERT  (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ;
diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc
index d14da386e..7e4482093 100644
--- a/test/regress/regress1/arith/arith-int-077.cvc
+++ b/test/regress/regress1/arith/arith-int-077.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ;
 ASSERT  (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2;
diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc
index 3197c6524..eacccc375 100644
--- a/test/regress/regress1/arith/arith-int-078.cvc
+++ b/test/regress/regress1/arith/arith-int-078.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ;
 ASSERT  (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ;
diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc
index 8be0f9a73..bf6b90c67 100644
--- a/test/regress/regress1/arith/arith-int-080.cvc
+++ b/test/regress/regress1/arith/arith-int-080.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ;
 ASSERT  (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14;
diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc
index 546148376..47cc66ae2 100644
--- a/test/regress/regress1/arith/arith-int-081.cvc
+++ b/test/regress/regress1/arith/arith-int-081.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8;
 ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ;
diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc
index 62bd45de7..a6245f036 100644
--- a/test/regress/regress1/arith/arith-int-082.cvc
+++ b/test/regress/regress1/arith/arith-int-082.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ;
 ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ;
diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc
index 6b1084353..3a7c635cc 100644
--- a/test/regress/regress1/arith/arith-int-083.cvc
+++ b/test/regress/regress1/arith/arith-int-083.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ;
 ASSERT  (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ;
diff --git a/test/regress/regress1/arith/arith-int-084.cvc b/test/regress/regress1/arith/arith-int-084.cvc
index 5f0e17afe..d4a0a966c 100644
--- a/test/regress/regress1/arith/arith-int-084.cvc
+++ b/test/regress/regress1/arith/arith-int-084.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ;
 ASSERT  (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ;
diff --git a/test/regress/regress1/arith/arith-int-085.cvc b/test/regress/regress1/arith/arith-int-085.cvc
index 74dd714e8..b1a343e73 100644
--- a/test/regress/regress1/arith/arith-int-085.cvc
+++ b/test/regress/regress1/arith/arith-int-085.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 %% down from 3
 x0, x1, x2, x3 : INT;
 ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ;
diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc
index 64c212b3c..6ee96589b 100644
--- a/test/regress/regress1/arith/arith-int-086.cvc
+++ b/test/regress/regress1/arith/arith-int-086.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ;
 ASSERT  (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ;
diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc
index 312c08917..b969df1a3 100644
--- a/test/regress/regress1/arith/arith-int-087.cvc
+++ b/test/regress/regress1/arith/arith-int-087.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ;
 ASSERT  (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ;
diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc
index 5212640be..de0d23844 100644
--- a/test/regress/regress1/arith/arith-int-088.cvc
+++ b/test/regress/regress1/arith/arith-int-088.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ;
 ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ;
diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc
index 7ff36d29e..e50daa9de 100644
--- a/test/regress/regress1/arith/arith-int-089.cvc
+++ b/test/regress/regress1/arith/arith-int-089.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ;
 ASSERT  (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ;
diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc
index 52b9c13f0..74d4ba4db 100644
--- a/test/regress/regress1/arith/arith-int-090.cvc
+++ b/test/regress/regress1/arith/arith-int-090.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ;
 ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ;
diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc
index 29a19db39..c03b544a3 100644
--- a/test/regress/regress1/arith/arith-int-091.cvc
+++ b/test/regress/regress1/arith/arith-int-091.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ;
 ASSERT  (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ;
diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc
index 51c8a6bc4..d080cde0c 100644
--- a/test/regress/regress1/arith/arith-int-092.cvc
+++ b/test/regress/regress1/arith/arith-int-092.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ;
 ASSERT  (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ;
diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc
index 7d2123d41..e910def47 100644
--- a/test/regress/regress1/arith/arith-int-093.cvc
+++ b/test/regress/regress1/arith/arith-int-093.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ;
 ASSERT  (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ;
diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc
index a5f1aefce..2204bba4e 100644
--- a/test/regress/regress1/arith/arith-int-094.cvc
+++ b/test/regress/regress1/arith/arith-int-094.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ;
 ASSERT  (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ;
diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc
index bc47d6f49..e803dbe9b 100644
--- a/test/regress/regress1/arith/arith-int-095.cvc
+++ b/test/regress/regress1/arith/arith-int-095.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x0, x1, x2, x3 : INT;
 ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ;
 ASSERT  (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ;
diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc
index 2f6cf3155..354ae180d 100644
--- a/test/regress/regress1/arith/arith-int-096.cvc
+++ b/test/regress/regress1/arith/arith-int-096.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ;
 ASSERT  (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28;
diff --git a/test/regress/regress1/arith/arith-int-097.cvc b/test/regress/regress1/arith/arith-int-097.cvc
index b05061192..67eb614eb 100644
--- a/test/regress/regress1/arith/arith-int-097.cvc
+++ b/test/regress/regress1/arith/arith-int-097.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ;
 ASSERT  (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ;
diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc
index 0d74dcb39..57a45de03 100644
--- a/test/regress/regress1/arith/arith-int-099.cvc
+++ b/test/regress/regress1/arith/arith-int-099.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ;
 ASSERT  (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ;
diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc
index 7e07bee14..66be1f8f7 100644
--- a/test/regress/regress1/arith/arith-int-100.cvc
+++ b/test/regress/regress1/arith/arith-int-100.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ;
 ASSERT  (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ;
diff --git a/test/regress/regress1/boolean.cvc b/test/regress/regress1/boolean.cvc
index eb0e7ab52..2c861c0f0 100644
--- a/test/regress/regress1/boolean.cvc
+++ b/test/regress/regress1/boolean.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 p : BOOLEAN;
 q : BOOLEAN;
 r : BOOLEAN;
diff --git a/test/regress/regress1/fmf/ko-bound-set.cvc b/test/regress/regress1/fmf/ko-bound-set.cvc
index eebcbc2f8..5306a1513 100644
--- a/test/regress/regress1/fmf/ko-bound-set.cvc
+++ b/test/regress/regress1/fmf/ko-bound-set.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 OPTION "finite-model-find";
 OPTION "fmf-bound-int";
 OPTION "produce-models";
diff --git a/test/regress/regress1/hole6.cvc b/test/regress/regress1/hole6.cvc
index dfa9b72d5..5ec31d801 100644
--- a/test/regress/regress1/hole6.cvc
+++ b/test/regress/regress1/hole6.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;
diff --git a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc
index f7407a2a5..6f2a8764b 100644
--- a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc
+++ b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 OPTION "finite-model-find";
 OPTION "fmf-bound-int";
 
diff --git a/test/regress/regress1/test12.cvc b/test/regress/regress1/test12.cvc
index 37687bee1..39ced0428 100644
--- a/test/regress/regress1/test12.cvc
+++ b/test/regress/regress1/test12.cvc
@@ -1,34 +1,34 @@
 % COMMAND-LINE: --incremental
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: valid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: valid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: valid
-% EXPECT: valid
-% EXPECT: valid
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: entailed
+% EXPECT: entailed
+% EXPECT: entailed
 A: TYPE;
 P_1: BOOLEAN;
 P_2: BOOLEAN;
diff --git a/test/regress/regress2/arith/arith-int-098.cvc b/test/regress/regress2/arith/arith-int-098.cvc
index 08cfd9c9c..cf20f2b61 100644
--- a/test/regress/regress2/arith/arith-int-098.cvc
+++ b/test/regress/regress2/arith/arith-int-098.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 x0, x1, x2, x3 : INT;
 ASSERT  (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ;
 ASSERT  (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12;
diff --git a/test/regress/regress2/hole7.cvc b/test/regress/regress2/hole7.cvc
index 1f762477a..e73588bad 100644
--- a/test/regress/regress2/hole7.cvc
+++ b/test/regress/regress2/hole7.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;
diff --git a/test/regress/regress2/hole8.cvc b/test/regress/regress2/hole8.cvc
index 705c95ea6..a46c4da97 100644
--- a/test/regress/regress2/hole8.cvc
+++ b/test/regress/regress2/hole8.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;
diff --git a/test/regress/regress2/typed_v1l50016-simp.cvc b/test/regress/regress2/typed_v1l50016-simp.cvc
index b4a1e4b32..1d576ab74 100644
--- a/test/regress/regress2/typed_v1l50016-simp.cvc
+++ b/test/regress/regress2/typed_v1l50016-simp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: invalid
+% EXPECT: not_entailed
 
 DATATYPE
   nat = succ(pred : nat) | zero,
diff --git a/test/regress/regress3/hole9.cvc b/test/regress/regress3/hole9.cvc
index e60839f7b..b86b3b039 100644
--- a/test/regress/regress3/hole9.cvc
+++ b/test/regress/regress3/hole9.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;
diff --git a/test/regress/regress4/hole10.cvc b/test/regress/regress4/hole10.cvc
index ebc8279d3..fb4c41b35 100644
--- a/test/regress/regress4/hole10.cvc
+++ b/test/regress/regress4/hole10.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index 141db4eea..2ce50949b 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -29,8 +29,8 @@ int main() {
   ExprManager em;
   Options opts;
   SmtEngine smt(&em);
-  Result r = smt.query(em.mkConst(true));
+  Result r = smt.checkEntailed(em.mkConst(true));
 
-  return (Result::VALID == r) ? 0 : 1;
+  return (Result::ENTAILED == r) ? 0 : 1;
 }
 
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp
index fb9714d4b..2924359e8 100644
--- a/test/system/statistics.cpp
+++ b/test/system/statistics.cpp
@@ -35,9 +35,10 @@ int main() {
   Expr y = em.mkVar("y", em.integerType());
   smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
   Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
-  Result r = smt.query(q);
+  Result r = smt.checkEntailed(q);
 
-  if(r != Result::INVALID) {
+  if (r != Result::NOT_ENTAILED)
+  {
     exit(1);
   }
 
@@ -47,7 +48,7 @@ int main() {
   }
 
   smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
-  r = smt.query(q);
+  r = smt.checkEntailed(q);
   Statistics stats2 = smt.getStatistics();
   bool different = false;
   for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
@@ -68,5 +69,5 @@ int main() {
   }
 #endif /* CVC4_STATISTICS_ON */
 
-  return r == Result::VALID ? 0 : 1;
+  return r == Result::ENTAILED ? 0 : 1;
 }
diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp
index a7266e0b0..8698fde0e 100644
--- a/test/system/two_smt_engines.cpp
+++ b/test/system/two_smt_engines.cpp
@@ -28,9 +28,9 @@ int main() {
   Options opts;
   SmtEngine smt(&em);
   SmtEngine smt2(&em);
-  Result r = smt.query(em.mkConst(true));
-  Result r2 = smt2.query(em.mkConst(true));
+  Result r = smt.checkEntailed(em.mkConst(true));
+  Result r2 = smt2.checkEntailed(em.mkConst(true));
 
-  return r == Result::VALID && r2 == Result::VALID ? 0 : 1;
+  return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1;
 }
 
diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
index ab5d65e72..cbfc9cf23 100644
--- a/test/unit/api/result_black.h
+++ b/test/unit/api/result_black.h
@@ -29,9 +29,8 @@ class ResultBlack : public CxxTest::TestSuite
   void testIsSat();
   void testIsUnsat();
   void testIsSatUnknown();
-  void testIsValid();
-  void testIsInvalid();
-  void testIsValidUnknown();
+  void testIsEntailed();
+  void testIsEntailmentUnknown();
 
  private:
   std::unique_ptr<Solver> d_solver;
@@ -44,9 +43,9 @@ void ResultBlack::testIsNull()
   TS_ASSERT(!res_null.isSat());
   TS_ASSERT(!res_null.isUnsat());
   TS_ASSERT(!res_null.isSatUnknown());
-  TS_ASSERT(!res_null.isValid());
-  TS_ASSERT(!res_null.isInvalid());
-  TS_ASSERT(!res_null.isValidUnknown());
+  TS_ASSERT(!res_null.isEntailed());
+  TS_ASSERT(!res_null.isNotEntailed());
+  TS_ASSERT(!res_null.isEntailmentUnknown());
   Sort u_sort = d_solver->mkUninterpretedSort("u");
   Term x = d_solver->mkVar(u_sort, "x");
   d_solver->assertFormula(x.eqTerm(x));
@@ -100,27 +99,24 @@ void ResultBlack::testIsSatUnknown()
   TS_ASSERT(res.isSatUnknown());
 }
 
-void ResultBlack::testIsValid()
+void ResultBlack::testIsEntailed()
 {
+  d_solver->setOption("incremental", "true");
   Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkValid();
-  TS_ASSERT(res.isValid());
-  TS_ASSERT(!res.isValidUnknown());
-}
-
-void ResultBlack::testIsInvalid()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res = d_solver->checkValid();
-  TS_ASSERT(res.isInvalid());
-  TS_ASSERT(!res.isValidUnknown());
+  Term x = d_solver->mkConst(u_sort, "x");
+  Term y = d_solver->mkConst(u_sort, "y");
+  Term a = x.eqTerm(y).notTerm();
+  Term b = x.eqTerm(y);
+  d_solver->assertFormula(a);
+  Result entailed = d_solver->checkEntailed(a);
+  TS_ASSERT(entailed.isEntailed());
+  TS_ASSERT(!entailed.isEntailmentUnknown());
+  Result not_entailed = d_solver->checkEntailed(b);
+  TS_ASSERT(not_entailed.isNotEntailed());
+  TS_ASSERT(!not_entailed.isEntailmentUnknown());
 }
 
-void ResultBlack::testIsValidUnknown()
+void ResultBlack::testIsEntailmentUnknown()
 {
   d_solver->setLogic("QF_NIA");
   d_solver->setOption("incremental", "false");
@@ -128,9 +124,9 @@ void ResultBlack::testIsValidUnknown()
   Sort int_sort = d_solver->getIntegerSort();
   Term x = d_solver->mkVar(int_sort, "x");
   d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkValid();
-  TS_ASSERT(!res.isValid());
-  TS_ASSERT(res.isValidUnknown());
+  Result res = d_solver->checkEntailed(x.eqTerm(x));
+  TS_ASSERT(!res.isEntailed());
+  TS_ASSERT(res.isEntailmentUnknown());
   TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
 }
 
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 0eefde700..9fd1b7789 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -95,10 +95,9 @@ class SolverBlack : public CxxTest::TestSuite
   void testPop3();
 
   void testSimplify();
-  void testCheckValid1();
-  void testCheckValid2();
-  void testCheckValidAssuming1();
-  void testCheckValidAssuming2();
+  void testCheckEntailed();
+  void testCheckEntailed1();
+  void testCheckEntailed2();
 
   void testSetInfo();
   void testSetLogic();
@@ -1104,51 +1103,28 @@ void SolverBlack::testSimplify()
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
 }
 
-void SolverBlack::testCheckValid1()
+void SolverBlack::testCheckEntailed()
 {
   d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-  TS_ASSERT_THROWS(d_solver->checkValid(), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
+                   CVC4ApiException&);
 }
 
-void SolverBlack::testCheckValid2()
+void SolverBlack::testCheckEntailed1()
 {
+  Sort boolSort = d_solver->getBooleanSort();
+  Term x = d_solver->mkConst(boolSort, "x");
+  Term y = d_solver->mkConst(boolSort, "y");
+  Term z = d_solver->mkTerm(AND, x, y);
   d_solver->setOption("incremental", "true");
-
-  Sort realSort = d_solver->getRealSort();
-  Sort intSort = d_solver->getIntegerSort();
-
-  // Constants
-  Term x = d_solver->mkConst(intSort, "x");
-  Term y = d_solver->mkConst(realSort, "y");
-  // Values
-  Term three = d_solver->mkReal(3);
-  Term neg2 = d_solver->mkReal(-2);
-  Term two_thirds = d_solver->mkReal(2, 3);
-  // Terms
-  Term three_y = d_solver->mkTerm(MULT, three, y);
-  Term diff = d_solver->mkTerm(MINUS, y, x);
-  // Formulas
-  Term x_geq_3y = d_solver->mkTerm(GEQ, x, three_y);
-  Term x_leq_y = d_solver->mkTerm(LEQ, x, y);
-  Term neg2_lt_x = d_solver->mkTerm(LT, neg2, x);
-  // Assertions
-  Term assertions = d_solver->mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-  d_solver->assertFormula(assertions);
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-}
-
-void SolverBlack::testCheckValidAssuming1()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->checkValidAssuming(d_solver->mkTrue()),
-                   CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
 }
 
-void SolverBlack::testCheckValidAssuming2()
+void SolverBlack::testCheckEntailed2()
 {
   d_solver->setOption("incremental", "true");
 
@@ -1185,15 +1161,15 @@ void SolverBlack::testCheckValidAssuming2()
                            p_f_y                             // p(f(y))
                        });
 
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
   d_solver->assertFormula(assertions);
   TS_ASSERT_THROWS_NOTHING(
-      d_solver->checkValidAssuming(d_solver->mkTerm(DISTINCT, x, y)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(
+      d_solver->checkEntailed(d_solver->mkTerm(DISTINCT, x, y)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(
       {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
-  TS_ASSERT_THROWS(d_solver->checkValidAssuming(n), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->checkEntailed(n), CVC4ApiException&);
   TS_ASSERT_THROWS(
-      d_solver->checkValidAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
+      d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
       CVC4ApiException&);
 }