1 files changed, 6 insertions, 1 deletions
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index d44321a35..82515c6a4 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -24,6 +24,7 @@
 
 using namespace std;
 using namespace CVC4::kind;
+using namespace CVC4::theory;
 
 namespace CVC4 {
 namespace preprocessing {
@@ -135,7 +136,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
     if (pas.getKind() == FORALL)
     {
       // preprocess the quantified formula
-      pas = theory::quantifiers::QuantifiersRewriter::preprocess(pas);
+      TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas);
+      if (!trn.isNull())
+      {
+        pas = trn.getNode();
+      }
       Trace("sygus-infer-debug") << "  ...preprocessed to " << pas << std::endl;
     }
     if (pas.getKind() == FORALL)