summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--NEWS2
-rw-r--r--src/expr/command.cpp3
2 files changed, 3 insertions, 2 deletions
diff --git a/NEWS b/NEWS
index eb991f74c..0532716a9 100644
--- a/NEWS
+++ b/NEWS
@@ -6,7 +6,7 @@ Changes since 1.2
* We no longer permit model or proof generation if there's been an
intervening push/pop.
* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
- resolved
+ resolved.
Changes since 1.1
=================
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 36336a959..423bf3234 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1118,7 +1118,8 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
smtEngine->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
} catch(UnrecognizedOptionException&) {
- d_commandStatus = new CommandUnsupported();
+ // As per SMT-LIB spec, silently accept unknown set-info keys
+ d_commandStatus = CommandSuccess::instance();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback