From a158366e1e7fdc76e00926393b9d091870e30bad Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Jun 2021 12:11:13 +0200 Subject: [PATCH] Fix issues when poly is disabled (#6668) Recent changes introduced issues when libpoly is disabled. --- src/smt/set_defaults.cpp | 4 ++-- src/theory/arith/nl/nonlinear_extension.cpp | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) 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; -- 2.30.2