"Fix" (disable) portfolio when using quantifiers

Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags

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

2 files changed, 10 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 069e5473e..08fdbec95 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -576,6 +576,10 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
   setLogic(LogicInfo(s));
 }
 
+LogicInfo SmtEngine::getLogicInfo() const {
+  return d_logic;
+}
+
 // This function is called when d_logic has just been changed.
 // The LogicInfo isn't passed in explicitly, because that might
 // tempt people in the code to use the (potentially unlocked)
@@ -1094,7 +1098,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
         }
         return preSkolemizeQuantifiers( nn, polarity, fvs );
       }else{
-        Assert( n.getKind()==AND || n.getKind()==OR );
+        Assert( n.getKind() == kind::AND || n.getKind() == kind::OR );
         std::vector< Node > children;
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e906863ad..fb456a4a4 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -318,6 +318,11 @@ public:
   void setLogic(const LogicInfo& logic) throw(ModalException);
 
   /**
+   * Get the logic information currently set
+   */
+  LogicInfo getLogicInfo() const;
+
+  /**
    * Set information about the script executing.
    */
   void setInfo(const std::string& key, const CVC4::SExpr& value)