Merge branch 'master' into rmCDAttrrmCDAttr

35 files changed, 781 insertions, 114 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index b29585f3b..3780b0b5b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -118,7 +118,6 @@ option(ENABLE_PROFILING        "Enable support for gprof profiling")
 #    > allows to detect if set by user (default: IGNORE)
 #    > only necessary for options set for ENABLE_BEST
 cvc5_option(USE_ABC           "Use ABC for AIG bit-blasting")
-cvc5_option(USE_CADICAL       "Use CaDiCaL SAT solver")
 cvc5_option(USE_CLN           "Use CLN instead of GMP")
 cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 cvc5_option(USE_GLPK          "Use GLPK simplex solver")
@@ -417,10 +416,7 @@ if(USE_ABC)
   add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS})
 endif()
 
-if(USE_CADICAL)
-  find_package(CaDiCaL REQUIRED)
-  add_definitions(-DCVC5_USE_CADICAL)
-endif()
+find_package(CaDiCaL REQUIRED)
 
 if(USE_CLN)
   set(GPL_LIBS "${GPL_LIBS} cln")
@@ -651,7 +647,6 @@ print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
 print_config("Python2                   " ${USE_PYTHON2})
 message("")
 print_config("ABC                       " ${USE_ABC})
-print_config("CaDiCaL                   " ${USE_CADICAL})
 print_config("CryptoMiniSat             " ${USE_CRYPTOMINISAT})
 print_config("GLPK                      " ${USE_GLPK})
 print_config("Kissat                    " ${USE_KISSAT})
diff --git a/NEWS b/NEWS
index 1943d7f00..8e0ace2cf 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,7 @@ Changes since CVC4 1.8
 ======================
 
 New Features:
+* CaDiCaL is now a required dependency.
 * SymFPU is now a required dependency.
 * New unsat-core production modes based on the new proof infrastructure
   (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
diff --git a/configure.sh b/configure.sh
index 25203f8a6..4ba153a75 100755
--- a/configure.sh
+++ b/configure.sh
@@ -59,7 +59,6 @@ The following flags enable optional packages (disable with --no-<option name>).
   --cln                    use CLN instead of GMP
   --glpk                   use GLPK simplex solver
   --abc                    use the ABC AIG library
-  --cadical                use the CaDiCaL SAT solver [default=yes]
   --cryptominisat          use the CryptoMiniSat SAT solver
   --kissat                 use the Kissat SAT solver
   --poly                   use the LibPoly library [default=yes]
@@ -108,7 +107,6 @@ abc=default
 asan=default
 assertions=default
 auto_download=default
-cadical=ON
 cln=default
 comp_inc=default
 coverage=default
@@ -174,7 +172,6 @@ do
     # Best configuration
     --best)
       abc=ON
-      cadical=ON
       cln=ON
       cryptominisat=ON
       glpk=ON
@@ -198,9 +195,6 @@ do
     --name) die "missing argument to $1 (try -h)" ;;
     --name=*) build_dir=${1##*=} ;;
 
-    --cadical) cadical=ON;;
-    --no-cadical) cadical=OFF;;
-
     --cln) cln=ON;;
     --no-cln) cln=OFF;;
 
@@ -379,8 +373,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
 [ $abc != default ] \
   && cmake_opts="$cmake_opts -DUSE_ABC=$abc"
-[ $cadical != default ] \
-  && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical"
 [ $cln != default ] \
   && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
 [ $cryptominisat != default ] \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d7da67cbe..b3f27b703 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1185,9 +1185,9 @@ if(USE_ABC)
   target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES})
   target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR})
 endif()
-if(USE_CADICAL)
-  target_link_libraries(cvc5 PRIVATE CaDiCaL)
-endif()
+
+target_link_libraries(cvc5 PRIVATE CaDiCaL)
+
 if(USE_CLN)
   target_link_libraries(cvc5 PRIVATE CLN)
 endif()
diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java
new file mode 100644
index 000000000..f8c6b05c5
--- /dev/null
+++ b/src/api/java/cvc5/Grammar.java
@@ -0,0 +1,87 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+public class Grammar extends AbstractPointer {
+  // region construction and destruction
+  Grammar(Solver solver, long pointer) {
+    super(solver, pointer);
+  }
+
+  protected static native void deletePointer(long pointer);
+
+  public long getPointer() {
+    return pointer;
+  }
+
+  @Override
+  public void finalize() {
+    deletePointer(pointer);
+  }
+
+  // endregion
+
+  /**
+   * Add \p rule to the set of rules corresponding to \p ntSymbol.
+   * @param ntSymbol the non-terminal to which the rule is added
+   * @param rule the rule to add
+   */
+  public void addRule(Term ntSymbol, Term rule) {
+    addRule(pointer, ntSymbol.getPointer(), rule.getPointer());
+  }
+
+  private native void addRule(
+      long pointer, long ntSymbolPointer, long rulePointer);
+
+  /**
+   * Add \p rules to the set of rules corresponding to \p ntSymbol.
+   * @param ntSymbol the non-terminal to which the rules are added
+   * @param rules the rules to add
+   */
+  public void addRules(Term ntSymbol, Term[] rules) {
+    long[] pointers = Utils.getPointers(rules);
+    addRules(pointer, ntSymbol.getPointer(), pointers);
+  }
+
+  public native void addRules(
+      long pointer, long ntSymbolPointer, long[] rulePointers);
+
+  /**
+   * Allow \p ntSymbol to be an arbitrary constant.
+   * @param ntSymbol the non-terminal allowed to be any constant
+   */
+  void addAnyConstant(Term ntSymbol) {
+    addAnyConstant(pointer, ntSymbol.getPointer());
+  }
+
+  private native void addAnyConstant(long pointer, long ntSymbolPointer);
+
+  /**
+   * Allow \p ntSymbol to be any input variable to corresponding
+   * synth-fun/synth-inv with the same sort as \p ntSymbol.
+   * @param ntSymbol the non-terminal allowed to be any input constant
+   */
+  void addAnyVariable(Term ntSymbol) {
+    addAnyVariable(pointer, ntSymbol.getPointer());
+  }
+
+  private native void addAnyVariable(long pointer, long ntSymbolPointer);
+
+  /**
+   * @return a string representation of this grammar.
+   */
+  protected native String toString(long pointer);
+}
diff --git a/src/api/java/jni/cvc5_Grammar.cpp b/src/api/java/jni/cvc5_Grammar.cpp
new file mode 100644
index 000000000..95af2108f
--- /dev/null
+++ b/src/api/java/jni/cvc5_Grammar.cpp
@@ -0,0 +1,120 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#include "cvc5_Grammar.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_deletePointer(JNIEnv*,
+                                                       jclass,
+                                                       jlong pointer)
+{
+  delete reinterpret_cast<Grammar*>(pointer);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addRule
+ * Signature: (JJJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addRule(JNIEnv* env,
+                                                 jobject,
+                                                 jlong pointer,
+                                                 jlong ntSymbolPointer,
+                                                 jlong rulePointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  Term* rule = reinterpret_cast<Term*>(rulePointer);
+  current->addRule(*ntSymbol, *rule);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addRules
+ * Signature: (JJ[J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addRules(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer,
+                                                  jlong ntSymbolPointer,
+                                                  jlongArray rulePointers)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  std::vector<Term> rules = getObjectsFromPointers<Term>(env, rulePointers);
+  current->addRules(*ntSymbol, rules);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addAnyConstant
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyConstant(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer,
+                                                        jlong ntSymbolPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  current->addAnyConstant(*ntSymbol);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    addAnyVariable
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyVariable(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer,
+                                                        jlong ntSymbolPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer);
+  current->addAnyVariable(*ntSymbol);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_Grammar
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Grammar_toString(JNIEnv* env,
+                                                     jobject,
+                                                     jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Grammar* current = reinterpret_cast<Grammar*>(pointer);
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 9d980267d..623b2f943 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -153,6 +153,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Solver(Options*) except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
+        Sort getNullSort() except +
         Sort getRealSort() except +
         Sort getRegExpSort() except +
         Sort getRoundingModeSort() except +
@@ -178,10 +179,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkTerm(Op op, const vector[Term]& children) except +
         Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except +
         Op mkOp(Kind kind) except +
-        Op mkOp(Kind kind, Kind k) except +
         Op mkOp(Kind kind, const string& arg) except +
         Op mkOp(Kind kind, uint32_t arg) except +
         Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except +
+        Op mkOp(Kind kind, const vector[uint32_t]& args) except +
         # Sygus related functions
         Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
         Term mkSygusVar(Sort sort, const string& symbol) except +
@@ -207,9 +208,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkRegexpEmpty() except +
         Term mkRegexpSigma() except +
         Term mkEmptySet(Sort s) except +
+        Term mkEmptyBag(Sort s) except +
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
         Term mkString(const wstring& s) except +
+        Term mkString(const string& s, bint useEscSequences) except +
         Term mkEmptySequence(Sort sort) except +
         Term mkUniverseSet(Sort sort) except +
         Term mkBitVector(uint32_t size) except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 874c63c3d..4bb9da3d1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -470,6 +470,11 @@ cdef class Solver:
         sort.csort = self.csolver.getIntegerSort()
         return sort
 
+    def getNullSort(self):
+        cdef Sort sort = Sort(self)
+        sort.csort = self.csolver.getNullSort()
+        return sort
+
     def getRealSort(self):
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getRealSort()
@@ -672,8 +677,8 @@ cdef class Solver:
         result.cterm = self.csolver.mkTuple(csorts, cterms)
         return result
 
-
-    def mkOp(self, kind k, arg0=None, arg1 = None):
+    @expand_list_arg(num_req_args=0)
+    def mkOp(self, kind k, *args):
         '''
         Supports the following uses:
                 Op mkOp(Kind kind)
@@ -683,28 +688,30 @@ cdef class Solver:
                 Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)
         '''
         cdef Op op = Op(self)
+        cdef vector[int] v
 
-        if arg0 is None:
+        if len(args) == 0:
             op.cop = self.csolver.mkOp(k.k)
-        elif arg1 is None:
-            if isinstance(arg0, kind):
-                op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k)
-            elif isinstance(arg0, str):
+        elif len(args) == 1:
+            if isinstance(args[0], str):
                 op.cop = self.csolver.mkOp(k.k,
                                            <const string &>
-                                           arg0.encode())
-            elif isinstance(arg0, int):
-                op.cop = self.csolver.mkOp(k.k, <int?> arg0)
+                                           args[0].encode())
+            elif isinstance(args[0], int):
+                op.cop = self.csolver.mkOp(k.k, <int?> args[0])
+            elif isinstance(args[0], list):
+                for a in args[0]:
+                    v.push_back((<int?> a))
+                op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)   
             else:
                 raise ValueError("Unsupported signature"
-                                 " mkOp: {}".format(" X ".join([str(k), str(arg0)])))
-        else:
-            if isinstance(arg0, int) and isinstance(arg1, int):
-                op.cop = self.csolver.mkOp(k.k, <int> arg0,
-                                                       <int> arg1)
+                                 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
+        elif len(args) == 2:
+            if isinstance(args[0], int) and isinstance(args[1], int):
+                op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1])
             else:
                 raise ValueError("Unsupported signature"
-                                 " mkOp: {}".format(" X ".join([k, arg0, arg1])))
+                                 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
         return op
 
     def mkTrue(self):
@@ -778,17 +785,24 @@ cdef class Solver:
         term.cterm = self.csolver.mkEmptySet(s.csort)
         return term
 
+    def mkEmptyBag(self, Sort s):
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkEmptyBag(s.csort)
+        return term
 
     def mkSepNil(self, Sort sort):
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkSepNil(sort.csort)
         return term
 
-    def mkString(self, str s):
+    def mkString(self, str s, useEscSequences = None):
         cdef Term term = Term(self)
         cdef Py_ssize_t size
         cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
-        term.cterm = self.csolver.mkString(c_wstring(tmp, size))
+        if isinstance(useEscSequences, bool):
+            term.cterm = self.csolver.mkString(s.encode(), <bint> useEscSequences)
+        else:
+            term.cterm = self.csolver.mkString(c_wstring(tmp, size))
         PyMem_Free(tmp)
         return term
 
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 1befb34ea..c6b004574 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -120,24 +120,23 @@ std::string Configuration::copyright() {
      << "See licenses/antlr3-LICENSE for copyright and licensing information."
      << "\n\n";
 
-  if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
+  ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
+     << "third party libraries.\n\n";
+
+  ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
+     << "  See https://github.com/arminbiere/cadical for copyright "
+     << "information.\n\n";
+
+  if (Configuration::isBuiltWithAbc()
       || Configuration::isBuiltWithCryptominisat()
       || Configuration::isBuiltWithKissat()
       || Configuration::isBuiltWithEditline())
   {
-    ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
-       << "third party libraries.\n\n";
     if (Configuration::isBuiltWithAbc()) {
       ss << "  ABC - A System for Sequential Synthesis and Verification\n"
          << "  See http://bitbucket.org/alanmi/abc for copyright and\n"
          << "  licensing information.\n\n";
     }
-    if (Configuration::isBuiltWithCadical())
-    {
-      ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
-         << "  See https://github.com/arminbiere/cadical for copyright "
-         << "information.\n\n";
-    }
     if (Configuration::isBuiltWithCryptominisat())
     {
       ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
@@ -241,8 +240,6 @@ bool Configuration::isBuiltWithAbc() {
   return IS_ABC_BUILD;
 }
 
-bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; }
-
 bool Configuration::isBuiltWithCryptominisat() {
   return IS_CRYPTOMINISAT_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 2a7df1b4a..71c79c22e 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -103,8 +103,6 @@ public:
 
   static bool isBuiltWithAbc();
 
-  static bool isBuiltWithCadical();
-
   static bool isBuiltWithCryptominisat();
 
   static bool isBuiltWithKissat();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 39c5e89e9..b348da380 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -96,12 +96,6 @@ namespace cvc5 {
 #  define IS_ABC_BUILD false
 #endif /* CVC5_USE_ABC */
 
-#if CVC5_USE_CADICAL
-#define IS_CADICAL_BUILD true
-#else /* CVC5_USE_CADICAL */
-#define IS_CADICAL_BUILD false
-#endif /* CVC5_USE_CADICAL */
-
 #if CVC5_USE_CRYPTOMINISAT
 #  define IS_CRYPTOMINISAT_BUILD true
 #else /* CVC5_USE_CRYPTOMINISAT */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d31d2e58f..07138dce3 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -146,15 +146,6 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
     throw OptionException(ss.str());
   }
 
-  if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
-  {
-    std::stringstream ss;
-    ss << "option `" << option
-       << "' requires a CaDiCaL build of cvc5; this binary was not built with "
-          "CaDiCaL support";
-    throw OptionException(ss.str());
-  }
-
   if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
   {
     std::stringstream ss;
@@ -397,7 +388,6 @@ void OptionsHandler::showConfiguration(const std::string& option,
   print_config_cond("abc", Configuration::isBuiltWithAbc());
   print_config_cond("cln", Configuration::isBuiltWithCln());
   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
-  print_config_cond("cadical", Configuration::isBuiltWithCadical());
   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9aee1df22..3b3f80e6c 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -84,11 +84,6 @@ public:
                        const std::string& flag,
                        const std::string& value);
 
-  template <class T>
-  void checkSatSolverEnabled(const std::string& option,
-                             const std::string& flag,
-                             T m);
-
   void checkBvSatSolver(const std::string& option,
                         const std::string& flag,
                         SatSolverMode m);
@@ -171,20 +166,6 @@ public:
 
 }; /* class OptionHandler */
 
-template <class T>
-void OptionsHandler::checkSatSolverEnabled(const std::string& option,
-                                           const std::string& flag,
-                                           T m)
-{
-#if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \
-    && !defined(CVC5_USE_KISSAT)
-  std::stringstream ss;
-  ss << "option `" << option
-     << "' requires cvc5 to be built with CryptoMiniSat or CaDiCaL or Kissat";
-  throw OptionException(ss.str());
-#endif
-}
-
 }  // namespace options
 }  // namespace cvc5
 
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index a42b30773..c1cf0338a 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -688,9 +688,9 @@ enum class PfRule : uint32_t
   //================================================= Array rules
   // ======== Read over write
   // Children: (P:(not (= i1 i2)))
-  // Arguments: ((select (store a i2 e) i1))
+  // Arguments: ((select (store a i1 e) i2))
   // ----------------------------------------
-  // Conclusion: (= (select (store a i2 e) i1) (select a i1))
+  // Conclusion: (= (select (store a i1 e) i2) (select a i2))
   ARRAYS_READ_OVER_WRITE,
   // ======== Read over write, contrapositive
   // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index ec8919b0b..ddf20f5a1 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -17,8 +17,6 @@
 
 #include "prop/cadical.h"
 
-#ifdef CVC5_USE_CADICAL
-
 #include "base/check.h"
 #include "util/statistics_registry.h"
 
@@ -191,5 +189,3 @@ CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry,
 
 }  // namespace prop
 }  // namespace cvc5
-
-#endif  // CVC5_USE_CADICAL
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index b5e26df9f..46c7c7e42 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -20,8 +20,6 @@
 #ifndef CVC5__PROP__CADICAL_H
 #define CVC5__PROP__CADICAL_H
 
-#ifdef CVC5_USE_CADICAL
-
 #include "prop/sat_solver.h"
 
 #include <cadical.hpp>
@@ -103,5 +101,4 @@ class CadicalSolver : public SatSolver
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC5_USE_CADICAL
 #endif  // CVC5__PROP__CADICAL_H
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 40853b33a..4897f8e6a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -21,14 +21,15 @@
 #include "base/output.h"
 #include "expr/node.h"
 #include "options/bv_options.h"
+#include "printer/printer.h"
 #include "proof/clause_id.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
 #include "smt/dump.h"
 #include "smt/smt_engine.h"
-#include "printer/printer.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
@@ -52,7 +53,8 @@ CnfStream::CnfStream(SatSolver* satSolver,
       d_registrar(registrar),
       d_name(name),
       d_removable(false),
-      d_resourceManager(rm)
+      d_resourceManager(rm),
+      d_stats(name)
 {
 }
 
@@ -139,6 +141,7 @@ void CnfStream::ensureLiteral(TNode n)
       n.toString().c_str(),
       n.getType().toString().c_str());
   Trace("cnf") << "ensureLiteral(" << n << ")\n";
+  TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
   if (hasLiteral(n))
   {
     ensureMappingForLiteral(n);
@@ -722,6 +725,7 @@ void CnfStream::convertAndAssert(TNode node,
                << ", negated = " << (negated ? "true" : "false")
                << ", removable = " << (removable ? "true" : "false") << ")\n";
   d_removable = removable;
+  TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
   convertAndAssert(node, negated);
 }
 
@@ -760,5 +764,11 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
   }
 }
 
