diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-08-21 03:26:30 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-08-21 03:26:30 -0400 |
commit | ebaa44a4b93b00614b41ef38f36112883ee27626 (patch) | |
tree | 63d96f971254e6a0b1ed67958629f414ec2f2957 /src/smt | |
parent | d0072ab29c7e9213ca6773b89e393f381bca0126 (diff) |
better handling for conflicting options with nonlinear arith (bug 646)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 192485dcc..66487e4a4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1544,14 +1544,23 @@ void SmtEngine::setDefaults() { if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) { if (options::produceModels()) { + if(options::produceModels.wasSetByUser()) { + throw OptionException("produce-model not supported with nonlinear arith"); + } Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; setOption("produce-models", SExpr("false")); } if (options::produceAssignments()) { + if(options::produceAssignments.wasSetByUser()) { + throw OptionException("produce-assignments not supported with nonlinear arith"); + } Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl; setOption("produce-assignments", SExpr("false")); } if (options::checkModels()) { + if(options::checkModels.wasSetByUser()) { + throw OptionException("check-models not supported with nonlinear arith"); + } Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl; setOption("check-models", SExpr("false")); } |