From 96f66b5c2bb1feaf594fc1facbd2fb44e0f71cb0 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Apr 2017 14:19:51 -0500
Subject: Minor fixes.

---
 src/options/quantifiers_options   | 2 +-
 src/printer/smt2/smt2_printer.cpp | 3 ++-
 src/smt/smt_engine.cpp            | 3 +++
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cd6333225..a5ecc8e72 100644
--- 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 57c02f3c7..247ef2431 100644
--- 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 1407daadc..a95ce7b8d 100644
--- 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...
-- 
cgit v1.2.3