diff --git a/src/kind.cpp b/src/kind.cpp
index 49d09084..f3032aad 100644
--- a/src/kind.cpp
+++ b/src/kind.cpp
@@ -55,6 +55,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_NEG: o << "EVAL_NEG"; break;
     case Kind::EVAL_MUL: o << "EVAL_MUL"; break;
     case Kind::EVAL_INT_DIV: o << "EVAL_INT_DIV"; break;
+    case Kind::EVAL_INT_MOD: o << "EVAL_INT_MOD"; break;
     case Kind::EVAL_RAT_DIV: o << "EVAL_RAT_DIV"; break;
     case Kind::EVAL_IS_NEG: o << "EVAL_IS_NEG"; break;
     // strings
@@ -113,6 +114,7 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_NEG: ss << "neg";break;
         case Kind::EVAL_MUL: ss << "mul";break;
         case Kind::EVAL_INT_DIV: ss << "zdiv";break;
+        case Kind::EVAL_INT_MOD: ss << "zmod";break;
         case Kind::EVAL_RAT_DIV: ss << "qdiv";break;
         case Kind::EVAL_IS_NEG: ss << "is_neg";break;
         // strings
@@ -188,6 +190,7 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_NEG:
     case Kind::EVAL_MUL:
     case Kind::EVAL_INT_DIV:
+    case Kind::EVAL_INT_MOD:
     case Kind::EVAL_RAT_DIV:
     case Kind::EVAL_IS_NEG:
     // strings
diff --git a/src/kind.h b/src/kind.h
index e75c7a91..4be3f58d 100644
--- a/src/kind.h
+++ b/src/kind.h
@@ -65,6 +65,7 @@ enum class Kind
   EVAL_NEG,
   EVAL_MUL,
   EVAL_INT_DIV,
+  EVAL_INT_MOD,
   EVAL_RAT_DIV,
   EVAL_IS_NEG,
   // strings
diff --git a/src/literal.cpp b/src/literal.cpp
index 674bb5aa..68836bfa 100644
--- a/src/literal.cpp
+++ b/src/literal.cpp
@@ -259,7 +259,9 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
       }
       break;
     case Kind::EVAL_INT_DIV:
+    case Kind::EVAL_INT_MOD:
     {
+      bool isDiv = (k==Kind::EVAL_INT_DIV);
       switch (ka)
       {
         case Kind::NUMERAL:
@@ -267,7 +269,8 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
           const Integer& d = args[1]->d_int;
           if (d.sgn()!=0)
           {
-            return Literal(Integer(args[0]->d_int.euclidianDivideQuotient(d)));
+            return Literal(isDiv ? args[0]->d_int.euclidianDivideQuotient(d) : 
+                                  args[0]->d_int.euclidianDivideRemainder(d));
           }
         }
           break;
@@ -277,7 +280,8 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
           {
             return Literal();
           }
-          return Literal(ka, BitVector(args[0]->d_bv.unsignedDivTotal(args[1]->d_bv)));
+          return Literal(ka, isDiv ? args[0]->d_bv.unsignedDivTotal(args[1]->d_bv) : 
+                                     args[0]->d_bv.unsignedRemTotal(args[1]->d_bv));
           break;
         default: break;
       }
diff --git a/src/state.cpp b/src/state.cpp
index 8c6c218a..bf261db0 100644
--- a/src/state.cpp
+++ b/src/state.cpp
@@ -56,6 +56,7 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("neg", Kind::EVAL_NEG);
   bindBuiltinEval("mul", Kind::EVAL_MUL);
   bindBuiltinEval("zdiv", Kind::EVAL_INT_DIV);
+  bindBuiltinEval("zmod", Kind::EVAL_INT_MOD);
   bindBuiltinEval("qdiv", Kind::EVAL_RAT_DIV);
   bindBuiltinEval("is_neg", Kind::EVAL_IS_NEG);
   bindBuiltinEval("to_z", Kind::EVAL_TO_INT);
