Add mkInteger to the API (#5274)

This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:

Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

45 files changed, 355 insertions, 257 deletions

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 191bb83bd..307c30709 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -58,8 +58,8 @@ int main()
   Term p = slv.mkConst(intPred, "p");
 
   // Constants
-  Term zero = slv.mkReal(0);
-  Term one = slv.mkReal(1);
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
 
   // Terms
   Term f_x = slv.mkTerm(APPLY_UF, f, x);
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 00c0b9810..d9d3c9e9c 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -39,7 +39,7 @@ void test(Solver& slv, Sort& consListSort)
   Term t = slv.mkTerm(
       APPLY_CONSTRUCTOR,
       consList.getConstructorTerm("cons"),
-      slv.mkReal(0),
+      slv.mkInteger(0),
       slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
 
   std::cout << "t is " << t << std::endl
@@ -124,7 +124,7 @@ void test(Solver& slv, Sort& consListSort)
             << "sort of cons is "
             << paramConsList.getConstructorTerm("cons").getSort() << std::endl
             << std::endl;
-  Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50));
+  Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50));
   std::cout << "Assert " << assertion << std::endl;
   slv.assertFormula(assertion);
   std::cout << "Expect sat." << std::endl;
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 2d6636d0f..2e70460af 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -39,8 +39,8 @@ int main()
   Term y = slv.mkConst(real, "y");
 
   // Constants
-  Term three = slv.mkReal(3);
-  Term neg2 = slv.mkReal(-2);
+  Term three = slv.mkInteger(3);
+  Term neg2 = slv.mkInteger(-2);
   Term two_thirds = slv.mkReal(2, 3);
 
   // Terms
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 253365c9d..ed3fe0be5 100644
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -46,8 +46,8 @@ if __name__ == "__main__":
     p = slv.mkConst(intPred, "p")
 
     # Constants
-    zero = slv.mkReal(0)
-    one = slv.mkReal(1)
+    zero = slv.mkInteger(0)
+    one = slv.mkInteger(1)
 
     # Terms
     f_x = slv.mkTerm(kinds.ApplyUf, f, x)
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 8ae2c29fd..6eef4478d 100644
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -33,7 +33,7 @@ def test(slv, consListSort):
     # "nil" is a constructor too
 
     t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"),
-                   slv.mkReal(0),
+                   slv.mkInteger(0),
                    slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil")))
 
     print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
@@ -82,7 +82,7 @@ def test(slv, consListSort):
     print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
     print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort())
 
-    assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkReal(50))
+    assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkInteger(50))
     print("Assert", assertion)
     slv.assertFormula(assertion)
     print("Expect sat.")
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index f85171150..94ce730a3 100644
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -33,8 +33,8 @@ if __name__ == "__main__":
     y = slv.mkConst(real, "y")
 
     # Constants
-    three = slv.mkReal(3)
-    neg2 = slv.mkReal(-2)
+    three = slv.mkInteger(3)
+    neg2 = slv.mkInteger(-2)
     two_thirds = slv.mkReal(2, 3)
 
     # Terms
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
index 1b0c34f44..7ed5448cd 100644
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -42,9 +42,9 @@ if __name__ == "__main__":
     # Sequence length: |x.y.empty|
     concat_len = slv.mkTerm(kinds.SeqLength, concat)
     # |x.y.empty| > 1
-    formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkReal(1))
+    formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1))
     # Sequence unit: seq(1)
-    unit = slv.mkTerm(kinds.SeqUnit, slv.mkReal(1))
+    unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1))
     # x = seq(1)
     formula2 = slv.mkTerm(kinds.Equal, x, unit)
 
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 67d9808e7..77de3e5b3 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -62,9 +62,9 @@ if __name__ == "__main__":
 
     # Find me an element in 1, 2 intersection 2, 3, if there is one.
 
-    one = slv.mkReal(1)
-    two = slv.mkReal(2)
-    three = slv.mkReal(3)
+    one = slv.mkInteger(1)
+    two = slv.mkInteger(2)
+    three = slv.mkInteger(3)
 
     singleton_one = slv.mkSingleton(integer, one)
     singleton_two = slv.mkSingleton(integer, two)
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index c007b4bb5..1e85c56bb 100644
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -51,7 +51,7 @@ if __name__ == "__main__":
     # Length of y: |y|
     leny = slv.mkTerm(kinds.StringLength, y)
     # |y| >= 0
-    formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkReal(0))
+    formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkInteger(0))
 
     # Regular expression: (ab[c-e]*f)|g|h
     r = slv.mkTerm(kinds.RegexpUnion,
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index d331c9f9e..a85902961 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -41,8 +41,8 @@ if __name__ == "__main__":
   start_bool = slv.mkVar(boolean, "StartBool")
 
   # define the rules
-  zero = slv.mkReal(0)
-  one = slv.mkReal(1)
+  zero = slv.mkInteger(0)
+  one = slv.mkInteger(1)
 
   plus = slv.mkTerm(kinds.Plus, start, start)
   minus = slv.mkTerm(kinds.Minus, start, start)
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 7a8f89c68..cfa342f35 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -38,7 +38,7 @@ if __name__ == "__main__":
   start = slv.mkVar(integer, "Start")
 
   # define the rules
-  zero = slv.mkReal(0)
+  zero = slv.mkInteger(0)
   neg_x = slv.mkTerm(kinds.Uminus, x)
   plus = slv.mkTerm(kinds.Plus, x, start)
 
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index f71091371..4e7465382 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -30,9 +30,9 @@ if __name__ == "__main__":
   integer = slv.getIntegerSort()
   boolean = slv.getBooleanSort()
 
-  zero = slv.mkReal(0)
-  one = slv.mkReal(1)
-  ten = slv.mkReal(10)
+  zero = slv.mkInteger(0)
+  one = slv.mkInteger(1)
+  ten = slv.mkInteger(10)
 
   # declare input variables for functions
   x = slv.mkVar(integer, "x")
diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp
index 3783d35c4..63d5aac96 100644
--- a/examples/api/sequences.cpp
+++ b/examples/api/sequences.cpp
@@ -47,9 +47,9 @@ int main()
   // Sequence length: |x.y.empty|
   Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
   // |x.y.empty| > 1
-  Term formula1 = slv.mkTerm(GT, concat_len, slv.mkReal(1));
+  Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1));
   // Sequence unit: seq(1)