+CnfStream::Statistics::Statistics(const std::string& name)
+    : d_cnfConversionTime(smtStatisticsRegistry().registerTimer(
+        name + "::CnfStream::cnfConversionTime"))
+{
+}
+
 }  // namespace prop
 }  // namespace cvc5
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 2959ae726..aeed97380 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -309,6 +309,14 @@ class CnfStream {
 
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
+
+ private:
+  struct Statistics
+  {
+    Statistics(const std::string& name);
+    TimerStat d_cnfConversionTime;
+  } d_stats;
+
 }; /* class CnfStream */
 
 }  // namespace prop
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index fe3a5ecff..62b2f655c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -107,7 +107,8 @@ PropEngine::PropEngine(TheoryEngine* te,
                               userContext,
                               &d_outMgr,
                               rm,
-                              FormulaLitPolicy::TRACK);
+                              FormulaLitPolicy::TRACK,
+                              "prop");
 
   // connect theory proxy
   d_theoryProxy->finishInit(d_cnfStream);
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 446f72451..0855cbda5 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -53,13 +53,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry,
 SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry,
                                            const std::string& name)
 {
-#ifdef CVC5_USE_CADICAL
   CadicalSolver* res = new CadicalSolver(registry, name);
   res->init();
   return res;
-#else
-  Unreachable() << "cvc5 was not compiled with CaDiCaL support.";
-#endif
 }
 
 SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry,
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index 417d345cb..c76a8a2e7 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -25,8 +25,6 @@ SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
         name + "definitionExpansionTime")),
       d_numConstantProps(
           smtStatisticsRegistry().registerInt(name + "numConstantProps")),