diff --git a/src/type_checker.cpp b/src/type_checker.cpp
index aee13a61..2703e74a 100644
--- a/src/type_checker.cpp
+++ b/src/type_checker.cpp
@@ -151,6 +151,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
       break;
     case Kind::EVAL_IS_EQ:
     case Kind::EVAL_INT_DIV:
+    case Kind::EVAL_INT_MOD:
     case Kind::EVAL_RAT_DIV:
     case Kind::EVAL_TO_BV:
     case Kind::EVAL_FIND:
@@ -1274,6 +1275,7 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
       return d_state.mkBoolType().getValue();
     case Kind::EVAL_HASH:
     case Kind::EVAL_INT_DIV:
+    case Kind::EVAL_INT_MOD:
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_LENGTH:
     case Kind::EVAL_FIND:
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 52665beb..1397b88c 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -25,15 +25,6 @@ const Integer& BitVector::getValue() const { return d_value; }
 
 Integer BitVector::toInteger() const { return d_value; }
 
-Integer BitVector::toSignedInteger() const
-{
-  unsigned size = d_size;
-  Integer sign_bit = d_value.extractBitRange(1, size - 1);
-  Integer val = d_value.extractBitRange(size - 1, 0);
-  Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
-  return res;
-}
-
 std::string BitVector::toString(unsigned int base) const
 {
   std::string str = d_value.toString(base);
@@ -57,24 +48,6 @@ size_t BitVector::hash() const
   return std::hash<size_t>()(d_value.hash()) ^ std::hash<size_t>()(d_size);
 }
 
-BitVector& BitVector::setBit(uint32_t i, bool value)
-{
-  Assert(i < d_size);
-  d_value.setBit(i, value);
-  return *this;
-}
-
-bool BitVector::isBitSet(uint32_t i) const
-{
-  Assert(i < d_size);
-  return d_value.isBitSet(i);
-}
-
-unsigned BitVector::isPow2() const
-{
-  return d_value.isPow2();
-}
-
 /* -----------------------------------------------------------------------
  * Operators
  * ----------------------------------------------------------------------- */
@@ -103,30 +76,6 @@ bool operator==(const BitVector& a, const BitVector& b)
   return a.getValue() == b.getValue();
 }
 
-/* Signed Inequality ----------------------------------------------------- */
-
-bool BitVector::signedLessThan(const BitVector& y) const
-{
-  Assert(d_size == y.d_size);
-  Assert(d_value.sgn()>=0);
-  Assert(y.d_value.sgn() >= 0);
-  Integer a = (*this).toSignedInteger();
-  Integer b = y.toSignedInteger();
-
-  return b > a;
-}
-
-bool BitVector::signedLessThanEq(const BitVector& y) const
-{
-  Assert(d_size == y.d_size);
-  Assert(d_value.sgn() >= 0);
-  Assert(y.d_value.sgn() >= 0);
-  Integer a = (*this).toSignedInteger();
-  Integer b = y.toSignedInteger();
-
-  return b >= a;
-}
-
 /* Bit-wise operations --------------------------------------------------- */
 
 BitVector operator^(const BitVector& a, const BitVector& b)
@@ -199,127 +148,4 @@ BitVector BitVector::unsignedRemTotal(const BitVector& y) const
   return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
 }
 