-  Term unit = slv.mkTerm(SEQ_UNIT, slv.mkReal(1));
+  Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1));
   // x = seq(1)
   Term formula2 = slv.mkTerm(EQUAL, x, unit);
 
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index fd85858a2..549b68e0d 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -69,9 +69,9 @@ int main()
 
   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
   {
-    Term one = slv.mkReal(1);
-    Term two = slv.mkReal(2);
-    Term three = slv.mkReal(3);
+    Term one = slv.mkInteger(1);
+    Term two = slv.mkInteger(2);
+    Term three = slv.mkInteger(3);
 
     Term singleton_one = slv.mkSingleton(integer, one);
     Term singleton_two = slv.mkSingleton(integer, two);
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index ad8df9ffa..556c49c8e 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -56,7 +56,7 @@ int main()
   // Length of y: |y|
   Term leny = slv.mkTerm(STRING_LENGTH, y);
   // |y| >= 0
-  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0));
+  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
 
   // Regular expression: (ab[c-e]*f)|g|h
   Term r = slv.mkTerm(REGEXP_UNION,
diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index b85529554..b2d6e9215 100644
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -74,8 +74,8 @@ int main()
   Term start_bool = slv.mkVar(boolean, "StartBool");
 
   // define the rules
-  Term zero = slv.mkReal(0);
-  Term one = slv.mkReal(1);
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
 
   Term plus = slv.mkTerm(PLUS, start, start);
   Term minus = slv.mkTerm(MINUS, start, start);
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index 4cfbe84fa..ea8256c70 100644
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -69,7 +69,7 @@ int main()
   Term start = slv.mkVar(integer, "Start");
 
   // define the rules
-  Term zero = slv.mkReal(0);
+  Term zero = slv.mkInteger(0);
   Term neg_x = slv.mkTerm(UMINUS, x);
   Term plus = slv.mkTerm(PLUS, x, start);
 
diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 710265113..d57d9be4e 100644
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -53,9 +53,9 @@ int main()
   Sort integer = slv.getIntegerSort();
   Sort boolean = slv.getBooleanSort();
 
-  Term zero = slv.mkReal(0);
-  Term one = slv.mkReal(1);
-  Term ten = slv.mkReal(10);
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
+  Term ten = slv.mkInteger(10);
 
   // declare input variables for functions
   Term x = slv.mkVar(integer, "x");
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 49a4f576e..e648b9994 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -32,16 +32,16 @@ int main() {
 
   Term x = slv.mkConst(integer, "x");
   Term y = slv.mkConst(integer, "y");
-  Term zero = slv.mkReal(0);
+  Term zero = slv.mkInteger(0);
 
   Term x_positive = slv.mkTerm(Kind::GT, x, zero);
   Term y_positive = slv.mkTerm(Kind::GT, y, zero);
 
-  Term two = slv.mkReal(2);
+  Term two = slv.mkInteger(2);
   Term twox = slv.mkTerm(Kind::MULT, two, x);
   Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y);
 
-  Term three = slv.mkReal(3);
+  Term three = slv.mkInteger(3);
   Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three);
 
   Term formula =
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 7596b4771..538cb359f 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -40,7 +40,7 @@ int main() {
   std::cout << "Made expression : " << quantpospx << std::endl;
 
   //make ~P( 5 )
-  Term five = slv.mkReal(5);
+  Term five = slv.mkInteger(5);
   Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five);
   Term negpfive = slv.mkTerm(Kind::NOT, pfive);
   std::cout << "Made expression : " << negpfive << std::endl;
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be82a517f..507e270bb 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -34,6 +34,7 @@
 #include "api/cvc4cpp.h"
 
 #include <cstring>
+#include <regex>
 #include <sstream>
 
 #include "base/check.h"
@@ -1603,7 +1604,7 @@ Kind Term::getKindHelper() const
   // (string) versions back to sequence. All operators where this is
   // necessary are such that their first child is of sequence type, which
   // we check here.
-  if (getNumChildren() > 0 && (*this)[0].getSort().isSequence())
+  if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence())
   {
     switch (d_node->getKind())
     {
@@ -1626,9 +1627,22 @@ Kind Term::getKindHelper() const
   }
   // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
   // INTERNAL_KIND.
+  if(isCastedReal())
+  {
+    return CONST_RATIONAL;
+  }
   return intToExtKind(d_node->getKind());
 }
 
+bool Term::isCastedReal() const
+{
+  if(d_node->getKind() == kind::CAST_TO_REAL)
+  {
+    return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger();
+  }
+  return false;
+}
+
 bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; }
 
 bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; }
@@ -1649,12 +1663,20 @@ size_t Term::getNumChildren() const
   {
     return d_node->getNumChildren() + 1;
   }
+  if(isCastedReal())
+  {
+    return 0;
+  }
   return d_node->getNumChildren();
 }
 
 Term Term::operator[](size_t index) const
 {
   CVC4_API_CHECK_NOT_NULL;
+
+  // check the index within the number of children
+  CVC4_API_CHECK(index < getNumChildren()) << "index out of bound";
+
   // special cases for apply kinds
   if (isApplyKind(d_node->getKind()))
   {
@@ -1763,12 +1785,6 @@ Op Term::getOp() const
 
 bool Term::isNull() const { return isNullHelper(); }
 
-bool Term::isValue() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return d_node->isConst();
-}
-
 Term Term::getConstArrayBase() const
 {
   CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
@@ -3109,16 +3125,20 @@ Term Solver::mkValHelper(T t) const
 
 Term Solver::mkRealFromStrHelper(const std::string& s) const
 {
-  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
-   * throws an std::invalid_argument exception. For consistency, we treat it
-   * as invalid. */
-  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
-      << "a string representing an integer, real or rational value.";
-
-  CVC4::Rational r = s.find('/') != std::string::npos
-                         ? CVC4::Rational(s)
-                         : CVC4::Rational::fromDecimal(s);
-  return mkValHelper<CVC4::Rational>(r);
+  try
+  {
+    CVC4::Rational r = s.find('/') != std::string::npos
+                           ? CVC4::Rational(s)
+                           : CVC4::Rational::fromDecimal(s);
+    return mkValHelper<CVC4::Rational>(r);
+  }
+  catch (const std::invalid_argument& e)
+  {
+    std::stringstream message;
+    message << "Cannot construct Real or Int from string argument '" << s << "'"
+            << std::endl;
+    throw std::invalid_argument(message.str());
+  }
 }
 
 Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
@@ -3725,24 +3745,66 @@ Term Solver::mkPi() const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkInteger(const std::string& s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(std::regex_match(s, std::regex("-?\\d+")), s)
+      << " an integer ";
+  Term integer = mkRealFromStrHelper(s);
+  CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s)
+      << " an integer";
+  return integer;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkInteger(int64_t val) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Term integer = mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  Assert(integer.getSort() == getIntegerSort());
+  return integer;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkReal(const std::string& s) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkRealFromStrHelper(s);
+  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+   * throws an std::invalid_argument exception. For consistency, we treat it
+   * as invalid. */
+  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
+      << "a string representing a real or rational value.";
+  Term rational = mkRealFromStrHelper(s);
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::ensureRealSort(const Term t) const
+{
+  CVC4_API_ARG_CHECK_EXPECTED(
+      t.getSort() == getIntegerSort() || t.getSort() == getRealSort(),
+      " an integer or real term");
+  if (t.getSort() == getIntegerSort())
+  {
+    Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node);
+    return Term(this, n);
+  }
+  return t;
+}
+
 Term Solver::mkReal(int64_t val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkReal(int64_t num, int64_t den) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3918,10 +3980,17 @@ Term Solver::mkConstArray(Sort sort, Term val) const
   CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
-  CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
+  CVC4_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort()))
       << "Value does not match element sort.";
-  Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll(
-      TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr())));
+  // handle the special case of (CAST_TO_REAL n) where n is an integer
+  Node n = *val.d_node;
+  if (val.isCastedReal())
+  {
+    // this is safe because the constant array stores its type
+    n = n[0];
+  }
+  Term res = mkValHelper<CVC4::ArrayStoreAll>(
+      CVC4::ArrayStoreAll(TypeNode::fromType(*sort.d_type), n));
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 646695c64..c05390e42 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -982,13 +982,6 @@ class CVC4_PUBLIC Term
   bool isNull() const;
 
   /**
-   * Check if this is a Term representing a value.
-   *
-   * @return true if this is a Term representing a value
-   */
-  bool isValue() const;
-
-  /**
    *  Return the base (element stored at all indices) of a constant array
    *  throws an exception if the kind is not CONST_ARRAY
    *  @return the base value
@@ -1176,6 +1169,11 @@ class CVC4_PUBLIC Term
   Kind getKindHelper() const;
 
   /**
+   * returns true if the current term is a constant integer that is casted into
+   * real using the operator CAST_TO_REAL, and returns false otherwise
+   */
+  bool isCastedReal() const;
+  /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
    * memory allocation (CVC4::Expr is already ref counted, so this could be
@@ -2580,12 +2578,26 @@ class CVC4_PUBLIC Solver
    * @return a constant representing Pi
    */
   Term mkPi() const;
+  /**
+   * Create an integer constant from a string.
+   * @param s the string representation of the constant, may represent an
+   *          integer (e.g., "123").
+   * @return a constant of sort Integer assuming 's' represents an integer)
+   */
+  Term mkInteger(const std::string& s) const;
+
+  /**
+   * Create an integer constant from a c++ int.
+   * @param val the value of the constant
+   * @return a constant of sort Integer
+   */
+  Term mkInteger(int64_t val) const;
 
   /**
    * Create a real constant from a string.
    * @param s the string representation of the constant, may represent an
    *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
-   * @return a constant of sort Real or Integer (if 's' represents an integer)
+   * @return a constant of sort Real
    */
   Term mkReal(const std::string& s) const;
 
@@ -2600,7 +2612,7 @@ class CVC4_PUBLIC Solver
    * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
+   * @return a constant of sort Real
    */
   Term mkReal(int64_t num, int64_t den) const;
 
@@ -3461,10 +3473,10 @@ class CVC4_PUBLIC Solver
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
    * to being of sort integer).
-   * @param term a term of sort integer or real
+   * @param t a term of sort integer or real
    * @return a term of sort real
    */
-  Term ensureRealSort(Term expr) const;
+  Term ensureRealSort(Term t) const;
 
   /**
    * Create n-ary term of given kind. This handles the cases of left/right
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 73ccde14a..113895ad7 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -173,6 +173,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term mkFalse() except +
         Term mkBoolean(bint val) except +
         Term mkPi() except +
+        Term mkInteger(const string& s) except +
         Term mkReal(const string& s) except +
         Term mkRegexpEmpty() except +
         Term mkRegexpSigma() except +
@@ -329,7 +330,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
-        bint isValue() except +
         Term getConstArrayBase() except +
         vector[Term] getConstSequenceElements() except +
         Term notTerm() except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 188b678d1..4cdd60893 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -664,6 +664,12 @@ cdef class Solver:
         term.cterm = self.csolver.mkPi()
         return term
 
+    def mkInteger(self, val):
+        cdef Term term = Term(self)
+        integer = int(val)
+        term.cterm = self.csolver.mkInteger("{}".format(integer).encode())
+        return term
+
     def mkReal(self, val, den=None):
         cdef Term term = Term(self)
         if den is None:
@@ -1448,9 +1454,6 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
-    def isValue(self):
-        return self.cterm.isValue()
-
     def getConstArrayBase(self):
         cdef Term term = Term(self.solver)
         term.cterm = self.cterm.getConstArrayBase()
@@ -1502,7 +1505,6 @@ cdef class Term:
     def toPythonObj(self):
         '''
         Converts a constant value Term to a Python object.
-        Requires isValue to hold.
 
         Currently supports:
           Boolean -- returns a Python bool
@@ -1514,9 +1516,6 @@ cdef class Term:
           String  -- returns a Python Unicode string
         '''
 
-        if not self.isValue():
-            raise RuntimeError("Cannot call toPythonObj on a non-const Term")
-
         string_repr = self.cterm.toString().decode()
         assert string_repr
         sort = self.getSort()
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 92383dcd1..ed21f8f9c 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -45,7 +45,8 @@ ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value)
       "expr type `%s' does not match constituent type of array type `%s'",
       value.getType().toString().c_str(),
       type.toString().c_str());
-
+  Trace("arrays") << "constructing constant array of type: '" << type
+                  << "' and value: '" << value << "'" << std::endl;
   PrettyCheckArgument(
       value.isConst(), value, "ArrayStoreAll requires a constant expression");
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 292871d2a..0bb41b483 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2177,13 +2177,6 @@ simpleTerm[CVC4::api::Term& f]
        * literals, we can use the push/pop scope. */
       /* PARSER_STATE->popScope(); */
       t = SOLVER->mkArraySort(t, t2);
