From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 2 Jun 2021 10:11:13 +0000 (+0200)
Subject: Fix issues when poly is disabled (#6668)
X-Git-Tag: cvc5-1.0.0~1662
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a158366e1e7fdc76e00926393b9d091870e30bad;p=cvc5.git

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 135fabf5f..96081e97b 100644
--- 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 7f97c4122..1bb558d1b 100644
--- 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;