-/* Extend operations ----------------------------------------------------- */
-
-BitVector BitVector::zeroExtend(unsigned n) const
-{
-  return BitVector(d_size + n, d_value);
-}
-
-BitVector BitVector::signExtend(unsigned n) const
-{
-  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
-  if (sign_bit == Integer("0"))
-  {
-    return BitVector(d_size + n, d_value);
-  }
-  Integer val = d_value.oneExtend(d_size, n);
-  return BitVector(d_size + n, val);
-}
-
-/* Shift operations ------------------------------------------------------ */
-
-BitVector BitVector::leftShift(const BitVector& y) const
-{
-  Integer zero("0");
-  if (y.d_value > Integer(d_size))
-  {
-    return BitVector(d_size, zero);
-  }
-  if (y.d_value == zero)
-  {
-    return *this;
-  }
-  // making sure we don't lose information casting
-  //Assert(y.d_value < Integer(1).multiplyByPow2(32));
-  uint32_t amount = y.d_value.toUnsignedInt();
-  Integer res = d_value.multiplyByPow2(amount);
-  return BitVector(d_size, res);
-}
-
-BitVector BitVector::logicalRightShift(const BitVector& y) const
-{
-  Integer zero(0);
-  if (y.d_value > Integer(d_size))
-  {
-    return BitVector(d_size, zero);
-  }
-  // making sure we don't lose information casting
-  //Assert(y.d_value < Integer(1).multiplyByPow2(32));
-  uint32_t amount = y.d_value.toUnsignedInt();
-  Integer res = d_value.divByPow2(amount);
-  return BitVector(d_size, res);
-}
-
-BitVector BitVector::arithRightShift(const BitVector& y) const
-{
-  Integer zero(0);
-  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
-  if (y.d_value > Integer(d_size))
-  {
-    if (sign_bit == zero)
-    {
-      return BitVector(d_size, zero);
-    }
-    else
-    {
-      return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size)+(-Integer(1)));
-    }
-  }
-
-  if (y.d_value == zero)
-  {
-    return *this;
-  }
-
-  // making sure we don't lose information casting
-  //Assert(y.d_value < Integer(1).multiplyByPow2(32));
-
-  uint32_t amount = y.d_value.toUnsignedInt();
-  Integer rest = d_value.divByPow2(amount);
-
-  if (sign_bit == Integer(0))
-  {
-    return BitVector(d_size, rest);
-  }
-  Integer res = rest.oneExtend(d_size - amount, amount);
-  return BitVector(d_size, res);
-}
-
-/* -----------------------------------------------------------------------
- * Static helpers.
- * ----------------------------------------------------------------------- */
-
-BitVector BitVector::mkZero(unsigned size)
-{
-  Assert(size > 0);
-  return BitVector(size);
-}
-
-BitVector BitVector::mkOne(unsigned size)
-{
-  Assert(size > 0);
-  return BitVector(size, 1u);
-}
-
-BitVector BitVector::mkOnes(unsigned size)
-{
-  Assert(size > 0);
-  return BitVector(1, Integer(1)).signExtend(size - 1);
-}
-
-BitVector BitVector::mkMinSigned(unsigned size)
-{
-  Assert(size > 0);
-  BitVector res(size);
-  res.setBit(size - 1, true);
-  return res;
-}
-
-BitVector BitVector::mkMaxSigned(unsigned size)
-{
-  Assert(size > 0);
-  return ~BitVector::mkMinSigned(size);
-}
-
 }  // namespace cvc5::internal
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index b9f83b5d..11c398a1 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -81,27 +81,10 @@ class BitVector
 
   /* Return value. */
   Integer toInteger() const;
-  /* Return Integer corresponding to two's complement interpretation of this. */
-  Integer toSignedInteger() const;
   /* Return (binary) string representation. */
   std::string toString(unsigned int base = 2) const;
   /* Return hash value. */
   size_t hash() const;
-  /**
-   * Set bit at index 'i' to given value.
-   * Returns a reference to this bit-vector to allow for chaining.
-   *
-   * value: True to set bit to 1, and false to set it to 0.
-   *
-   * Note: Least significant bit is at index 0.
-   */
-  BitVector& setBit(uint32_t i, bool value);
-
-  /** Return true if bit at index 'i' is 1, and false otherwise. */
-  bool isBitSet(uint32_t i) const;
-
-  /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
-  unsigned isPow2() const;
 
   /* -----------------------------------------------------------------------
    ** Operators
@@ -115,14 +98,6 @@ class BitVector
   /* Return the bit range from index 'high' to index 'low'. */
   BitVector extract(unsigned high, unsigned low) const;
 