-      if(!f.isValue()) {
-        std::stringstream ss;
-        ss << "expected constant term inside array constant, but found "
-           << "nonconstant term" << std::endl
-           << "the term: " << f;
-        PARSER_STATE->parseError(ss.str());
-      }
       if(!t2.isComparableTo(f.getSort())) {
         std::stringstream ss;
         ss << "type mismatch inside array constant term:" << std::endl
@@ -2207,18 +2200,12 @@ simpleTerm[CVC4::api::Term& f]
       std::stringstream strRat;
       strRat << r;
       f = SOLVER->mkReal(strRat.str());
-      if(f.getSort().isInteger()) {
-        // Must cast to Real to ensure correct type is passed to parametric type constructors.
-        // We do this cast using division with 1.
-        // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory.
-        f = MK_TERM(api::DIVISION, f, SOLVER->mkReal(1));
-      }
     }
   | INTEGER_LITERAL {
       Rational r = AntlrInput::tokenToRational($INTEGER_LITERAL);
       std::stringstream strRat;
       strRat << r;
-      f = SOLVER->mkReal(strRat.str());
+      f = SOLVER->mkInteger(strRat.str());
     }
     /* bitvector literals */
   | HEX_LITERAL
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7c1c5dc3e..7647f8e53 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1710,7 +1710,7 @@ identifier[CVC4::ParseOp& p]
         // we adopt a special syntax (_ tupSel n)
         p.d_kind = api::APPLY_SELECTOR;
         // put m in expr so that the caller can deal with this case
-        p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m));
+        p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
@@ -1735,7 +1735,7 @@ termAtomic[CVC4::api::Term& atomTerm]
   : INTEGER_LITERAL
     {
       std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
-      atomTerm = SOLVER->mkReal(intStr);
+      atomTerm = SOLVER->mkInteger(intStr);
     }
   | DECIMAL_LITERAL
     {
@@ -1830,7 +1830,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
     {
       std::stringstream sIntLit;
       sIntLit << $INTEGER_LITERAL;
-      api::Term n = SOLVER->mkReal(sIntLit.str());
+      api::Term n = SOLVER->mkInteger(sIntLit.str());
       std::vector<api::Term> values;
       values.push_back( n );
       std::string attr_name(AntlrInput::tokenText($tok));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 629164593..edeb47f06 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1055,33 +1055,22 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError("Too many arguments to array constant.");
     }
     api::Term constVal = args[0];
-    if (!constVal.isValue())
+
+    // To parse array constants taking reals whose values are specified by
+    // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
+    // the fact that (/ 1 3) is the division of constants 1 and 3, and not
+    // the resulting constant rational value. Thus, we must construct the
+    // resulting rational here. This also is applied for integral real values
+    // like 5.0 which are converted to (/ 5 1) to distinguish them from
+    // integer constants. We must ensure numerator and denominator are
+    // constant and the denominator is non-zero.
+    if (constVal.getKind() == api::DIVISION)
     {
-      // To parse array constants taking reals whose values are specified by
-      // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
-      // the fact that (/ 1 3) is the division of constants 1 and 3, and not
-      // the resulting constant rational value. Thus, we must construct the
-      // resulting rational here. This also is applied for integral real values
-      // like 5.0 which are converted to (/ 5 1) to distinguish them from
-      // integer constants. We must ensure numerator and denominator are
-      // constant and the denominator is non-zero.
-      if (constVal.getKind() == api::DIVISION && constVal[0].isValue()
-          && constVal[1].isValue()
-          && !constVal[1].getExpr().getConst<Rational>().isZero())
-      {
-        std::stringstream sdiv;
-        sdiv << constVal[0] << "/" << constVal[1];
-        constVal = d_solver->mkReal(sdiv.str());
-      }
-      if (!constVal.isValue())
-      {
-        std::stringstream ss;
-        ss << "expected constant term inside array constant, but found "
-           << "nonconstant term:" << std::endl
-           << "the term: " << constVal;
-        parseError(ss.str());
-      }
+      std::stringstream sdiv;
+      sdiv << constVal[0] << "/" << constVal[1];
+      constVal = d_solver->mkReal(sdiv.str());
     }
+
     if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
     {
       std::stringstream ss;
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index b99376685..8e29c25f1 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -477,7 +477,7 @@ definedPred[CVC4::ParseOp& p]
       api::Term body =
           MK_TERM(api::AND,
                   MK_TERM(api::NOT,
-                          MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                          MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
                   MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
@@ -537,7 +537,7 @@ thfDefinedPred[CVC4::ParseOp& p]
       api::Term body = MK_TERM(
           api::AND,
           MK_TERM(api::NOT,
-                  MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                  MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
           MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
@@ -708,7 +708,7 @@ definedFun[CVC4::ParseOp& p]
                                                   n,
                                                   SOLVER->mkReal(2)),
                                           SOLVER->mkReal(1, 2))),
-                          SOLVER->mkReal(2))));
+                          SOLVER->mkInteger(2))));
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
       }
