"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.)

1 files changed, 5 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 ) );