-  /* Signed Inequality ----------------------------------------------------- */
-
-  /* Return true if this is signed less than bit-vector 'y'. */
-  bool signedLessThan(const BitVector& y) const;
-
-  /* Return true if this is signed less than or equal to bit-vector 'y'. */
-  bool signedLessThanEq(const BitVector& y) const;
-
   /* Arithmetic operations ------------------------------------------------- */
 
   /* Total division function.
@@ -136,46 +111,6 @@ class BitVector
    * (this % y), otherwise.  */
   BitVector unsignedRemTotal(const BitVector& y) const;
 
-  /* Extend operations ----------------------------------------------------- */
-
-  /* Return a bit-vector representing this extended by 'n' zero bits. */
-  BitVector zeroExtend(unsigned n) const;
-
-  /* Return a bit-vector representing this extended by 'n' bits of the value
-   * of the signed bit. */
-  BitVector signExtend(unsigned n) const;
-
-  /* Shift operations ------------------------------------------------------ */
-
-  /* Return a bit-vector representing a left shift of this by 'y'. */
-  BitVector leftShift(const BitVector& y) const;
-
-  /* Return a bit-vector representing a logical right shift of this by 'y'. */
-  BitVector logicalRightShift(const BitVector& y) const;
-
-  /* Return a bit-vector representing an arithmetic right shift of this
-   * by 'y'.*/
-  BitVector arithRightShift(const BitVector& y) const;
-
-  /* -----------------------------------------------------------------------
-   ** Static helpers.
-   * ----------------------------------------------------------------------- */
-
-  /* Create zero bit-vector of given size. */
-  static BitVector mkZero(unsigned size);
-
-  /* Create bit-vector representing value 1 of given size. */
-  static BitVector mkOne(unsigned size);
-
-  /* Create bit-vector of ones of given size. */
-  static BitVector mkOnes(unsigned size);
-
-  /* Create bit-vector representing the minimum signed value of given size. */
-  static BitVector mkMinSigned(unsigned size);
-
-  /* Create bit-vector representing the maximum signed value of given size. */
-  static BitVector mkMaxSigned(unsigned size);
-
  private:
   /**
    * Class invariants:
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
index 8198889f..524c1e35 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer.cpp
@@ -76,23 +76,6 @@ Integer Integer::multiplyByPow2(uint32_t pow) const
   return Integer(result);
 }
 
-void Integer::setBit(uint32_t i, bool value)
-{
-  if (value)
-  {
-    mpz_setbit(d_value.get_mpz_t(), i);
-  }
-  else
-  {
-    mpz_clrbit(d_value.get_mpz_t(), i);
-  }
-}
-
-bool Integer::isBitSet(uint32_t i) const
-{
-  return extractBitRange(1, i).sgn()!=0;
-}
-
 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const
 {
   // check that the size is accurate
@@ -140,38 +123,16 @@ Integer Integer::floorDivideRemainder(const Integer& y) const
   return Integer(r);
 }
 
-void Integer::floorQR(Integer& q,
-                      Integer& r,
-                      const Integer& x,
-                      const Integer& y)
-{
-  mpz_fdiv_qr(q.d_value.get_mpz_t(),
-              r.d_value.get_mpz_t(),
-              x.d_value.get_mpz_t(),
-              y.d_value.get_mpz_t());
-}
-
-Integer Integer::ceilingDivideQuotient(const Integer& y) const
-{
-  mpz_class q;
-  mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
-  return Integer(q);
-}
-
-Integer Integer::ceilingDivideRemainder(const Integer& y) const
-{
-  mpz_class r;
-  mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
-  return Integer(r);
-}
-
 void Integer::euclidianQR(Integer& q,
                           Integer& r,
                           const Integer& x,
                           const Integer& y)
 {
   // compute the floor and then fix the value up if needed.
-  floorQR(q, r, x, y);
+  mpz_fdiv_qr(q.d_value.get_mpz_t(),
+              r.d_value.get_mpz_t(),
+              x.d_value.get_mpz_t(),
+              y.d_value.get_mpz_t());
 
   if (r.sgn()<0)
   {
@@ -213,14 +174,6 @@ Integer Integer::euclidianDivideRemainder(const Integer& y) const
   return r;
 }
 
-Integer Integer::exactQuotient(const Integer& y) const
-{
-  //Assert(y.divides(*this));
-  mpz_class q;
-  mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
-  return Integer(q);
-}
-
 Integer Integer::modByPow2(uint32_t exp) const
 {
   mpz_class res;
@@ -228,13 +181,6 @@ Integer Integer::modByPow2(uint32_t exp) const
   return Integer(res);
 }
 
-Integer Integer::divByPow2(uint32_t exp) const
-{
-  mpz_class res;
-  mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
-  return Integer(res);
-}
-
 int Integer::sgn() const { return mpz_sgn(d_value.get_mpz_t()); }
 
 Integer Integer::pow(uint32_t exp) const
@@ -244,40 +190,6 @@ Integer Integer::pow(uint32_t exp) const
   return Integer(result);
 }
 
-Integer Integer::modAdd(const Integer& y, const Integer& m) const
-{
-  mpz_class res;
-  mpz_add(res.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
-  mpz_mod(res.get_mpz_t(), res.get_mpz_t(), m.d_value.get_mpz_t());
-  return Integer(res);
-}
-
-Integer Integer::modMultiply(const Integer& y, const Integer& m) const
-{
-  mpz_class res;
-  mpz_mul(res.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
-  mpz_mod(res.get_mpz_t(), res.get_mpz_t(), m.d_value.get_mpz_t());
-  return Integer(res);
-}
-
-Integer Integer::modInverse(const Integer& m) const
-{
-  //Assert(m > 0) << "m must be greater than zero";
-  mpz_class res;
-  if (mpz_invert(res.get_mpz_t(), d_value.get_mpz_t(), m.d_value.get_mpz_t())
-      == 0)
-  {
-    return Integer(-1);
-  }
-  return Integer(res);
-}
-
-bool Integer::divides(const Integer& y) const
-{
-  int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
-  return res != 0;
-}
-
 std::string Integer::toString(int base) const { return d_value.get_str(base); }
 
 
@@ -297,23 +209,6 @@ size_t Integer::gmpHash(const mpz_t toHash)
   return hash;
 }
 
-bool Integer::testBit(unsigned n) const
-{
-  return mpz_tstbit(d_value.get_mpz_t(), n);
-}
-
-unsigned Integer::isPow2() const
-{
-  if (d_value <= 0) return 0;
-  // check that the number of ones in the binary representation is 1
-  if (mpz_popcount(d_value.get_mpz_t()) == 1)
-  {
-    // return the index of the first one plus 1
-    return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
-  }
-  return 0;
-}
-
 size_t Integer::length() const
 {
   if (sgn() == 0)
diff --git a/src/util/integer.h b/src/util/integer.h
index dfa7fa69..40d4c918 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -70,12 +70,6 @@ class Integer
   /** Return this*(2^pow). */
   Integer multiplyByPow2(uint32_t pow) const;
 