@@ -1747,7 +1747,15 @@ NUMBER
   : ( SIGN[pos]? num=DECIMAL
       { std::stringstream ss;
         ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num);
-        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
+        std::string str = ss.str();
+        if (str.find(".") == std::string::npos)
+        {
+          PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str);
+        }
+        else
+        {
+          PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str);
+        }
       }
     | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
       {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index bab619dce..9ccf02301 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -644,6 +644,8 @@ void CvcPrinter::toStream(
       opType = PREFIX;
       break;
     case kind::TO_REAL:
+    case kind::CAST_TO_REAL:
+    {
       if (n[0].getKind() == kind::CONST_RATIONAL)
       {
         // print the constant as a rational
@@ -655,6 +657,7 @@ void CvcPrinter::toStream(
         toStream(out, n[0], depth, types, false);
       }
       return;
+    }
     case kind::DIVISIBLE:
       out << "DIVISIBLE(";
       toStream(out, n[0], depth, types, false);
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8815f9632..a0cd8cf9c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -477,10 +477,10 @@ void Smt2Printer::toStream(std::ostream& out,
   bool typeChildren = false;  // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real
   // operator
   Kind k = n.getKind();
-  if(n.getNumChildren() != 0 &&
-     k != kind::INST_PATTERN_LIST &&
-     k != kind::APPLY_TYPE_ASCRIPTION &&
-     k != kind::CONSTRUCTOR_TYPE) {
+  if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST
+      && k != kind::APPLY_TYPE_ASCRIPTION && k != kind::CONSTRUCTOR_TYPE
+      && k != kind::CAST_TO_REAL)
+  {
     out << '(';
   }
   switch(k) {
@@ -603,11 +603,17 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::ABS:
   case kind::IS_INTEGER:
   case kind::TO_INTEGER:
-  case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
     out << smtKindString(k, d_variant) << " ";
     break;
+  case kind::TO_REAL:
+  case kind::CAST_TO_REAL:
+  {
+    // (to_real 5) is printed as 5.0
+    out << n[0] << ".0";
+    return;
+  }
   case kind::IAND:
     out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
     stillNeedToPrintParams = false;
@@ -1029,7 +1035,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }
     }
   }
-  if(n.getNumChildren() != 0) {
+  if (n.getNumChildren() != 0)
+  {
     out << parens.str() << ')';
   }
 }/* Smt2Printer::toStream(TNode) */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index dc91d678e..a65fbd961 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -138,7 +138,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::TO_INTEGER:
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
-      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::POW:
       return RewriteResponse(REWRITE_DONE, t);
     case kind::PI:
@@ -198,7 +198,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       }
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
-      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::TO_INTEGER:
       if(t[0].isConst()) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor())));
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index e563d8f66..fc8f76ee4 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -80,9 +80,16 @@ operator LEQ 2 "less than or equal, x <= y"
 operator GT 2 "greater than, x > y"
 operator GEQ 2 "greater than or equal, x >= y"
 
-operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
-operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)"
-operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+operator IS_INTEGER   1 "term-is-integer predicate (parameter is a real-sorted term)"
+operator TO_INTEGER   1 "convert term to integer by the floor function (parameter is a real-sorted term)"
+operator TO_REAL      1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+
+# CAST_TO_REAL is added to distinguish between integers casted to reals internally, and
+# integers casted to reals or using the API \
+# Solver::mkReal(int val) would return an internal node (CAST_TO_REAL val), but in the api it appears as term (val) \
+# Solver::mkTerm(TO_REAL, Solver::mkInteger(int val)) would return both term and node (TO_REAL val) \
+# This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val))
+operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API"
 
 typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
@@ -99,9 +106,10 @@ typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
 
-typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
+typerule TO_REAL      ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_INTEGER   ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule IS_INTEGER   "SimpleTypeRule<RBool, AReal>"
 
 typerule ABS "SimpleTypeRule<RInteger, AInteger>"
 typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9dd18d84b..0aa9cd4b3 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -60,12 +60,13 @@ public:
         }
       }
     }
-    switch(Kind k = n.getKind()) {
+    switch (Kind k = n.getKind())
+    {
       case kind::TO_REAL:
-        return realType;
-      case kind::TO_INTEGER:
-        return integerType;
-      default: {
+      case kind::CAST_TO_REAL: return realType;
+      case kind::TO_INTEGER: return integerType;
+      default:
+      {
         bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
         return (isInteger && !isDivision ? integerType : realType);
       }
diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp
index 73629a0d0..2168d053e 100644
--- a/test/api/reset_assertions.cpp
+++ b/test/api/reset_assertions.cpp
@@ -31,7 +31,7 @@ int main()
 
   Sort real = slv.getRealSort();
   Term x = slv.mkConst(real, "x");
-  Term four = slv.mkReal(4);
+  Term four = slv.mkInteger(4);
   Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
   slv.assertFormula(xEqFour);
   std::cout << slv.checkSat() << std::endl;
@@ -43,7 +43,7 @@ int main()
   Sort arrayType = slv.mkArraySort(indexType, elementType);
   Term array = slv.mkConst(arrayType, "array");
   Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
-  Term ten = slv.mkReal(10);
+  Term ten = slv.mkInteger(10);
   Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
   slv.assertFormula(arrayAtFour_eq_ten);
   std::cout << slv.checkSat() << std::endl;
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index f0a55cf79..1b1efb07e 100644
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -135,10 +135,10 @@ int validate_getters(void)
   Sort integer = slv.getIntegerSort();
 
   /* A "random" constant */
-  Term random_constant = slv.mkReal(0xDEADBEEF);
+  Term random_constant = slv.mkInteger(0xDEADBEEF);
 
   /* Another random constant */
-  Term expr_nil_val = slv.mkReal(0xFBADBEEF);
+  Term expr_nil_val = slv.mkInteger(0xFBADBEEF);
 
   /* Our nil term */
   Term nil = slv.mkSepNil(integer);
diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2
index b75f535d5..c8d3bb348 100644
--- a/test/regress/regress0/get-value-reals-ints.smt2
+++ b/test/regress/regress0/get-value-reals-ints.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6)))
+; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2.0) 1.0)) (neg_int (- 6)))
 (set-info :smt-lib-version 2.0)
 (set-option :produce-models true)
 (set-logic QF_LIRA)
diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2
index 09ec0917f..d27581114 100644
--- a/test/regress/regress0/get-value-reals.smt2
+++ b/test/regress/regress0/get-value-reals.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1)))
+; EXPECT: ((pos_int (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2.0) 1.0)))
 (set-info :smt-lib-version 2.0)
 (set-option :produce-models true)
 (set-logic QF_LRA)
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
index bf0d97e9d..afbd09d0f 100644
--- a/test/unit/api/grammar_black.h
+++ b/test/unit/api/grammar_black.h
@@ -57,7 +57,7 @@ void GrammarBlack::testAddRule()
   TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&);
   TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkInteger(0)), CVC4ApiException&);
 
   d_solver->synthFun("f", {}, boolean, g);
 
@@ -83,7 +83,7 @@ void GrammarBlack::testAddRules()
   TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&);
   TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkReal(0)}), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkInteger(0)}), CVC4ApiException&);
 
   d_solver->synthFun("f", {}, boolean, g);
 
diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
index 0321f03d0..5a0d5101f 100644
--- a/test/unit/api/python/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
@@ -38,7 +38,7 @@ def test_add_rule():
   with pytest.raises(Exception):
     g.addRule(nts, solver.mkBoolean(false))
   with pytest.raises(Exception):
-    g.addRule(start, solver.mkReal(0))
+    g.addRule(start, solver.mkInteger(0))
 
   # expecting no errors
   solver.synthFun("f", {}, boolean, g)
@@ -68,7 +68,7 @@ def test_add_rules():
   with pytest.raises(Exception):
     g.addRules(nts, {solver.mkBoolean(False)})
   with pytest.raises(Exception):
-    g.addRules(start, {solver.mkReal(0)})
+    g.addRules(start, {solver.mkInteger(0)})
   #Expecting no errors
   solver.synthFun("f", {}, boolean, g)
 
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 9c25b584f..a0c1b4681 100644
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -103,26 +103,12 @@ def test_get_op():
     assert fx.getOp() == solver.mkOp(kinds.ApplyUf)
 
 
-def test_is_const():
-    solver = pycvc4.Solver()
-    intsort = solver.getIntegerSort()
-    one = solver.mkReal(1)
-    x = solver.mkConst(intsort, 'x')
-    xpone = solver.mkTerm(kinds.Plus, x, one)
-    onepone = solver.mkTerm(kinds.Plus, one, one)
-    assert not x.isValue()
-    assert one.isValue()
-    assert not xpone.isValue()
-    assert not onepone.isValue()
-
 def test_const_sequence_elements():
     solver = pycvc4.Solver()
     realsort = solver.getRealSort()
     seqsort = solver.mkSequenceSort(realsort)
     s = solver.mkEmptySequence(seqsort)
 
-    assert s.isValue()
-
     assert s.getKind() == kinds.ConstSequence
     # empty sequence has zero elements
     cs = s.getConstSequenceElements()
diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py
index 3ce08f6b8..eb15e7469 100644
--- a/test/unit/api/python/test_to_python_obj.py
+++ b/test/unit/api/python/test_to_python_obj.py
@@ -15,7 +15,7 @@ def testGetBool():
 
 def testGetInt():
     solver = pycvc4.Solver()
-    two = solver.mkReal(2)
+    two = solver.mkInteger(2)
     assert two.toPythonObj() == 2
 
 
@@ -27,7 +27,7 @@ def testGetReal():
     neg34 = solver.mkReal("-3/4")
     assert neg34.toPythonObj() == Fraction(-3, 4)
 
-    neg1 = solver.mkReal("-1")
+    neg1 = solver.mkInteger("-1")
     assert neg1.toPythonObj() == -1
 
 
@@ -40,12 +40,10 @@ def testGetBV():
 def testGetArray():
     solver = pycvc4.Solver()
     arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
-    zero_array = solver.mkConstArray(arrsort, solver.mkReal(0))
-    stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2))
-    stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3))
-    stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5))
-
-    assert stores.isValue()
+    zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0))
+    stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5))
 
     array_dict = stores.toPythonObj()
 
@@ -58,10 +56,7 @@ def testGetArray():
 
 def testGetSymbol():
     solver = pycvc4.Solver()
-    x = solver.mkConst(solver.getBooleanSort(), "x")
-
-    with pytest.raises(RuntimeError):
-        x.toPythonObj()
+    solver.mkConst(solver.getBooleanSort(), "x")
 
 
 def testGetString():
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 8b8c6dd58..1324e3890 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -72,6 +72,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkPi();
   void testMkPosInf();
   void testMkPosZero();
+  void testMkInteger();
   void testMkReal();
   void testMkRegexpEmpty();
   void testMkRegexpSigma();
@@ -598,7 +599,7 @@ void SolverBlack::testMkFloatingPoint()
 {
   Term t1 = d_solver->mkBitVector(8);
   Term t2 = d_solver->mkBitVector(4);
-  Term t3 = d_solver->mkReal(2);
+  Term t3 = d_solver->mkInteger(2);
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
     TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPoint(3, 5, t1));
@@ -742,6 +743,47 @@ void SolverBlack::testMkOp()
 
 void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
 
+void SolverBlack::testMkInteger()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger("123"));
+  TS_ASSERT_THROWS(d_solver->mkInteger("1.23"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("1/23"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("12/3"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(".2"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("2."), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(""), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("asdf"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("1.2/3"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("."), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("/"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("2/"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("/2"), CVC4ApiException&);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123")));
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.23")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1/23")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("12/3")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".2")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2.")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("asdf")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.2/3")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2/")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/2")), CVC4ApiException&);
+
+  int32_t val1 = 1;
+  int64_t val2 = -1;
+  uint32_t val3 = 1;
+  uint64_t val4 = -1;
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val3));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
+}
+
 void SolverBlack::testMkReal()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("123"));
