Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

4 files changed, 166 insertions, 121 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 40b757598..8957ad7f7 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -458,7 +458,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         goto next_worklist;
       }
 
-      if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
+      if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) {
         // still need to rewrite e.g. function applications over boolean
         Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
         Node n;
@@ -682,20 +682,22 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             goto next_worklist;
           }
         } else if(!t.isSort() && t.getNumChildren() > 0) {
-          for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
-            if((*i).isBoolean()) {
-              vector<TypeNode> argTypes(t.begin(), t.end());
-              replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
-              TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
-              Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
-                                    newType, "a variable introduced by Boolean-term conversion",
-                                    NodeManager::SKOLEM_EXACT_NAME);
-              Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-              top.setAttribute(BooleanTermAttr(), n);
-              d_varCache[top] = n;
-              result.top() << n;
-              worklist.pop();
-              goto next_worklist;
+          if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){
+            for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
+              if((*i).isBoolean()) {
+                vector<TypeNode> argTypes(t.begin(), t.end());
+                replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
+                TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
+                Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+                                      newType, "a variable introduced by Boolean-term conversion",
+                                      NodeManager::SKOLEM_EXACT_NAME);
+                Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+                top.setAttribute(BooleanTermAttr(), n);
+                d_varCache[top] = n;
+                result.top() << n;
+                worklist.pop();
+                goto next_worklist;
+              }
             }
           }
         }
@@ -714,6 +716,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
       case kind::RR_REWRITE:
       case kind::RR_DEDUCTION:
       case kind::RR_REDUCTION:
+      case kind::SEP_STAR:
+      case kind::SEP_WAND:
         // not yet supported
         result.top() << top;
         worklist.pop();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5bd1cbdfc..08495c936 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -94,6 +94,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"
+#include "theory/sep/theory_sep.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
@@ -552,10 +553,10 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   unsigned d_simplifyAssertionsDepth;
 