-  /** Set the ith bit of the current Integer to 'value'.  */
-  void setBit(uint32_t i, bool value);
-
-  /** Return true if bit at index 'i' is 1, and false otherwise. */
-  bool isBitSet(uint32_t i) const;
-
   /**
    * Returns the integer with the binary representation of 'size' bits
    * extended with 'amount' 1's.
@@ -99,18 +93,6 @@ class Integer
   /** Returns r == this - floor(this/y)*y */
   Integer floorDivideRemainder(const Integer& y) const;
 
-  /** Computes a floor quotient and remainder for x divided by y.  */
-  static void floorQR(Integer& q,
-                      Integer& r,
-                      const Integer& x,
-                      const Integer& y);
-
-  /** Returns the ceil(this / y). */
-  Integer ceilingDivideQuotient(const Integer& y) const;
-
-  /** Returns the ceil(this / y). */
-  Integer ceilingDivideRemainder(const Integer& y) const;
-
   /**
    * Computes a quotient and remainder according to Boute's Euclidean
    * definition. euclidianDivideQuotient, euclidianDivideRemainder.
@@ -137,50 +119,15 @@ class Integer
    */
   Integer euclidianDivideRemainder(const Integer& y) const;
 
-  /** If y divides *this, then exactQuotient returns (this/y). */
-  Integer exactQuotient(const Integer& y) const;
-
   /** Returns y mod 2^exp. */
   Integer modByPow2(uint32_t exp) const;
 