@@ -839,8 +881,8 @@ void SolverBlack::testMkTerm()
   std::vector<Term> v1 = {a, b};
   std::vector<Term> v2 = {a, Term()};
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
-  std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
-  std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
+  std::vector<Term> v4 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
+  std::vector<Term> v5 = {d_solver->mkInteger(1), Term()};
   std::vector<Term> v6 = {};
   Solver slv;
 
@@ -896,10 +938,10 @@ void SolverBlack::testMkTermFromOp()
   Sort bv32 = d_solver->mkBitVectorSort(32);
   Term a = d_solver->mkConst(bv32, "a");
   Term b = d_solver->mkConst(bv32, "b");
-  std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
-  std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
+  std::vector<Term> v1 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
+  std::vector<Term> v2 = {d_solver->mkInteger(1), Term()};
   std::vector<Term> v3 = {};
-  std::vector<Term> v4 = {d_solver->mkReal(5)};
+  std::vector<Term> v4 = {d_solver->mkInteger(5)};
   Solver slv;
 
   // simple operator terms
@@ -948,13 +990,13 @@ void SolverBlack::testMkTermFromOp()
 
   // mkTerm(Op op, Term child) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkInteger(1)));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(
-      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkInteger(0)),
       CVC4ApiException&);
   TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
 
@@ -962,19 +1004,19 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(APPLY_CONSTRUCTOR,
                        consTerm1,
-                       d_solver->mkReal(0),
+                       d_solver->mkInteger(0),
                        d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
   TS_ASSERT_THROWS(
-      d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
+      d_solver->mkTerm(opterm2, d_solver->mkInteger(1), d_solver->mkInteger(2)),
       CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()),
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkInteger(1), Term()),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)),
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkInteger(1)),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
                               consTerm1,
-                              d_solver->mkReal(0),
+                              d_solver->mkInteger(0),
                               d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
                    CVC4ApiException&);
 
@@ -982,7 +1024,7 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->mkTerm(
-          opterm2, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+          opterm2, d_solver->mkInteger(1), d_solver->mkInteger(1), Term()),
       CVC4ApiException&);
 
   // mkTerm(Op op, const std::vector<Term>& children) const
@@ -1004,7 +1046,7 @@ void SolverBlack::testMkTuple()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTuple(
       {d_solver->mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}));
   TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkReal("5")}));
+      d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkInteger("5")}));
 
   TS_ASSERT_THROWS(d_solver->mkTuple({}, {d_solver->mkBitVector("101", 2)}),
                    CVC4ApiException&);
@@ -1054,7 +1096,7 @@ void SolverBlack::testMkConstArray()
 {
   Sort intSort = d_solver->getIntegerSort();
   Sort arrSort = d_solver->mkArraySort(intSort, intSort);
-  Term zero = d_solver->mkReal(0);
+  Term zero = d_solver->mkInteger(0);
   Term constArr = d_solver->mkConstArray(arrSort, zero);
 
   TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
@@ -1064,7 +1106,7 @@ void SolverBlack::testMkConstArray()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
   Solver slv;
-  Term zero2 = slv.mkReal(0);
+  Term zero2 = slv.mkInteger(0);
   Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
   TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
   TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
@@ -1454,7 +1496,7 @@ void SolverBlack::testGetOp()
 
   Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm);
   Term listcons1 = d_solver->mkTerm(
-      APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil);
+      APPLY_CONSTRUCTOR, consTerm, d_solver->mkInteger(1), listnil);
   Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
 
   TS_ASSERT(listnil.hasOp());
@@ -1542,8 +1584,8 @@ void SolverBlack::testGetUnsatCore3()
   Term y = d_solver->mkConst(uSort, "y");
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
   Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
@@ -1601,8 +1643,8 @@ void SolverBlack::testGetValue3()
   Term z = d_solver->mkConst(uSort, "z");
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
   Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
@@ -1985,11 +2027,11 @@ void SolverBlack::testSimplify()
 
   Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
-  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkReal("23"));
+  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkInteger("23"));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2));
   TS_ASSERT(i1 != i2);
   TS_ASSERT(i1 != d_solver->simplify(i2));
-  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkReal(0));
+  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkInteger(0));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3));
   TS_ASSERT(i1 != i3);
   TS_ASSERT(i1 == d_solver->simplify(i3));
@@ -1998,7 +2040,7 @@ void SolverBlack::testSimplify()
   Term dt1 = d_solver->mkTerm(
       APPLY_CONSTRUCTOR,
       consList.getConstructorTerm("cons"),
-      d_solver->mkReal(0),
+      d_solver->mkInteger(0),
       d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
   Term dt2 = d_solver->mkTerm(
@@ -2075,8 +2117,8 @@ void SolverBlack::testCheckEntailed2()
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
   // Values
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   // Terms
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
@@ -2158,8 +2200,8 @@ void SolverBlack::testCheckSatAssuming2()
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
   // Values
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   // Terms
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
@@ -2279,7 +2321,7 @@ void SolverBlack::testSynthFun()
   g1.addRule(start1, d_solver->mkBoolean(false));
 
   Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
-  g2.addRule(start2, d_solver->mkReal(0));
+  g2.addRule(start2, d_solver->mkInteger(0));
 
   TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("", {}, boolean));
   TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f1", {x}, boolean));
@@ -2314,7 +2356,7 @@ void SolverBlack::testSynthInv()
   g1.addRule(start1, d_solver->mkBoolean(false));
 
   Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
-  g2.addRule(start2, d_solver->mkReal(0));
+  g2.addRule(start2, d_solver->mkInteger(0));
 
   TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("", {}));
   TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i1", {x}));
@@ -2328,7 +2370,7 @@ void SolverBlack::testAddSygusConstraint()
 {
   Term nullTerm;
   Term boolTerm = d_solver->mkBoolean(true);
-  Term intTerm = d_solver->mkReal(1);
+  Term intTerm = d_solver->mkInteger(1);
 
   TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm));
   TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&);