-      d_cnfConversionTime(
-          smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")),
       d_numAssertionsPre(smtStatisticsRegistry().registerInt(
           name + "numAssertionsPreITERemoval")),
       d_numAssertionsPost(smtStatisticsRegistry().registerInt(
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index 441721a54..db914b560 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -30,8 +30,6 @@ struct SmtEngineStatistics
   TimerStat d_definitionExpansionTime;
   /** number of constant propagations found during nonclausal simp */
   IntStat d_numConstantProps;
-  /** time spent converting to CNF */
-  TimerStat d_cnfConversionTime;
   /** Number of assertions before ite removal */
   IntStat d_numAssertionsPre;
   /** Number of assertions after ite removal */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index d7b70f501..f5783ab6b 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -239,7 +239,6 @@ void SmtSolver::processAssertions(Assertions& as)
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
-    TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
     const std::vector<Node>& assertions = ap.ref();
     // It is important to distinguish the input assertions from the skolem
     // definitions, as the decision justification heuristic treates the latter
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index a38dfdfe5..357a54b1a 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
+#include "options/bv_options.h"
 
 namespace cvc5 {
 namespace theory {
@@ -129,6 +130,15 @@ Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
   return utils::mkConst(bits.size(), value);
 }
 
+void BBSimple::computeRelevantTerms(std::set<Node>& termSet)
+{
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER);
+  for (const auto& var : d_variables)
+  {
+    termSet.insert(var);
+  }
+}
+
 bool BBSimple::collectModelValues(TheoryModel* m,
                                   const std::set<Node>& relevantTerms)
 {
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index ebbb2891f..ec0899145 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -53,6 +53,8 @@ class BBSimple : public TBitblaster<Node>
   /** Create 'bits' for variable 'var'. */
   void makeVariable(TNode var, Bits& bits) override;
 
+  /** Add d_variables to termSet. */
+  void computeRelevantTerms(std::set<Node>& termSet);
   /** Collect model values for all relevant terms given in 'relevantTerms'. */
   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
 
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 8ff4318c0..6ccc6c7c1 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -32,7 +32,7 @@ class BVSolver
   BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
       : d_state(state), d_im(inferMgr){};
 
-  virtual ~BVSolver(){};
+  virtual ~BVSolver() {}
 
   /**
    * Returns true if we need an equality engine. If so, we initialize the
@@ -71,7 +71,7 @@ class BVSolver
 
   virtual bool needsCheckLastEffort() { return false; }
 
-  virtual void propagate(Theory::Effort e){};
+  virtual void propagate(Theory::Effort e) {}
 
   virtual TrustNode explain(TNode n)
   {
@@ -80,17 +80,20 @@ class BVSolver
     return TrustNode::null();
   }
 
+  /** Additionally collect terms relevant for collecting model values. */
+  virtual void computeRelevantTerms(std::set<Node>& termSet) {}
+
   /** Collect model values in m based on the relevant terms given by termSet */
   virtual bool collectModelValues(TheoryModel* m,
                                   const std::set<Node>& termSet) = 0;
 
   virtual std::string identify() const = 0;
 
-  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
+  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }
 
-  virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
+  virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
 
-  virtual void presolve(){};
+  virtual void presolve() {}
 
   virtual void notifySharedTerm(TNode t) {}
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index dc2c7e2a3..3ae4a7f0a 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -96,17 +96,19 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
   {
     case options::SatSolverMode::CRYPTOMINISAT:
       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
-          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
+          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
       break;
     default:
       d_satSolver.reset(prop::SatSolverFactory::createCadical(
-          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
+          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
   }
   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                         d_bbRegistrar.get(),
                                         d_nullContext.get(),
                                         nullptr,
-                                        smt::currentResourceManager()));
+                                        smt::currentResourceManager(),
+                                        prop::FormulaLitPolicy::INTERNAL,
+                                        "theory::bv::BVSolverBitblast"));
 }
 
 void BVSolverBitblast::postCheck(Theory::Effort level)