-  /** Returns y / 2^exp. */
-  Integer divByPow2(uint32_t exp) const;
-
   /** Return 1 if this is > 0, 0 if it is 0, and -1 if it is < 0. */
   int sgn() const;
 
   /** Raise this Integer to the power 'exp'. */
   Integer pow(uint32_t exp) const;
 
-  /** Compute addition of this Integer x + y modulo m. */
-  Integer modAdd(const Integer& y, const Integer& m) const;
-
-  /** Compute multiplication of this Integer x * y modulo m. */
-  Integer modMultiply(const Integer& y, const Integer& m) const;
-
-  /**
-   * Compute modular inverse x^-1 of this Integer x modulo m with m > 0.
-   * Returns a value x^-1 with 0 <= x^-1 < m such that x * x^-1 = 1 modulo m
-   * if such an inverse exists, and -1 otherwise.
-   *
-   * Such an inverse only exists if
-   *   - x is non-zero
-   *   - x and m are coprime, i.e., if gcd (x, m) = 1
-   *
-   * Note that if x and m are coprime, then x^-1 > 0 if m > 1 and x^-1 = 0
-   * if m = 1 (the zero ring).
-   */
-  Integer modInverse(const Integer& m) const;
-
-  /**
-   * Return true if 'y' divides this integer.
-   * Note: All non-zero integers devide zero, and zero does not divide zero.
-   */
-  bool divides(const Integer& y) const;
-
-  /** Return the absolute value of this integer.  */
-  Integer abs() const;
-
   /** Return a string representation of this Integer. */
   std::string toString(int base = 10) const;
 
@@ -193,20 +140,6 @@ class Integer
   /** */
   static size_t gmpHash(const mpz_t toHash);
 
-  /**
-   * Returns true iff bit n is set.
-   *
-   * @param n the bit to test (0 == least significant bit)
-   * @return true if bit n is set in this integer; false otherwise
-   */
-  bool testBit(unsigned n) const;
-
-  /**
-   * Returns k if the integer is equal to 2^(k-1)
-   * @return k if the integer is equal to 2^(k-1) and 0 otherwise
-   */
-  unsigned isPow2() const;
-
   /**
    * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}.
    * If x == 0, returns 1.
diff --git a/src/util/rational.h b/src/util/rational.h
index edf576b0..bb02718a 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -68,13 +68,6 @@ class Rational
     return Integer(q);
   }
 
-  Integer ceiling() const
-  {
-    mpz_class q;
-    mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
-    return Integer(q);
-  }
-
   Rational& operator=(const Rational& x)
   {
     if (this == &x) return *this;
diff --git a/user_manual.md b/user_manual.md
index 3791fe11..cca12a18 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -435,6 +435,9 @@ Arithmetic operators:
 - `(alf.zdiv t1 t2)`
     - If `t1` and `t2` are numeral values and `t2` is non-zero, then this returns the integer division (floor) of `t1` and `t2`.
     - If `t1` and `t2` are bitwise values of the same category and bitwidth, then this returns their (total, unsigned) division, where division by zero returns the max unsigned value.
+- `(alf.zmod t1 t2)`
+    - If `t1` and `t2` are numeral values and `t2` is non-zero, then this returns the integer remainder of `t1` and `t2`.
+    - If `t1` and `t2` are bitwise values of the same category and bitwidth, then this returns their (total, unsigned) remainder, where remainder by zero returns `t1`.
 - `(alf.is_neg t1)`
     - If `t1` is an arithmetic value, this returns `true` if `t1` is zero and `false` otherwise. Otherwise, this operator is not evaluated.