diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-07 11:22:44 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-07 11:22:44 -0500 |
commit | 60978d75345cc4e939cf12f57ead93cbb08823ab (patch) | |
tree | bcf9dc7392d5d7536db2d697ce657b600a76f3e7 /src/smt/smt_engine.cpp | |
parent | f134f6845711821583c594acab5008eb5662888e (diff) |
Change option names for nl.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5ef77f9d8..8ae432162 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1979,8 +1979,8 @@ void SmtEngine::setDefaults() { options::arraysLazyRIntro1.set(false); } - // Non-linear arithmetic does not support models unless nlAlg is enabled - if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlAlg() ) { + // Non-linear arithmetic does not support models unless nlExt is enabled + if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlExt() ) { if (options::produceModels()) { if(options::produceModels.wasSetByUser()) { throw OptionException("produce-model not supported with nonlinear arith"); @@ -3998,7 +3998,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if( options::nlAlgPurify() ){ + if( options::nlExtPurify() ){ hash_map<Node, Node, NodeHashFunction> cache; hash_map<Node, Node, NodeHashFunction> bcache; std::vector< Node > var_eq; |