summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-08-01 22:17:18 +0000
committerMorgan Deters <mdeters@gmail.com>2012-08-01 22:17:18 +0000
commitac7c25f879b222cadefca492102e277488df2bf2 (patch)
tree942c2fdc8dbf5e8370934e8ebc6d63a3dc84fd16 /src/smt/smt_engine.h
parent1e94b6229e01806f3065066d8eb4917253ef8862 (diff)
a couple fixes to SmtEngine::setOption(). thanks Andy for the report!
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h9
1 files changed, 6 insertions, 3 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 53454b109..59f66521c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -554,11 +554,14 @@ public:
/**
* Used as a predicate for options preprocessor.
*/
- static void beforeSearch(std::string option, bool value, SmtEngine* smt) {
- if(smt != NULL && (smt->d_queryMade || smt->d_problemExtended)) {
+ static void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
+ // FIXME: should be the following test...
+ // if(smt != NULL && (smt->d_queryMade || smt->d_problemExtended)) {
+ // ...but addToModelType() etc. make a stronger assumption:
+ if(smt != NULL && smt->d_fullyInited) {
std::stringstream ss;
ss << "cannot change option `" << option << "' after assertions have been made";
- throw OptionException(ss.str());
+ throw ModalException(ss.str());
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback