Minor fixes.

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cd6333225d07feec31452b393b3cd777b815c972..a5ecc8e7256a4d25e0ccd36d40f360d80965c96f 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -314,7 +314,7 @@ option cbqiLitDepend --cbqi-lit-dep bool :default true
   dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation
 option cbqiInnermost --cbqi-innermost bool :read-write :default true
  only process innermost quantified formulas in counterexample-based quantifier instantiation
-option cbqiNestedQE --cbqi-nested-qe bool :default false
+option cbqiNestedQE --cbqi-nested-qe bool :read-write :default false
  process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation
  
 option quantEpr --quant-epr bool :default false :read-write

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 57c02f3c728e9557169a23402d5b6aa76584c783..247ef2431014e29cb9ac7aab4588af719d21fcbf 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1495,7 +1495,7 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Var
       out << "(" << maybeQuoteSymbol(d.getName());
       out << " " << d.getNumParameters() << ")";
     }
-    out << ") ";
+    out << ") (";
     for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
           i_end = datatypes.end();
         i != i_end; ++i) {
@@ -1504,6 +1504,7 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Var
       toStream( out, d );
       out << ")" << endl;
     }
+    out << ")";
   }else{
     out << " () (";
     for(vector<DatatypeType>::const_iterator i = datatypes.begin(),

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1407daadc77d2e505bbab43327b89453f8edcca3..a95ce7b8d1df860468ade7f00216378f58153339 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1871,6 +1871,9 @@ void SmtEngine::setDefaults() {
         //only instantiation should happen at last call when model is avaiable
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
+    }else{
+      //only supported in pure arithmetic
+      options::cbqiNestedQE.set(false);
     }
   }
   //implied options...