@@ -236,6 +238,21 @@ TrustNode BVSolverBitblast::explain(TNode n)
   return d_im.explainLit(n);
 }
 
+void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
+{
+  /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
+   * equalities. As a result, these equalities are not handled by the equality
+   * engine and terms below these equalities do not appear in `termSet`.
+   * We need to make sure that we compute model values for all relevant terms
+   * in BitblastMode::EAGER and therefore add all variables from the
+   * bit-blaster to `termSet`.
+   */
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    d_bitblaster->computeRelevantTerms(termSet);
+  }
+}
+
 bool BVSolverBitblast::collectModelValues(TheoryModel* m,
                                           const std::set<Node>& termSet)
 {
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 31d9443c8..c5134c6fc 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -64,6 +64,8 @@ class BVSolverBitblast : public BVSolver
 
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
+  void computeRelevantTerms(std::set<Node>& termSet) override;
+
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 22b05b026..3d7f11f6d 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -175,6 +175,11 @@ bool TheoryBV::needsCheckLastEffort()
   return d_internal->needsCheckLastEffort();
 }
 
+void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
+{
+  return d_internal->computeRelevantTerms(termSet);
+}
+
 bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
   return d_internal->collectModelValues(m, termSet);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4b3a1f3b2..e884f621c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -83,6 +83,8 @@ class TheoryBV : public Theory
 
   TrustNode explain(TNode n) override;
 
