Make regular options access const (#8754)

[cvc5.git] / src / smt / sygus_solver.cpp

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 2a5bf1b51e0a86604c115549955cb23070cc1ebc..e14c6041b67549357e2dd9da04f75cff1352020d 100644 (file)
--- 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