SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

(this commit was certified error- and warning-free by the test-and-commit script.)

2 files changed, 2 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e28520e70..364a786cf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1656,7 +1656,6 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
   SmtScope smts(this);
-
   finalOptionsAreSet();
   doPendingPops();
 
@@ -1725,7 +1724,6 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
 
   SmtScope smts(this);
-
   finalOptionsAreSet();
   doPendingPops();
 
@@ -2159,11 +2157,11 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
 
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
+  SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssertionsCommand();
   }
-  SmtScope smts(this);
   Trace("smt") << "SMT getAssertions()" << endl;
   if(!options::interactive()) {
     const char* msg =
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index deec881e4..187b29114 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -46,7 +46,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
     Dump("benchmark") << SetOptionCommand(key, value);
   }
 
-  string optarg = value.getValue();
+  string optionarg = value.getValue();
 
   ${smt_setoption_handlers}