X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsmt%2Fsygus_solver.cpp;h=e14c6041b67549357e2dd9da04f75cff1352020d;hb=97a870f131138662d93299c76ef49865bbc6f546;hp=2a5bf1b51e0a86604c115549955cb23070cc1ebc;hpb=9a191a3fae2abfc68be734ca5790024fea93e9f1;p=cvc5.git

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 2a5bf1b51..e14c6041b 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -376,8 +376,8 @@ void SygusSolver::checkSynthSolution(Assertions& as,
     // Start new SMT engine to check solutions
     std::unique_ptr<SolverEngine> solChecker;
     initializeSygusSubsolver(solChecker, as);
-    solChecker->getOptions().smt.checkSynthSol = false;
-    solChecker->getOptions().quantifiers.sygusRecFun = false;
+    solChecker->getOptions().writeSmt().checkSynthSol = false;
+    solChecker->getOptions().writeQuantifiers().sygusRecFun = false;
     Assert(conj.getKind() == FORALL);
     Node conjBody = conj[1];
     // we must expand definitions here, since define-fun may contain the