diff options
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; |