-  /** whether certain preprocess steps are necessary */
-  bool d_needsExpandDefs;
-  bool d_needsRewriteBoolTerms;
-  bool d_needsConstrainSubTypes;
+  /** TODO: whether certain preprocess steps are necessary */
+  //bool d_needsExpandDefs;
+  //bool d_needsRewriteBoolTerms;
+  //bool d_needsConstrainSubTypes;
 
 public:
   /**
@@ -684,9 +685,9 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
-    d_needsExpandDefs(true),
-    d_needsRewriteBoolTerms(true),
-    d_needsConstrainSubTypes(true), //TODO
+    //d_needsExpandDefs(true),
+    //d_needsRewriteBoolTerms(true),
+    //d_needsConstrainSubTypes(true), //TODO
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
@@ -990,7 +991,7 @@ public:
           Trace("smt-qe-debug") << "   return : " << ret << std::endl;
           //recursive (for nested quantification)
           ret = replaceQuantifiersWithInstantiations( reti, insts, visited );
-        }     
+        }
       }else if( n.getNumChildren()>0 ){
         bool childChanged = false;
         std::vector< Node > children;
@@ -1061,12 +1062,16 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
 
   // The ProofManager is constructed before any other proof objects such as
   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
-  // initialized in TheoryEngine and PropEngine respectively. 
+  // initialized in TheoryEngine and PropEngine respectively.
   Assert(d_proofManager == NULL);
+
+  // d_proofManager must be created before Options has been finished
+  // being parsed from the input file. Because of this, we cannot trust
+  // that options::proof() is set correctly yet.
 #ifdef CVC4_PROOF
   d_proofManager = new ProofManager();
 #endif
-  
+
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, d_userContext,
@@ -1078,7 +1083,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
     TheoryConstructor::addTheory(d_theoryEngine, id);
     //register with proof engine if applicable
-    THEORY_PROOF(ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); );
+#ifdef CVC4_PROOF
+    ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
+#endif
   }
 
   d_private->addUseTheoryListListener(d_theoryEngine);
@@ -1100,7 +1107,7 @@ void SmtEngine::finishInit() {
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   // ensure that our heuristics are properly set up
   setDefaults();
-  
+
   Trace("smt-debug") << "Making decision engine..." << std::endl;
 
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
@@ -1147,6 +1154,13 @@ void SmtEngine::finishInit() {
   d_dumpCommands.clear();
 
   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
+  PROOF({
+      for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+        ProofManager::currentPM()->getTheoryProofEngine()->
+          finishRegisterTheory(d_theoryEngine->theoryOf(id));
+      }
+    });
+
   Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
 }
 
@@ -1237,8 +1251,14 @@ SmtEngine::~SmtEngine() throw() {
     delete d_decisionEngine;
     d_decisionEngine = NULL;
 
-    PROOF(delete d_proofManager;);
-    PROOF(d_proofManager = NULL;);
+
+// d_proofManager is always created when proofs are enabled at configure time.
+// Becuase of this, this code should not be wrapped in PROOF() which
+// additionally checks flags such as options::proof().
+#ifdef CVC4_PROOF
+    delete d_proofManager;
+    d_proofManager = NULL;
+#endif
 
     delete d_stats;
     d_stats = NULL;
@@ -1306,9 +1326,9 @@ void SmtEngine::setDefaults() {
   }
   else if (options::solveIntAsBV() > 0) {
     d_logic = LogicInfo("QF_BV");
-  // } else if (d_logic.getLogicString() == "QF_UFBV" &&
-  //            options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-  //   d_logic = LogicInfo("QF_BV");
+  } else if (d_logic.getLogicString() == "QF_UFBV" &&
+             options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+    d_logic = LogicInfo("QF_BV");
   }
 
   // set strings-exp
@@ -1333,6 +1353,10 @@ void SmtEngine::setDefaults() {
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
+    if(! options::fmfInstEngine.wasSetByUser()) {
+      options::fmfInstEngine.set( true );
+      Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl;
+    }
     /*
     if(! options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );
@@ -1709,20 +1733,24 @@ void SmtEngine::setDefaults() {
     //must have finite model finding on
     options::finiteModelFind.set( true );
   }
-  
+
   //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
   if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
     if( !options::instWhenStrictInterleave.wasSetByUser() ){
       options::instWhenStrictInterleave.set( false );
     }
   }
-  
+
   //local theory extensions
   if( options::localTheoryExt() ){
     if( !options::instMaxLevel.wasSetByUser() ){
       options::instMaxLevel.set( 0 );
     }
   }
+  if( options::instMaxLevel()!=-1 ){
+    Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
+    options::cbqi.set(false);
+  }
 
   if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
     options::fmfBoundInt.set( true );
@@ -1783,13 +1811,15 @@ void SmtEngine::setDefaults() {
   }
 
   //apply counterexample guided instantiation options
-  if( options::cegqiSingleInv() ){
-    options::ceGuidedInst.set( true );
+  if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){
+    if( !options::ceGuidedInst.wasSetByUser() ){
+      options::ceGuidedInst.set( true );
+    }
   }
   if( options::ceGuidedInst() ){
     //counterexample-guided instantiation for sygus
-    if( !options::cegqiSingleInv.wasSetByUser() ){
-      options::cegqiSingleInv.set( true );
+    if( !options::cegqiSingleInvMode.wasSetByUser() ){
+      options::cegqiSingleInvMode.set( quantifiers::CEGQI_SI_MODE_USE );
     }
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );
@@ -1824,8 +1854,8 @@ void SmtEngine::setDefaults() {
     }
   }
   //counterexample-guided instantiation for non-sygus
-  // enable if any quantifiers with arithmetic or datatypes
-  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
+  // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
+  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
       options::cbqiAll() ){
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
@@ -2583,8 +2613,9 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) {
             case kind::CONST_RATIONAL: {
               Rational constant = current.getConst<Rational>();
               AlwaysAssert(constant.isIntegral());
+              AlwaysAssert(constant >= 0);
               BitVector bv(size, constant.getNumerator());
-              if (bv.getValue() != constant.getNumerator()) {
+              if (bv.toSignedInt() != constant.getNumerator()) {
                 throw TypeCheckingException(current.toExpr(), string("Not enough bits for constant in intToBV: ") + current.toString());
               }
               result = nm->mkConst(bv);
@@ -3837,7 +3868,7 @@ void SmtEnginePrivate::processAssertions() {
        ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
      }
      );
-  
+
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if( options::ceGuidedInst() ){
@@ -3856,8 +3887,8 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
-      !d_smt.d_logic.isPure(THEORY_BV)) {
-    //    && d_smt.d_logic.getLogicString() != "QF_UFBV")
+      !d_smt.d_logic.isPure(THEORY_BV) &&
+      d_smt.d_logic.getLogicString() != "QF_UFBV") {
     throw ModalException("Eager bit-blasting does not currently support theory combination. "
                          "Note that in a QF_BV problem UF symbols can be introduced for division. "
                          "Try --bv-div-zero-const to interpret division by zero as a constant.");
@@ -3885,7 +3916,6 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-
   dumpAssertions("pre-constrain-subtypes", d_assertions);
   {
     // Any variables of subtype types need to be constrained properly.
@@ -3965,6 +3995,10 @@ void SmtEnginePrivate::processAssertions() {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
     dumpAssertions("post-strings-pp", d_assertions);
   }
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) {
+    //separation logic solver needs to register the entire input
+    ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() );
+  }
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
     //remove rewrite rules
@@ -4220,7 +4254,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
   dumpAssertions("post-everything", d_assertions);
-  
+
 
   //set instantiation level of everything to zero
   if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
@@ -4410,74 +4444,75 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx
   Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
   Expr e_check = e;
   Node conj = Node::fromExpr( e );
-  Assert( conj.getKind()==kind::FORALL );
-  //possibly run quantifier elimination to make formula into single invocation
-  if( conj[1].getKind()==kind::EXISTS ){
-    Node conj_se = conj[1][1];
-    
-    Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
-    quantifiers::SingleInvocationPartition sip( kind::APPLY );
-    sip.init( conj_se );
-    Trace("smt-synth") << "...finished, got:" << std::endl;
-    sip.debugPrint("smt-synth");
-    
-    if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
-      //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
-      //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), 
-      //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
-    
-      //create new smt engine to do quantifier elimination
-      SmtEngine smt_qe( d_exprManager );
-      smt_qe.setLogic(getLogicInfo());
-      Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl;
-      //partition variables
-      std::vector< Node > qe_vars;
-      std::vector< Node > nqe_vars;
-      for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){
-        Node v = sip.d_all_vars[i];
-        if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){
-          qe_vars.push_back( v );
-        }else{
-          nqe_vars.push_back( v );
+  if( conj.getKind()==kind::FORALL ){
+    //possibly run quantifier elimination to make formula into single invocation
+    if( conj[1].getKind()==kind::EXISTS ){
+      Node conj_se = conj[1][1];
+
+      Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
+      quantifiers::SingleInvocationPartition sip( kind::APPLY );
+      sip.init( conj_se );
+      Trace("smt-synth") << "...finished, got:" << std::endl;
+      sip.debugPrint("smt-synth");
+
+      if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
+        //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
+        //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ),
+        //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
+
+        //create new smt engine to do quantifier elimination
+        SmtEngine smt_qe( d_exprManager );
+        smt_qe.setLogic(getLogicInfo());
+        Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl;
+        //partition variables
+        std::vector< Node > qe_vars;
+        std::vector< Node > nqe_vars;
+        for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){
+          Node v = sip.d_all_vars[i];
+          if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){
+            qe_vars.push_back( v );
+          }else{
+            nqe_vars.push_back( v );
+          }
         }
+        std::vector< Node > orig;
+        std::vector< Node > subs;
+        //skolemize non-qe variables
+        for( unsigned i=0; i<nqe_vars.size(); i++ ){
+          Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" );
+          orig.push_back( nqe_vars[i] );
+          subs.push_back( k );
+          Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
+        }
+        for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){
+          orig.push_back( sip.d_func_inv[it->first] );
+          Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" );
+          subs.push_back( k );
+          Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl;
+        }
+        Node conj_se_ngsi = sip.getFullSpecification();
+        Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
+        Assert( !qe_vars.empty() );
+        conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
+
+        Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
+        Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
+        Trace("smt-synth") << "Result : " << qe_res << std::endl;
+
+        //create single invocation conjecture
+        Node qe_res_n = Node::fromExpr( qe_res );
+        qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
+        if( !nqe_vars.empty() ){
+          qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n );
+        }
+        Assert( conj.getNumChildren()==3 );
+        qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] );
+        Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl;
+        e_check = qe_res_n.toExpr();
       }
-      std::vector< Node > orig;
-      std::vector< Node > subs;
-      //skolemize non-qe variables
-      for( unsigned i=0; i<nqe_vars.size(); i++ ){
-        Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" );
-        orig.push_back( nqe_vars[i] );
-        subs.push_back( k );
-        Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
-      }
-      for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){
-        orig.push_back( sip.d_func_inv[it->first] );
-        Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" );
-        subs.push_back( k );
-        Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl;
-      }
-      Node conj_se_ngsi = sip.getFullSpecification();
-      Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
-      Assert( !qe_vars.empty() );
-      conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
-      
-      Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
-      Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
-      Trace("smt-synth") << "Result : " << qe_res << std::endl;
-      
-      //create single invocation conjecture
-      Node qe_res_n = Node::fromExpr( qe_res );
-      qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
-      if( !nqe_vars.empty() ){
-        qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n );
-      }
-      Assert( conj.getNumChildren()==3 );
-      qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] );
-      Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl;
-      e_check = qe_res_n.toExpr();
     }
   }
-  
+
   return checkSatisfiability( e_check, true, false );
 }
 
@@ -5104,7 +5139,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
     Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
   }
   Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
-  Node n_e = Node::fromExpr( e );  
+  Node n_e = Node::fromExpr( e );
   if( n_e.getKind()!=kind::EXISTS ){
     throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
   }
@@ -5131,7 +5166,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       InternalError(ss.str().c_str());
     }
     //get the instantiations for all quantified formulas
-    std::map< Node, std::vector< Node > > insts;    
+    std::map< Node, std::vector< Node > > insts;
     d_theoryEngine->getInstantiations( insts );
     //find the quantified formula that corresponds to the input
     Node top_q;
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 5634a4651..808f5162c 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -63,14 +63,21 @@ void SmtEngine::checkProof() {
 
   Chat() << "checking proof..." << endl;
 
-  if ( !(d_logic.isPure(theory::THEORY_BOOL) ||
-           d_logic.isPure(theory::THEORY_BV) ||
-           d_logic.isPure(theory::THEORY_ARRAY) ||
-           (d_logic.isPure(theory::THEORY_UF) &&
-            ! d_logic.hasCardinalityConstraints())) ||
-       d_logic.isQuantified()) {
-    // no checking for these yet
-    Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl;
+  std::string logicString = d_logic.getLogicString();
+
+  if (!(
+        // Pure logics
+        logicString == "QF_UF" ||
+        logicString == "QF_AX" ||
+        logicString == "QF_BV" ||
+        // Non-pure logics
+        logicString == "QF_AUF" ||
+        logicString == "QF_UFBV" ||
+        logicString == "QF_ABV" ||
+        logicString == "QF_AUFBV"
+        )) {
+    // This logic is not yet supported
+    Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl;
     return;
   }
 
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index e00be40d4..9407ff498 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -49,7 +49,6 @@ inline bool smtEngineInScope() {
 // FIXME: Maybe move into SmtScope?
 inline ProofManager* currentProofManager() {
 #if IS_PROOFS_BUILD
-  Assert(options::proof() || options::unsatCores());
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current->d_proofManager;
 #else /* IS_PROOFS_BUILD */