+  void computeRelevantTerms(std::set<Node>& termSet) override;
+
   /** Collect model values in m based on the relevant terms given by termSet */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 1255bf270..8b3ce944e 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -43,6 +43,10 @@ def test_get_integer_sort(solver):
     solver.getIntegerSort()
 
 
+def test_get_null_sort(solver):
+    solver.getNullSort()
+
+
 def test_get_real_sort(solver):
     solver.getRealSort()
 
@@ -244,6 +248,15 @@ def test_mk_set_sort(solver):
         slv.mkSetSort(solver.mkBitVectorSort(4))
 
 
+def test_mk_bag_sort(solver):
+    solver.mkBagSort(solver.getBooleanSort())
+    solver.mkBagSort(solver.getIntegerSort())
+    solver.mkBagSort(solver.mkBitVectorSort(4))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkBagSort(solver.mkBitVectorSort(4))
+
+
 def test_mk_sequence_sort(solver):
     solver.mkSequenceSort(solver.getBooleanSort())
     solver.mkSequenceSort(\
@@ -277,6 +290,42 @@ def test_mk_tuple_sort(solver):
         slv.mkTupleSort([solver.getIntegerSort()])
 
 
+def test_mk_bit_vector(solver):
+    size0 = 0
+    size1 = 8
+    size2 = 32
+    val1 = 2
+    val2 = 2
+    solver.mkBitVector(size1, val1)
+    solver.mkBitVector(size2, val2)
+    solver.mkBitVector("1010", 2)
+    solver.mkBitVector("1010", 10)
+    solver.mkBitVector("1234", 10)
+    solver.mkBitVector("1010", 16)
+    solver.mkBitVector("a09f", 16)
+    solver.mkBitVector(8, "-127", 10)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(size0, val1)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(size0, val2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector("", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector("10", 3)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector("20", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(8, "101010101", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(8, "-256", 10)
+    assert solver.mkBitVector("1010", 2) == solver.mkBitVector("10", 10)
+    assert solver.mkBitVector("1010", 2) == solver.mkBitVector("a", 16)
+    assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101"
+    assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111"
+    assert solver.mkBitVector(8, "-1", 10) ==\
+            solver.mkBitVector(8, "FF", 16)
+
+
 def test_mk_var(solver):
     boolSort = solver.getBooleanSort()
     intSort = solver.getIntegerSort()
@@ -312,6 +361,26 @@ def test_mk_uninterpreted_const(solver):
         slv.mkUninterpretedConst(solver.getBooleanSort(), 1)
 
 
+def test_mk_abstract_value(solver):
+    solver.mkAbstractValue("1")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("0")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("-1")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("1.2")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("1/2")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("asdf")
+
+    solver.mkAbstractValue(1)
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue(-1)
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue(0)
+
+
 def test_mk_floating_point(solver):
     t1 = solver.mkBitVector(8)
     t2 = solver.mkBitVector(4)
@@ -345,6 +414,17 @@ def test_mk_empty_set(solver):
         slv.mkEmptySet(s)
 
 
+def test_mk_empty_bag(solver):
+    slv = pycvc5.Solver()
+    s = solver.mkBagSort(solver.getBooleanSort())
+    solver.mkEmptyBag(pycvc5.Sort(solver))
+    solver.mkEmptyBag(s)
+    with pytest.raises(RuntimeError):
+        solver.mkEmptyBag(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        slv.mkEmptyBag(s)
+
+
 def test_mk_empty_sequence(solver):
     slv = pycvc5.Solver()
     s = solver.mkSequenceSort(solver.getBooleanSort())
@@ -379,6 +459,33 @@ def test_mk_pos_zero(solver):
     solver.mkPosZero(3, 5)
 
 
+def test_mk_op(solver):
+    # mkOp(Kind kind, Kind k)
+    with pytest.raises(ValueError):
+        solver.mkOp(kinds.BVExtract, kinds.Equal)
+
+    # mkOp(Kind kind, const std::string& arg)
+    solver.mkOp(kinds.Divisible, "2147483648")
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.BVExtract, "asdf")
+
+    # mkOp(Kind kind, uint32_t arg)
+    solver.mkOp(kinds.Divisible, 1)
+    solver.mkOp(kinds.BVRotateLeft, 1)
+    solver.mkOp(kinds.BVRotateRight, 1)
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.BVExtract, 1)
+
+    # mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
+    solver.mkOp(kinds.BVExtract, 1, 1)
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.Divisible, 1, 2)
+
+    # mkOp(Kind kind, std::vector<uint32_t> args)
+    args = [1, 2, 2]
+    solver.mkOp(kinds.TupleProject, args)
+
+
 def test_mk_pi(solver):
     solver.mkPi()
 
@@ -526,11 +633,210 @@ def test_mk_sep_nil(solver):
         slv.mkSepNil(solver.getIntegerSort())
 
 
+def test_mk_string(solver):
+    solver.mkString("")
+    solver.mkString("asdfasdf")
+    str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\""
+    str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\
+            "\"asdf\\u{5c}nasdf\""
+
+
+def test_mk_term(solver):
+    bv32 = solver.mkBitVectorSort(32)
+    a = solver.mkConst(bv32, "a")
+    b = solver.mkConst(bv32, "b")
+    v1 = [a, b]
+    v2 = [a, pycvc5.Term(solver)]
+    v3 = [a, solver.mkTrue()]
+    v4 = [solver.mkInteger(1), solver.mkInteger(2)]
+    v5 = [solver.mkInteger(1), pycvc5.Term(solver)]
+    v6 = []
+    slv = pycvc5.Solver()
+
+    # mkTerm(Kind kind) const
+    solver.mkPi()
+    solver.mkTerm(kinds.RegexpEmpty)
+    solver.mkTerm(kinds.RegexpSigma)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ConstBV)
+
+    # mkTerm(Kind kind, Term child) const
+    solver.mkTerm(kinds.Not, solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Not, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Not, a)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.Not, solver.mkTrue())
+
+    # mkTerm(Kind kind, Term child1, Term child2) const
+    solver.mkTerm(kinds.Equal, a, b)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, a, solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.Equal, a, b)
+
+    # mkTerm(Kind kind, Term child1, Term child2, Term child3) const
+    solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(),
+                      solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver),
+                      solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(),
+                      pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(),
+                   solver.mkTrue())
+
+    # mkTerm(Kind kind, const std::vector<Term>& children) const
+    solver.mkTerm(kinds.Equal, v1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, v2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, v3)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Distinct, v6)
+
+
+def test_mk_term_from_op(solver):
+    bv32 = solver.mkBitVectorSort(32)
+    a = solver.mkConst(bv32, "a")
+    b = solver.mkConst(bv32, "b")
+    v1 = [solver.mkInteger(1), solver.mkInteger(2)]
+    v2 = [solver.mkInteger(1), pycvc5.Term(solver)]
+    v3 = []
+    v4 = [solver.mkInteger(5)]
+    slv = pycvc5.Solver()
+
+    # simple operator terms
+    opterm1 = solver.mkOp(kinds.BVExtract, 2, 1)
+    opterm2 = solver.mkOp(kinds.Divisible, 1)
+
+    # list datatype
+    sort = solver.mkParamSort("T")
+    listDecl = solver.mkDatatypeDecl("paramlist", sort)
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    cons.addSelector("head", sort)
+    cons.addSelectorSelf("tail")
+    listDecl.addConstructor(cons)
+    listDecl.addConstructor(nil)
+    listSort = solver.mkDatatypeSort(listDecl)
+    intListSort =\
+        listSort.instantiate([solver.getIntegerSort()])
+    c = solver.mkConst(intListSort, "c")
+    lis = listSort.getDatatype()
+
+    # list datatype constructor and selector operator terms
+    consTerm1 = lis.getConstructorTerm("cons")
+    consTerm2 = lis.getConstructor("cons").getConstructorTerm()
+    nilTerm1 = lis.getConstructorTerm("nil")
+    nilTerm2 = lis.getConstructor("nil").getConstructorTerm()
+    headTerm1 = lis["cons"].getSelectorTerm("head")
+    headTerm2 = lis["cons"].getSelector("head").getSelectorTerm()
+    tailTerm1 = lis["cons"].getSelectorTerm("tail")
+    tailTerm2 = lis["cons"]["tail"].getSelectorTerm()
+
+    # mkTerm(Op op, Term term) const
+    solver.mkTerm(kinds.ApplyConstructor, nilTerm1)
+    solver.mkTerm(kinds.ApplyConstructor, nilTerm2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplySelector, nilTerm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplySelector, consTerm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplyConstructor, consTerm2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplySelector, headTerm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.ApplyConstructor, nilTerm1)
+
+    # mkTerm(Op op, Term child) const
+    solver.mkTerm(opterm1, a)
+    solver.mkTerm(opterm2, solver.mkInteger(1))
+    solver.mkTerm(kinds.ApplySelector, headTerm1, c)
+    solver.mkTerm(kinds.ApplySelector, tailTerm2, c)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, a)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0))
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(opterm1, a)
+
+    # mkTerm(Op op, Term child1, Term child2) const
+    solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0),
+                  solver.mkTerm(kinds.ApplyConstructor, nilTerm1))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1, a, b)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1))
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.ApplyConstructor,\
+                        consTerm1,\
+                        solver.mkInteger(0),\
+                        solver.mkTerm(kinds.ApplyConstructor, nilTerm1))
+
+    # mkTerm(Op op, Term child1, Term child2, Term child3) const
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1, a, b, a)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1),
+                      pycvc5.Term(solver))
+
+    # mkTerm(Op op, const std::vector<Term>& children) const
+    solver.mkTerm(opterm2, v4)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, v1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, v2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, v3)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(opterm2, v4)
+
+
 def test_mk_true(solver):
     solver.mkTrue()
     solver.mkTrue()
 
 