@@ -2344,7 +2386,7 @@ void SolverBlack::testAddSygusInvConstraint()
   Sort real = d_solver->getRealSort();
 
   Term nullTerm;
-  Term intTerm = d_solver->mkReal(1);
+  Term intTerm = d_solver->mkInteger(1);
 
   Term inv = d_solver->declareFun("inv", {real}, boolean);
   Term pre = d_solver->declareFun("pre", {real}, boolean);
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 786b60bb3..bebfc6e1f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -42,7 +42,6 @@ class TermBlack : public CxxTest::TestSuite
   void testTermCompare();
   void testTermChildren();
   void testSubstitute();
-  void testIsValue();
   void testConstArray();
   void testConstSequenceElements();
 
@@ -100,7 +99,7 @@ void TermBlack::testGetKind()
   Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS_NOTHING(p.getKind());
 
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS_NOTHING(zero.getKind());
 
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
@@ -146,7 +145,7 @@ void TermBlack::testGetSort()
   TS_ASSERT_THROWS_NOTHING(p.getSort());
   TS_ASSERT(p.getSort() == funSort2);
 
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS_NOTHING(zero.getSort());
   TS_ASSERT(zero.getSort() == intSort);
 
@@ -227,7 +226,7 @@ void TermBlack::testGetOp()
 
   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
   Term consTerm = d_solver.mkTerm(
-      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm);
+      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
   Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
   Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
 
@@ -272,7 +271,7 @@ void TermBlack::testNotTerm()
   TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
   Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
   TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
@@ -308,7 +307,7 @@ void TermBlack::testAndTerm()
   TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
@@ -374,7 +373,7 @@ void TermBlack::testOrTerm()
   TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
@@ -440,7 +439,7 @@ void TermBlack::testXorTerm()
   TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
@@ -506,7 +505,7 @@ void TermBlack::testEqTerm()
   TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
@@ -572,7 +571,7 @@ void TermBlack::testImpTerm()
   TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
@@ -639,7 +638,7 @@ void TermBlack::testIteTerm()
   Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
@@ -660,17 +659,17 @@ void TermBlack::testIteTerm()
 
 void TermBlack::testTermAssignment()
 {
-  Term t1 = d_solver.mkReal(1);
+  Term t1 = d_solver.mkInteger(1);
   Term t2 = t1;
-  t2 = d_solver.mkReal(2);
-  TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+  t2 = d_solver.mkInteger(2);
+  TS_ASSERT_EQUALS(t1, d_solver.mkInteger(1));
 }
 
 void TermBlack::testTermCompare()
 {
-  Term t1 = d_solver.mkReal(1);
-  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
-  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+  Term t1 = d_solver.mkInteger(1);
+  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
   TS_ASSERT(t2 >= t3);
   TS_ASSERT(t2 <= t3);
   TS_ASSERT((t1 > t2) != (t1 < t2));
@@ -680,8 +679,8 @@ void TermBlack::testTermCompare()
 void TermBlack::testTermChildren()
 {
   // simple term 2+3
-  Term two = d_solver.mkReal(2);
-  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3));
+  Term two = d_solver.mkInteger(2);
+  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
   TS_ASSERT(t1[0] == two);
   TS_ASSERT(t1.getNumChildren() == 2);
   Term tnull;
@@ -702,7 +701,7 @@ void TermBlack::testTermChildren()
 void TermBlack::testSubstitute()
 {
   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
-  Term one = d_solver.mkReal(1);
+  Term one = d_solver.mkInteger(1);
   Term ttrue = d_solver.mkTrue();
   Term xpx = d_solver.mkTerm(PLUS, x, x);
   Term onepone = d_solver.mkTerm(PLUS, one, one);
@@ -750,34 +749,27 @@ void TermBlack::testSubstitute()
   TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
 }
 
-void TermBlack::testIsValue()
-{
-  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
-  Term one = d_solver.mkReal(1);
-  Term xpone = d_solver.mkTerm(PLUS, x, one);
-  Term onepone = d_solver.mkTerm(PLUS, one, one);
-  TS_ASSERT(!x.isValue());
-  TS_ASSERT(one.isValue());
-  TS_ASSERT(!xpone.isValue());
-  TS_ASSERT(!onepone.isValue());
-  Term tnull;
-  TS_ASSERT_THROWS(tnull.isValue(), CVC4ApiException&);
-}
-
 void TermBlack::testConstArray()
 {
   Sort intsort = d_solver.getIntegerSort();
   Sort arrsort = d_solver.mkArraySort(intsort, intsort);
   Term a = d_solver.mkConst(arrsort, "a");
-  Term one = d_solver.mkReal(1);
+  Term one = d_solver.mkInteger(1);
   Term constarr = d_solver.mkConstArray(arrsort, one);
 
-  TS_ASSERT(!a.isValue());
-  TS_ASSERT(constarr.isValue());
-
   TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY);
   TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
   TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&);
+
+  arrsort =
+      d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
+  Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
+  Term stores = d_solver.mkTerm(
+      STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
+  stores =
+      d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
+  stores =
+      d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
 }
 
 void TermBlack::testConstSequenceElements()
@@ -786,7 +778,6 @@ void TermBlack::testConstSequenceElements()
   Sort seqsort = d_solver.mkSequenceSort(realsort);
   Term s = d_solver.mkEmptySequence(seqsort);
 
-  TS_ASSERT(s.isValue());
 
   TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE);
   // empty sequence has zero elements
diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index c098ca9b8..f06c1f77d 100644
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -56,7 +56,7 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
     Sort realSort = d_slv->getRealSort();
     Sort intSort = d_slv->getIntegerSort();
     Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort));
-    Term one = d_slv->mkReal(1);
+    Term one = d_slv->mkInteger(1);
     Term singletonInt = d_slv->mkSingleton(intSort, one);
     Term singletonReal = d_slv->mkSingleton(realSort, one);
     // (union