1 files changed, 16 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index fb4f7e831..c1daa9288 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -605,9 +605,15 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
                                        double rinc,
                                        unsigned depth)
 {
-  Assert(tn.isDatatype());
+  if (!tn.isDatatype())
+  {
+    return getRandomValue(tn);
+  }
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  Assert(dt.isSygus());
+  if (!dt.isSygus())
+  {
+    return getRandomValue(tn);
+  }
   Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
   Trace("sygus-sample-grammar")
       << "Sygus random value " << tn << ", depth = " << depth
@@ -671,9 +677,15 @@ void SygusSampler::registerSygusType(TypeNode tn)
   if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end())
   {
     d_rvalue_cindices[tn].clear();
-    Assert(tn.isDatatype());
+    if (!tn.isDatatype())
+    {
+      return;
+    }
     const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-    Assert(dt.isSygus());
+    if (!dt.isSygus())
+    {
+      return;
+    }
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       const DatatypeConstructor& dtc = dt[i];