+def test_mk_tuple(solver):
+    solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)])
+    solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")])
+
+    with pytest.raises(RuntimeError):
+        solver.mkTuple([], [solver.mkBitVector("101", 2)])
+    with pytest.raises(RuntimeError):
+        solver.mkTuple([solver.mkBitVectorSort(4)],
+                       [solver.mkBitVector("101", 2)])
+    with pytest.raises(RuntimeError):
+        solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")])
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector("101", 2)])
+    with pytest.raises(RuntimeError):
+        slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)])
+
+
 def test_mk_universe_set(solver):
     solver.mkUniverseSet(solver.getBooleanSort())
     with pytest.raises(RuntimeError):
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9ad4f7e8a..444e4c7f6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -670,6 +670,7 @@ set(regress_0_tests
   regress0/issue5743.smt2
   regress0/issue5947.smt2
   regress0/issue6605-2-abd-triv.smt2
+  regress0/issue6741.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
   regress0/ite_real_valid.smtv1.smt2
diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2
index 01840dffa..34007f6aa 100644
--- a/test/regress/regress0/bv/eager-inc-cadical.smt2
+++ b/test/regress/regress0/bv/eager-inc-cadical.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: cadical
 ; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager
 (set-logic QF_BV)
 (set-option :incremental true)
diff --git a/test/regress/regress0/issue6741.smt2 b/test/regress/regress0/issue6741.smt2
new file mode 100644
index 000000000..0fbf4edeb
--- /dev/null
+++ b/test/regress/regress0/issue6741.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --bv-solver=bitblast --bitblast=eager --check-models
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 1))
+(declare-fun y () (_ BitVec 1))
+(assert (= y (ite (= x (_ bv1 1)) (_ bv1 1) (_ bv0 1))))
+(assert (= y (_ bv1 1)))
+(check-sat)
diff --git a/test/unit/api/java/cvc5/GrammarTest.java b/test/unit/api/java/cvc5/GrammarTest.java
new file mode 100644
index 000000000..76a80f55e
--- /dev/null
+++ b/test/unit/api/java/cvc5/GrammarTest.java
@@ -0,0 +1,137 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Abdalrhman Mohamed, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the Java API functions.
+ */
+
+package cvc5;
+
+import static cvc5.Kind.*;
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.Arrays;
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class GrammarTest {
+  private Solver d_solver;
+
+  @BeforeEach
+  void setUp() {
+    d_solver = new Solver();
+  }
+
+  @Test
+  void addRule() {
+    Sort bool = d_solver.getBooleanSort();
+    Sort integer = d_solver.getIntegerSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false)));
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRule(nullTerm, d_solver.mkBoolean(false)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(start, nullTerm));
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRule(nts, d_solver.mkBoolean(false)));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRule(start, d_solver.mkInteger(0)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(start, nts));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g);
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRule(start, d_solver.mkBoolean(false)));
+  }
+
+  @Test
+  void addRules() {
+    Sort bool = d_solver.getBooleanSort();
+    Sort integer = d_solver.getIntegerSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(
+        () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(nullTerm, new Term[] {d_solver.mkBoolean(false)}));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm}));
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(nts, new Term[] {d_solver.mkBoolean(false)}));
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(start, new Term[] {d_solver.mkInteger(0)}));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRules(start, new Term[] {nts}));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g);
+
+    assertThrows(CVC5ApiException.class,
+        () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
+  }
+
+  @Test
+  void addAnyConstant() {
+    Sort bool = d_solver.getBooleanSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(() -> g.addAnyConstant(start));
+    assertDoesNotThrow(() -> g.addAnyConstant(start));
+
+    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nullTerm));
+    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nts));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g);
+
+    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start));
+  }
+
+  @Test
+  void addAnyVariable() {
+    Sort bool = d_solver.getBooleanSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term x = d_solver.mkVar(bool);
+    Term start = d_solver.mkVar(bool);
+    Term nts = d_solver.mkVar(bool);
+
+    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start});
+    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+
+    assertDoesNotThrow(() -> g1.addAnyVariable(start));
+    assertDoesNotThrow(() -> g1.addAnyVariable(start));
+    assertDoesNotThrow(() -> g2.addAnyVariable(start));
+
+    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nullTerm));
+    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nts));
+
+    d_solver.synthFun("f", new Term[] {}, bool, g1);
+
+    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(start));
+  }
+}