1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e25e8a225..2e0fa75fe 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -540,6 +540,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     Trace("cegqi-engine") << "Check side condition..." << std::endl;
     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
     SmtEngine scSmt(nm->toExprManager());
+    scSmt.setIsInternalSubsolver();
     scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
     scSmt.assertFormula(sc.toExpr());
     Result r = scSmt.checkSat();
@@ -572,6 +573,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     {
       Trace("cegqi-engine") << "  *** Verify with subcall..." << std::endl;
       SmtEngine verifySmt(nm->toExprManager());
+      verifySmt.setIsInternalSubsolver();
       verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
       verifySmt.assertFormula(query.toExpr());
       Result r = verifySmt.checkSat();