Fix issues when poly is disabled (#6668)

Recent changes introduced issues when libpoly is disabled.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 135fabf5f03a325dc6d311df171fb6e2cfff17ac..96081e97b6e1170da90ffbf35e6a7c0916a80247 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1523,12 +1523,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (opts.wasSetByUser(options::nlCad))
     {
       std::stringstream ss;
-      ss << "Cannot use " << options::nlCad.name << " without configuring with --poly.";
+      ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly.";
       throw OptionException(ss.str());
     }
     else
     {
-      Notice() << "Cannot use --" << options::nlCad.name
+      Notice() << "Cannot use --" << options::arith::nlCad__name
                << " without configuring with --poly." << std::endl;
       opts.arith.nlCad = false;
       opts.arith.nlExt = options::NlExtMode::FULL;

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 7f97c4122f656a6699fa0439229d57a7089f1e46..1bb558d1b9fe57228260acd331d1d4cc8a488fc5 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -27,6 +27,7 @@
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;