3 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 8366fe4e1..a8e5d74b6 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -186,7 +186,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   return RewriteResponse(REWRITE_DONE, in);
 }
 
-Kind getOperatorKindForSygusBuiltin(Node op)
+Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op)
 {
   Assert(op.getKind() != BUILTIN);
   if (op.getKind() == LAMBDA)
@@ -212,7 +212,7 @@ Kind getOperatorKindForSygusBuiltin(Node op)
   {
     return APPLY_UF;
   }
-  return NodeManager::operatorToKind(op);
+  return UNDEFINED_KIND;
 }
 
 Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 7d91544e1..a6c95b893 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -121,6 +121,13 @@ public:
   *   C( x, y ) and z
   */
  static bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
+ /** get operator kind for sygus builtin
+  *
+  * This returns the Kind corresponding to applications of the operator op
+  * when building the builtin version of sygus terms. This is used by the
+  * function mkSygusTerm.
+  */
+ static Kind getOperatorKindForSygusBuiltin(Node op);
  /** make sygus term
   *
   * This function returns a builtin term f( children[0], ..., children[n] )
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp
index 5def5fc95..f2b131f21 100644
--- a/src/theory/quantifiers/fmf/ambqi_builder.cpp
+++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp
@@ -13,6 +13,8 @@
  **/
 
 #include "theory/quantifiers/fmf/ambqi_builder.h"
+
+#include "base/cvc4_check.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
@@ -367,8 +369,8 @@ void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int cur
   }else{
     TypeNode tn = m->getVariable( q, depth ).getType();
     if( v==depth ){
-      unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
-      Assert( numReps>0 && numReps < 32 );
+      const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
+      CVC4_CHECK(numReps > 0 && numReps < 32);
       for( unsigned i=0; i<numReps; i++ ){
         d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
       }